OAI/NumberTheory/DukePrimeDegree/Entropy/ConullFiberEntropyOrder.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Entropy order from refinement of conull fibers

A finer future observation need only determine a kernel outside a null set. Its conditional entropy is then at most the kernel-label entropy; no support of that kernel on the finer future fibers is required.

  1. lemma OAI.DukePrimeDegree.condExp_condExp_of_ae_measurable_sets line 18
  2. theorem OAI.DukePrimeDegree.conditionalSigmaEntropy_le_of_ae_measurable_sets line 38
  3. theorem OAI.DukePrimeDegree.conditionalSigmaEntropy_le_of_conull_fibers line 74

    Source documentation

    The finer observation can carry extra information: only determination of the coarser label on a conull set is used.

    theorem conditionalSigmaEntropy_le_of_conull_fibers
    {Y S T α : Type*} [mY : MeasurableSpace Y]
    [StandardBorelSpace Y] [Nonempty Y]
    [MeasurableSpace S] [MeasurableEq S] [MeasurableSpace T] [Fintype α]
    (μ : Measure Y) [IsProbabilityMeasure μ]
    (F : Y → S) (hF : Measurable F) (G : Y → T) (hG : Measurable G)
    (E : Set Y) (hE : ∀ᵐ x ∂μ, x ∈ E)
    (hconst : ∀ x ∈ E, ∀ y ∈ E, F x=F y → G x=G y)
    (P : Y → α) (hP : ∀ a, MeasurableSet {y | P y=a}) :
    conditionalSigmaEntropy (mY := mY) μ P (MeasurableSpace.comap F inferInstance) ≤
…