SourceStrongDyadicMaximal.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Finite rectangular maximal averages on the actual nested line grids. The constants are uniform in both scale cutoffs.

def OAI.LipschitzHilbert.DyadicLineGrid.verticalMaximal line 11
def OAI.LipschitzHilbert.DyadicLineGrid.strongDyadicMaximal line 14
theorem OAI.LipschitzHilbert.DyadicLineGrid.verticalMaximal_measurable line 18
theorem OAI.LipschitzHilbert.DyadicLineGrid.strongDyadicMaximal_measurable line 22
theorem OAI.LipschitzHilbert.DyadicLineGrid.verticalMaximal_energy line 27

theorem OAI.LipschitzHilbert.DyadicLineGrid.strongDyadicMaximal_energy line 49

Source documentation

The composition of the two actual dyadic maximal operators has squared L² norm at most sixteen, independently of the number of scales.

theorem strongDyadicMaximal_energy (qx qy topx topy : ℤ) (Nx Ny : ℕ)
    {f : ℝ×ℝ → ℝ} (hfmeas : Measurable f) (hf : MemLp f 2 (volume.prod volume)) :
    MemLp (strongDyadicMaximal qx qy topx topy Nx Ny f) 2 (volume.prod volume) ∧
    (∫ z, (strongDyadicMaximal qx qy topx topy Nx Ny f z)^2 ∂volume.prod volume) ≤
      16*∫ z, (f z)^2 ∂volume.prod volume := by
…

Mentions: OAI.LipschitzHilbert.DyadicLineGrid.strongDyadicMaximal

theorem OAI.LipschitzHilbert.DyadicLineGrid.abs_cellMean_le_dyadicMaximal line 62
theorem OAI.LipschitzHilbert.DyadicLineGrid.horizontalMaximal_nonneg line 71
theorem OAI.LipschitzHilbert.DyadicLineGrid.verticalMaximal_nonneg line 74
theorem OAI.LipschitzHilbert.DyadicLineGrid.strongDyadicMaximal_nonneg line 77
theorem OAI.LipschitzHilbert.DyadicLineGrid.cellMean_mono line 83
Source documentation
Monotonicity of a literal cell average; integrability is only needed on the one cell in question.
```
theorem cellMean_mono (q k : ℤ) (x : ℝ) {f g : ℝ → ℝ}
    (hf : IntegrableOn f (cell q k (index q k x)))
    (hg : IntegrableOn g (cell q k (index q k x)))
    (hfg : ∀ y∈cell q k (index q k x), f y≤g y) :
    cellMean q k f x≤cellMean q k g x := by
…
```
Mentions: OAI.LipschitzHilbert.DyadicLineGrid.cell, OAI.LipschitzHilbert.DyadicLineGrid.index, OAI.LipschitzHilbert.DyadicLineGrid.cellMean