Differentiability of graph-straightening charts #
The ambient chart ContinuousLinearMap.projectionGraphChart and its inverse inherit
the differentiability of the graph map g at the projected point. Both have
explicit linear-shear differentials. In particular, a graph map with zero derivative gives
an ambient chart with identity derivative, as needed to identify the tangent space of a
local invariant disk.
theorem
ContinuousLinearMap.contDiffAt_projectionGraphChart
{𝕜 : Type u_1}
{E : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
(P : E →L[𝕜] E)
(g : E → E)
{U : Set E}
(hU : IsOpen U)
(hg : ContinuousOn g (↑(↑P).range ∩ U))
(hPg : ∀ v ∈ ↑(↑P).range ∩ U, P (g v) = 0)
{n : WithTop ℕ∞}
{z : E}
(hgs : ContDiffAt 𝕜 n g (P z))
:
ContDiffAt 𝕜 n (↑(P.projectionGraphChart g hU hg hPg)) z
The graph chart is C^n wherever g is C^n at the projected point.
theorem
ContinuousLinearMap.contDiffAt_projectionGraphChart_symm
{𝕜 : Type u_1}
{E : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
(P : E →L[𝕜] E)
(g : E → E)
{U : Set E}
(hU : IsOpen U)
(hg : ContinuousOn g (↑(↑P).range ∩ U))
(hPg : ∀ v ∈ ↑(↑P).range ∩ U, P (g v) = 0)
{n : WithTop ℕ∞}
{z : E}
(hgs : ContDiffAt 𝕜 n g (P z))
:
ContDiffAt 𝕜 n (↑(P.projectionGraphChart g hU hg hPg).symm) z
The inverse chart is C^n wherever g is C^n at the projected point.
theorem
ContinuousLinearMap.hasFDerivAt_projectionGraphChart
{𝕜 : Type u_1}
{E : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
(P : E →L[𝕜] E)
(g : E → E)
{U : Set E}
(hU : IsOpen U)
(hg : ContinuousOn g (↑(↑P).range ∩ U))
(hPg : ∀ v ∈ ↑(↑P).range ∩ U, P (g v) = 0)
{z : E}
{D : E →L[𝕜] E}
(hgs : HasFDerivAt g D (P z))
:
HasFDerivAt (↑(P.projectionGraphChart g hU hg hPg)) (ContinuousLinearMap.id 𝕜 E - D ∘SL P) z
The differential of the straightening chart is the corresponding linear shear.
theorem
ContinuousLinearMap.hasFDerivAt_projectionGraphChart_symm
{𝕜 : Type u_1}
{E : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
(P : E →L[𝕜] E)
(g : E → E)
{U : Set E}
(hU : IsOpen U)
(hg : ContinuousOn g (↑(↑P).range ∩ U))
(hPg : ∀ v ∈ ↑(↑P).range ∩ U, P (g v) = 0)
{z : E}
{D : E →L[𝕜] E}
(hgs : HasFDerivAt g D (P z))
:
HasFDerivAt (↑(P.projectionGraphChart g hU hg hPg).symm) (ContinuousLinearMap.id 𝕜 E + D ∘SL P) z
The differential of the inverse graph chart is the inverse linear shear.