WeylDiagonalAction.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Diagonal invariance and ergodicity under coordinate permutations

def OAI.DukePrimeDegree.reindexLogCoordinates line 13
Source documentation
The original last coordinate is restored before the coordinates are permuted.
```
def reindexLogCoordinates (d : ℕ) (e : Equiv.Perm (Fin (d+1)))
    (u : LogCoordinates d) : LogCoordinates d :=
…
```
lemma OAI.DukePrimeDegree.reindex_diagonalFlow line 17
lemma OAI.DukePrimeDegree.reindex_diagonalFlow_conjugacy line 31
lemma OAI.DukePrimeDegree.reindex_diagonalFlow_reverse line 37

theorem OAI.DukePrimeDegree.diagonal_invariant_reindex line 49

Source documentation

The full diagonal action remains invariant after reindexing.

theorem diagonal_invariant_reindex (d : ℕ) (e : Equiv.Perm (Fin (d+1)))
    (μ : Measure (X (d+1)))
    (hA : ∀ u : LogCoordinates d, μ.map (fun x => rightAction x (diagonalFlow u))=μ)
    (u : LogCoordinates d) :
    (μ.map (quotientReindex e)).map (fun x => rightAction x (diagonalFlow u)) =
      μ.map (quotientReindex e) := by
…

Mentions: OAI.DukePrimeDegree.diagonalFlow, OAI.DukePrimeDegree.quotientReindex

theorem OAI.DukePrimeDegree.diagonal_ergodic_reindex line 67

Source documentation

Ergodicity uses the full diagonal group, whose parameters are permuted along with the coordinates.

theorem diagonal_ergodic_reindex (d : ℕ) (e : Equiv.Perm (Fin (d+1)))
    (μ : Measure (X (d+1)))
    [ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d+1)) μ] :
    ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d+1))
      (μ.map (quotientReindex e)) := by
…

Mentions: OAI.DukePrimeDegree.quotientReindex