StoppedBoundaryRestart.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The stopped restart identity at every future time. Positive gauge measure on each nondegenerate trace segment and nullity of the real axis force interior trace times to be dense. This is a measurable path property, hence transfers through the actual stopped trace law. Continuity of the published inverse-map boundary extension then gives the identity also at boundary visits.

theorem OAI.SLEExactGauge.StoppedBoundaryRestart.segment_has_interior_time line 24

Source documentation

A positive-mass trace segment cannot lie on the null real axis.

theorem segment_has_interior_time
    (γ : ℝ≥0 → ℂ) (μ : Measure ℂ) (hH : ∀ u, 0 ≤ (γ u).im)
    (hnull : μ (range ((↑) : ℝ → ℂ)) = 0)
    {s t : ℝ≥0} (hpos : 0 < μ (γ '' Icc s t)) :
    ∃ u ∈ Icc s t, γ u ∈ upperHalfPlane := by
…

Mentions: OAI.SLEExactGauge.upperHalfPlane

theorem OAI.SLEExactGauge.StoppedBoundaryRestart.dense_interior_times line 41

Source documentation

Positive mass on every positive-time segment makes the interior trace visits dense, including at time zero.

theorem dense_interior_times
    (γ : ℝ≥0 → ℂ) (μ : Measure ℂ) (hH : ∀ u, 0 ≤ (γ u).im)
    (hnull : μ (range ((↑) : ℝ → ℂ)) = 0)
    (hpos : ∀ s t : ℝ≥0, 0 < s → s < t → 0 < μ (γ '' Icc s t)) :
    Dense {u : ℝ≥0 | γ u ∈ upperHalfPlane} := by
…

Mentions: OAI.SLEExactGauge.upperHalfPlane

def OAI.SLEExactGauge.StoppedBoundaryRestart.CountableInteriorHits line 60
Source documentation
Countably many open hit tests encode dense interior trace times.
```
def CountableInteriorHits (p : C(ℝ≥0, ℂ)) : Prop :=
…
```
theorem OAI.SLEExactGauge.StoppedBoundaryRestart.countableInteriorHits_iff line 65
theorem OAI.SLEExactGauge.StoppedBoundaryRestart.measurableSet_countableInteriorHits line 83
def OAI.SLEExactGauge.StoppedBoundaryRestart.GoodBoundaryPath line 108
theorem OAI.SLEExactGauge.StoppedBoundaryRestart.measurableSet_goodBoundaryPath line 111

theorem OAI.SLEExactGauge.StoppedBoundaryRestart.extend_restart_identity line 124

Source documentation

Only continuity and density are needed to fill in the boundary-time values of an inverse-chart identity.

theorem extend_restart_identity
    (p : C(ℝ≥0, ℂ)) (γ : ℝ≥0 → ℂ) (hγ : Continuous γ)
    (Fbar : ℂ → OnePoint ℂ)
    (hFbar : ContinuousOn Fbar {z : ℂ | 0 ≤ z.im})
    (hp : GoodBoundaryPath p)
    (heq : ∀ t, p t ∈ upperHalfPlane → (γ t : OnePoint ℂ) = Fbar (p t)) :
    ∀ t, (γ t : OnePoint ℂ) = Fbar (p t) := by
…

Mentions: OAI.SLEExactGauge.StoppedBoundaryRestart.GoodBoundaryPath, OAI.SLEExactGauge.upperHalfPlane

theorem OAI.SLEExactGauge.StoppedBoundaryRestart.ordinarySLE_ae_goodBoundaryPath line 142
Source documentation
The proved lower Hausdorff estimate and real-axis nullity give the measurable dense-interior path property for ordinary SLE.
```
theorem ordinarySLE_ae_goodBoundaryPath
    {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
    {κ : ℝ} (hκ : 0 < κ) (hκ8 : κ < 8)
    (γ : Ω → ℝ≥0 → ℂ) (hcont : ∀ ω, Continuous (γ ω))
    (hSLE : IsOrdinaryChordalSLE κ γ P) :
    ∀ᵐ ω ∂P, GoodBoundaryPath (sourceTracePath γ hcont ω) := by
…
```
Mentions: OAI.SLEExactGauge.IsOrdinaryChordalSLE, OAI.SLEExactGauge.StoppedBoundaryRestart.GoodBoundaryPath, OAI.SLEExactGauge.sourceTracePath

theorem OAI.SLEExactGauge.StoppedBoundaryRestart.stopped_boundary_restart line 165

Source documentation

The actual stopped trace law admits the continuous boundary restart identity at every future time, conditional only on the cited deterministic Rohde–Schramm boundary-extension input.

theorem stopped_boundary_restart
    {Ω : 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 : PublishedLoewnerBoundaryExtension) :
    ∃ Φ : C(ℝ≥0, ℝ) → C(ℝ≥0, ℂ), Measurable Φ ∧
      (∀ ω, Φ (sourceDriverPath B hc ω) = sourceTracePath γ (fun ω => (hw ω).1) ω) ∧
      ∀ (τ : Ω → ℝ≥0)
…

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

theorem OAI.SLEExactGauge.StoppedBoundaryRestart.boundary_restart_tube_transfer line 231

Source documentation

A tube event maps back to the physical domain at every time, including boundary visits, under the continuous boundary restart identity.

theorem boundary_restart_tube_transfer
    (p : C(ℝ≥0, ℂ)) (γ : ℝ≥0 → ℂ) (τ : ℝ≥0) (Fbar : ℂ → OnePoint ℂ)
    (heq : ∀ t, (γ (τ + t) : OnePoint ℂ) = Fbar (p t))
    (N V O W : Set ℂ)
    (hN : MapsTo Fbar N (((↑) : ℂ → OnePoint ℂ) '' O))
    (hV : MapsTo Fbar V (((↑) : ℂ → OnePoint ℂ) '' W))
    (hp : p ∈ pathTubeEvent N V) :
    ∃ T : ℝ≥0, 0 < T ∧ MapsTo (fun t => γ (τ + t)) (Icc 0 T) O ∧ γ (τ + T) ∈ W := by
…

Mentions: OAI.SLEExactGauge.pathTubeEvent

theorem OAI.SLEExactGauge.StoppedBoundaryRestart.restricted_tube_probability_le line 251

Source documentation

A past-restricted stopped-law tube probability is a lower bound for any physical event containing that tube almost surely. This formulation uses the full-measure boundary restart identity without imposing pathwise identities on exceptional samples.

theorem restricted_tube_probability_le
    {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω}
    (p : Ω → C(ℝ≥0, ℂ)) (hp : Measurable p) (Q : Measure C(ℝ≥0, ℂ))
    (A C : Set Ω) (hC : MeasurableSet C) (N V : Set ℂ)
    (hN : IsOpen N) (hV : IsOpen V)
    (hlaw : (P.restrict A).map p = P A • Q)
    (htransfer : ∀ᵐ ω ∂P, p ω ∈ pathTubeEvent N V → ω ∈ C) :
    P A * Q (pathTubeEvent N V) ≤ P (A ∩ C) := by
…

Mentions: OAI.SLEExactGauge.pathTubeEvent