OAI/Analysis/LipschitzHilbert/Trees/LineGridPrimitive.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Cell averages of a derivative are boundary differences. This is the high-frequency half of the manuscript's dyadic comparison.

  1. theorem OAI.LipschitzHilbert.FiniteLineGrid.average_deriv_eq line 17
  2. theorem OAI.LipschitzHilbert.FiniteLineGrid.average_deriv_cell_energy line 36
  3. theorem OAI.LipschitzHilbert.FiniteLineGrid.average_deriv_energy line 56

    Source documentation

    Each sample is charged by at most two adjacent cells, giving the exact boundary-sampling reduction used for high-frequency bands.

    theorem average_deriv_energy (g : FiniteLineGrid) (A : ℝ → ℝ)
    (hA : Differentiable ℝ A) (hd : Continuous (deriv A))
    {level : ℕ} (hl : level ≤ g.depth) :
    (∫ x, |g.average g.lineMeasure (deriv A) level x| ^ 2 ∂g.lineMeasure) ≤
      4 * (g.meshWidth level)⁻¹ * ∑ i : Fin (g.branching ^ level + 1),
        |A (g.origin + g.meshWidth level * i.val)| ^ 2 := by
…

    Mentions: OAI.LipschitzHilbert.FiniteLineGrid