OAI/NumberTheory/DukePrimeDegree/Geometry/SmallMatrixLength.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Quantitative logarithmic length near the identity

The algebraic inverse identity bounds the inverse norm by two on a half-unit operator ball. Consequently logarithmic length is bounded by three times the displacement norm there.

  1. lemma OAI.DukePrimeDegree.specialLinear_inverse_norm_le_two line 18
  2. lemma OAI.DukePrimeDegree.matrixLogLength_le_three_norm line 37
  3. lemma OAI.DukePrimeDegree.matrixLogLength_le_three_card_radius line 54