OAI/NumberTheory/DukePrimeDegree/Entropy/ZeroEntropyAllRoots.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A zero-entropy regular element has atomic leaves in both root directions

  1. lemma OAI.DukePrimeDegree.atomic_positive_root_of_zero_entropy line 15
  2. theorem OAI.DukePrimeDegree.all_roots_atomic_of_zero_regular_entropy line 31

    Source documentation

    Time reversal gives zero entropy in the opposite chamber. Reindexing that chamber lets the same proved positive-root lower bound apply there.

    theorem all_roots_atomic_of_zero_regular_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)) μ]
    (hz : measureEntropy μ (fun x => rightAction x (diagonalOneParameter ell hell (-1)))=0) :
    ∀ (i j : Fin (d+1)) (hij : i ≠ j), ∀ᵐ x ∂μ,
      intrinsicRootLeaf hij μ x=Measure.dirac 0 := by
…

    Mentions: OAI.DukePrimeDegree.allPositiveRoots