FiniteCenteredConsistency.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Exact consistency of the finite centered laws on the past of an earlier conformal-radius stop. Extended stopping times are exhausted through finite cutoffs; the finite centered laws give the earlier stop finite time almost surely.

lemma OAI.SLEExactGauge.IsCapacityTwoWitness.physicalStoppedGreen_at_or_before line 18

theorem OAI.SLEExactGauge.finiteCenteredLaw_consistent_at_finite_stop line 37

Source documentation

Finite-stop consistency holds on the entire earlier stopped past, including events on which the later radius level is never reached.

theorem finiteCenteredLaw_consistent_at_finite_stop
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
    {B : ℝ≥0 → Ω → ℝ} (hB : IsBrownianReal B P)
    (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 : ∀ᵐ ω ∂P, IsCapacityTwoWitness
      (fun t => Real.sqrt κ * B t ω) (γ ω) (G ω) (F ω))
    (z : ℂ) (hz : z ∈ upperHalfPlane) (v V : ℝ) (hv : 0 ≤ v) (hvV : v ≤ V)
    (σ : Ω → ℝ≥0)
    (hσ : IsStoppingTime (Filtration.natural B
…

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

lemma OAI.SLEExactGauge.stopped_past_cover_of_ae_finite line 84

theorem OAI.SLEExactGauge.finiteCenteredLaw_earlier_stop_ae_finite line 104

Source documentation

Every earlier stop is finite under a later finite centered law, even when it is infinite on a set of positive original probability.

theorem finiteCenteredLaw_earlier_stop_ae_finite
    {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
    {B : ℝ≥0 → Ω → ℝ} (hB : IsBrownianReal B P)
    (hc : ∀ ω, Continuous (fun t => B t ω))
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (γ : Ω → ℝ≥0 → ℂ) (G F : Ω → ℝ≥0 → ℂ → ℂ)
    (hw : ∀ᵐ ω ∂P, IsCapacityTwoWitness
      (fun t => Real.sqrt κ * B t ω) (γ ω) (G ω) (F ω))
    (z : ℂ) (hz : z ∈ upperHalfPlane) (v V : ℝ) (hv : 0 ≤ v) (hvV : v ≤ V)
    (σ : Ω → WithTop ℝ≥0)
    (hbefore : ∀ᵐ ω ∂P, σ ω ≤ radiusLevelTime (γ ω) (G ω) z v) :
    ∀ᵐ ω ∂finiteCenteredLaw P κ B γ G z V, σ ω ≠ ⊤ := by
…

Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.upperHalfPlane, OAI.SLEExactGauge.radiusLevelTime, OAI.SLEExactGauge.finiteCenteredLaw

theorem OAI.SLEExactGauge.finiteCenteredLaw_consistent_at_extended_stop line 128

Source documentation

Extended-stop consistency. The sole geometric requirement is that this stop occur no later than the earlier conformal-radius level almost surely under the original law.

theorem finiteCenteredLaw_consistent_at_extended_stop
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
    {B : ℝ≥0 → Ω → ℝ} (hB : IsBrownianReal B P)
    (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 : ∀ᵐ ω ∂P, IsCapacityTwoWitness
      (fun t => Real.sqrt κ * B t ω) (γ ω) (G ω) (F ω))
    (z : ℂ) (hz : z ∈ upperHalfPlane) (v V : ℝ) (hv : 0 ≤ v) (hvV : v ≤ V)
    (σ : Ω → WithTop ℝ≥0)
    (hσ : IsStoppingTime (Filtration.natural B
…

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

theorem OAI.SLEExactGauge.finiteCenteredLaw_consistent_at_radius_stop line 176

Source documentation

The cover application: any stopping-time version of the actual radius-v time has exactly the same stopped-past law under every later finite centered measure.

theorem finiteCenteredLaw_consistent_at_radius_stop
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
    {B : ℝ≥0 → Ω → ℝ} (hB : IsBrownianReal B P)
    (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 : ∀ᵐ ω ∂P, IsCapacityTwoWitness
      (fun t => Real.sqrt κ * B t ω) (γ ω) (G ω) (F ω))
    (z : ℂ) (hz : z ∈ upperHalfPlane) (v V : ℝ) (hv : 0 ≤ v) (hvV : v ≤ V)
    (σ : Ω → WithTop ℝ≥0)
    (hσ : IsStoppingTime (Filtration.natural B
…

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