# Documentation

Mathlib.Analysis.Calculus.Deriv.AffineMap

# 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} {E : Type u_2} [] (f : 𝕜 →ᵃ[𝕜] E) {x : 𝕜} :
HasStrictDerivAt (f) (f.linear 1) x
theorem AffineMap.hasDerivAtFilter {𝕜 : Type u_1} {E : Type u_2} [] (f : 𝕜 →ᵃ[𝕜] E) {L : } {x : 𝕜} :
HasDerivAtFilter (f) (f.linear 1) x L
theorem AffineMap.hasDerivWithinAt {𝕜 : Type u_1} {E : Type u_2} [] (f : 𝕜 →ᵃ[𝕜] E) {s : Set 𝕜} {x : 𝕜} :
HasDerivWithinAt (f) (f.linear 1) s x
theorem AffineMap.hasDerivAt {𝕜 : Type u_1} {E : Type u_2} [] (f : 𝕜 →ᵃ[𝕜] E) {x : 𝕜} :
HasDerivAt (f) (f.linear 1) x
theorem AffineMap.derivWithin {𝕜 : Type u_1} {E : Type u_2} [] (f : 𝕜 →ᵃ[𝕜] E) {s : Set 𝕜} {x : 𝕜} (hs : ) :
derivWithin (f) s x = f.linear 1
@[simp]
theorem AffineMap.deriv {𝕜 : Type u_1} {E : Type u_2} [] (f : 𝕜 →ᵃ[𝕜] E) {x : 𝕜} :
deriv (f) x = f.linear 1
theorem AffineMap.differentiableAt {𝕜 : Type u_1} {E : Type u_2} [] (f : 𝕜 →ᵃ[𝕜] E) {x : 𝕜} :
DifferentiableAt 𝕜 (f) x
theorem AffineMap.differentiable {𝕜 : Type u_1} {E : Type u_2} [] (f : 𝕜 →ᵃ[𝕜] E) :
theorem AffineMap.differentiableWithinAt {𝕜 : Type u_1} {E : Type u_2} [] (f : 𝕜 →ᵃ[𝕜] E) {s : Set 𝕜} {x : 𝕜} :
DifferentiableWithinAt 𝕜 (f) s x
theorem AffineMap.differentiableOn {𝕜 : Type u_1} {E : Type u_2} [] (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} {E : Type u_2} [] {a : E} {b : E} {x : 𝕜} :
HasStrictDerivAt (↑()) (b - a) x
theorem AffineMap.hasDerivAt_lineMap {𝕜 : Type u_1} {E : Type u_2} [] {a : E} {b : E} {x : 𝕜} :
HasDerivAt (↑()) (b - a) x
theorem AffineMap.hasDerivWithinAt_lineMap {𝕜 : Type u_1} {E : Type u_2} [] {a : E} {b : E} {s : Set 𝕜} {x : 𝕜} :
HasDerivWithinAt (↑()) (b - a) s x