OAI/NumberTheory/DukePrimeDegree/Entropy/CountableAuxiliaryEntropy.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Countable auxiliary observations with finite Shannon entropy

Increasing finite clippings recover the exact combined future sigma algebra. The entropy cost is bounded by the full countable Shannon sum.

  1. lemma OAI.DukePrimeDegree.observationSigma_encoded_pair line 17
  2. lemma OAI.DukePrimeDegree.auxiliaryFutureSigma_eq line 30
  3. lemma OAI.DukePrimeDegree.auxiliaryFutureSigma_monotone line 41
  4. lemma OAI.DukePrimeDegree.auxiliaryFutureSigma_generate line 50
  5. theorem OAI.DukePrimeDegree.predecessor_countable_auxiliary_entropyRate_le line 67

    Source documentation

    A finite-entropy auxiliary observation may be adjoined at a cost of its Shannon entropy, even when the main countable observation has infinite Shannon entropy.

    theorem predecessor_countable_auxiliary_entropyRate_le
    {Y : Type*} [MeasurableSpace Y] [StandardBorelSpace Y] [Nonempty Y]
    (μ : Measure Y) [IsProbabilityMeasure μ]
    {T : Y → Y} (hT : MeasurePreserving T μ μ)
    (Q : Y → ℕ) (hQ : Measurable Q)
    {M : ℕ} (B : Y → Fin (M+1)) (hB : Measurable B)
    (href : ∀ x y, Q x=Q y → Q (T x)=Q (T y) → B x=B y)
    (decode : ℕ → Fin (M+1) → ℕ) (hdecode : ∀ x, decode (Q (T x)) (B x)=Q x)
    (R : Y → ℕ) (hR : Measurable R)
    (hfinite : Summable (fun n => Real.negMulLog (μ.real {x | R x=n})))
    (K : ℕ) :
    observationEntropyRate μ T (heightClip Q K) ≤
…

    Mentions: OAI.DukePrimeDegree.heightClip