CountableShannonInformation.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Integrable information for the countable return observations

The summable atom estimates for return refinements give the actual integrable information function, and bound every finite recoding.

lemma OAI.DukePrimeDegree.integrableOn_observationInformation_fiber line 16
lemma OAI.DukePrimeDegree.setIntegral_observationInformation_fiber line 25

theorem OAI.DukePrimeDegree.countable_observationInformation_integrable line 40

Source documentation

Summable Shannon terms are sufficient for integrability of the countable partition's pointwise information.

theorem countable_observationInformation_integrable
    {Y α : Type*} [MeasurableSpace Y] [Countable α]
    (μ : Measure Y) [IsProbabilityMeasure μ] (P : Y → α)
    (hP : ∀ a, MeasurableSet {y | P y=a})
    (hs : Summable (fun a => Real.negMulLog (μ.real {y | P y=a}))) :
    Integrable (observationInformation μ P) μ := by
…

Mentions: OAI.DukePrimeDegree.observationInformation

theorem OAI.DukePrimeDegree.integral_countable_observationInformation line 57
lemma OAI.DukePrimeDegree.ae_observation_fiber_pos line 75

theorem OAI.DukePrimeDegree.finite_recode_entropy_le_countable_information line 88

Source documentation

Every finite recoding is bounded by the same countable Shannon sum.

theorem finite_recode_entropy_le_countable_information
    {Y α β : Type*} [MeasurableSpace Y] [Countable α] [Fintype β]
    (μ : Measure Y) [IsProbabilityMeasure μ] (P : Y → α)
    (hP : ∀ a, MeasurableSet {y | P y=a})
    (hs : Summable (fun a => Real.negMulLog (μ.real {y | P y=a})))
    (f : α → β) (hf : ∀ b, MeasurableSet {y | f (P y)=b}) :
    observationEntropy μ (f ∘ P) ≤ ∑' a, Real.negMulLog (μ.real {y | P y=a}) := by
…