EntropyInverse.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Time reversal of entropy

Reversing a finite orbit name and shifting its starting point does not change its Shannon entropy. This proves equality of Kolmogorov--Sinai entropy for mutually inverse measure-preserving maps, as used in EKL (2006), equation (3.2).

def OAI.DukePrimeDegree.reverseWordEquiv line 22
Source documentation
Reversal is a permutation of the finite word alphabet.
```
def reverseWordEquiv (α : Type*) (N : ℕ) : (Fin N → α) ≃ (Fin N → α) where
…
```
lemma OAI.DukePrimeDegree.inverse_orbitName line 28

theorem OAI.DukePrimeDegree.orbitEntropy_inverse line 42

Source documentation

Finite block entropies agree exactly under time reversal.

theorem orbitEntropy_inverse {Y α : Type*} [MeasurableSpace Y] [Fintype α]
    (μ : Measure Y) (T S : Y → Y)
    (hT : MeasurePreserving T μ μ) (hS : Measurable S)
    (hST : Function.LeftInverse S T)
    (P : Y → α) (hP : ∀ a, MeasurableSet {y | P y = a}) (N : ℕ) :
    observationEntropy μ (orbitName S P N) =
      observationEntropy μ (orbitName T P N) := by
…

theorem OAI.DukePrimeDegree.observationEntropyRate_inverse line 61

Source documentation

Equality holds for every finite observation, before taking the supremum.

theorem observationEntropyRate_inverse {Y α : Type*}
    [MeasurableSpace Y] [Fintype α]
    (μ : Measure Y) (T S : Y → Y)
    (hT : MeasurePreserving T μ μ) (hS : Measurable S)
    (hST : Function.LeftInverse S T)
    (P : Y → α) (hP : ∀ a, MeasurableSet {y | P y = a}) :
    observationEntropyRate μ S P = observationEntropyRate μ T P := by
…

theorem OAI.DukePrimeDegree.measureEntropy_inverse line 74

Source documentation

Entropy is invariant under reversing an invertible measure-preserving map.

theorem measureEntropy_inverse {Y : Type*} [MeasurableSpace Y]
    (μ : Measure Y) (T S : Y → Y)
    (hT : MeasurePreserving T μ μ) (hS : Measurable S)
    (hST : Function.LeftInverse S T) :
    measureEntropy μ S = measureEntropy μ T := by
…