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.lineMapis 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 ℕ∞}
:
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 ℕ∞}
:
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)