OAI/Analysis/FiniteFactor/FiniteProductAbsoluteContinuity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.infinitePi_update_law line 13

   Source documentation

   Replacing one independent coordinate is a measurable pushforward of a single fresh draw and the original full product.

   theorem infinitePi_update_law {ι X : Type*} [DecidableEq ι] [MeasurableSpace X]
       (μ : ι → Measure X) [∀ i, IsProbabilityMeasure (μ i)]
       (i : ι) (ν : Measure X) [IsProbabilityMeasure ν] :
       (ν.prod (Measure.infinitePi μ)).map (fun z : X × (ι → X) => Function.update z.2 i z.1) =
         Measure.infinitePi (Function.update μ i ν) := by
   …

2. theorem OAI.FiniteFactor.infinitePi_ac_of_finite_changes line 66

   Source documentation

   Absolute continuity survives finitely many coordinate changes. No assertion about arbitrary infinite families of absolutely continuous marginals is used.

   theorem infinitePi_ac_of_finite_changes {ι X : Type*} [DecidableEq ι] [MeasurableSpace X]
       (μ ν : ι → Measure X) [∀ i, IsProbabilityMeasure (μ i)]
       [∀ i, IsProbabilityMeasure (ν i)] (F : Finset ι)
       (hac : ∀ i ∈ F, ν i ≪ μ i) (heq : ∀ i ∉ F, ν i = μ i) :
       Measure.infinitePi ν ≪ Measure.infinitePi μ := by
   …