OAI/Analysis/FiniteFactor/ProductKernel.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.independentKernel line 15

   Source documentation

   Products of Markov kernels, with measurability proved on the generating finite cylinders and extended to the entire product sigma algebra.

   def independentKernel {ι : Type*} {X Y : ι → Type*}
       [∀ i, MeasurableSpace (X i)] [∀ i, MeasurableSpace (Y i)]
       (κ : ∀ i, Kernel (X i) (Y i)) [∀ i, IsMarkovKernel (κ i)] :
       Kernel (∀ i, X i) (∀ i, Y i) where
   …

2. instance OAI.FiniteFactor.independentKernel_markov line 29
3. theorem OAI.FiniteFactor.independentKernel_pi line 36
4. theorem OAI.FiniteFactor.lintegral_infinitePi_finset_prod line 44
5. theorem OAI.FiniteFactor.independentKernel_compProd line 57

   Source documentation

   Full-vector disintegration commutes with an arbitrary independent product. The equality is of measures on all measurable sets, not just rectangles.

   theorem independentKernel_compProd {ι : Type*} {X Y : ι → Type*}
       [∀ i, MeasurableSpace (X i)] [∀ i, MeasurableSpace (Y i)]
       (μ : ∀ i, Measure (X i)) [∀ i, IsProbabilityMeasure (μ i)]
       (κ : ∀ i, Kernel (X i) (Y i)) [∀ i, IsMarkovKernel (κ i)] :
       ((Measure.infinitePi μ) ⊗ₘ (independentKernel κ)).map
         (fun z i => (z.1 i, z.2 i)) = Measure.infinitePi (fun i => (μ i) ⊗ₘ (κ i)) := by
   …

   Mentions: OAI.FiniteFactor.independentKernel