WeightedJetExpressions.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform weighted estimates for actual coordinate-jet expressions. The scale exponent is the algebraic excess-jet loss and is independent of the requested output derivative order.

lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.parameter_smooth line 15

theorem OAI.ClosedSurfaceR4.JetPolynomial.Expression.compact_expression_bound line 24

Source documentation

Compact low-jet control bounds every finite correction expression. Only the numerical prefactor depends on the output derivative order.

theorem compact_expression_bound {U : Set Base} {O K : Set LowJet}
    (hU : IsOpen U) (hO : IsOpen O) (hK : IsCompact K) (hKO : K ⊆ O)
    (e : Expression) (he : e.SmoothCoeffs O) (m : ℕ) (B : ℝ) (hB : 1 ≤ B) :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ (G : Base → Space) (s : ℝ), 0 < s → s ≤ 1 →
      ContDiff ℝ ∞ G → Set.MapsTo (lowJet G) U K →
      WeightedBound U s (m + e.order) B (lowJet G) →
      ∀ t ∈ Set.Icc (0 : ℝ) 1,
        WeightedBound U s m (D / s ^ e.loss) (fun p => e.eval G (p, t)) := by
…

Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.LowJet, OAI.ClosedSurfaceR4.JetPolynomial.Expression, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.JetPolynomial.lowJet