MultipointCutoff.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Exhaustion of successful multipoint paths by nonsingular cutoffs. Each point is monitored only through its own completion time. Later swallowing of an already completed point does not enter this lemma.

lemma OAI.SLEExactGauge.Multipoint.eventually_compact_positive_reciprocal line 15

theorem OAI.SLEExactGauge.Multipoint.successful_path_eventually_inside_cutoff line 29

Source documentation

On a successful path, finitely many individually stopped points admit one common height, angle, and physical-time cutoff.

theorem successful_path_eventually_inside_cutoff
    {ι : Type*} [Finite ι] (T : ι → ℝ) (Y θ : ι → ℝ → ℝ)
    (hY : ∀ i, ContinuousOn (Y i) (Icc 0 (T i)))
    (hθ : ∀ i, ContinuousOn (θ i) (Icc 0 (T i)))
    (hYpos : ∀ i t, t ∈ Icc 0 (T i) → 0 < Y i t)
    (hθpos : ∀ i t, t ∈ Icc 0 (T i) → 0 < θ i t)
    (hθpi : ∀ i t, t ∈ Icc 0 (T i) → θ i t < Real.pi) :
    ∀ᶠ n : ℕ in atTop, ∀ i,
      T i < (n : ℝ)+1 ∧ ∀ t ∈ Icc 0 (T i),
        1 / ((n : ℝ)+1) < Y i t ∧
        1 / ((n : ℝ)+1) < θ i t ∧
        θ i t < Real.pi - 1 / ((n : ℝ)+1) := by
…

lemma OAI.SLEExactGauge.Multipoint.measure_le_of_eventual_cutoffs line 59

Source documentation

Bounds for nonsingular stopped products pass to the successful event when each successful path eventually lies inside every cutoff.

lemma measure_le_of_eventual_cutoffs {Ω : Type*} [MeasurableSpace Ω]
    (P : Measure Ω) (E : Set Ω) (cutoff : ℕ → Set Ω) (C : ℝ≥0∞)
    (hcover : ∀ ω ∈ E, ∀ᶠ n : ℕ in atTop, ω ∈ cutoff n)
    (hbound : ∀ n, P (cutoff n) ≤ C) : P E ≤ C := by
…