Smooth affine maps

This file contains results about smoothness of affine maps.

Main results

• ContinuousAffineMap.contDiff: a continuous affine map is smooth.
• AffineMap.contDiff_lineMap_uncurry: AffineMap.lineMap is smooth in its three arguments, jointly and pointwise.

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 AffineMap.contDiff_lineMap_uncurry {𝕜 : Type u_1} {V : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] {n : WithTop ℕ∞} : ContDiff 𝕜 n fun (pqc : V × V × 𝕜) => (lineMap pqc.1 pqc.2.1) pqc.2.2

AffineMap.lineMap is smooth in all three arguments.

theorem AffineMap.contDiff_lineMap {𝕜 : Type u_1} {V : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] (p₀ p₁ : V) {n : WithTop ℕ∞} : ContDiff 𝕜 n ⇑(lineMap p₀ p₁)

AffineMap.lineMap is smooth as a function 𝕜 → V.

theorem ContDiffWithinAt.lineMap {𝕜 : Type u_1} {V : Type u_2} {E : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f₁ f₂ : E → V} {g : E → 𝕜} {s : Set E} {x : E} {n : WithTop ℕ∞} (h₁ : ContDiffWithinAt 𝕜 n f₁ s x) (h₂ : ContDiffWithinAt 𝕜 n f₂ s x) (hg : ContDiffWithinAt 𝕜 n g s x) : ContDiffWithinAt 𝕜 n (fun (x : E) => (AffineMap.lineMap (f₁ x) (f₂ x)) (g x)) s x

theorem ContDiffAt.lineMap {𝕜 : Type u_1} {V : Type u_2} {E : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f₁ f₂ : E → V} {g : E → 𝕜} {x : E} {n : WithTop ℕ∞} (h₁ : ContDiffAt 𝕜 n f₁ x) (h₂ : ContDiffAt 𝕜 n f₂ x) (hg : ContDiffAt 𝕜 n g x) : ContDiffAt 𝕜 n (fun (x : E) => (AffineMap.lineMap (f₁ x) (f₂ x)) (g x)) x

theorem ContDiffOn.lineMap {𝕜 : Type u_1} {V : Type u_2} {E : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f₁ f₂ : E → V} {g : E → 𝕜} {s : Set E} {n : WithTop ℕ∞} (h₁ : ContDiffOn 𝕜 n f₁ s) (h₂ : ContDiffOn 𝕜 n f₂ s) (hg : ContDiffOn 𝕜 n g s) : ContDiffOn 𝕜 n (fun (x : E) => (AffineMap.lineMap (f₁ x) (f₂ x)) (g x)) s

theorem ContDiff.lineMap {𝕜 : Type u_1} {V : Type u_2} {E : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f₁ f₂ : E → V} {g : E → 𝕜} {n : WithTop ℕ∞} (h₁ : ContDiff 𝕜 n f₁) (h₂ : ContDiff 𝕜 n f₂) (hg : ContDiff 𝕜 n g) : ContDiff 𝕜 n fun (x : E) => (AffineMap.lineMap (f₁ x) (f₂ x)) (g x)