OAI/Geometry/SurfaceImmersion/Whitney/SmoothRelativeFrame.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A continuous compact relative frame can be smoothed while retaining injectivity and the exact prescribed derivative near its exterior.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.HPrincipleBridge.smooth_relative_frame line 14
  2. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.HPrincipleBridge.realize_continuous_relative_frame line 54

    Source documentation

    The formal field in the relative h-principle may be merely continuous; its exact exterior equality is retained in the smooth realization.

    theorem realize_continuous_relative_frame {f : Plane → Vec}
    {A : Plane → Plane →L[ℝ] Vec} (hf : ContDiff ℝ ∞ f) (hA : Continuous 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