OAI/Probability/SLE/Mass/LevelRadonExtraction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SLEExactGauge.Multipoint.convexLevelMeasure line 18
2. lemma OAI.SLEExactGauge.Multipoint.convexLevelMeasure_finite_on_compacts line 24
3. lemma OAI.SLEExactGauge.Multipoint.integral_convexLevelMeasure line 40
4. theorem OAI.SLEExactGauge.Multipoint.exists_common_halfPlane_test_limits_with_pairings line 63
5. theorem OAI.SLEExactGauge.Multipoint.exists_common_halfPlane_test_limits line 125
6. theorem OAI.SLEExactGauge.Multipoint.exists_common_level_radon_limits line 149

   Source documentation

   The same convex level measures have one Radon limit at all times in an arbitrary countable list. The spatial determining family is constructed, and is not an additional input.

   theorem exists_common_level_radon_limits
       {Ω : Type*} [MeasurableSpace Ω]
       {P : Measure Ω} {B : ℝ≥0 → Ω → ℝ} (hB : IsBrownianReal B P)
       (hm : ∀ t, Measurable (B t)) (hBm : Measurable (Function.uncurry B))
       (hBc : ∀ ω, Continuous (fun t => B t ω)) (hB0 : ∀ ω, B 0 ω = 0)
       {κ : ℝ} (hκ : 0 < κ) (hκ8 : κ < 8)
       (γ : Ω → ℝ≥0 → ℂ) (G F : Ω → ℝ≥0 → ℂ → ℂ)
       (hw : ∀ ω, IsCapacityTwoWitness (fun t => Real.sqrt κ * B t ω) (γ ω) (G ω) (F ω))
       (hgrowth : PublishedDiskUnivalentGrowth)
       (u : ℕ → ℝ) (hu : ∀ n, 0 ≤ u n) (t : ℕ → ℝ≥0∞) :
       ∃ s : ℕ → Finset ℕ, ∃ w : ℕ → ℕ → ℝ,
         (∀ n i, i ∈ s n → 0 ≤ w n i) ∧ (∀ n, ∑ i ∈ s n, w n i = 1) ∧
   …

   Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.PublishedDiskUnivalentGrowth