SurfaceFormalImmersion.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Relative local convex integration transferred through an actual surface chart.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.surface_formal_immersion line 17

Source documentation

A constructed injective field removes precisely the singularities in the chosen compact coordinate region; every exterior germ is preserved.

theorem surface_formal_immersion (c : OpenPartialHomeomorph M Base)
    (hcs : ContMDiffOn planeModel 𝓘(ℝ,Base) ∞ c c.source)
    (hci : ContMDiffOn 𝓘(ℝ,Base) planeModel ∞ c.symm c.target)
    {f : M → ProjectionTarget 3} (hf : ContMDiff planeModel 𝓘(ℝ,ProjectionTarget 3) ∞ f)
    {φ : Base → ProjectionTarget 3} (hφ : ContDiff ℝ ∞ φ)
    {O : Set Base} (hO : IsOpen O) (hOt : O ⊆ c.target)
    (hmatch : EqOn φ (f ∘ c.symm) O)
    {A : Base → Base →L[ℝ] ProjectionTarget 3} (hA : ContDiff ℝ ∞ A)
    {K₀ K₁ : Set Base} (hK₀ : IsCompact K₀) (hK₁ : IsCompact K₁)
    (h01 : K₀ ⊆ interior K₁) (hK₁O : K₁ ⊆ O)
    (hs : tsupport (A-fderiv ℝ φ) ⊆ interior K₀)
    (hAI : ∀ x ∈ K₁, Function.Injective (A x)) :
…

Mentions: OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.ProjectionTarget