OAI/NumberTheory/DukePrimeDegree/Entropy/SelfConditionalKernelMap.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DukePrimeDegree.measurableSet_kernel_selfConstant line 13
2. theorem OAI.DukePrimeDegree.selfConstant_kernel_map line 29

   Source documentation

   No global injectivity of the coordinate map is required. The actual ambient kernel must agree almost everywhere with the pushed local kernel.

   theorem selfConstant_kernel_map
       {Z Y : Type*} [MeasurableSpace Z] [MeasurableSpace Y] [StandardBorelSpace Y]
       (ρ : Measure Z) (η : Kernel Z Z) [IsMarkovKernel η]
       (hstat : ρ.bind η=ρ)
       (hself : ∀ᵐ z ∂ρ, ∀ᵐ w ∂η z, η w=η z)
       (F : Z → Y) (hF : Measurable F)
       (κ : Kernel Y Y) [IsMarkovKernel κ]
       (hversion : ∀ᵐ z ∂ρ, κ (F z)=(η z).map F) :
       ∀ᵐ x ∂ρ.map F, ∀ᵐ y ∂κ x, κ y=κ x := by
   …