OAI/Probability/SLE/Geometry/RandomSpatialTesting.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SLEExactGauge.pairedMeasure line 18
2. lemma OAI.SLEExactGauge.pairedMeasure_measurable line 22
3. lemma OAI.SLEExactGauge.pairedMeasure_rectangle line 32
4. lemma OAI.SLEExactGauge.pairedMeasure_lintegral line 46
5. lemma OAI.SLEExactGauge.finite_spatial_test_measurable line 57
6. lemma OAI.SLEExactGauge.measurable_measure_restrict line 67
7. theorem OAI.SLEExactGauge.conditional_random_spatial_test_finite line 79

   Source documentation

   Finite mean kernels that agree after restriction to every past event agree on every nonnegative joint past/spatial test. Pointwise masses may be unbounded; only their total mean must be finite.

   theorem conditional_random_spatial_test_finite
       {Ω X : Type*} [mΩ : MeasurableSpace Ω] [MeasurableSpace X]
       (m : MeasurableSpace Ω) (hm : m ≤ mΩ) (P : @Measure Ω mΩ)
       (μ ν : Ω → Measure X)
       (hμ : @Measurable Ω (Measure X) mΩ inferInstance μ)
       (hν : @Measurable Ω (Measure X) mΩ inferInstance ν)
       (hμfin : ∀ ω, IsFiniteMeasure (μ ω)) (hνfin : ∀ ω, IsFiniteMeasure (ν ω))
       (hmean : P.bind μ univ < ∞)
       (hevent : ∀ A : Set Ω, MeasurableSet[m] A →
         (P.restrict A).bind μ = (P.restrict A).bind ν)
       (f : Ω × X → ℝ≥0∞) (hf : @Measurable (Ω × X) ℝ≥0∞ (m.prod inferInstance) _ f) :
       ∫⁻ ω, ∫⁻ x, f (ω,x) ∂μ ω ∂P = ∫⁻ ω, ∫⁻ x, f (ω,x) ∂ν ω ∂P := by
   …

8. theorem OAI.SLEExactGauge.conditional_random_spatial_test_on line 123

   Source documentation

   A local version for a fixed finite spatial set, suitable for compact restrictions of locally finite random Radon measures.

   theorem conditional_random_spatial_test_on
       {Ω X : Type*} [mΩ : MeasurableSpace Ω] [MeasurableSpace X]
       (m : MeasurableSpace Ω) (hm : m ≤ mΩ) (P : @Measure Ω mΩ)
       (μ ν : Ω → Measure X)
       (hμ : @Measurable Ω (Measure X) mΩ inferInstance μ)
       (hν : @Measurable Ω (Measure X) mΩ inferInstance ν)
       (K : Set X) (hK : MeasurableSet K)
       (hμK : ∀ ω, μ ω K < ∞) (hνK : ∀ ω, ν ω K < ∞)
       (hmean : P.bind μ K < ∞)
       (hevent : ∀ A : Set Ω, MeasurableSet[m] A →
         (P.restrict A).bind μ = (P.restrict A).bind ν)
       (f : Ω × X → ℝ≥0∞) (hf : @Measurable (Ω × X) ℝ≥0∞ (m.prod inferInstance) _ f) :
   …

9. theorem OAI.SLEExactGauge.conditional_random_spatial_test line 159

   Source documentation

   Countably many finite-mean spatial pieces suffice; neither random measure needs finite mass on the entire space.

   theorem conditional_random_spatial_test
       {Ω X : Type*} [mΩ : MeasurableSpace Ω] [MeasurableSpace X]
       (m : MeasurableSpace Ω) (hm : m ≤ mΩ) (P : @Measure Ω mΩ)
       (μ ν : Ω → Measure X)
       (hμ : @Measurable Ω (Measure X) mΩ inferInstance μ)
       (hν : @Measurable Ω (Measure X) mΩ inferInstance ν)
       (K : ℕ → Set X) (hKm : ∀ n, MeasurableSet (K n))
       (hdis : Pairwise (fun i j => Disjoint (K i) (K j))) (hcover : ⋃ n, K n = univ)
       (hμK : ∀ n ω, μ ω (K n) < ∞) (hνK : ∀ n ω, ν ω (K n) < ∞)
       (hmean : ∀ n, P.bind μ (K n) < ∞)
       (hevent : ∀ A : Set Ω, MeasurableSet[m] A →
         (P.restrict A).bind μ = (P.restrict A).bind ν)
   …