StoppedTubePassage.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Passage after a stopping time from countably many open tube certificates. The stopped trace law gives independence for each fixed tube. A countable cover of pasts then gives pointwise positive conditional passage probability; no common support probability is assumed.

theorem OAI.SLEExactGauge.conditional_passage_positive_on_certificate line 25

Source documentation

A fixed positive-law test, certified on a past event, forces the conditional passage probability to be positive on that event.

theorem conditional_passage_positive_on_certificate
    {Ω X : Type*} [mΩ : MeasurableSpace Ω] [mX : MeasurableSpace X]
    (P : Measure Ω) [IsFiniteMeasure P] (ν : Measure X)
    (m : MeasurableSpace Ω) (hm : m ≤ mΩ)
    (Y : Ω → X) (hY : Measurable[mΩ] Y)
    (hlaw : ∀ A : Set Ω, MeasurableSet[m] A →
      @Measure.map Ω X mΩ mX Y (P.restrict A) = P A • ν)
    (A C : Set Ω) (hA : MeasurableSet[m] A) (hC : MeasurableSet[mΩ] C)
    (B : Set X) (hB : MeasurableSet B) (hBpos : 0 < ν B)
    (hcert : A ∩ Y ⁻¹' B ⊆ C) :
    ∀ᵐ ω ∂P, ω ∈ A → 0 < P⁻[C.indicator (fun _ => 1) | m] ω := by
…

theorem OAI.SLEExactGauge.conditional_passage_positive_of_countable_certificates line 71

Source documentation

Countably many past-measurable tube certificates suffice even when their positive support probabilities depend on the certificate.

theorem conditional_passage_positive_of_countable_certificates
    {Ω X : Type*} [mΩ : MeasurableSpace Ω] [mX : MeasurableSpace X]
    (P : Measure Ω) [IsFiniteMeasure P] (ν : Measure X)
    (m : MeasurableSpace Ω) (hm : m ≤ mΩ)
    (Y : Ω → X) (hY : Measurable[mΩ] Y)
    (hlaw : ∀ A : Set Ω, MeasurableSet[m] A →
      @Measure.map Ω X mΩ mX Y (P.restrict A) = P A • ν)
    (E C : Set Ω) (hC : MeasurableSet[mΩ] C)
    (A : ℕ → Set Ω) (hA : ∀ i, MeasurableSet[m] (A i))
    (B : ℕ → Set X) (hB : ∀ i, MeasurableSet (B i))
    (hBpos : ∀ i, 0 < ν (B i))
    (hcert : ∀ i, A i ∩ Y ⁻¹' B i ⊆ C)
…

theorem OAI.SLEExactGauge.stopped_geometric_tube_passages line 98

Source documentation

The actual Brownian stopped trace law and the published geometric support input give conditional positivity for countably certified geometric continuations. The same realization also has the actual conformal restart identity, so the certificates can be checked in the original domain.

theorem stopped_geometric_tube_passages
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    (κ : ℝ) (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 ω))
    (hpublished : PublishedGeometricTubeSupport P γ) :
    ∃ Φ : C(ℝ≥0, ℝ) → C(ℝ≥0, ℂ), Measurable Φ ∧
      (∀ ω, Φ (sourceDriverPath B hc ω) =
        sourceTracePath γ (fun ω => (hw ω).1) ω) ∧
…

Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.PublishedGeometricTubeSupport, OAI.SLEExactGauge.sourceDriverPath, OAI.SLEExactGauge.sourceTracePath