# 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} [NormedSpace ๐ E] (f : ๐ โแต[๐] E) {x : ๐} :
HasStrictDerivAt (โf) (f.linear 1) x
theorem AffineMap.hasDerivAtFilter {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] (f : ๐ โแต[๐] E) {L : Filter ๐} {x : ๐} :
HasDerivAtFilter (โf) (f.linear 1) x L
theorem AffineMap.hasDerivWithinAt {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] (f : ๐ โแต[๐] E) {s : Set ๐} {x : ๐} :
HasDerivWithinAt (โf) (f.linear 1) s x
theorem AffineMap.hasDerivAt {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] (f : ๐ โแต[๐] E) {x : ๐} :
HasDerivAt (โf) (f.linear 1) x
theorem AffineMap.derivWithin {๐ : Type u_1} [] {E : Type u_2} [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} [] {E : Type u_2} [NormedSpace ๐ E] (f : ๐ โแต[๐] E) {x : ๐} :
deriv (โf) x = f.linear 1
theorem AffineMap.differentiableAt {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] (f : ๐ โแต[๐] E) {x : ๐} :
DifferentiableAt ๐ (โf) x
theorem AffineMap.differentiable {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] (f : ๐ โแต[๐] E) :
Differentiable ๐ โf
theorem AffineMap.differentiableWithinAt {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] (f : ๐ โแต[๐] E) {s : Set ๐} {x : ๐} :
DifferentiableWithinAt ๐ (โf) s x
theorem AffineMap.differentiableOn {๐ : Type u_1} [] {E : Type u_2} [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} [] {E : Type u_2} [NormedSpace ๐ E] {a : E} {b : E} {x : ๐} :
HasStrictDerivAt (โ()) (b - a) x
theorem AffineMap.hasDerivAt_lineMap {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] {a : E} {b : E} {x : ๐} :
HasDerivAt (โ()) (b - a) x
theorem AffineMap.hasDerivWithinAt_lineMap {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] {a : E} {b : E} {s : Set ๐} {x : ๐} :
HasDerivWithinAt (โ()) (b - a) s x