OAI/NumberTheory/DukePrimeDegree/Geometry/MatrixLogLength.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

A concrete subadditive length on the real special linear group

The logarithmic matrix length is symmetric under inversion and controls small matrix displacements. It is used to construct observables with uniform control along right root translations.

  1. def OAI.DukePrimeDegree.matrixLogLength line 18
  2. lemma OAI.DukePrimeDegree.matrixLogLength_nonneg line 21
  3. lemma OAI.DukePrimeDegree.matrixLogLength_one line 25
  4. lemma OAI.DukePrimeDegree.matrixLogLength_inv line 28
  5. lemma OAI.DukePrimeDegree.log_norm_mul_sub_one_le line 31
  6. lemma OAI.DukePrimeDegree.matrixLogLength_mul_le line 45
  7. lemma OAI.DukePrimeDegree.matrixLogLength_eq_zero_iff line 55
  8. def OAI.DukePrimeDegree.matrixLogGroupNorm line 70
  9. theorem OAI.DukePrimeDegree.continuous_matrixLogLength line 77
  10. lemma OAI.DukePrimeDegree.matrixLogLength_le_displacements line 88
  11. lemma OAI.DukePrimeDegree.norm_sub_one_lt_of_matrixLogLength_lt line 95
  12. lemma OAI.DukePrimeDegree.norm_sub_one_le_exp_matrixLogLength line 106
  13. theorem OAI.DukePrimeDegree.tendsto_one_of_matrixLogLength_tendsto_zero line 116