OAI/NumberTheory/DukePrimeDegree/Geometry/UpperRootMeasureCovariance.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Translation and diagonal covariance of based full-root measures

  1. def OAI.DukePrimeDegree.upperRootTranslate line 15
  2. lemma OAI.DukePrimeDegree.upperRootWord_rebase line 21
  3. lemma OAI.DukePrimeDegree.upperRootWord_translate line 26
  4. lemma OAI.DukePrimeDegree.upperRootRebase_translate line 31
  5. lemma OAI.DukePrimeDegree.upperRootRebase_rebase line 38
  6. lemma OAI.DukePrimeDegree.centerUpperRootMeasure_smul line 45
  7. lemma OAI.DukePrimeDegree.basedUpperRootMeasure_smul line 50
  8. lemma OAI.DukePrimeDegree.centerUpperRootMeasure_translate line 56
  9. lemma OAI.DukePrimeDegree.basedUpperRootMeasure_translate line 66
  10. lemma OAI.DukePrimeDegree.centerUpperRootMeasure_center line 73
  11. lemma OAI.DukePrimeDegree.basedUpperRootMeasure_center line 83
  12. lemma OAI.DukePrimeDegree.centerUpperRootMeasure_unit_lt_top line 90
  13. lemma OAI.DukePrimeDegree.basedUpperRootMeasure_rebase line 98
  14. lemma OAI.DukePrimeDegree.upperRootRebase_dilation line 110
  15. lemma OAI.DukePrimeDegree.centerUpperRootMeasure_dilation line 126
  16. lemma OAI.DukePrimeDegree.basedUpperRootMeasure_dilation line 140