OAI/Analysis/LipschitzHilbert/Fourier/HighFrequencyAverage.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The high-frequency cell-average bound from a band-scale primitive.

  1. theorem OAI.LipschitzHilbert.FiniteLineGrid.primitive_average_energy line 15
  2. theorem OAI.LipschitzHilbert.FiniteLineGrid.primitive_average_decay line 45

    Source documentation

    Inserting the primitive's band-scale L² estimate yields the small ratio of band scale to mesh scale.

    theorem primitive_average_decay (g : FiniteLineGrid) (A : ℝ → ℝ)
    (hA : Differentiable ℝ A) (hd : Continuous (deriv A))
    (hA2 : MemLp A 2 volume) (hd2 : MemLp (deriv A) 2 volume)
    {level : ℕ} (hl : level ≤ g.depth) {δ : ℝ} (hδ : 0 < δ)
    (hδmesh : δ ≤ g.meshWidth level) {C : ℝ}
    (hprimitive : (∫ x, A x ^ 2) ≤ C * δ ^ 2 * ∫ x, deriv A x ^ 2) :
    (∫ x, |g.average g.lineMeasure (deriv A) level x| ^ 2 ∂g.lineMeasure) ≤
      (8 * (C + 1) * δ / g.meshWidth level) * ∫ x, deriv A x ^ 2 := by
…

    Mentions: OAI.LipschitzHilbert.FiniteLineGrid