LaminarChains.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Iterated Carleson sums for a finite laminar family

The family is indexed by occurrences, so equal geometric intervals from different bins retain their multiplicity. Iterating the actual Carleson mass bound controls every non-strict nested-chain sum.

def OAI.LipschitzHilbert.tupleIntersection line 28
def OAI.LipschitzHilbert.laminarChainWeight line 31
theorem OAI.LipschitzHilbert.laminarChainWeight_nonneg line 38
def OAI.LipschitzHilbert.tupleHeadTailEquiv line 48
theorem OAI.LipschitzHilbert.sum_laminarChainWeight_succ line 54

theorem OAI.LipschitzHilbert.sum_laminarChainWeight_le line 67

Source documentation

The second inequality of count:moment, with repeated intervals allowed.

theorem sum_laminarChainWeight_le (Q : ι → Set X) (μ : Measure X) (P₀ : Set X)
    {A : ℝ} (hA : 0 ≤ A)
    (hcarleson : ∀ P, P = P₀ ∨ P ∈ Set.range Q →
      (∑ i, if Q i ⊆ P then μ.real (Q i) else 0) ≤ A * μ.real P)
    (n : ℕ) {P : Set X} (hP : P = P₀ ∨ P ∈ Set.range Q) :
    (∑ a : Fin n → ι, laminarChainWeight Q μ n P a) ≤ A ^ n * μ.real P := by
…

Mentions: OAI.LipschitzHilbert.laminarChainWeight

theorem OAI.LipschitzHilbert.tupleIntersection_succ line 95
theorem OAI.LipschitzHilbert.laminarChainWeight_eq_intersection line 104

theorem OAI.LipschitzHilbert.sorted_intersection_mass_le_chain line 122

Source documentation

Monotonicity of the scale rank turns every nonempty intersection into an actual nested chain; empty intersections contribute zero.

theorem sorted_intersection_mass_le_chain (Q : ι → Set X) (μ : Measure X)
    (rank : ι → ℤ)
    (horder : ∀ i j, rank j ≤ rank i → (Q i ∩ Q j).Nonempty → Q j ⊆ Q i)
    (n : ℕ) (P : Set X) (a : Fin n → ι) (hsub : ∀ j, Q (a j) ⊆ P)
    (hsorted : Antitone (rank ∘ a)) :
    μ.real (tupleIntersection Q P a) ≤ laminarChainWeight Q μ n P a := by
…

Mentions: OAI.LipschitzHilbert.tupleIntersection, OAI.LipschitzHilbert.laminarChainWeight