Smooth affine maps

This file contains results about smoothness of affine maps.

Main definitions:

• ContinuousAffineMap.contDiff: a continuous affine map is smooth

theorem ContinuousAffineMap.contDiff {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] {n : WithTop ℕ∞} (f : V →ᴬ[𝕜] W) : ContDiff 𝕜 n ⇑f

A continuous affine map between normed vector spaces is smooth.

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

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

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

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

@[simp]

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