ExtendedRibbonStep.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

First-front stops may be infinite on failed experiments. Exhaust the admissible event through finite horizons, so the actual finite-stop restart bound applies without requiring completion on failed samples.

def OAI.SLEExactGauge.shiftedActualTrace line 20
def OAI.SLEExactGauge.ActualRibbonAdmissible line 24

theorem OAI.SLEExactGauge.actual_ribbon_restart_at_extended_stop line 33

Source documentation

The quantitative actual ribbon restart bound extends to a stopping time finite on the admissible past event. All future traces use the original random completion time, rather than its horizon truncations.

theorem actual_ribbon_restart_at_extended_stop
    {Ω : Type*} [mΩ : MeasurableSpace Ω] (P : Measure Ω)
    (ℱ : Filtration ℝ≥0 mΩ)
    (U : Ω → ℝ≥0 → ℝ) (γ : Ω → ℝ≥0 → ℂ)
    (hc : ∀ ω, Continuous (γ ω)) (G F : Ω → ℝ≥0 → ℂ → ℂ)
    (C L : ℝ≥0) (ε κ v c : ℝ) (q : ℝ≥0∞) (S : Set C(ℝ≥0, ℂ))
    (hfiniteStep : ∀ (σ : Ω → ℝ≥0)
      (hσ : IsStoppingTime ℱ (fun ω => (σ ω : WithTop ℝ≥0))) (E : Set Ω),
      (∀ᵐ ω ∂P, ω ∈ E → ActualRibbonAdmissible U γ G F C L ε κ v c S ω (σ ω)) →
      ∀ A : Set Ω, MeasurableSet[hσ.measurableSpace] A → A ⊆ E →
        q * P A ≤ P (A ∩ {ω | shiftedActualTrace γ hc ω (σ ω) ∈ S}))
    (τ : Ω → WithTop ℝ≥0) (hτ : IsStoppingTime ℱ τ)
…

Mentions: OAI.SLEExactGauge.ActualRibbonAdmissible, OAI.SLEExactGauge.shiftedActualTrace

theorem OAI.SLEExactGauge.uniform_conditional_actual_ribbon_step_extended line 97

Source documentation

Actual adapted ribbon passages at the possibly infinite first-front stops used by the dense experiment. The constants are the same uniform constants obtained at finite stops from the published analytic inputs.

theorem uniform_conditional_actual_ribbon_step_extended
    {Ω : Type} [mΩ : MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (B : ℝ≥0 → Ω → ℝ) (hB : IsBrownianReal B P)
    (hm : ∀ t, Measurable (B t)) (hc : ∀ ω, Continuous (fun t => B t ω))
    (γ : Ω → ℝ≥0 → ℂ) (G F : Ω → ℝ≥0 → ℂ → ℂ)
    (hw : ∀ ω, IsCapacityTwoWitness (fun t => Real.sqrt κ * B t ω)
      (γ ω) (G ω) (F ω))
    (hcompact : PublishedHalfPlaneUnivalentCompactness)
    (hboundary : PublishedFiniteLoewnerBoundaryExtension)
    (hsupport : PublishedGeometricTubeSupport P γ)
    (hplanar : PublishedPlanarDiskOpenness)
…

Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.PublishedHalfPlaneUnivalentCompactness, OAI.SLEExactGauge.PublishedFiniteLoewnerBoundaryExtension, OAI.SLEExactGauge.PublishedGeometricTubeSupport, OAI.SLEExactGauge.PublishedPlanarDiskOpenness