OAI/Probability/SLE/Geometry/NormalizedCanonicalRestart.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SLEExactGauge.normalizedRestartDriverPath line 25
2. lemma OAI.SLEExactGauge.normalizedRestartDriverPath_driver line 30
3. lemma OAI.SLEExactGauge.measurable_boundary_scale_family line 44
4. theorem OAI.SLEExactGauge.source_normalized_canonical_witness_boundary_restart line 60

   Source documentation

   The same canonical trace factor realizes every positive, past-measurable normalization of the restart, with its actual capacity witness and an all-time identity through the corresponding finite boundary chart.

   theorem source_normalized_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