PeriodicNormalStability.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform normal margins over the compact position-period domain.

theorem OAI.ClosedSurfaceR4.VelocityFrame.periodic_leading_normal_stability line 17

Source documentation

A full real fast phase costs no compactness: periodicity reduces the normal estimate to one compact period.

theorem periodic_leading_normal_stability {K : Set A} (hK : IsCompact K)
    {X Y C : A → Vec} (hX : Continuous X) (hY : Continuous Y) (hC : Continuous C)
    (V : A → C(Period, Vec))
    (hVs : Continuous (fun p : A × ℝ => V p.1 (p.2 : Period)))
    (hD : ∀ p ∈ K, gramDet (Y p) (C p) ≠ 0)
    (hYV : ∀ p ∈ K, ∀ θ : Period, Y p ⬝ᵥ V p θ = 0)
    (hCV : ∀ p ∈ K, ∀ θ : Period, C p ⬝ᵥ V p θ = 0)
    (hV0 : ∀ p ∈ K, ∀ θ : Period, V p θ ≠ 0) :
    ∃ ε c : ℝ, 0 < ε ∧ 0 < c ∧ ∀ p ∈ K, ∀ t : ℝ, ∀ H : NormalTriple,
      ‖H-![leadingTangent (X p) (Y p) (C p) (V p (t : Period)),Y p,C p]‖ < ε →
      gramDet (H 0) (H 1) ≠ 0 ∧ c < ‖realNormalPart (H 0) (H 1) (H 2)‖ := by
…

Mentions: OAI.ClosedSurfaceR4.VelocityFrame.NormalTriple, OAI.ClosedSurfaceR4.VelocityFrame.leadingTangent

theorem OAI.ClosedSurfaceR4.VelocityFrame.periodic_normal_stability_of_linear_error line 46

Source documentation

Componentwise O(z) errors in x, y and yy preserve a uniform normal margin for all sufficiently small fast scales.

theorem periodic_normal_stability_of_linear_error {K : Set A} (hK : IsCompact K)
    {X Y C : A → Vec} (hX : Continuous X) (hY : Continuous Y) (hC : Continuous C)
    (V : A → C(Period, Vec))
    (hVs : Continuous (fun p : A × ℝ => V p.1 (p.2 : Period)))
    (hD : ∀ p ∈ K, gramDet (Y p) (C p) ≠ 0)
    (hYV : ∀ p ∈ K, ∀ θ : Period, Y p ⬝ᵥ V p θ = 0)
    (hCV : ∀ p ∈ K, ∀ θ : Period, C p ⬝ᵥ V p θ = 0)
    (hV0 : ∀ p ∈ K, ∀ θ : Period, V p θ ≠ 0)
    (D : ℝ) (hD0 : 0 ≤ D) :
    ∃ η c : ℝ, 0 < η ∧ 0 < c ∧ ∀ z : ℝ, 0 < z → z < η →
      ∀ p ∈ K, ∀ t : ℝ, ∀ x y b : Vec,
      ‖x-leadingTangent (X p) (Y p) (C p) (V p (t : Period))‖ ≤ D*z →
…

Mentions: OAI.ClosedSurfaceR4.VelocityFrame.leadingTangent