CanonicalRootCoefficients.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Canonical coefficients applied to the published entropy formula

def OAI.DukePrimeDegree.CanonicalRootEntropyFormula line 21
Source documentation
The canonical root entropy identity of EKL (2006), Proposition 3.1(3).
```
def CanonicalRootEntropyFormula : Prop :=
…
```
def OAI.DukePrimeDegree.canonicalRootEntropyCoefficients line 28
Source documentation
The canonical entropy formula, together with the elementary coefficient properties, gives root entropy coefficients.
```
def canonicalRootEntropyCoefficients (hformula : CanonicalRootEntropyFormula d μ) :
    RootEntropyCoefficients d μ where
…
```
Mentions: OAI.DukePrimeDegree.CanonicalRootEntropyFormula, OAI.DukePrimeDegree.RootEntropyCoefficients

theorem OAI.DukePrimeDegree.canonicalRootCoefficient_zero_or_one line 38

Source documentation

The canonical entropy formula forces the coefficients to be zero or one.

theorem canonicalRootCoefficient_zero_or_one
    [ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d + 1)) μ]
    (hd : 2 < d + 1) (hformula : CanonicalRootEntropyFormula d μ)
    (i j : Fin (d + 1)) :
    canonicalRootCoefficient d μ i j = 0 ∨ canonicalRootCoefficient d μ i j = 1 :=
…

Mentions: OAI.DukePrimeDegree.CanonicalRootEntropyFormula, OAI.DukePrimeDegree.canonicalRootCoefficient

theorem OAI.DukePrimeDegree.exists_invariant_root_of_canonical_entropy_formula line 47

Source documentation

The canonical entropy formula turns positive metric entropy into invariance under a root subgroup.

theorem exists_invariant_root_of_canonical_entropy_formula
    [ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d + 1)) μ]
    (hd : 2 < d + 1) (hformula : CanonicalRootEntropyFormula d μ)
    (ell : Fin (d + 1) → ℝ) (hell : ∑ i, ell i = 0)
    (hpos : 0 < measureEntropy μ
      (fun x => rightAction x (diagonalOneParameter ell hell 1))) :
    ∃ (i j : Fin (d + 1)) (hij : i ≠ j), ∀ t : ℝ,
      μ.map (fun x => rightAction x (Matrix.SpecialLinearGroup.transvection hij t)) = μ :=
…

Mentions: OAI.DukePrimeDegree.CanonicalRootEntropyFormula