MultipointCutoffExhaustion.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Integer localization bounds eventually contain every successful finite family of completion prefixes. Height monotonicity reduces the spatial bound to the two endpoints of each individual prefix.

theorem OAI.SLEExactGauge.Multipoint.completion_prefixes_bounded_by_nat line 15

theorem OAI.SLEExactGauge.Multipoint.eventually_localization_after_completed line 56

Source documentation

The standard integer localizations eventually survive beyond any fixed successful completion horizon. Their frozen completion times may be horizon truncations, provided those truncations eventually agree.

theorem eventually_localization_after_completed
    {Ω ι : Type*} [mΩ : MeasurableSpace Ω] [Fintype ι]
    (B : ℝ≥0 → Ω → ℝ) (hm : ∀ t, Measurable (B t))
    (hBc : ∀ ω, Continuous (fun t => B t ω))
    (κ A : ℝ) (hA : 0 ≤ A) (z : ι → ℂ)
    (τ : ℕ → ι → Ω → ℝ≥0)
    (γ : Ω → ℝ≥0 → ℂ) (G F : Ω → ℝ≥0 → ℂ → ℂ)
    (hw : ∀ ω, IsCapacityTwoWitness (fun t => Real.sqrt κ*B t ω)
      (γ ω) (G ω) (F ω))
    (S : ∀ n : ℕ, LocalizedState B hm κ (-(A+n+1)) (A+n+1) (A+n+1)
      ((n : ℝ≥0)+1) z (τ n) γ G)
    (ω : Ω) (σ : ι → ℝ≥0) (T : ℝ≥0)
…

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