HeightObservationEntropy.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Entropy controlled by the increments of a height

A finite label reconstructed from its next value and a finite increment code has entropy rate bounded by the entropy of that code. In particular, all finite truncations of a height changing by at most one have entropy rate at most log 3, regardless of the height's integrability.

lemma OAI.DukePrimeDegree.observationEntropy_recode_le line 26
lemma OAI.DukePrimeDegree.observationEntropyRate_le_oneStep line 41

theorem OAI.DukePrimeDegree.observationEntropyRate_le_incrementEntropy line 59

Source documentation

A one-step reconstruction code bounds the entropy rate.

theorem observationEntropyRate_le_incrementEntropy
    (μ : Measure Y) [IsProbabilityMeasure μ]
    {T : Y → Y} (hT : MeasurePreserving T μ μ)
    (P : Y → α) (hP : Measurable P) (D : Y → β) (hD : Measurable D)
    (decode : α → β → α) (hdecode : ∀ y, decode (P (T y)) (D y)=P y) :
    observationEntropyRate μ T P ≤ observationEntropy μ D := by
…

def OAI.DukePrimeDegree.heightClip line 86
lemma OAI.DukePrimeDegree.heightClip_measurable line 89

theorem OAI.DukePrimeDegree.heightClip_increment_model line 96

Source documentation

A finite clipped height is reconstructed from its next value and a three-valued increment; the middle code means that the label did not change.

theorem heightClip_increment_model {T : Y → Y} (hT : Measurable T)
    (H : Y → ℕ) (hH : Measurable H)
    (hstep : ∀ y, H (T y) ≤ H y+1 ∧ H y ≤ H (T y)+1) (N : ℕ) :
    ∃ (D : Y → Fin 3) (decode : Fin (N+1) → Fin 3 → Fin (N+1)),
      Measurable D ∧
      (∀ y, decode (heightClip H N (T y)) (D y)=heightClip H N y) ∧
      (∀ y, D y=1 ↔ heightClip H N (T y)=heightClip H N y) := by
…

Mentions: OAI.DukePrimeDegree.heightClip

theorem OAI.DukePrimeDegree.heightClip_entropyRate_le_log_three line 151