OAI/Probability/SLE/Geometry/FiniteBoundaryRestart.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SLEExactGauge.closed_halfplane_map_ext line 23
2. lemma OAI.SLEExactGauge.finite_boundary_extension_family_measurable line 46
3. theorem OAI.SLEExactGauge.source_stopped_finiteBoundaryPath_measurable line 61

   Source documentation

   Finite boundary evaluations are determined by the stopping-time past.

   theorem source_stopped_finiteBoundaryPath_measurable
       (hpublished : PublishedFiniteLoewnerBoundaryExtension)
       {Ω : 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, ℂ),
         Measurable[hτ.measurableSpace] Fb ∧
   …

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

4. theorem OAI.SLEExactGauge.source_measurable_finite_boundary_restart line 91

   Source documentation

   The actual future trace is the finite boundary image of the fresh trace, using a chart measurable in precisely the same stopped past.

   theorem source_measurable_finite_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 : PublishedFiniteLoewnerBoundaryExtension)
       (τ : Ω → ℝ≥0)
       (hτ : IsStoppingTime (Filtration.natural B (fun t => (hm t).stronglyMeasurable))
         (fun ω => (τ ω : WithTop ℝ≥0))) :
   …

   Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.PublishedFiniteLoewnerBoundaryExtension