OAI/Geometry/SurfaceImmersion/Whitney/SupportedFormalImmersion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Compact relative realization of a constructed smooth formal immersion. This only removes singularities where an injective formal field is supplied.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.HPrincipleBridge.supported_formal_immersion line 13

    Source documentation

    A compact formal correction is integrated without changing exterior germs.

    theorem supported_formal_immersion {f : Plane → Vec} {A : Plane → Plane →L[ℝ] Vec}
    (hf : ContDiff ℝ ∞ f) (hA : ContDiff ℝ ∞ A)
    {K₀ K₁ : Set Plane} (hK₀ : IsCompact K₀) (hK₁ : IsCompact K₁)
    (h01 : K₀ ⊆ interior K₁)
    (hs : tsupport (A-fderiv ℝ f) ⊆ interior K₀)
    (hAI : ∀ x ∈ K₁, Function.Injective (A x)) :
    ∃ g : Plane → Vec, ContDiff ℝ ∞ g ∧ tsupport (g-f) ⊆ K₁ ∧
      (∀ x ∈ K₁, Function.Injective (fderiv ℝ g x)) ∧
      (∀ x ∉ interior K₀, g =ᶠ[𝓝 x] f) ∧
      ∀ x ∉ K₁, Function.Injective (fderiv ℝ g x) ↔
        Function.Injective (fderiv ℝ f x) := by
…

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