OAI/NumberTheory/DukePrimeDegree/Entropy/BilateralFiniteCodes.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DukePrimeDegree.bilateralFiniteCode line 16
2. theorem OAI.DukePrimeDegree.bilateralFiniteCode_measurable line 25
3. def OAI.DukePrimeDegree.truncateBilateralCode line 37
4. theorem OAI.DukePrimeDegree.truncate_bilateralFiniteCode line 45
5. theorem OAI.DukePrimeDegree.bilateralFiniteCode_sigma_monotone line 53
6. theorem OAI.DukePrimeDegree.bilateralFiniteCode_sigma_generate line 66
7. theorem OAI.DukePrimeDegree.conditional_bilateralFiniteCode_tendsto line 127
8. theorem OAI.DukePrimeDegree.diagonal_positive_iterate line 141
9. theorem OAI.DukePrimeDegree.shifted_window_symbol line 147
10. theorem OAI.DukePrimeDegree.bilateralFiniteCode_entropyRate_le line 162

    Source documentation

    A bilateral finite code is a factor of a shifted finite orbit window, so it has no more entropy than the clipped countable observation.

    theorem bilateralFiniteCode_entropyRate_le (d : ℕ)
        (ell : Fin (d+1) → ℝ) (hell : ∑ i, ell i=0)
        (Q : X (d+1) → ℕ) (hQ : Measurable Q)
        (μ : Measure (X (d+1))) [IsProbabilityMeasure μ]
        (hA : ∀ u : LogCoordinates d, μ.map (fun x => rightAction x (diagonalFlow u))=μ)
        (m : ℕ) :
        observationEntropyRate μ
          (fun z => rightAction z (diagonalOneParameter ell hell (-1)))
          (bilateralFiniteCode ell hell Q m) ≤
        observationEntropyRate μ
          (fun z => rightAction z (diagonalOneParameter ell hell (-1))) (heightClip Q m) := by
    …

    Mentions: OAI.DukePrimeDegree.diagonalFlow, OAI.DukePrimeDegree.bilateralFiniteCode, OAI.DukePrimeDegree.heightClip

11. theorem OAI.DukePrimeDegree.entropyRate_le_of_bilateral_heightClip_bounds line 234

    Source documentation

    The small neutral fibers make a uniform entropy bound on all finite clips of Q an entropy bound for every finite measurable observation.

    theorem entropyRate_le_of_bilateral_heightClip_bounds (d : ℕ)
        (ell : Fin (d+1) → ℝ) (hell : ∑ i, ell i=0)
        (Q : X (d+1) → ℕ) (hQ : Measurable Q)
        (μ : Measure (X (d+1))) [IsProbabilityMeasure μ]
        (hA : ∀ u : LogCoordinates d, μ.map (fun x => rightAction x (diagonalFlow u))=μ)
        (hlift : ∀ x y, y ∈ bilateralNameFiber ell hell Q x →
          ∃ g ∈ matrixBall (d+1) 1, rightAction x g=y ∧
            ∀ t : ℝ, Commute g (diagonalOneParameter ell hell t))
        (B : ℝ)
        (hbound : ∀ m, observationEntropyRate μ
          (fun z => rightAction z (diagonalOneParameter ell hell (-1))) (heightClip Q m) ≤ B)
        {k : ℕ} (P : X (d+1) → Fin k) (hP : Measurable P) :
    …

    Mentions: OAI.DukePrimeDegree.diagonalFlow, OAI.DukePrimeDegree.bilateralNameFiber, OAI.DukePrimeDegree.heightClip

12. theorem OAI.DukePrimeDegree.measureEntropy_le_of_bilateral_heightClip_bounds line 280
13. theorem OAI.DukePrimeDegree.measureEntropy_eq_iSup_heightClip_of_neutral_fibers line 304

    Source documentation

    For the constructed neutral-fiber observation, the full metric entropy is the supremum of the entropy rates of its finite clips.

    theorem measureEntropy_eq_iSup_heightClip_of_neutral_fibers (d : ℕ)
        (ell : Fin (d+1) → ℝ) (hell : ∑ i, ell i=0)
        (Q : X (d+1) → ℕ) (hQ : Measurable Q)
        (μ : Measure (X (d+1))) [IsProbabilityMeasure μ]
        (hA : ∀ u : LogCoordinates d, μ.map (fun x => rightAction x (diagonalFlow u))=μ)
        (hlift : ∀ x y, y ∈ bilateralNameFiber ell hell Q x →
          ∃ g ∈ matrixBall (d+1) 1, rightAction x g=y ∧
            ∀ t : ℝ, Commute g (diagonalOneParameter ell hell t)) :
        measureEntropy μ (fun z => rightAction z (diagonalOneParameter ell hell (-1))) =
          ⨆ m, ENNReal.ofReal (observationEntropyRate μ
            (fun z => rightAction z (diagonalOneParameter ell hell (-1))) (heightClip Q m)) := by
    …

    Mentions: OAI.DukePrimeDegree.diagonalFlow, OAI.DukePrimeDegree.bilateralNameFiber, OAI.DukePrimeDegree.heightClip