OAI/Probability/SLE/Geometry/CanonicalRestartWitness.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SLEExactGauge.canonical_driver_isBrownian line 25

   Source documentation

   Evaluation on the canonical continuous-driver law is the same Brownian motion law, so the trace-generation input below is applied to a Brownian driver.

   theorem canonical_driver_isBrownian
       {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω}
       (B : ℝ≥0 → Ω → ℝ) (hB : IsBrownianReal B P)
       (hm : ∀ t, Measurable (B t)) (hc : ∀ ω, Continuous (fun t => B t ω)) :
       IsBrownianReal (fun (t : ℝ≥0) (p : C(ℝ≥0, ℝ)) => p t)
         (P.map (sourceDriverPath B hc)) := by
   …

   Mentions: OAI.SLEExactGauge.sourceDriverPath

2. theorem OAI.SLEExactGauge.exists_measurable_canonical_witness line 39
3. theorem OAI.SLEExactGauge.canonical_witness_pullback line 68
4. theorem OAI.SLEExactGauge.canonical_witness_original_trace line 81
5. theorem OAI.SLEExactGauge.source_canonical_witness_boundary_restart line 106

   Source documentation

   The same fresh path has an actual capacity witness and realizes the all-time finite-boundary restart identity. The only new instance of trace generation is its explicit specialization to the original driver path law.

   theorem source_canonical_witness_boundary_restart
       {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
       (κ : ℝ) (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 : PublishedTraceGeneration (P.map (sourceDriverPath B hc)) κ (fun t p => p t))
       (hboundary : PublishedFiniteLoewnerBoundaryExtension)
       (τ : Ω → ℝ≥0)
       (hτ : IsStoppingTime (Filtration.natural B (fun t => (hm t).stronglyMeasurable))
         (fun ω => (τ ω : WithTop ℝ≥0))) :
   …

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