WeightedLowCoefficients.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform angular-slice estimates for smooth low-jet coefficients on a compact admissible set. The angular parameter adds no scale loss.

lemma OAI.ClosedSurfaceR4.JetPolynomial.weighted_lowJet_pair line 14

theorem OAI.ClosedSurfaceR4.JetPolynomial.compact_low_coefficient line 33

Source documentation

The same constant controls every angular slice over the unit period.

theorem compact_low_coefficient {U : Set Base} {O K : Set LowJet}
    (hU : IsOpen U) (hO : IsOpen O) (hK : IsCompact K) (hKO : K ⊆ O)
    {c : LowJet × ℝ → ℝ} (hc : ContDiffOn ℝ ∞ c (O ×ˢ Set.univ))
    (m : ℕ) (B : ℝ) (hB : 1 ≤ B) :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ (Q : Base → LowJet) (s : ℝ), 0 < s →
      ContDiffOn ℝ ∞ Q U → Set.MapsTo Q U K → WeightedBound U s m B Q →
      ∀ t ∈ Set.Icc (0 : ℝ) 1, WeightedBound U s m D (fun p => c (Q p, t)) := by
…

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