OAI/NumberTheory/DukePrimeDegree/Dynamics/ShearingKappa.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

A scale for noncentral return matrices

The scale is the maximum of the diagonal difference and a homogeneous off-diagonal size. The latter uses the square root of the quadratic coefficient and a finite sum of the other linear coefficients. This equivalent choice of norm gives exactly the two scaling regimes used in EKL (2006), Lemma 4.6.

  1. def OAI.DukePrimeDegree.rootShearingOffDiagonalSize line 23
  2. def OAI.DukePrimeDegree.rootShearingMovingSize line 26
  3. def OAI.DukePrimeDegree.rootShearingKappa line 29
  4. lemma OAI.DukePrimeDegree.rootShearingOffDiagonalSize_nonneg line 32
  5. lemma OAI.DukePrimeDegree.rootShearingOffDiagonalSize_row_bound line 38
  6. lemma OAI.DukePrimeDegree.rootShearingOffDiagonalSize_col_bound line 47
  7. lemma OAI.DukePrimeDegree.rootShearingMovingSize_nonneg line 56
  8. lemma OAI.DukePrimeDegree.rootShearingKappa_nonneg line 60
  9. theorem OAI.DukePrimeDegree.rootShearingKappa_pos_of_noncentral line 64
  10. theorem OAI.DukePrimeDegree.rootShearingMovingSize_conjugate line 99
  11. theorem OAI.DukePrimeDegree.rootShearingKappa_conjugate line 124
  12. theorem OAI.DukePrimeDegree.continuous_rootShearingKappa line 131