OAI/Probability/SLE/Geometry/RandomKernelSupport.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SLEExactGauge.restricted_random_set_measurable line 15
2. lemma OAI.SLEExactGauge.setLIntegral_random_indicator line 31
3. theorem OAI.SLEExactGauge.ae_avoids_random_set_of_conditional_kernel line 46

   Source documentation

   If the conditional mean measures agree on every past event, then the first measure gives no mass to any jointly past-measurable random set which the second measure avoids.

   theorem ae_avoids_random_set_of_conditional_kernel
       {Ω 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))
       (hcover : ∀ x, ∃ n, x ∈ K n)
       (hμK : ∀ n ω, μ ω (K n) < ∞)
       (hνK : ∀ n, ∀ᵐ ω ∂P, ν ω (K n) < ∞)
       (hmean : ∀ n, P.bind μ (K n) < ∞)
       (hevent : ∀ E : Set Ω, MeasurableSet[m] E →
   …