RootCoefficientReduction.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The entropy formula and invariant root blocks

The root coefficients satisfy the entropy formula, zero criterion and Haar normalization of EKL (2006), Proposition 3.1. The commutator and shearing arguments give invariance in the high- and low-entropy cases.

structure OAI.DukePrimeDegree.RootEntropyCoefficients line 24
Source documentation
Root entropy coefficients as in EKL (2006), Proposition 3.1, with zero diagonal.
```
structure RootEntropyCoefficients (d : ℕ) (μ : Measure (X (d + 1)))
    [IsFiniteMeasure μ] where
…
```
lemma OAI.DukePrimeDegree.RootEntropyCoefficients.atomless_of_pos line 44
lemma OAI.DukePrimeDegree.RootEntropyCoefficients.nontrivial_of_pos line 51
lemma OAI.DukePrimeDegree.RootEntropyCoefficients.balanced line 60
lemma OAI.DukePrimeDegree.RootEntropyCoefficients.two_step line 65
lemma OAI.DukePrimeDegree.RootEntropyCoefficients.symmetric line 79
lemma OAI.DukePrimeDegree.RootEntropyCoefficients.invariant_of_positive_row line 85
Source documentation
The high-entropy case: a third positive coefficient in the same row forces invariance. The two applications of the commutator theorem are explicit, so no converse to the Haar normalization is required.
```
lemma invariant_of_positive_row {a b c : Fin (d + 1)}
    (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c)
    (hposab : 0 < C.coefficient a b) (hposac : 0 < C.coefficient a c) :
    ∀ t : ℝ, μ.map (fun x => rightAction x
      (Matrix.SpecialLinearGroup.transvection hab t)) = μ := by
…
```
lemma OAI.DukePrimeDegree.RootEntropyCoefficients.invariant_of_positive_column line 99

theorem OAI.DukePrimeDegree.RootEntropyCoefficients.invariant_of_pos line 115

Source documentation

Combining the proved high- and low-entropy cases turns each positive root coefficient into actual invariance of the ambient measure.

theorem invariant_of_pos (hd : 2 < d + 1) {i j : Fin (d + 1)} (hij : i ≠ j)
    (hpos : 0 < C.coefficient i j) :
    ∀ t : ℝ, μ.map (fun x => rightAction x
      (Matrix.SpecialLinearGroup.transvection hij t)) = μ := by
…

theorem OAI.DukePrimeDegree.RootEntropyCoefficients.zero_or_one line 133

theorem OAI.DukePrimeDegree.RootEntropyCoefficients.exists_invariant_root_of_entropy_pos line 144

Source documentation

Positive entropy supplies a nontrivial invariant root subgroup.

theorem exists_invariant_root_of_entropy_pos (hd : 2 < d + 1)
    (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)) = μ := by
…