StoppedBoundaryMeasurability.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Boundary charts are measurable from the stopped past. Their values on the real line are limits of measurable interior values, so choosing the published continuous extension introduces no additional random information.

abbrev OAI.SLEExactGauge.closedHalfPlane line 18
theorem OAI.SLEExactGauge.isClosed_closedHalfPlane line 20
instance OAI.SLEExactGauge.onePointComplexPolishSpace line 23
instance OAI.SLEExactGauge.onePointComplexMeasurableSpace line 27
instance OAI.SLEExactGauge.onePointComplexBorelSpace line 28

theorem OAI.SLEExactGauge.boundary_extension_eval_measurable line 38

Source documentation

A boundary evaluation is the limit along vertical interior approaches.

theorem boundary_extension_eval_measurable
    {Ω : Type*} [MeasurableSpace Ω]
    (f : Ω → ℂ → ℂ) (Fb : Ω → C(closedHalfPlane, OnePoint ℂ))
    (hf : ∀ z ∈ upperHalfPlane, Measurable (fun ω => f ω z))
    (hext : ∀ ω (z : closedHalfPlane), z.1 ∈ upperHalfPlane →
      Fb ω z = (f ω z : OnePoint ℂ))
    (z : closedHalfPlane) : Measurable (fun ω => Fb ω z) := by
…

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

theorem OAI.SLEExactGauge.closed_halfplane_boundary_map_measurable line 78
Source documentation
Borel measurability of a closed-half-plane continuous map is detected by its evaluations on a countable dense set.
```
theorem closed_halfplane_boundary_map_measurable
    {Ω : Type*} [MeasurableSpace Ω]
    (Fb : Ω → C(closedHalfPlane, OnePoint ℂ))
    (hFb : ∀ z, Measurable (fun ω => Fb ω z)) : Measurable Fb :=
…
```
Mentions: OAI.SLEExactGauge.closedHalfPlane
theorem OAI.SLEExactGauge.boundary_extension_family_measurable line 84

theorem OAI.SLEExactGauge.source_stopped_boundaryPath_measurable line 95

Source documentation

The actual normalized inverse at a finite stopping time admits a past-measurable family of continuous boundary extensions.

theorem source_stopped_boundaryPath_measurable
    (hpublished : PublishedLoewnerBoundaryExtension)
    {Ω : Type*} [m : MeasurableSpace Ω] (B : ℝ≥0 → Ω → ℝ)
    (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 ω))
    (τ : Ω → ℝ≥0)
    (hτ : IsStoppingTime (Filtration.natural B (fun t => (hm t).stronglyMeasurable))
      (fun ω => (τ ω : WithTop ℝ≥0))) :
    ∃ Fb : Ω → C(closedHalfPlane, OnePoint ℂ),
      Measurable[hτ.measurableSpace] Fb ∧
…

Mentions: OAI.SLEExactGauge.PublishedLoewnerBoundaryExtension, OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.closedHalfPlane