NeutralRelativeEntropy.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Relative entropy of finite names over the bilateral itinerary factor

theorem OAI.DukePrimeDegree.diagonal_negative_iterate line 16
theorem OAI.DukePrimeDegree.bilateral_name_entropy_le_robust_error line 23

theorem OAI.DukePrimeDegree.bilateral_name_entropy_sublinear line 90

Source documentation

Conditioning on the actual bilateral itinerary leaves a sublinear amount of information in every finite measurable observation.

theorem bilateral_name_entropy_sublinear {n k : ℕ}
    (ell : Fin n → ℝ) (hell : ∑ i, ell i=0)
    (Q : X n → ℕ) (hQ : Measurable Q)
    (hlift : ∀ x y, y ∈ bilateralNameFiber ell hell Q x →
      ∃ g ∈ matrixBall n 1, rightAction x g=y ∧
        ∀ t : ℝ, Commute g (diagonalOneParameter ell hell t))
    (μ : Measure (X n)) [IsProbabilityMeasure μ]
    (hT : MeasurePreserving
      (fun z => rightAction z (diagonalOneParameter ell hell (-1))) μ μ)
    (P : X n → Fin k) (hP : Measurable P)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ M : ℕ, ∀ N : ℕ,
…

Mentions: OAI.DukePrimeDegree.bilateralNameFiber

theorem OAI.DukePrimeDegree.bilateral_name_relative_entropy_tendsto_zero line 118