CarlesonExponential.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

From factorial counting moments to an exponential tail

For a finite count the exponential series can be integrated using a constant summable majorant. The exact factorial moment bound therefore gives exponential average at most two and the required Markov tail.

theorem OAI.LipschitzHilbert.factorial_moments_exponential_bound line 26
theorem OAI.LipschitzHilbert.exponential_moment_tail line 82

theorem OAI.LipschitzHilbert.laminar_count_exponential_tail line 105

Source documentation

Exact exponential tail for the finite occurrence count in one root.

theorem laminar_count_exponential_tail {ι : Type*} [Fintype ι]
    (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)
    (lambda : ℝ) :
    μ.real ({x | lambda < laminarCount Q x} ∩ P₀) ≤
      2 * μ.real P₀ * Real.exp (-lambda / (2 * A)) := by
…

Mentions: OAI.LipschitzHilbert.laminarCount