OAI/NumberTheory/DukePrimeDegree/Entropy/AuxiliaryPredecessorEntropy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DukePrimeDegree.predecessor_factor_entropyRate_le line 16
2. lemma OAI.DukePrimeDegree.conditionalSigmaEntropy_wholeFuture_le_observationEntropy line 46
3. theorem OAI.DukePrimeDegree.predecessor_auxiliary_entropyRate_le line 65

   Source documentation

   The finite auxiliary label contributes only its one-step Shannon entropy; the main term is conditioned on the combined entire future.

   theorem predecessor_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)
       {L : ℕ} (R : Y → Fin (L+1)) (hR : Measurable R) (K : ℕ) :
       observationEntropyRate μ T (heightClip Q K) ≤
         conditionalSigmaEntropy μ B
           (MeasurableSpace.comap
   …

   Mentions: OAI.DukePrimeDegree.heightClip