LaminarCarleson.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Factorial moments of a finite laminar count

This proves equation count:moment of §6. The hypotheses are the actual Carleson mass bound on the root and selected intervals and the geometric ordering of intersecting intervals by their scale.

def OAI.LipschitzHilbert.laminarCount line 26
theorem OAI.LipschitzHilbert.measurable_laminarCount line 28
theorem OAI.LipschitzHilbert.laminarCount_nonneg line 34
theorem OAI.LipschitzHilbert.laminarCount_le_card line 40
theorem OAI.LipschitzHilbert.tupleIntersection_comp_perm line 50
theorem OAI.LipschitzHilbert.product_indicators_eq_tuple_indicator line 63
theorem OAI.LipschitzHilbert.integral_laminarCount_pow line 70

theorem OAI.LipschitzHilbert.laminar_count_moment line 89

Source documentation

The finite laminar Carleson moment bound, with exact factorial constant.

theorem laminar_count_moment (Q : ι → Set X) (μ : Measure X) (rank : ι → ℤ)
    (hQ : ∀ i, MeasurableSet (Q i)) {P₀ : Set X} (hPfinite : μ P₀ ≠ ⊤)
    (hsub : ∀ i, Q i ⊆ P₀)
    (horder : ∀ i j, rank j ≤ rank i → (Q i ∩ Q j).Nonempty → Q j ⊆ Q i)
    {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 : ℕ) :
    (∫ x in P₀, laminarCount Q x ^ n ∂μ) ≤
      (n.factorial : ℝ) * A ^ n * μ.real P₀ := by
…

Mentions: OAI.LipschitzHilbert.laminarCount