OAI/Probability/SLE/Mass/RandomRadonLimit.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SLEExactGauge.exists_measurable_random_radon_limit line 20

   Source documentation

   An almost-sure regular vague limit of random positive measures has a measurable regular version. The approximants need only have measurable compact-test integrals.

   theorem exists_measurable_random_radon_limit
       {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) (μ : ℕ → Ω → Measure X)
       (hmeas : ∀ n (f : C_c(X,ℝ)), Measurable (fun ω => ∫ x, f x ∂μ n ω))
       (hex : ∀ᵐ ω ∂P, ∃ ν : Measure X, ν.Regular ∧
         ∀ f : C_c(X,ℝ), Tendsto (fun n => ∫ x, f x ∂μ n ω) atTop (𝓝 (∫ x, f x ∂ν))) :
       ∃ ν : Ω → Measure X, Measurable ν ∧
         (∀ ω, (ν ω).Regular ∧ IsFiniteMeasureOnCompacts (ν ω)) ∧
         ∀ᵐ ω ∂P, ∀ f : C_c(X,ℝ),
           Tendsto (fun n => ∫ x, f x ∂μ n ω) atTop (𝓝 (∫ x, f x ∂ν ω)) := by
   …

2. theorem OAI.SLEExactGauge.exists_measurable_countable_radon_limits line 63

   Source documentation

   Countably many times retain one common event of convergence, and each selected time slice is a measurable locally finite regular random measure.

   theorem exists_measurable_countable_radon_limits
       {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) (μ : ℕ → ℕ → Ω → Measure X)
       (hmeas : ∀ n j (f : C_c(X,ℝ)), Measurable (fun ω => ∫ x, f x ∂μ n j ω))
       (hex : ∀ᵐ ω ∂P, ∃ ν : ℕ → Measure X, (∀ j, (ν j).Regular) ∧
         ∀ j (f : C_c(X,ℝ)), Tendsto (fun n => ∫ x, f x ∂μ n j ω) atTop (𝓝 (∫ x, f x ∂ν j))) :
       ∃ ν : ℕ → Ω → Measure X, (∀ j, Measurable (ν j)) ∧
         (∀ j ω, (ν j ω).Regular ∧ IsFiniteMeasureOnCompacts (ν j ω)) ∧
         ∀ᵐ ω ∂P, ∀ j (f : C_c(X,ℝ)),
           Tendsto (fun n => ∫ x, f x ∂μ n j ω) atTop (𝓝 (∫ x, f x ∂ν j ω)) := by
   …

3. theorem OAI.SLEExactGauge.radon_test_limit_unique line 83

   Source documentation

   Regular vague limits of the same sequence are unique.

   theorem radon_test_limit_unique (μ : ℕ → Measure X) (ν η : Measure X)
       [ν.Regular] [η.Regular]
       (hν : ∀ f : C_c(X,ℝ), Tendsto (fun n => ∫ x, f x ∂μ n) atTop (𝓝 (∫ x, f x ∂ν)))
       (hη : ∀ f : C_c(X,ℝ), Tendsto (fun n => ∫ x, f x ∂μ n) atTop (𝓝 (∫ x, f x ∂η))) :
       ν=η :=
   …

4. theorem OAI.SLEExactGauge.aemeasurable_radon_of_test_limits_ae line 93

   Source documentation

   Any pathwise version of the same limit is almost everywhere measurable, useful when the approximants are measurable in a smaller stopped or deterministic-time sigma algebra.

   theorem aemeasurable_radon_of_test_limits_ae
       {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) (μ : ℕ → Ω → Measure X)
       (ν : Ω → Measure X)
       (hmeas : ∀ n (f : C_c(X,ℝ)), Measurable (fun ω => ∫ x, f x ∂μ n ω))
       (hν : ∀ᵐ ω ∂P, (ν ω).Regular)
       (hlim : ∀ᵐ ω ∂P, ∀ f : C_c(X,ℝ),
         Tendsto (fun n => ∫ x, f x ∂μ n ω) atTop (𝓝 (∫ x, f x ∂ν ω))) :
       AEMeasurable ν P := by
   …