OAI/Analysis/LipschitzHilbert/Trees/SourceGlobalDyadicMaximal.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A uniform L² bound for actual dyadic cell averages on the whole line. The root intervals are glued using their true measurable partition.

  1. def OAI.LipschitzHilbert.DyadicLineGrid.cellMean line 12
  2. def OAI.LipschitzHilbert.DyadicLineGrid.dyadicMaximal line 15
  3. theorem OAI.LipschitzHilbert.DyadicLineGrid.cellMean_measurable line 18
  4. theorem OAI.LipschitzHilbert.DyadicLineGrid.dyadicMaximal_measurable line 21
  5. theorem OAI.LipschitzHilbert.DyadicLineGrid.dyadicMaximal_nonneg line 25
  6. theorem OAI.LipschitzHilbert.DyadicLineGrid.dyadicMaximal_eq_on_root line 28
  7. theorem OAI.LipschitzHilbert.DyadicLineGrid.dyadicMaximal_root_memLp line 38
  8. theorem OAI.LipschitzHilbert.DyadicLineGrid.dyadicMaximal_root_energy line 48
  9. theorem OAI.LipschitzHilbert.DyadicLineGrid.dyadicMaximal_energy line 62

    Source documentation

    Actual finite dyadic maximal averages are L² bounded on Lebesgue measure with constant four in squared norm, uniformly in both cutoffs.

    theorem dyadicMaximal_energy (q top : ℤ) (N : ℕ) {f : ℝ → ℝ}
    (hf : MemLp f 2 volume) :
    MemLp (dyadicMaximal q top N f) 2 volume ∧
    (∫ x, (dyadicMaximal q top N f x)^2) ≤ 4*∫ x, (f x)^2 := by
…

    Mentions: OAI.LipschitzHilbert.DyadicLineGrid.dyadicMaximal