Shear charts of a normed space

Given a linear homeomorphism A : V × W ≃L[𝕜] Y and a map g : V → W which is C^m on an open set, the shear (u, w) ↦ (u, w - g u) of the graph of g is a partial homeomorphism of Y, C^m with C^m inverse, once read through A.

Main declarations

• ContinuousLinearEquiv.exists_contDiffOn_shear: the existence of such a shear chart, with its explicit formula and source.

theorem ContinuousLinearEquiv.exists_contDiffOn_shear {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} {Y : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] {m : WithTop ℕ∞} (A : (V × W) ≃L[𝕜] Y) (c₀ : Y) {U : Set V} (hU : IsOpen U) {g : V → W} (hg : ContDiffOn 𝕜 m g U) : ∃ (Ψ : OpenPartialHomeomorph Y Y), ContDiffOn 𝕜 m (↑Ψ) Ψ.source ∧ ContDiffOn 𝕜 m (↑Ψ.symm) Ψ.target ∧ (∀ (x : Y), x ∈ Ψ.source ↔ (A.symm (x - c₀)).1 ∈ U) ∧ ∀ (x : Y), ↑Ψ x = A ((A.symm (x - c₀)).1, (A.symm (x - c₀)).2 - g (A.symm (x - c₀)).1)

A shear chart of a normed space: given a linear homeomorphism A : V × W ≃ Y, a basepoint c₀ and a map g : V → W which is C^m on an open set U, there is a partial homeomorphism of Y, C^m with C^m inverse, which sends x to A (u, w - g u), where (u, w) = A⁻¹ (x - c₀), and whose source is the set of points with u ∈ U.