# Derivatives of affine maps #

In this file we prove formulas for one-dimensional derivatives of affine maps `f : 𝕜 →ᵃ[𝕜] E`. We also specialise some of these results to `AffineMap.lineMap` because it is useful to transfer MVT from dimension 1 to a domain in higher dimension.

## TODO #

Add theorems about `deriv`s and `fderiv`s of `ContinuousAffineMap`s once they will be ported to Mathlib 4.

## Keywords #

affine map, derivative, differentiability

source
theorem AffineMap.hasStrictDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜 →ᵃ[𝕜] E) {x : 𝕜} :
HasStrictDerivAt (⇑f) (f.linear 1) x
source
theorem AffineMap.hasDerivAtFilter {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜 →ᵃ[𝕜] E) {L : Filter 𝕜} {x : 𝕜} :
HasDerivAtFilter (⇑f) (f.linear 1) x L
source
theorem AffineMap.hasDerivWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜 →ᵃ[𝕜] E) {s : Set 𝕜} {x : 𝕜} :
HasDerivWithinAt (⇑f) (f.linear 1) s x
source
theorem AffineMap.hasDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜 →ᵃ[𝕜] E) {x : 𝕜} :
HasDerivAt (⇑f) (f.linear 1) x
source
theorem AffineMap.derivWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜 →ᵃ[𝕜] E) {s : Set 𝕜} {x : 𝕜} (hs : UniqueDiffWithinAt 𝕜 s x) :
derivWithin (⇑f) s x = f.linear 1
source
@[simp]
theorem AffineMap.deriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜 →ᵃ[𝕜] E) {x : 𝕜} :
deriv (⇑f) x = f.linear 1
source
theorem AffineMap.differentiableAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜 →ᵃ[𝕜] E) {x : 𝕜} :
DifferentiableAt 𝕜 (⇑f) x
source
theorem AffineMap.differentiable {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜 →ᵃ[𝕜] E) :
Differentiable 𝕜 ⇑f
source
theorem AffineMap.differentiableWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜 →ᵃ[𝕜] E) {s : Set 𝕜} {x : 𝕜} :
DifferentiableWithinAt 𝕜 (⇑f) s x
source
theorem AffineMap.differentiableOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜 →ᵃ[𝕜] E) {s : Set 𝕜} :
DifferentiableOn 𝕜 (⇑f) s

### Line map #

In this section we specialize some lemmas to `AffineMap.lineMap` because this map is very useful to deduce higher-dimensional lemmas from one-dimensional versions.

source
theorem AffineMap.hasStrictDerivAt_lineMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {a b : E} {x : 𝕜} :
HasStrictDerivAt (⇑(lineMap a b)) (b - a) x
source
theorem AffineMap.hasDerivAt_lineMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {a b : E} {x : 𝕜} :
HasDerivAt (⇑(lineMap a b)) (b - a) x
source
theorem AffineMap.hasDerivWithinAt_lineMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {a b : E} {s : Set 𝕜} {x : 𝕜} :
HasDerivWithinAt (⇑(lineMap a b)) (b - a) s x