WeightedPhaseExpressions.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Two-scale estimates for the actual higher-jet expressions, with a varying angular phase. The slow-jet loss is independent of the output derivative order.

lemma OAI.ClosedSurfaceR4.JetPolynomial.weighted_pair line 13
lemma OAI.ClosedSurfaceR4.JetPolynomial.Expression.phase_smooth line 28

theorem OAI.ClosedSurfaceR4.JetPolynomial.Expression.compact_phase_bound line 38

Source documentation

The constant is uniform over the open spatial domain and the phase. The two scales are kept separate: differentiation is weighted at τ, whereas higher jets only cost powers of the slower scale s.

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

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