OAI/Analysis/LipschitzHilbert/Trees/SourceAllStrongMaximal.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Countable-scale coordinate maximal functions on the plane, with uniform strong L² control.

  1. def OAI.LipschitzHilbert.DyadicLineGrid.allHorizontalMaximal line 11
  2. def OAI.LipschitzHilbert.DyadicLineGrid.allVerticalMaximal line 14
  3. def OAI.LipschitzHilbert.DyadicLineGrid.allStrongMaximal line 17
  4. theorem OAI.LipschitzHilbert.DyadicLineGrid.allHorizontalMaximal_measurable line 20
  5. theorem OAI.LipschitzHilbert.DyadicLineGrid.allVerticalMaximal_measurable line 24
  6. theorem OAI.LipschitzHilbert.DyadicLineGrid.allStrongMaximal_measurable line 28
  7. theorem OAI.LipschitzHilbert.DyadicLineGrid.allHorizontalMaximal_nonneg line 32
  8. theorem OAI.LipschitzHilbert.DyadicLineGrid.allVerticalMaximal_nonneg line 35
  9. theorem OAI.LipschitzHilbert.DyadicLineGrid.allStrongMaximal_nonneg line 38
  10. theorem OAI.LipschitzHilbert.DyadicLineGrid.allHorizontalMaximal_energy line 41
  11. theorem OAI.LipschitzHilbert.DyadicLineGrid.allVerticalMaximal_energy line 62
  12. theorem OAI.LipschitzHilbert.DyadicLineGrid.allStrongMaximal_energy line 83

    Source documentation

    Strong dyadic L² control at every integer scale, with no finite truncation remaining in the statement.

    theorem allStrongMaximal_energy (qx qy : ℤ) {f : ℝ×ℝ → ℝ}
    (hfmeas : Measurable f) (hf : MemLp f 2 (volume.prod volume)) :
    MemLp (allStrongMaximal qx qy f) 2 (volume.prod volume) ∧
    (∫ z, (allStrongMaximal qx qy f z)^2 ∂volume.prod volume)≤
      16*∫ z, (f z)^2 ∂volume.prod volume := by
…

    Mentions: OAI.LipschitzHilbert.DyadicLineGrid.allStrongMaximal