BinCarleson.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A finite Carleson mass bound from disjoint intervals within each bin.

theorem OAI.LipschitzHilbert.sum_bin_indicators_le line 20

Source documentation

At a point, pairwise disjointness within each bin prevents that bin's function from being counted more than once.

theorem sum_bin_indicators_le (Q : ι → Set X) (bin : ι → B) (f : B → X → ℝ)
    (hf : ∀ b x, 0 ≤ f b x)
    (hdisj : ∀ i j, i ≠ j → bin i = bin j → Disjoint (Q i) (Q j)) (x : X) :
    (∑ i, (Q i).indicator (f (bin i)) x) ≤ ∑ b, f b x := by
…

theorem OAI.LipschitzHilbert.finite_bin_carleson line 41

Source documentation

The finite mass bound underlying the line counting lemma. Different bins may select the same interval; disjointness is needed only within a bin.

theorem finite_bin_carleson (Q : ι → Set X) (bin : ι → B) (f : B → X → ℝ)
    (μ : Measure X) {P : Set X} (hP : MeasurableSet P) (hPfinite : μ P ≠ ∞)
    (hQ : ∀ i, MeasurableSet (Q i)) (hsub : ∀ i, Q i ⊆ P)
    (hf : ∀ b, IntegrableOn (f b) P μ) (hnonneg : ∀ b x, 0 ≤ f b x)
    (hdisj : ∀ i j, i ≠ j → bin i = bin j → Disjoint (Q i) (Q j))
    {β C : ℝ} (hβ : 0 < β) (hsum : ∀ x ∈ P, (∑ b, f b x) ≤ C)
    (hbad : ∀ i, β * μ.real (Q i) ≤ ∫ x in Q i, f (bin i) x ∂μ) :
    (∑ i, μ.real (Q i)) ≤ (C / β) * μ.real P := by
…

theorem OAI.LipschitzHilbert.finite_bin_carleson_of_finite_sums line 75

Source documentation

The same estimate for an arbitrary bin type, using only a uniform bound on its finite partial sums.

theorem finite_bin_carleson_of_finite_sums {B' : Type*}
    (Q : ι → Set X) (bin : ι → B') (f : B' → X → ℝ)
    (μ : Measure X) {P : Set X} (hP : MeasurableSet P) (hPfinite : μ P ≠ ∞)
    (hQ : ∀ i, MeasurableSet (Q i)) (hsub : ∀ i, Q i ⊆ P)
    (hf : ∀ b, IntegrableOn (f b) P μ) (hnonneg : ∀ b x, 0 ≤ f b x)
    (hdisj : ∀ i j, i ≠ j → bin i = bin j → Disjoint (Q i) (Q j))
    {β C : ℝ} (hβ : 0 < β) (hsum : ∀ s : Finset B', ∀ x ∈ P, (∑ b ∈ s, f b x) ≤ C)
    (hbad : ∀ i, β * μ.real (Q i) ≤ ∫ x in Q i, f (bin i) x ∂μ) :
    (∑ i, μ.real (Q i)) ≤ (C / β) * μ.real P := by
…