WeightedMixedJets.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform mixed-variation bounds with the sharp excess-jet scale loss.

theorem OAI.ClosedSurfaceR4.JetPolynomial.MixedExpression.compact_mixed_bound line 15

Source documentation

Unit weighted bounds on the direction maps cost their full jet orders; the base map costs only the order beyond its controlled second jet.

theorem compact_mixed_bound {U : Set Base} {O K : Set LowJet}
    (hU : IsOpen U) (hO : IsOpen O) (hK : IsCompact K) (hKO : K ⊆ O)
    (e : MixedExpression) (he : e.SmoothCoeffs O) (m : ℕ) (B : ℝ) (hB : 1 ≤ B) :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ (G : Fin 4 → Base → Space) (s : ℝ), 0 < s → s ≤ 1 →
      (∀ i, ContDiff ℝ ∞ (G i)) → Set.MapsTo (lowJet (G 0)) U K →
      WeightedBound U s (m + e.order) B (lowJet (G 0)) →
      (∀ i : Fin 3, WeightedBound U s (m + e.order) 1 (G i.succ)) →
      ∀ 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.MixedExpression, OAI.ClosedSurfaceR4.JetPolynomial.Space, OAI.ClosedSurfaceR4.JetPolynomial.lowJet