CenteredStoppedTails.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Tail events of increasing canonical scalars under consistent finite laws. Only the stopped past is transported when the terminal level is increased.

theorem OAI.SLEExactGauge.finiteCenteredLaw_stoppedScalar_tail_mono line 14

lemma OAI.SLEExactGauge.stoppedScalar_tail_moment_bound line 59

Source documentation

A finite-law moment gives a tail bound without constructing an infinite centered path law. This form is convenient before taking the level supremum.

lemma stoppedScalar_tail_moment_bound
    {Ω : Type*} [MeasurableSpace Ω] (Q : Measure Ω)
    (X : Ω → ℝ) (hX : Measurable X)
    (b : ℝ) (hb : 0 ≤ b) (n : ℕ) :
    ENNReal.ofReal (b^n)*Q {ω | b ≤ X ω} ≤ ∫⁻ ω, ENNReal.ofReal (X ω)^n ∂Q := by
…