RootBlocks.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The invariant root blocks

The canonical root entropy identity makes the invariant-root relation an equivalence relation. The associated subgroup is defined by its root generators and fixes the measure.

lemma OAI.DukePrimeDegree.diagonal_preserves line 25
lemma OAI.DukePrimeDegree.rootInvarianceRelation_iff_coefficient line 31
lemma OAI.DukePrimeDegree.rootInvarianceRelation_symm line 51
def OAI.DukePrimeDegree.invariantRootSetoid line 63
Source documentation
The blocks are equivalence classes of actual root invariance.
```
def invariantRootSetoid : Setoid (Fin (d + 1)) where
…
```
def OAI.PrimeDegreePackets.invariantRootGeneratedGroup line 74
Source documentation
The group generated by all root groups preserving the actual measure.
```
def invariantRootGeneratedGroup {n : ℕ} (μ : Measure (X n)) : Subgroup (G n) :=
…
```
Mentions: OAI.PrimeDegreePackets.X, OAI.PrimeDegreePackets.G
lemma OAI.PrimeDegreePackets.invariantRootGeneratedGroup_le line 78
lemma OAI.PrimeDegreePackets.root_mem_invariantRootGeneratedGroup line 86
lemma OAI.PrimeDegreePackets.measure_map_rootGeneratedGroup line 91
theorem OAI.PrimeDegreePackets.diagonal_normalizes_rootGeneratedGroup line 97
Source documentation
Every real diagonal flow normalizes the group generated by invariant root groups, since it only rescales each root parameter.
```
theorem diagonal_normalizes_rootGeneratedGroup {n : ℕ} (μ : Measure (X n))
    (ell : Fin n → ℝ) (hell : ∑ i, ell i = 0) (t : ℝ) :
    diagonalOneParameter ell hell t ∈
      Subgroup.normalizer (invariantRootGeneratedGroup μ : Set (G n)) := by
…
```
Mentions: OAI.PrimeDegreePackets.X, OAI.PrimeDegreePackets.diagonalOneParameter, OAI.PrimeDegreePackets.invariantRootGeneratedGroup, OAI.PrimeDegreePackets.G