OAI/NumberTheory/DukePrimeDegree/Entropy/ConditionalInformationClipping.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite present observations with a fixed conditioning sigma algebra

An integrable countable information function is the limit of the conditional entropies of finite clips. The conditioning is kept fixed; in the application it is the entire future together with the transverse coordinate, rather than the future of a clipped observation.

  1. lemma OAI.DukePrimeDegree.conditionalInformation_heightClip_eventually line 23
  2. lemma OAI.DukePrimeDegree.ae_conditionalInformation_heightClip_bounds line 32
  3. theorem OAI.DukePrimeDegree.conditionalSigmaEntropy_heightClip_tendsto line 68

    Source documentation

    Finite present-label clips recover the mean countable information, with no finite-Shannon-entropy assumption on the full countable label.

    theorem conditionalSigmaEntropy_heightClip_tendsto
    (m : MeasurableSpace Y) [mY : MeasurableSpace Y]
    (μ : Measure Y) [IsFiniteMeasure μ]
    (Q : Y → ℕ) (hQ : Measurable Q) (hm : m ≤ mY)
    (hpos : ∀ᵐ y ∂μ,
      0 < (μ[({z | Q z = Q y}.indicator (fun _ => (1 : ℝ))) | m]) y)
    (hint : Integrable (conditionalInformation μ Q m) μ) :
    Tendsto (fun N => conditionalSigmaEntropy μ (heightClip Q N) m) atTop
      (𝓝 (∫ y, conditionalInformation μ Q m y ∂μ)) := by
…

    Mentions: OAI.DukePrimeDegree.conditionalInformation, OAI.DukePrimeDegree.heightClip