OAI/NumberTheory/DukePrimeDegree/Entropy/CountableFutureConditioning.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite approximation of a countable future observation

The countable geometric observations can be used for conditioning without assuming finite Shannon entropy. Their conditioning sigma algebra is the increasing limit of finite observations, and finite-label conditional entropy converges along this limit.

  1. def OAI.DukePrimeDegree.finiteCountableObservation line 22
  2. lemma OAI.DukePrimeDegree.finiteCountableObservation_measurable line 26
  3. lemma OAI.DukePrimeDegree.finiteCountableObservation_monotone line 31
  4. lemma OAI.DukePrimeDegree.finiteCountableObservation_generate line 38
  5. lemma OAI.DukePrimeDegree.finiteCountableFuture_generate line 45
  6. theorem OAI.DukePrimeDegree.conditionalSigmaEntropy_countableFuture_limit line 57

    Source documentation

    Only the observed finite label needs finite entropy. The extra future observation may take countably many values.

    theorem conditionalSigmaEntropy_countableFuture_limit {α : Type*} [Fintype α]
    (μ : Measure Y) [IsFiniteMeasure μ] (P : Y → α)
    {T : Y → Y} (hT : Measurable T) {Q : Y → ℕ} (hQ : Measurable Q)
    (m₀ : MeasurableSpace Y) (hm₀ : m₀ ≤ mY) :
    Tendsto (fun m => conditionalSigmaEntropy (mY := mY) μ P
…