OAI/Geometry/SurfaceImmersion/Whitney/ActualProfileCollar.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The positive boundary invariant on the zero-amplitude collar survives small errors in the five profiles. No large angular derivative is needed there.

  1. def OAI.ClosedSurfaceR4.GeometryPreservation.collarInvariant line 13
  2. lemma OAI.ClosedSurfaceR4.GeometryPreservation.continuousAt_collarInvariant line 16
  3. theorem OAI.ClosedSurfaceR4.GeometryPreservation.compact_profile_collar line 33
  4. theorem OAI.ClosedSurfaceR4.GeometryPreservation.compact_actual_profile_collar line 69

    Source documentation

    Transfer collar positivity to nonvanishing and antipode avoidance for the actual second form, using the intrinsic curvature lower bound.

    theorem compact_actual_profile_collar {X : Type*} [TopologicalSpace X] [CompactSpace X]
    {J : X → BoundaryProfile} (hJ : Continuous J)
    (hreg : ∀ x, J x ∈ regularBoundaryProfiles)
    {b c k : X → ℝ} (hb : Continuous b) (hc : Continuous c) (hk : Continuous k)
    (hpos : ∀ x, 0 < (profileCoefficients (J x) 1 * b x +
      profileCoefficients (J x) 0 * c x)^2 + k x * b x^2) :
    ∃ η : ℝ, 0 < η ∧ ∀ x : X, ∀ F : RField 4, ContDiff ℝ ∞ F →
      ∀ z : ℝ, ∀ p : Base, ‖realBoundaryProfile F z p-J x‖ < η →
      k x ≤ coordinateGauss (realMetric F dx dx) (realMetric F dx dy) (realMetric F dy dy) p →
      realSecondForm F (b x,c x) (b x,c x) p ≠ 0 ∧
      normalize (realSecondForm F (b x,c x) (b x,c x) p) ≠
        -profilePreferred (realBoundaryProfile F z p) := by
…

    Mentions: OAI.ClosedSurfaceR4.GeometryPreservation.BoundaryProfile, OAI.ClosedSurfaceR4.GeometryPreservation.regularBoundaryProfiles, OAI.ClosedSurfaceR4.GeometryPreservation.profileCoefficients, OAI.ClosedSurfaceR4.GeometryPreservation.realBoundaryProfile, OAI.ClosedSurfaceR4.GeometryPreservation.profilePreferred