The derivative of continuous affine maps

For detailed documentation of the Fréchet derivative, see the module docstring of Mathlib/Analysis/Calculus/FDeriv/Basic.lean.

This file contains the usual formulas (and existence assertions) for the derivative of continuous affine maps.

Continuous affine maps

theorem ContinuousAffineMap.hasFDerivAtFilter {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →ᴬ[𝕜] F) {L : Filter (E × E)} : HasFDerivAtFilter (⇑f) f.contLinear L

theorem ContinuousAffineMap.hasStrictFDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →ᴬ[𝕜] F) {x : E} : HasStrictFDerivAt (⇑f) f.contLinear x

theorem ContinuousAffineMap.hasFDerivWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →ᴬ[𝕜] F) {x : E} {s : Set E} : HasFDerivWithinAt (⇑f) f.contLinear s x

theorem ContinuousAffineMap.hasFDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →ᴬ[𝕜] F) {x : E} : HasFDerivAt (⇑f) f.contLinear x

@[simp]

theorem ContinuousAffineMap.differentiableAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →ᴬ[𝕜] F) {x : E} : DifferentiableAt 𝕜 (⇑f) x

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

@[simp]

theorem ContinuousAffineMap.fderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →ᴬ[𝕜] F) {x : E} : fderiv 𝕜 (⇑f) x = f.contLinear

theorem ContinuousAffineMap.fderivWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →ᴬ[𝕜] F) {x : E} {s : Set E} (hxs : UniqueDiffWithinAt 𝕜 s x) : fderivWithin 𝕜 (⇑f) s x = f.contLinear

@[simp]

theorem ContinuousAffineMap.differentiable {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →ᴬ[𝕜] F) : Differentiable 𝕜 ⇑f

theorem ContinuousAffineMap.differentiableOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →ᴬ[𝕜] F) {s : Set E} : DifferentiableOn 𝕜 (⇑f) s