OAI/Geometry/Convex/GeneralMahler/EvalGap.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Primitive identities and notation for layer to spectral comparisons.

  1. lemma OAI.GeneralMahler.pj_sym line 12
  2. lemma OAI.GeneralMahler.j_smul_left line 13
  3. lemma OAI.GeneralMahler.pj_norm line 15
  4. lemma OAI.GeneralMahler.pj_scale line 24
  5. lemma OAI.GeneralMahler.mixed_proj line 31
  6. def OAI.GeneralMahler.FieldMat.eVal line 44
  7. lemma OAI.GeneralMahler.FieldMat.pEval line 45
  8. lemma OAI.GeneralMahler.FieldMat.smEval line 48
  9. def OAI.GeneralMahler.FieldMat.EC line 52
  10. lemma OAI.GeneralMahler.FieldMat.Em line 53
  11. lemma OAI.GeneralMahler.FieldMat.Ep line 56
  12. lemma OAI.GeneralMahler.FieldMat.vanishEC line 61
  13. lemma OAI.GeneralMahler.FieldMat.gapM line 72
  14. def OAI.GeneralMahler.FieldMat.LL line 96
  15. lemma OAI.GeneralMahler.FieldMat.gap line 101
  16. lemma OAI.GeneralMahler.FieldMat.nest line 130