ExtendedMarkedAngle.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The good-angle event at an actual radius level belongs to that literal stopping time's past. Infinite stopping times are excluded explicitly. Measurability follows by finite cutoff exhaustion of the stopped chart.

def OAI.SLEExactGauge.extendedMarkedGood line 17

Source documentation

The stopped marked state at a finite extended stopping time.

def extendedMarkedGood {Ω : Type*} (κ : ℝ) (B : ℝ≥0 → Ω → ℝ)
    (γ : Ω → ℝ≥0 → ℂ) (G : Ω → ℝ≥0 → ℂ → ℂ)
    (σ : Ω → WithTop ℝ≥0) (z : ℂ) (s : ℝ) : Set Ω :=
…

lemma OAI.SLEExactGauge.stoppedMarkedGood_time_congr line 22
lemma OAI.SLEExactGauge.extendedMarkedGood_measurable line 33
lemma OAI.SLEExactGauge.extendedMarkedGood_eq_actual_angle line 72
lemma OAI.SLEExactGauge.canonical_good_angle_eq_extendedMarkedGood line 87

theorem OAI.SLEExactGauge.canonical_good_angle_measurable_at_radius line 127

Source documentation

The jointly measurable canonical angle event also belongs to the literal actual radius stop's past.

theorem canonical_good_angle_measurable_at_radius
    {Ω : 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) (u s : ℝ) (hu : 0 ≤ u) :
    MeasurableSet[(actual_radiusLevelTime_stopping hB hm hBm hc hB0 κ hκ hκ8
      γ G F hw z hz u hu).measurableSpace]
…

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

theorem OAI.SLEExactGauge.actual_good_angle_measurable_at_radius line 146

Source documentation

The same stopped-past measurability for the literal geometric angle.

theorem actual_good_angle_measurable_at_radius
    {Ω : 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) (u s : ℝ) (hu : 0 ≤ u) :
    MeasurableSet[(actual_radiusLevelTime_stopping hB hm hBm hc hB0 κ hκ hκ8
      γ G F hw z hz u hu).measurableSpace]
…

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