CountableObservationInformation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Finite clipping of a countable observation

At a sampled point, clipping above its observed value leaves its atom unchanged. Positive atom mass also gives a common information bound.

lemma OAI.DukePrimeDegree.heightClip_atom_eq_of_lt line 19
lemma OAI.DukePrimeDegree.observationInformation_heightClip_eventually line 26
lemma OAI.DukePrimeDegree.observationInformation_heightClip_le line 34

theorem OAI.DukePrimeDegree.integral_kernel_heightClip_information_tendsto line 47

Source documentation

Integrable countable information is recovered by its finite clips, without requiring finite Shannon entropy of the countable observation.

theorem integral_kernel_heightClip_information_tendsto
    {S V : Type*} [MeasurableSpace S] [MeasurableSpace V]
    (ρ : Measure (S × V)) [IsFiniteMeasure ρ]
    (κ : Kernel S V) [IsMarkovKernel κ]
    (Q : S × V → ℕ) (hQ : Measurable Q)
    (hpos : ∀ᵐ z ∂ρ, 0 < κ z.1 {v | Q (z.1,v) = Q z})
    (hint : Integrable
      (fun z => observationInformation (κ z.1) (fun v => Q (z.1,v)) z.2) ρ) :
    Tendsto (fun N => ∫ z,
      observationInformation (κ z.1) (fun v => heightClip Q N (z.1,v)) z.2 ∂ρ)
      atTop (𝓝 (∫ z, observationInformation (κ z.1) (fun v => Q (z.1,v)) z.2 ∂ρ)) := by
…

Mentions: OAI.DukePrimeDegree.observationInformation, OAI.DukePrimeDegree.heightClip