OAI/Probability/SLE/Loewner/CanonicalRadiusKernel.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SLEExactGauge.canonicalRadiusFamily line 18
2. def OAI.SLEExactGauge.canonicalRadius line 24
3. def OAI.SLEExactGauge.canonicalRadiusLevel line 27
4. lemma OAI.SLEExactGauge.canonicalRadius_measurable line 30
5. lemma OAI.SLEExactGauge.canonicalRadiusLevel_measurable line 33
6. lemma OAI.SLEExactGauge.canonicalRadius_eq line 36
7. lemma OAI.SLEExactGauge.canonicalRadiusLevel_eq line 44
8. lemma OAI.SLEExactGauge.measurable_canonicalRadiusLevel_random_state line 51
9. theorem OAI.SLEExactGauge.aemeasurable_radiusLevelTime_random_state line 60

   Source documentation

   A random measurable marked state has an actual radius-level time with a measurable version, with no point-dependent selection of an exceptional set.

   theorem aemeasurable_radiusLevelTime_random_state
       {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} (κ : ℝ)
       {Y : Ω → C(ℝ≥0, ℝ)} (hY : Measurable Y)
       (γ : Ω → ℝ≥0 → ℂ) (G F : Ω → ℝ≥0 → ℂ → ℂ)
       (hw : ∀ᵐ ω ∂P, IsCapacityTwoWitness
         (fun t => Real.sqrt κ * Y ω t) (γ ω) (G ω) (F ω))
       {u : Ω → ℝ} (hum : Measurable u) (hu : ∀ᵐ ω ∂P, 0 ≤ u ω)
       {z : Ω → ℂ} (hz : Measurable z) :
       AEMeasurable (fun ω => radiusLevelTime (γ ω) (G ω) (z ω) (u ω)) P := by
   …

   Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.radiusLevelTime

10. theorem OAI.SLEExactGauge.canonicalRadiusLevel_same_law_witness line 75

    Source documentation

    The same fixed kernel applies to any random driver with the canonical driver law, including the actual post-stopping driver.

    theorem canonicalRadiusLevel_same_law_witness
        {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω}
        (ν : Measure C(ℝ≥0, ℝ)) (κ : ℝ)
        (Φ : C(ℝ≥0, ℝ) → C(ℝ≥0, ℂ))
        (Gc Fc : C(ℝ≥0, ℝ) → ℝ≥0 → ℂ → ℂ)
        (hw : ∀ᵐ p ∂ν, IsCapacityTwoWitness
          (fun t => Real.sqrt κ * p t) (Φ p) (Gc p) (Fc p))
        (Y : Ω → C(ℝ≥0, ℝ)) (hY : Measurable Y) (hlaw : P.map Y = ν) :
        ∀ᵐ ω ∂P, ∀ u, 0 ≤ u → ∀ z,
          canonicalRadiusLevel κ (u, z, Y ω) =
            radiusLevelTime (Φ (Y ω)) (Gc (Y ω)) z u := by
    …

    Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.canonicalRadiusLevel, OAI.SLEExactGauge.radiusLevelTime

11. def OAI.SLEExactGauge.canonicalGreen line 90
12. lemma OAI.SLEExactGauge.canonicalGreen_measurable line 93
13. lemma OAI.SLEExactGauge.canonicalGreen_eq line 97
14. def OAI.SLEExactGauge.canonicalStoppedGreen line 106
15. lemma OAI.SLEExactGauge.canonicalStoppedGreen_measurable line 111
16. lemma OAI.SLEExactGauge.canonicalStoppedGreen_eq line 117
17. def OAI.SLEExactGauge.canonicalFiniteDensity line 130
18. lemma OAI.SLEExactGauge.canonicalFiniteDensity_measurable line 133
19. lemma OAI.SLEExactGauge.canonicalFiniteDensity_eq line 141
20. theorem OAI.SLEExactGauge.canonical_density_same_law_witness line 151

    Source documentation

    The tilted-density kernel is jointly measurable in level, marked point, and driver, and represents the actual density on one common full-measure set.

    theorem canonical_density_same_law_witness
        {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω}
        (ν : Measure C(ℝ≥0, ℝ)) (κ : ℝ)
        (Φ : C(ℝ≥0, ℝ) → C(ℝ≥0, ℂ))
        (Gc Fc : C(ℝ≥0, ℝ) → ℝ≥0 → ℂ → ℂ)
        (hw : ∀ᵐ p ∂ν, IsCapacityTwoWitness
          (fun t => Real.sqrt κ * p t) (Φ p) (Gc p) (Fc p))
        (Y : Ω → C(ℝ≥0, ℝ)) (hY : Measurable Y) (hlaw : P.map Y = ν) :
        ∀ᵐ ω ∂P, ∀ u, 0 ≤ u → ∀ z,
          canonicalStoppedGreen κ (u, z, Y ω) =
            stoppedGreen κ (fun t => Real.sqrt κ * Y ω t) (Φ (Y ω)) (Gc (Y ω)) z u ∧
          canonicalFiniteDensity κ (u, z, Y ω) = ENNReal.ofReal
    …

    Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.canonicalStoppedGreen, OAI.SLEExactGauge.stoppedGreen, OAI.SLEExactGauge.canonicalFiniteDensity

21. lemma OAI.SLEExactGauge.measurable_canonicalFiniteDensity_random_state line 170
22. theorem OAI.SLEExactGauge.canonical_finiteCenteredLaw_eq line 177