WeightedActualJets.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Actual jets have precisely one scale loss per derivative beyond the controlled second jet, with no loss for their first two derivatives.

lemma OAI.ClosedSurfaceR4.JetPolynomial.norm_coordinateVector_le line 13

theorem OAI.ClosedSurfaceR4.JetPolynomial.weighted_actual_jet line 22

Source documentation

A weighted bound on the second-jet map controls every actual higher jet.

theorem weighted_actual_jet {U : Set Base} (hU : IsOpen U) {G : Base → Space}
    (hG : ContDiff ℝ ∞ G) {s B : ℝ} (hs : 0 < s) (hB : 0 ≤ B)
    (m : ℕ) (w : List (Fin 2)) (a : Fin 4)
    (hb : WeightedBound U s (m + (w.length - 2)) B (lowJet G)) :
    WeightedBound U s m (B / s ^ (w.length - 2)) (jet G w a) := by
…

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