MetricEntropy.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The entropy functional in the published dynamical inputs

A finite measurable partition is represented by its finite-valued label map. Its length-N names encode the join of its first N inverse images under the transformation. The liminf definition agrees with the usual limit for invariant probabilities by subadditivity; proving that agreement and the published entropy theorems is still part of the outstanding work.

structure OAI.DukePrimeDegree.MeasurablePartition line 23
Source documentation
A finite measurable partition, allowing empty atoms.
```
structure MeasurablePartition (X : Type*) [MeasurableSpace X] (k : ℕ) where
…
```

def OAI.DukePrimeDegree.nameAtom line 28

Source documentation

The atoms of the joined partition through time N-1.

def nameAtom {X : Type*} [MeasurableSpace X] {k : ℕ}
    (P : MeasurablePartition X k) (T : X → X) (N : ℕ)
    (word : Fin N → Fin (k + 1)) : Set X :=
…

Mentions: OAI.DukePrimeDegree.MeasurablePartition

def OAI.DukePrimeDegree.blockEntropy line 34
Source documentation
Shannon entropy of the finite joined partition, with natural logs.
```
noncomputable def blockEntropy {X : Type*} [MeasurableSpace X] {k : ℕ}
    (P : MeasurablePartition X k) (T : X → X) (μ : Measure X) (N : ℕ) : ℝ :=
…
```
Mentions: OAI.DukePrimeDegree.MeasurablePartition
def OAI.DukePrimeDegree.partitionEntropyRate line 40
Source documentation
Entropy rate of one partition. The indexing N+1 avoids division by zero.
```
noncomputable def partitionEntropyRate {X : Type*} [MeasurableSpace X] {k : ℕ}
    (P : MeasurablePartition X k) (T : X → X) (μ : Measure X) : ℝ≥0∞ :=
…
```
Mentions: OAI.DukePrimeDegree.MeasurablePartition
def OAI.DukePrimeDegree.metricEntropy line 45
Source documentation
Kolmogorov--Sinai entropy, as the supremum over finite measurable partitions.
```
noncomputable def metricEntropy {X : Type*} [MeasurableSpace X]
    (T : X → X) (μ : Measure X) : ℝ≥0∞ :=
…
```