OAI/NumberTheory/DukePrimeDegree/Dynamics/SingleBlockProjection.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Local preservation of one nontrivial root block

The other root blocks need not preserve the component measure. Only the roots in the selected block and the vanishing of velocity entries crossing its boundary are used. This is the local stabilizer statement needed on a single-block ergodic component.

  1. lemma OAI.DukePrimeDegree.blockProjection_singleBlock_eq line 22
  2. lemma OAI.DukePrimeDegree.commute_singleBlockProjection_of_cross_zero line 38
  3. theorem OAI.DukePrimeDegree.singleBlockProjection_fixed_near_identity line 55