UniformPlanarRawBounds.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A common finite collection of Schwartz seminorm bounds gives a common raw-kernel constant for an entire packet family. The constant is explicit and independent of the particular planar profile.

theorem OAI.LipschitzHilbert.uniform_planar_raw_bounds line 17

Source documentation

The concrete general planar raw kernels and their horizontal derivatives obey uniform product-envelope bounds whenever the profile constant is uniformly bounded. The exact amplitude is (2^n*Cprof)*(M+2)*R^2, and differentiation costs exactly 1/l.

theorem uniform_planar_raw_bounds (f : SchwartzMap (ℝ × ℝ) ℂ) (n : ℕ)
    (Cprof : ℝ) (hprof : planarProfileConstant f (2 * n) ≤ Cprof)
    (a cy l W delta frequency scale R M : ℝ) (hl : 0 < l)
    (hR : 1 ≤ R) (hr : |scale / W| ≤ R) (hM : 0 ≤ M)
    (hs : |delta * l / W| ≤ 1) (hc : |frequency * delta * l| ≤ M)
    (i : Fin 3) (y x : ℝ) :
    ‖modulatedPlanarJet f a cy l W delta frequency scale y hl.ne' i x‖ ≤
      ((2 ^ n * Cprof) * (M + 2) * R ^ 2) *
        (lineEnvelope a l n x * lineEnvelope cy W n y) ∧
    ‖deriv (modulatedPlanarJet f a cy l W delta frequency scale y hl.ne' i) x‖ ≤
      (((2 ^ n * Cprof) * (M + 2) * R ^ 2) / l) *
        (lineEnvelope a l n x * lineEnvelope cy W n y) := by
…

Mentions: OAI.LipschitzHilbert.planarProfileConstant, OAI.LipschitzHilbert.modulatedPlanarJet, OAI.LipschitzHilbert.lineEnvelope