OAI/NumberTheory/DukePrimeDegree/Dynamics/ShearingDiagonal.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The two-coordinate shearing diagonal

In the row-lattice convention the weights are -1 at the root's row, +1 at its column, and zero elsewhere. Backward right translation contracts root time by exp (-2*t). The corresponding relative return matrix has a fixed diagonal difference, quadratic coefficient growing by exp (2*t), and other shearing coefficients growing by exp t. These are the rates in EKL (2006), Lemma 4.6.

  1. def OAI.DukePrimeDegree.rootPairWeights line 24
  2. lemma OAI.DukePrimeDegree.rootPairWeights_sum line 27
  3. lemma OAI.DukePrimeDegree.rootPairWeights_row line 30
  4. lemma OAI.DukePrimeDegree.rootPairWeights_col line 33
  5. lemma OAI.DukePrimeDegree.rootPairWeights_other line 36
  6. def OAI.DukePrimeDegree.rootPairFlow line 39
  7. def OAI.DukePrimeDegree.rootPairConjugate line 42
  8. lemma OAI.DukePrimeDegree.rootPairConjugate_diagonal line 45
  9. lemma OAI.DukePrimeDegree.rootPairConjugate_quadratic line 49
  10. lemma OAI.DukePrimeDegree.rootPairConjugate_row line 56
  11. lemma OAI.DukePrimeDegree.rootPairConjugate_col line 62
  12. theorem OAI.DukePrimeDegree.rootPairFlow_contracts_root line 68
  13. theorem OAI.DukePrimeDegree.rootPairFlow_preserving line 79
  14. theorem OAI.DukePrimeDegree.exists_rootPairFlow_return_good_set line 88