OAI/Dynamics/SmoothObstruction/PartitionEntropy.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SmoothObstruction.PartitionEntropy.mass line 17
2. def OAI.SmoothObstruction.PartitionEntropy.entropy line 18
3. lemma OAI.SmoothObstruction.PartitionEntropy.mass_nonneg line 21
4. lemma OAI.SmoothObstruction.PartitionEntropy.sum_mass line 23
5. lemma OAI.SmoothObstruction.PartitionEntropy.push_mass line 29
6. lemma OAI.SmoothObstruction.PartitionEntropy.entropy_comp_le line 42
7. lemma OAI.SmoothObstruction.PartitionEntropy.entropy_nonnegative line 48
8. lemma OAI.SmoothObstruction.PartitionEntropy.entropy_card_bound line 51
9. lemma OAI.SmoothObstruction.PartitionEntropy.leftMass_pair line 55
10. lemma OAI.SmoothObstruction.PartitionEntropy.rightMass_pair line 66
11. lemma OAI.SmoothObstruction.PartitionEntropy.entropy_pair_le line 75
12. lemma OAI.SmoothObstruction.PartitionEntropy.entropy_preserving line 83
13. def OAI.SmoothObstruction.PartitionEntropy.name line 91

    Source documentation

    The actual forward partition name, not an independent copy.

    def name (T : X → X) (P : X → α) (n : ℕ) (x : X) : Fin n → α :=
    …

14. lemma OAI.SmoothObstruction.PartitionEntropy.measurable_name line 95
15. lemma OAI.SmoothObstruction.PartitionEntropy.name_add line 100
16. theorem OAI.SmoothObstruction.PartitionEntropy.block_subadditive line 110

    Source documentation

    Exact subadditivity for finite partition names of a stationary system.

    theorem block_subadditive {T : X → X} (hT : MeasurePreserving T μ μ)
        {P : X → α} (hP : Measurable P) :
        Subadditive (fun n => entropy μ (name T P n)) := by
    …

    Mentions: OAI.SmoothObstruction.PartitionEntropy.entropy, OAI.SmoothObstruction.PartitionEntropy.name

17. theorem OAI.SmoothObstruction.PartitionEntropy.exists_block_rate line 127

    Source documentation

    Every individual finite partition has an entropy rate, by Fekete's lemma. The main theorem still needs a uniform bound over arbitrary partitions.

    theorem exists_block_rate {T : X → X} (hT : MeasurePreserving T μ μ)
        {P : X → α} (hP : Measurable P) :
        ∃ h : ℝ, 0 ≤ h ∧ h ≤ Real.log (Fintype.card α) ∧
          Tendsto (fun n : ℕ => entropy μ (name T P n) / n) atTop (𝓝 h) := by
    …

    Mentions: OAI.SmoothObstruction.PartitionEntropy.entropy, OAI.SmoothObstruction.PartitionEntropy.name

18. def OAI.SmoothObstruction.PartitionEntropy.errorCode line 156
19. def OAI.SmoothObstruction.PartitionEntropy.recover line 160
20. lemma OAI.SmoothObstruction.PartitionEntropy.recover_error line 165
21. lemma OAI.SmoothObstruction.PartitionEntropy.measurable_error line 172
22. lemma OAI.SmoothObstruction.PartitionEntropy.error_mass line 179
23. lemma OAI.SmoothObstruction.PartitionEntropy.error_entropy_bound line 194
24. lemma OAI.SmoothObstruction.PartitionEntropy.entropy_recover_le line 202
25. lemma OAI.SmoothObstruction.PartitionEntropy.names_error_le line 212

    Source documentation

    Compare genuine orbit names through pointwise error coding.

    lemma names_error_le {T : X → X} (hT : Measurable T) {P Q : X → α}
        (hP : Measurable P) (hQ : Measurable Q) (n : ℕ) :
        entropy μ (name T P n) ≤ entropy μ (name T Q n) +
          entropy μ (name T (errorCode P Q) n) := by
    …

    Mentions: OAI.SmoothObstruction.PartitionEntropy.entropy, OAI.SmoothObstruction.PartitionEntropy.name, OAI.SmoothObstruction.PartitionEntropy.errorCode

26. lemma OAI.SmoothObstruction.PartitionEntropy.entropy_name_one line 236
27. lemma OAI.SmoothObstruction.PartitionEntropy.block_rate_le_entropy line 249

    Source documentation

    If the genuine name entropy has a limit, its rate is at most the entropy of the one-time partition. No independence is assumed.

    lemma block_rate_le_entropy {T : X → X} (hT : MeasurePreserving T μ μ)
        {P : X → α} (hP : Measurable P) {h : ℝ}
        (hh : Tendsto (fun n : ℕ => entropy μ (name T P n) / n) atTop (𝓝 h)) :
        h ≤ entropy μ P := by
    …

    Mentions: OAI.SmoothObstruction.PartitionEntropy.entropy, OAI.SmoothObstruction.PartitionEntropy.name

28. lemma OAI.SmoothObstruction.PartitionEntropy.rate_approximation line 266

    Source documentation

    Quantitative approximation of rates by a finite observation. This is a real stationary-process entropy argument, not an assertion of a generator.

    lemma rate_approximation {T : X → X} (hT : MeasurePreserving T μ μ)
        {P Q : X → α} (hP : Measurable P) (hQ : Measurable Q) {h k : ℝ}
        (hh : Tendsto (fun n : ℕ => entropy μ (name T P n) / n) atTop (𝓝 h))
        (hk : Tendsto (fun n : ℕ => entropy μ (name T Q n) / n) atTop (𝓝 k)) :
        h ≤ k + Real.log 2 + μ.real {x | P x ≠ Q x} * Real.log (Fintype.card α) := by
    …

    Mentions: OAI.SmoothObstruction.PartitionEntropy.entropy, OAI.SmoothObstruction.PartitionEntropy.name

29. theorem OAI.SmoothObstruction.PartitionEntropy.finite_rate_of_approximants line 285

    Source documentation

    Sufficient approximation criterion for a uniform finite KS bound. The criterion requires actual measurable approximants with small error and uniform rate bound; it does not postulate the KS conclusion.

    theorem finite_rate_of_approximants {T : X → X} (hT : MeasurePreserving T μ μ)
        {C : ℝ} {P : X → α} (hP : Measurable P)
        (happrox : ∀ δ : ℝ, 0 < δ → ∃ Q : X → α, Measurable Q ∧
          μ.real {x | P x ≠ Q x} ≤ δ ∧ ∃ k : ℝ, k ≤ C ∧
            Tendsto (fun n : ℕ => entropy μ (name T Q n) / n) atTop (𝓝 k)) :
        ∃ h : ℝ, 0 ≤ h ∧ h ≤ C + Real.log 2 + 1 ∧
          Tendsto (fun n : ℕ => entropy μ (name T P n) / n) atTop (𝓝 h) := by
    …

    Mentions: OAI.SmoothObstruction.PartitionEntropy.entropy, OAI.SmoothObstruction.PartitionEntropy.name