LeadingProfileStability.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform C3 stability of the leading profiles on a compact spatial set, including every phase on the period circle.

lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.leadingProfileMap_uniform_near line 15
def OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.geometricLeadingProfile line 27

theorem OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.geometricLeadingProfile_stability line 38

Source documentation

The slow baseline may be replaced by the original map in all five leading profiles, using only its unweighted C3 error.

theorem geometricLeadingProfile_stability {S : TopologicalSpace.Opens JetPolynomial.Base}
    {F : JetPolynomial.Base → JetPolynomial.Space} (hF : ContDiff ℝ ∞ F)
    (hFO : MapsTo (lowJet F) S O) {K : Set JetPolynomial.Base}
    (hK : IsCompact K) (hKS : K ⊆ S) (ε : ℝ) (hε : 0 < ε) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ G : JetPolynomial.Base → JetPolynomial.Space,
      ∀ hG : ContDiff ℝ ∞ G, ∀ hGO : MapsTo (lowJet G) S O,
      WeightedBound S 1 3 δ (fun p => G p-F p) → ∀ p ∈ K, ∀ t : Period,
        ‖l.geometricLeadingProfile G hG hGO p t-l.geometricLeadingProfile F hF hFO p t‖ < ε := by
…

Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space