MultipointCutoffSuccess.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A successful path remains before the common localization boundary once its finitely many completion prefixes have strict bounds.

lemma OAI.SLEExactGauge.Multipoint.LocalizedState.at_cutoff_eq_actual line 14

theorem OAI.SLEExactGauge.Multipoint.LocalizedState.cutoff_after_completed line 35

Source documentation

Every point is monitored only up to its own completion. Once all completion prefixes satisfy the strict bounds, the localization cannot occur before the common completion horizon.

theorem LocalizedState.cutoff_after_completed
    {Ω ι : Type*} [mΩ : MeasurableSpace Ω] [Fintype ι]
    {B : ℝ≥0 → Ω → ℝ} {hm : ∀ t, Measurable (B t)}
    {κ lo hi M : ℝ} {H : ℝ≥0} {z : ι → ℂ} {τ : ι → Ω → ℝ≥0}
    {γ : Ω → ℝ≥0 → ℂ} {G : Ω → ℝ≥0 → ℂ → ℂ}
    (S : LocalizedState B hm κ lo hi M H z τ γ G) (ω : Ω)
    (T : ℝ≥0) (hT : T < H) (_hτ : ∀ i, τ i ω ≤ T)
    (hB : ∀ t : ℝ≥0, t ≤ T → |B t ω| < M)
    (hheight : ∀ i (t : ℝ≥0), t ≤ τ i ω →
      (logLoewnerCoordinates (G ω) (z i) t).1.im ∈ Ioo lo hi) :
    T < S.χ ω := by
…

Mentions: OAI.SLEExactGauge.Multipoint.LocalizedState, OAI.SLEExactGauge.logLoewnerCoordinates