OAI/NumberTheory/PrimePackets/ConditionalOrbitEntropy.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Entropy-rate comparison from one-step conditional entropy

The finite-block estimate here is the approximation step needed when replacing finite observations by successively finer geometric partitions.

  1. lemma OAI.PrimeDegreePackets.observationEntropy_unique line 20
  2. lemma OAI.PrimeDegreePackets.orbitName_one line 28
  3. lemma OAI.PrimeDegreePackets.conditionalOrbitEntropy_one line 35
  4. theorem OAI.PrimeDegreePackets.conditionalOrbitEntropy_le line 44
  5. theorem OAI.PrimeDegreePackets.observationEntropyRate_le_add_conditional line 86

    Source documentation

    A finite observation approximates entropy rates up to its one-step conditional entropy. This is the standard finite-partition approximation bound.

    theorem observationEntropyRate_le_add_conditional [Fintype α] [Fintype β]
    (μ : Measure Y) [IsProbabilityMeasure μ] {T : Y → Y}
    (hT : MeasurePreserving T μ μ) (P : Y → α) (Q : Y → β)
    (hP : ∀ a, MeasurableSet {y | P y = a})
    (hQ : ∀ b, MeasurableSet {y | Q y = b}) :
    observationEntropyRate μ T P ≤
      observationEntropyRate μ T Q + conditionalObservationEntropy μ P Q := by
…

    Mentions: OAI.PrimeDegreePackets.observationEntropyRate, OAI.PrimeDegreePackets.conditionalObservationEntropy