OAI/Analysis/LipschitzHilbert/Trees/SourceAxisMaximal.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual one-coordinate dyadic maximal operator on the plane. Fubini transfers the uniform line estimate without a dimension or scale count factor.

  1. def OAI.LipschitzHilbert.DyadicLineGrid.horizontalCellMean line 13
  2. def OAI.LipschitzHilbert.DyadicLineGrid.horizontalMaximal line 16
  3. theorem OAI.LipschitzHilbert.DyadicLineGrid.indexedCellIntegral_measurable line 19
  4. theorem OAI.LipschitzHilbert.DyadicLineGrid.horizontalCellMean_measurable line 27
  5. theorem OAI.LipschitzHilbert.DyadicLineGrid.horizontalMaximal_measurable line 41
  6. theorem OAI.LipschitzHilbert.DyadicLineGrid.horizontalMaximal_energy line 48

    Source documentation

    The horizontal maximal operator has squared L² norm at most four on the product Lebesgue measure.

    theorem horizontalMaximal_energy (q top : ℤ) (N : ℕ) {f : ℝ×ℝ → ℝ}
    (hfmeas : Measurable f) (hf : MemLp f 2 (volume.prod volume)) :
    MemLp (horizontalMaximal q top N f) 2 (volume.prod volume) ∧
    (∫ z, (horizontalMaximal q top N f z)^2 ∂volume.prod volume) ≤
      4*∫ z, (f z)^2 ∂volume.prod volume := by
…

    Mentions: OAI.LipschitzHilbert.DyadicLineGrid.horizontalMaximal