MultipointRadiusSwitches.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The three actual radius switches of one multipoint factor: activation, the midpoint of its radius clock, and completion. They reuse the literal radius-level stopping times and are truncated only at the common finite localization horizon.

def OAI.SLEExactGauge.Multipoint.switchLevel line 17
lemma OAI.SLEExactGauge.Multipoint.switchLevel_nonneg line 22
lemma OAI.SLEExactGauge.Multipoint.switchLevel_monotone line 29
lemma OAI.SLEExactGauge.Multipoint.switchLevel_midpoint_offset line 39
lemma OAI.SLEExactGauge.Multipoint.switchLevel_completion_offset line 45
lemma OAI.SLEExactGauge.cutoffStop_le_horizon line 54
Distinct definitions of this name: OAI/Probability/SLE/Geometry/ExtendedStopLocalization.lean:20 (different declaration text). Qualify references as OAI.SLEExactGauge.cutoffStop_le_horizon@path.
lemma OAI.SLEExactGauge.cutoffStop_mono line 60

theorem OAI.SLEExactGauge.actual_radius_factor_switches line 69

Source documentation

Concrete activation, midpoint, and completion stopping times for a regular actual SLE, all localized at the same horizon.

theorem actual_radius_factor_switches
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {B : ℝ≥0 → Ω → ℝ} (hB : IsBrownianReal B P)
    (hm : ∀ t, Measurable (B t))
    (hBm : Measurable (fun p : ℝ≥0 × Ω => B p.1 p.2))
    (hc : ∀ ω, Continuous (fun t => B t ω)) (hB0 : ∀ ω, B 0 ω = 0)
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (γ : Ω → ℝ≥0 → ℂ) (G F : Ω → ℝ≥0 → ℂ → ℂ)
    (hw : ∀ ω, IsCapacityTwoWitness (fun t => Real.sqrt κ * B t ω) (γ ω) (G ω) (F ω))
    (z : ℂ) (hz : z ∈ upperHalfPlane)
    (R b e : ℝ) (he : 0 < e) (heb : e ≤ b) (hbR : b ≤ R) (H : ℝ≥0) :
    let τ := fun j : Fin 3 => cutoffStop
…

Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.upperHalfPlane, OAI.SLEExactGauge.cutoffStop