DyadicLineCarleson.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual maximal bad intervals satisfy the finite Carleson bound.

theorem OAI.LipschitzHilbert.DyadicLineGrid.maximal_bad_carleson line 17

theorem OAI.LipschitzHilbert.DyadicLineGrid.maximal_bad_carleson_restricted line 45

Source documentation

Restricting a finite family of occurrences to any finite-measure test set preserves the same Carleson constant.

theorem maximal_bad_carleson_restricted {ι B : Type*} [Fintype ι]
    (q top : ℤ) (f : B → ℝ → ℝ) (bin : ι → B) (level pos : ι → ℤ)
    (hunique : ∀ i j, bin i = bin j → level i = level j → pos i = pos j → i = j)
    {β C : ℝ} (hβ : 0 < β)
    (hmax : ∀ i, MaximalBad q top (Bad q (f (bin i)) β) (level i) (pos i))
    (hf : ∀ b, Measurable (f b)) (hbound : ∀ b x, 0 ≤ f b x ∧ f b x ≤ 1)
    (hsum : ∀ s : Finset B, ∀ x, (∑ b ∈ s, f b x) ≤ C)
    {P : Set ℝ} (hP : MeasurableSet P) (hPfinite : volume P ≠ ∞) :
    (∑ i, if cell q (level i) (pos i) ⊆ P then volume.real (cell q (level i) (pos i)) else 0) ≤
      (C / β) * volume.real P := by
…

Mentions: OAI.LipschitzHilbert.DyadicLineGrid.MaximalBad, OAI.LipschitzHilbert.DyadicLineGrid.Bad, OAI.LipschitzHilbert.DyadicLineGrid.cell