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 derivs and fderivs of ContinuousAffineMaps once they will be ported to Mathlib 4.

Keywords

affine map, derivative, differentiability

theorem AffineMap.hasStrictDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜 →ᵃ[𝕜] E) {x : 𝕜} : HasStrictDerivAt (⇑f) (f.linear 1) x

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

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

theorem AffineMap.hasDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜 →ᵃ[𝕜] E) {x : 𝕜} : HasDerivAt (⇑f) (f.linear 1) x

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

@[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

theorem AffineMap.differentiableAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜 →ᵃ[𝕜] E) {x : 𝕜} : DifferentiableAt 𝕜 (⇑f) x

theorem AffineMap.differentiable {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜 →ᵃ[𝕜] E) : Differentiable 𝕜 ⇑f

theorem AffineMap.differentiableWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜 →ᵃ[𝕜] E) {s : Set 𝕜} {x : 𝕜} : DifferentiableWithinAt 𝕜 (⇑f) s x

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.

theorem AffineMap.hasStrictDerivAt_lineMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {a : E} {b : E} {x : 𝕜} : HasStrictDerivAt (⇑(AffineMap.lineMap a b)) (b - a) x

theorem AffineMap.hasDerivAt_lineMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {a : E} {b : E} {x : 𝕜} : HasDerivAt (⇑(AffineMap.lineMap a b)) (b - a) x

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