OAI/Probability/SLE/Mass/LevelApproximationAdapted.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SLEExactGauge.radiusLevelTime_le_iff_prefix line 17
2. lemma OAI.SLEExactGauge.capped_radiusLevelTime_dense line 41
3. lemma OAI.SLEExactGauge.prefix_time_measurable line 79
4. lemma OAI.SLEExactGauge.prefix_level_time_measurable line 106
5. theorem OAI.SLEExactGauge.actual_radius_prefix_measurable line 147
6. lemma OAI.SLEExactGauge.Multipoint.measurable_capped_green line 179
7. lemma OAI.SLEExactGauge.Multipoint.levelApproximationDensity_eq_cappedGreen line 195
8. theorem OAI.SLEExactGauge.Multipoint.levelApproximationDensity_past_measurable line 209
9. lemma OAI.SLEExactGauge.Multipoint.levelApproximationRealTest_past_measurable line 231
10. lemma OAI.SLEExactGauge.Multipoint.convexLevelMeasure_test_past_measurable line 253
11. theorem OAI.SLEExactGauge.Multipoint.level_radon_limit_has_past_measurable_version line 276

    Source documentation

    Every actual vague limit at a fixed time has a version measurable in that time's uncompleted natural filtration. The convex sequence is unchanged.

    theorem level_radon_limit_has_past_measurable_version
        {Ω : Type*} [mΩ : MeasurableSpace Ω] (P : Measure Ω)
        {B : ℝ≥0 → Ω → ℝ}
        (hm : ∀ t, Measurable (B t)) (hc : ∀ ω, Continuous (fun t => B t ω))
        {κ : ℝ} (hκ : 0 < κ) (hκ8 : κ < 8)
        (γ : Ω → ℝ≥0 → ℂ) (G F : Ω → ℝ≥0 → ℂ → ℂ)
        (hw : ∀ ω, IsCapacityTwoWitness (fun t => Real.sqrt κ * B t ω)
          (γ ω) (G ω) (F ω))
        (u : ℕ → ℝ) (hu : ∀ n, 0 ≤ u n) (s : ℕ → Finset ℕ) (w : ℕ → ℕ → ℝ)
        (hw₀ : ∀ n i, i ∈ s n → 0 ≤ w n i) (T : ℝ≥0)
        (ν : Ω → Measure upperHalfPlane)
        (hν : ∀ᵐ ω ∂P, (ν ω).Regular)
    …

    Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.upperHalfPlane