OAI/GroupTheory/PolycyclicRecognition/Geometry/SmoothLocalSection.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_smooth_local_section line 20

   Source documentation

   The section is an actual function smooth at the base point, and is a right inverse on a neighborhood; no global injectivity is required.

   theorem exists_smooth_local_section
       {P : V → M} {x₀ : V} {d : V ≃L[ℝ] E}
       (hP : ContMDiffAt (𝓘(ℝ,V)) (𝓘(ℝ,E)) ∞ P x₀)
       (hd : HasMFDerivAt (𝓘(ℝ,V)) (𝓘(ℝ,E)) P x₀ d.toContinuousLinearMap) :
       ∃ r : M → V, ContMDiffAt (𝓘(ℝ,E)) (𝓘(ℝ,V)) ∞ r (P x₀) ∧
         r (P x₀) = x₀ ∧ ∀ᶠ x in 𝓝 (P x₀), P (r x) = x := by
   …

2. theorem OAI.PolycyclicRecognition.contMDiffAt_from_right_parameters line 70

   Source documentation

   Smoothness in a parameter and local coordinates in the second variable descends through the actual smooth section.

   theorem contMDiffAt_from_right_parameters
       {P : V → M} {x₀ : V} {d : V ≃L[ℝ] E} {w₀ : W} {f : W × M → Y}
       (hP : ContMDiffAt (𝓘(ℝ,V)) (𝓘(ℝ,E)) ∞ P x₀)
       (hd : HasMFDerivAt (𝓘(ℝ,V)) (𝓘(ℝ,E)) P x₀ d.toContinuousLinearMap)
       (hf : ContMDiffAt ((𝓘(ℝ,EW)).prod (𝓘(ℝ,V))) (𝓘(ℝ,EY)) ∞
         (fun p : W × V => f (p.1,P p.2)) (w₀,x₀)) :
       ContMDiffAt ((𝓘(ℝ,EW)).prod (𝓘(ℝ,E))) (𝓘(ℝ,EY)) ∞ f (w₀,P x₀) := by
   …

3. theorem OAI.PolycyclicRecognition.contMDiff_of_smooth_mul_right line 92

   Source documentation

   Right translation moves smoothness at the identity to every point.

   theorem contMDiff_of_smooth_mul_right (a : Q × Q → Q)
       (h : ∀ g c, ContMDiffAt ((𝓘(ℝ,EG)).prod (𝓘(ℝ,EG))) (𝓘(ℝ,EG)) ∞
         (fun z : Q × Q => a (z.1,c * z.2)) (g,1)) :
       ContMDiff ((𝓘(ℝ,EG)).prod (𝓘(ℝ,EG))) (𝓘(ℝ,EG)) ∞ a := by
   …