OAI/Geometry/SurfaceImmersion/Whitney/RelativeImmersionHPrinciple.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ClosedSurfaceR4.FiniteOrderSmoothing.HPrincipleBridge.Plane line 10
2. abbrev OAI.ClosedSurfaceR4.FiniteOrderSmoothing.HPrincipleBridge.Vec line 11
3. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.HPrincipleBridge.localizedImmersionRel line 13
4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.HPrincipleBridge.localizedImmersionRel_open line 16
5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.HPrincipleBridge.localizedImmersionRel_ample line 21
6. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.HPrincipleBridge.realize_relative_frame line 46

   Source documentation

   The local h-principle realizes an injective formal differential while preserving the prescribed exterior germs.

   theorem realize_relative_frame {f : Plane → Vec} {A : Plane → Plane →L[ℝ] Vec}
       (hf : ContDiff ℝ ∞ f) (hA : ContDiff ℝ ∞ A)
       (L : Landscape Plane) (hcover : L.K₀ ∪ L.C = Set.univ)
       (hAI : ∀ x ∈ L.K₁, Function.Injective (A x))
       (hhol : ∀ᶠ x in 𝓝ˢ L.C, fderiv ℝ f x = A x)
       {ε : ℝ} (hε : 0 < ε) :
       ∃ g : Plane → Vec, ContDiff ℝ ∞ g ∧
         tsupport (g-f) ⊆ L.K₁ ∧ (∀ x, ‖g x-f x‖ < ε) ∧
         (∀ x ∈ L.K₁, Function.Injective (fderiv ℝ g x)) ∧
         ∀ x ∈ L.C, g =ᶠ[𝓝 x] f := by
   …

   Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.HPrincipleBridge.Plane, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.HPrincipleBridge.Vec