OAI/NumberTheory/DukePrimeDegree/Entropy/RegularRootEntropyLower.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DukePrimeDegree.positive_root_sum_le_diagonal_entropy line 17

   Source documentation

   The stationary whole-future kernel is constructed here; its existence, normalization and disintegration properties are not additional inputs.

   theorem positive_root_sum_le_diagonal_entropy (d : ℕ)
       (ell : Fin (d+1) → ℝ) (hell : ∑ i, ell i=0)
       (hgap : ∀ p : allPositiveRoots (d+1), Real.log 4 ≤ ell p.val.2-ell p.val.1)
       (μ : Measure (X (d+1))) [IsProbabilityMeasure μ]
       [ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d+1)) μ] :
       ENNReal.ofReal (∑ p : allPositiveRoots (d+1),
         (ell p.val.2-ell p.val.1) * canonicalRootCoefficient d μ p.val.1 p.val.2) ≤
         measureEntropy μ (fun x => rightAction x (diagonalOneParameter ell hell (-1))) := by
   …

   Mentions: OAI.DukePrimeDegree.allPositiveRoots, OAI.DukePrimeDegree.canonicalRootCoefficient

2. theorem OAI.DukePrimeDegree.diagonal_entropy_zero_iff_positive_coefficients_zero line 49

   Source documentation

   Zero metric entropy and zero actual expanding-root information are equivalent for these regular weights.

   theorem diagonal_entropy_zero_iff_positive_coefficients_zero (d : ℕ)
       (ell : Fin (d+1) → ℝ) (hell : ∑ i, ell i=0)
       (hgap : ∀ p : allPositiveRoots (d+1), Real.log 4 ≤ ell p.val.2-ell p.val.1)
       (μ : Measure (X (d+1))) [IsProbabilityMeasure μ]
       [ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d+1)) μ] :
       measureEntropy μ (fun x => rightAction x (diagonalOneParameter ell hell (-1)))=0 ↔
         ∀ p : allPositiveRoots (d+1), canonicalRootCoefficient d μ p.val.1 p.val.2=0 := by
   …

   Mentions: OAI.DukePrimeDegree.allPositiveRoots, OAI.DukePrimeDegree.canonicalRootCoefficient