AtomicRootPositivity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Positive entropy gives a positive actual root coefficient

theorem OAI.DukePrimeDegree.positive_root_coefficient_of_positive_diagonal_entropy line 17

Source documentation

This implication needs no numerical entropy formula. Its contrapositive is the proved zero-entropy theorem for atomic expanding roots.

theorem positive_root_coefficient_of_positive_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)) μ]
    (hpos : 0 < measureEntropy μ
      (fun x => rightAction x (diagonalOneParameter ell hell (-1)))) :
    ∃ i j : Fin (d+1), i < j ∧ 0 < canonicalRootCoefficient d μ i j := by
…

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

theorem OAI.DukePrimeDegree.positive_root_coefficient_of_regular_entropy line 40

Source documentation

The positive-entropy hypothesis used by the prime-degree application already supplies a positive root coefficient, without EKL Proposition3.1(3).

theorem positive_root_coefficient_of_regular_entropy (d : ℕ)
    (μ : Measure (X (d+1))) [IsProbabilityMeasure μ]
    [ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d+1)) μ]
    (hpos : 0 < measureEntropy μ (fun x => rightAction x
      (diagonalOneParameter (regularDiagonalWeights d) (regularDiagonalWeights_sum d) 1))) :
    ∃ i j : Fin (d+1), i < j ∧ 0 < canonicalRootCoefficient d μ i j := by
…

Mentions: OAI.DukePrimeDegree.canonicalRootCoefficient