OAI/NumberTheory/DukePrimeDegree/Dynamics/ShearingNormalizedProfile.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The normalized profile of an actual return matrix

The algebraic profile is the actual pivot displacement together with the remaining linear coefficients. Its normalization agrees with the previously defined shearing scale, and its size is controlled by the matrix displacement.

  1. lemma OAI.DukePrimeDegree.rootShearSize_nonneg line 22
  2. theorem OAI.DukePrimeDegree.rootShearingOffDiagonalSize_mul_le line 26
  3. theorem OAI.DukePrimeDegree.rootShearing_raw_profile_le_size line 50
  4. theorem OAI.DukePrimeDegree.rootShearing_normalized_profile_identity line 62
  5. theorem OAI.DukePrimeDegree.rootShearing_normalized_profile_le_size line 72