OAI/Probability/SLE/Mass/ConditionalRadonRandomTests.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SLEExactGauge.locallyFiniteKernelVersion line 18
2. lemma OAI.SLEExactGauge.ae_finite_on_compacts_of_compact_mean line 49
3. theorem OAI.SLEExactGauge.conditional_halfPlane_random_test line 68

   Source documentation

   Equality of conditional mean measures gives arbitrary jointly past-measurable tests. Only compact mean masses need be finite.

   theorem conditional_halfPlane_random_test
       {Ω : Type*} [mΩ : MeasurableSpace Ω]
       (m : MeasurableSpace Ω) (hm : m ≤ mΩ) (P : @Measure Ω mΩ)
       (μ ν : Ω → Measure upperHalfPlane) (hμ : Measurable[mΩ] μ) (hν : Measurable[mΩ] ν)
       (hμfin : ∀ᵐ ω ∂P, IsFiniteMeasureOnCompacts (μ ω))
       (hνfin : ∀ᵐ ω ∂P, IsFiniteMeasureOnCompacts (ν ω))
       (hmean : ∀ K : Set upperHalfPlane, IsCompact K → P.bind μ K < ∞)
       (hevent : ∀ A : Set Ω, MeasurableSet[m] A →
         (P.restrict A).bind μ=(P.restrict A).bind ν)
       (f : Ω × upperHalfPlane → ℝ≥0∞) (hf : Measurable[m.prod inferInstance] f) :
       (∫⁻ ω, ∫⁻ z, f (ω,z) ∂μ ω ∂P) = ∫⁻ ω, ∫⁻ z, f (ω,z) ∂ν ω ∂P := by
   …

   Mentions: OAI.SLEExactGauge.upperHalfPlane