ProfileCrossingChoice.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Transfer the compact turn/nonturn alternative to a unit normal path in the actual normal plane, with both required endpoint inequalities.

theorem OAI.ClosedSurfaceR4.GeometryPreservation.compact_actual_profile_crossing_choice line 19

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_crossing_choice (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‖ < η →
      -K ≤ coordinateGauss (realMetric F dx dx) (realMetric F dx dy) (realMetric F dy dy) p →
…

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