ActualProfileCrossing.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Transfer the compact turn/nonturn argument all the way to the two ordered crossing invariants of an actual smooth surface.

lemma OAI.ClosedSurfaceR4.GeometryPreservation.profileCoefficient_sub_le line 15

theorem OAI.ClosedSurfaceR4.GeometryPreservation.compact_actual_profile_crossings line 26

Source documentation

The turn threshold is chosen from the fixed metric and slope bounds, before the loop and its mixed/longitudinal derivatives are supplied.

theorem compact_actual_profile_crossings (sLo sHi K d T : ℝ)
    (hsLo : 0 < sLo) (hsHi : 0 < sHi) (hK : 0 ≤ K) (hd : 0 ≤ d) (hT : 0 ≤ T) :
    ∃ H : ℝ, 0 < H ∧ ∀ J : X → BoundaryProfile, Continuous J →
      (∀ x, J x ∈ regularBoundaryProfiles) →
      (∀ x, sLo ≤ profileCoefficients (J x) 0) →
      (∀ x, profileCoefficients (J x) 0 ≤ sHi) →
      (∀ x, |profileCoefficients (J x) 1| ≤ d) →
      (∀ x, profileCoefficients (J x) 3 = 0 → H+2 < |profileCoefficients (J x) 2|) →
      ∃ η : ℝ, 0 < η ∧ ∀ z : ℝ, 0 < z → z < η → ∀ x : X,
      ∀ F : RField 4, ContDiff ℝ ∞ F → ∀ p : Base,
      ‖realBoundaryProfile F z p-J x‖ < η →
      ∀ κ : ℝ,
…

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