OAI/NumberTheory/DukePrimeDegree/Geometry/RootProductShear.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Measure preservation of the three-root shear

For the root-order change in EK2003, Proposition 8.3, a noncommuting pair adds the product of its parameters to the commutator coordinate. If a factor is Dirac the shear vanishes. Otherwise commutator invariance makes the third factor translation invariant.

  1. def OAI.DukePrimeDegree.rootProductShear line 22
  2. lemma OAI.DukePrimeDegree.measurable_rootProductShear line 25
  3. theorem OAI.DukePrimeDegree.rootProductShear_preserves line 29
  4. theorem OAI.DukePrimeDegree.ae_intrinsic_rootProductShear_preserves line 58