OAI/Analysis/LipschitzHilbert/Trees/SourceAllDyadicMaximal.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Dyadic maximal averages over all integer scales. Uniform finite estimates give the countable-scale estimate without any scale loss.

  1. theorem OAI.LipschitzHilbert.DyadicLineGrid.dyadicWindow_mono line 12
  2. def OAI.LipschitzHilbert.DyadicLineGrid.allDyadicMaximal line 26
  3. theorem OAI.LipschitzHilbert.DyadicLineGrid.allDyadicMaximal_measurable line 29
  4. theorem OAI.LipschitzHilbert.DyadicLineGrid.allDyadicMaximal_nonneg line 33
  5. theorem OAI.LipschitzHilbert.DyadicLineGrid.cellMean_le_window line 36
  6. theorem OAI.LipschitzHilbert.DyadicLineGrid.allDyadicMaximal_energy line 53

    Source documentation

    The genuine dyadic maximal operator is L² bounded, and dominates all integer-scale averages simultaneously outside a single null set.

    theorem allDyadicMaximal_energy (q : ℤ) {f : ℝ → ℝ} (hf : MemLp f 2 volume) :
    MemLp (allDyadicMaximal q f) 2 volume ∧
    (∫ x, (allDyadicMaximal q f x)^2)≤4*∫ x, (f x)^2 ∧
    ∀ᵐ x ∂volume, ∀ k : ℤ, |cellMean q k f x|≤allDyadicMaximal q f x := by
…

    Mentions: OAI.LipschitzHilbert.DyadicLineGrid.allDyadicMaximal, OAI.LipschitzHilbert.DyadicLineGrid.cellMean