PhaseEntropy.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SmoothObstruction.CylinderApproximation.cylinders line 17
Source documentation
Cylinders pulled back along the actual coordinate map.
```
def cylinders : Set (Set X) := Set.preimage π '' measurableCylinders A
…
```
lemma OAI.SmoothObstruction.CylinderApproximation.algebra line 20
lemma OAI.SmoothObstruction.CylinderApproximation.generates line 29

lemma OAI.SmoothObstruction.CylinderApproximation.approximate_set line 36

Source documentation

Genuine approximation of arbitrary measurable sets by finite-coordinate sets, in an arbitrary finite measure on a coordinate subspace.

lemma approximate_set (μ : Measure X) [IsFiniteMeasure μ]
    (hπ : ‹MeasurableSpace X› = MeasurableSpace.comap π MeasurableSpace.pi)
    {s : Set X} (hs : MeasurableSet s) {ε : ℝ} (hε : 0 < ε) :
    ∃ (I : Finset ι) (S : Set (∀ i : I, A i)), MeasurableSet S ∧
      μ.real ((π ⁻¹' cylinder I S) ∆ s) < ε := by
…

theorem OAI.SmoothObstruction.CylinderApproximation.approximate_partition line 58

Source documentation

Every finite measurable observation admits a finite-coordinate approximation in measure. The output labels and their measurable meaning are preserved; overlaps of the approximating atoms cause only the stated symmetric-difference error.

theorem approximate_partition [∀ i, Fintype (A i)] [∀ i, MeasurableSingletonClass (A i)]
    (μ : Measure X) [IsProbabilityMeasure μ]
    (hπ : ‹MeasurableSpace X› = MeasurableSpace.comap π MeasurableSpace.pi)
    {q : ℕ} {P : X → Fin (q+1)} (hP : Measurable P) {δ : ℝ} (hδ : 0 < δ) :
    ∃ (J : Finset ι) (f : (∀ i : J, A i) → Fin (q+1)),
      Measurable (fun x => f (J.restrict (π x))) ∧
      μ.real {x | P x ≠ f (J.restrict (π x))} ≤ δ := by
…

def OAI.SmoothObstruction.PhaseEntropy.Coordinate line 113
instance OAI.SmoothObstruction.PhaseEntropy.(instance at line 116) line 116
instance OAI.SmoothObstruction.PhaseEntropy.(instance at line 118) line 118
instance OAI.SmoothObstruction.PhaseEntropy.(instance at line 120) line 120
instance OAI.SmoothObstruction.PhaseEntropy.(instance at line 122) line 122
def OAI.SmoothObstruction.PhaseEntropy.coordinates line 131
lemma OAI.SmoothObstruction.PhaseEntropy.symbol_iterate line 137
lemma OAI.SmoothObstruction.PhaseEntropy.phase_iterate line 149

theorem OAI.SmoothObstruction.PhaseEntropy.cylinder_rate_bound line 157

Source documentation

Every genuine cylinder observation on symbols and phases has rate at most log(card A). Initial phase data have finite cost and add zero entropy rate.

theorem cylinder_rate_bound (μ : Measure X) [IsProbabilityMeasure μ]
    {T : X → X} (hT : MeasurePreserving T μ μ)
    (hcoord : Measurable (coordinates s p))
    (hs : ∀ x t, s (T x) t = s x (t+1)) (hp : ∀ x i, p (T x) i = p x i + 1)
    {q : ℕ} (J : Finset (ℤ ⊕ ℕ)) (f : (∀ i : J, Coordinate A m i) → Fin (q+1)) :
    ∃ h : ℝ, h ≤ Real.log (Fintype.card A) ∧
      Tendsto (fun n : ℕ => entropy μ (name T (fun x => f (J.restrict (coordinates s p x))) n) / n)
        atTop (𝓝 h) := by
…

Mentions: OAI.SmoothObstruction.PhaseEntropy.coordinates, OAI.SmoothObstruction.PhaseEntropy.Coordinate

theorem OAI.SmoothObstruction.PhaseEntropy.all_partition_rates line 237

Source documentation

All finite measurable partitions on the actual coordinate subspace have one finite entropy bound; the cylinder approximation is constructed in measure.

theorem all_partition_rates (μ : Measure X) [IsProbabilityMeasure μ]
    {T : X → X} (hT : MeasurePreserving T μ μ)
    (hspace : ‹MeasurableSpace X› = MeasurableSpace.comap (coordinates s p) MeasurableSpace.pi)
    (hs : ∀ x t, s (T x) t = s x (t+1)) (hp : ∀ x i, p (T x) i = p x i + 1)
    {q : ℕ} {P : X → Fin (q+1)} (hP : Measurable P) :
    ∃ h : ℝ, 0 ≤ h ∧ h ≤ Real.log (Fintype.card A) + Real.log 2 + 1 ∧
      Tendsto (fun n : ℕ => entropy μ (name T P n) / n) atTop (𝓝 h) := by
…

Mentions: OAI.SmoothObstruction.PhaseEntropy.coordinates

def OAI.SmoothObstruction.blockEntropy line 261
Source documentation
The entropy of the length-n join of the partition with labels in Fin q.
Also declared: ComparatorChallenges/SmoothObstruction.lean:15 (same declaration text).
```
noncomputable def blockEntropy {X : Type*} [MeasurableSpace X]
    (μ : Measure X) (T : X → X) {q : ℕ} (P : X → Fin q) (n : ℕ) : ℝ :=
…
```
def OAI.SmoothObstruction.FiniteKSEntropy line 269
Source documentation
All finite-partition entropy rates exist and have one finite real upper bound. This spells out sup_P lim_n H(join_{j<n} T^{-j}P)/n < ∞ without choosing a value for limits of nonconvergent sequences. Empty atoms are allowed.
Also declared: ComparatorChallenges/SmoothObstruction.lean:23 (same declaration text).
```
def FiniteKSEntropy {X : Type*} [MeasurableSpace X]
    (μ : Measure X) (T : X → X) : Prop :=
…
```
lemma OAI.SmoothObstruction.blockEntropy_eq_nats line 276

theorem OAI.SmoothObstruction.PhaseEntropy.finiteKS line 294

Source documentation

The exact frozen finite-KS predicate for any finite-symbol cyclic phase subspace with its genuine coordinate sigma field.

theorem PhaseEntropy.finiteKS {A : Type} [Fintype A] [Nonempty A]
    [MeasurableSpace A] [MeasurableSingletonClass A]
    {m : ℕ → ℕ} [∀ i, NeZero (m i)] {X : Type*} [MeasurableSpace X]
    (s : X → ℤ → A) (p : X → ∀ i, ZMod (m i))
    (μ : Measure X) [IsProbabilityMeasure μ] {T : X → X}
    (hT : MeasurePreserving T μ μ)
    (hspace : ‹MeasurableSpace X› = MeasurableSpace.comap (coordinates s p) MeasurableSpace.pi)
    (hs : ∀ x t, s (T x) t = s x (t+1)) (hp : ∀ x i, p (T x) i = p x i + 1) :
    FiniteKSEntropy μ T := by
…

Mentions: OAI.SmoothObstruction.PhaseEntropy.coordinates, OAI.SmoothObstruction.FiniteKSEntropy