OAI/NumberTheory/PrimePackets/FiniteGeneratingObservations.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Actual finite generating observations on countably generated spaces

The observations record finitely many bits of Mathlib's canonical countable generating family. Thus the entropy approximation hypotheses are supplied by the measurable space itself, rather than assumed for an arbitrary sequence.

  1. lemma OAI.PrimeDegreePackets.observationSigma_comp_le line 19
  2. lemma OAI.PrimeDegreePackets.observationSigma_comp_injective line 24
  3. def OAI.PrimeDegreePackets.finiteGeneratingBits line 36
  4. lemma OAI.PrimeDegreePackets.finiteGeneratingBits_measurable line 39
  5. lemma OAI.PrimeDegreePackets.finiteGeneratingBits_monotone line 42
  6. lemma OAI.PrimeDegreePackets.finiteGeneratingBits_generate line 50
  7. def OAI.PrimeDegreePackets.finiteGeneratingObservation line 65
  8. lemma OAI.PrimeDegreePackets.finiteGeneratingObservation_sigma line 69
  9. lemma OAI.PrimeDegreePackets.finiteGeneratingObservation_measurable line 74
  10. lemma OAI.PrimeDegreePackets.finiteGeneratingObservation_monotone line 79
  11. lemma OAI.PrimeDegreePackets.finiteGeneratingObservation_generate line 83
  12. theorem OAI.PrimeDegreePackets.measureEntropy_eq_iSup_finiteGenerating line 89

    Source documentation

    On any countably generated measurable space, an explicit sequence of finite observations computes the full metric entropy.

    theorem measureEntropy_eq_iSup_finiteGenerating
    (μ : Measure Y) [IsProbabilityMeasure μ] {T : Y → Y}
    (hT : MeasurePreserving T μ μ) :
    measureEntropy μ T = ⨆ n, ENNReal.ofReal
      (observationEntropyRate μ T (finiteGeneratingObservation Y n)) :=
…

    Mentions: OAI.PrimeDegreePackets.measureEntropy, OAI.PrimeDegreePackets.observationEntropyRate, OAI.PrimeDegreePackets.finiteGeneratingObservation