FutureFiberMeasurability.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Conditional measurability from constancy on conull future fibers

Disintegration supplies the almost-everywhere factorization; no Borel choice of a representative of every future fiber is needed.

theorem OAI.DukePrimeDegree.condExp_eq_of_conull_fiber_constant line 18

theorem OAI.DukePrimeDegree.fiberConstant_kernel_information line 49

Source documentation

Once the actual kernel is constant on the complete future fibers, the additional kernel label carries no conditional information.

theorem fiberConstant_kernel_information
    {Y S : Type*} [mY : MeasurableSpace Y] [StandardBorelSpace Y] [Nonempty Y]
    [MeasurableSpace S] [MeasurableEq S]
    (μ : Measure Y) [IsProbabilityMeasure μ]
    (F : Y → S) (hF : Measurable F)
    (κ : Kernel Y Y) [IsMarkovKernel κ]
    (hstat : μ.bind κ=μ)
    (hself : ∀ᵐ x ∂μ, ∀ᵐ y ∂κ x, κ y=κ x)
    (hsupport : ∀ᵐ x ∂μ, ∀ᵐ y ∂κ x, F y=F x)
    (E : Set Y) (hE : ∀ᵐ x ∂μ, x ∈ E)
    (hconst : ∀ x ∈ E, ∀ y ∈ E, F x=F y → κ x=κ y)
    (Q : Y → ℕ) (hQ : Measurable Q) :
…