SelfConditionalKernel.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Conditional distributions from a stationary fiber kernel

A stationary kernel which is constant almost everywhere on each of its own probability fibers is the conditional distribution for the sigma algebra generated by that kernel. This is the precise extra condition needed beyond stationarity in the whole-future application.

theorem OAI.DukePrimeDegree.setIntegral_selfConstant_kernel line 24

theorem OAI.DukePrimeDegree.selfConstant_kernel_ae_eq_condExp line 63

Source documentation

The kernel evaluations are actual conditional probabilities.

theorem selfConstant_kernel_ae_eq_condExp
    (μ : Measure Y) [IsFiniteMeasure μ]
    (κ : Kernel Y Y) [IsMarkovKernel κ]
    (hstat : μ.bind κ = μ)
    (hself : ∀ᵐ x ∂μ, ∀ᵐ y ∂κ x, κ y = κ x)
    {A : Set Y} (hA : MeasurableSet A) :
    (fun x => (κ x).real A) =ᵐ[μ]
      μ[A.indicator (fun _ => (1 : ℝ)) | MeasurableSpace.comap κ inferInstance] := by
…

theorem OAI.DukePrimeDegree.selfConstant_kernel_conditionalEntropy line 85

theorem OAI.DukePrimeDegree.condDistrib_self_constant line 102

Source documentation

An actual regular conditional distribution has the required constancy on its fibers. This supplies the local case in quotient charts.

theorem condDistrib_self_constant {S : Type*} [MeasurableSpace S] [MeasurableEq S]
    [StandardBorelSpace Y] [Nonempty Y]
    (μ : Measure Y) [IsProbabilityMeasure μ]
    (F : Y → S) (hF : Measurable F) :
    ∀ᵐ x ∂μ, ∀ᵐ y ∂condDistrib id F μ (F x),
      condDistrib id F μ (F y) = condDistrib id F μ (F x) := by
…

theorem OAI.DukePrimeDegree.selfConstant_kernel_pushforward line 116

Source documentation

Self-consistency passes through a genuine measurable coordinate chart when the ambient kernel is its pushforward.

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