RandomBoundaryTubes.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Measurable continuation tubes whose physical boundary charts depend on the stopped past. Positivity of each section uses the published geometric support theorem only for one fixed open tube at a time.

def OAI.SLEExactGauge.ClosedPathProperty line 20
theorem OAI.SLEExactGauge.isClosed_closedPathProperty line 22
def OAI.SLEExactGauge.liftClosedPath line 33
Source documentation
Give arbitrary continuous paths a measurable closed-half-plane version. On every actual chordal trace this is precisely the original path.
```
def liftClosedPath (p : C(ℝ≥0, ℂ)) : C(ℝ≥0, closedHalfPlane) := by
…
```
Mentions: OAI.SLEExactGauge.closedHalfPlane
theorem OAI.SLEExactGauge.liftClosedPath_apply line 39
theorem OAI.SLEExactGauge.measurable_liftClosedPath line 43
def OAI.SLEExactGauge.pathTubeEventIn line 55
theorem OAI.SLEExactGauge.isOpen_pathTubeEventIn line 59
def OAI.SLEExactGauge.randomBoundaryTubeSet line 73
theorem OAI.SLEExactGauge.measurableSet_randomBoundaryTubeSet line 78

theorem OAI.SLEExactGauge.boundary_tube_positive_of_geometric_support line 90

Source documentation

Each physical open continuation has positive probability under the fresh trace law once one simple parameter route lies in it.

theorem boundary_tube_positive_of_geometric_support
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    (gp : Ω → C(ℝ≥0, ℂ)) (hclosed : ∀ ω, ClosedPathProperty (gp ω))
    (hsupport : PublishedGeometricTubeSupport P (fun ω => gp ω))
    (Fb : C(closedHalfPlane, OnePoint ℂ))
    (O W : Set (OnePoint ℂ)) (hO : IsOpen O) (hW : IsOpen W)
    (z : ℂ) (p : Path (0 : ℂ) z) (hinj : Function.Injective p)
    (hpH : ∀ t, t ≠ 0 → p t ∈ upperHalfPlane)
    (hroute : ∀ t, Fb ⟨p t, by
      by_cases ht : t = 0
      · simp [ht, closedHalfPlane]
      · exact (show 0 < (p t).im from hpH t ht).le⟩ ∈ O)
…

Mentions: OAI.SLEExactGauge.ClosedPathProperty, OAI.SLEExactGauge.PublishedGeometricTubeSupport, OAI.SLEExactGauge.closedHalfPlane, OAI.SLEExactGauge.upperHalfPlane

theorem OAI.SLEExactGauge.restart_law_liftClosedPath line 141

Source documentation

The restricted restart law also holds after applying the measurable closed-half-plane lift to the fresh path.

theorem restart_law_liftClosedPath
    {Ω : Type*} [mΩ : MeasurableSpace Ω] (P : Measure Ω)
    (m : MeasurableSpace Ω)
    (Y gp : Ω → C(ℝ≥0, ℂ)) (hY : Measurable[mΩ] Y) (hgp : Measurable[mΩ] gp)
    (hlaw : ∀ A : Set Ω, MeasurableSet[m] A →
      @Measure.map Ω C(ℝ≥0, ℂ) mΩ _ Y (P.restrict A) =
        P A • @Measure.map Ω C(ℝ≥0, ℂ) mΩ _ gp P) :
    ∀ A : Set Ω, MeasurableSet[m] A →
      @Measure.map Ω C(ℝ≥0, closedHalfPlane) mΩ _ (liftClosedPath ∘ Y) (P.restrict A) =
        P A • @Measure.map Ω C(ℝ≥0, closedHalfPlane) mΩ _ (liftClosedPath ∘ gp) P := by
…

Mentions: OAI.SLEExactGauge.closedHalfPlane, OAI.SLEExactGauge.liftClosedPath

theorem OAI.SLEExactGauge.conditional_random_boundary_tube_positive line 160

Source documentation

No uniform support constant is needed for random pasts. Pointwise simple access routes imply strictly positive conditional passage probability.

theorem conditional_random_boundary_tube_positive
    {Ω : Type*} [mΩ : MeasurableSpace Ω]
    (P : Measure Ω) [IsFiniteMeasure P]
    (m : MeasurableSpace Ω) (hm : m ≤ mΩ)
    (Y gp : Ω → C(ℝ≥0, ℂ)) (hY : Measurable[mΩ] Y) (hgp : Measurable[mΩ] gp)
    (hlaw : ∀ A : Set Ω, MeasurableSet[m] A →
      @Measure.map Ω C(ℝ≥0, ℂ) mΩ _ Y (P.restrict A) =
        P A • @Measure.map Ω C(ℝ≥0, ℂ) mΩ _ gp P)
    (hclosed : ∀ ω, ClosedPathProperty (gp ω))
    (hsupport : @PublishedGeometricTubeSupport Ω mΩ P (fun ω => gp ω))
    (Fb : Ω → C(closedHalfPlane, OnePoint ℂ)) (hFb : Measurable[m] Fb)
    (O W : Set (OnePoint ℂ)) (hO : IsOpen O) (hW : IsOpen W)
…

Mentions: OAI.SLEExactGauge.ClosedPathProperty, OAI.SLEExactGauge.PublishedGeometricTubeSupport, OAI.SLEExactGauge.closedHalfPlane