OAI/Geometry/Convex/GeneralMahler/Frame/Diagonal.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Borel choice of diagonalizing frame. Everything computed in a diagonalization is defined on a full orthogonal matrix and its entries.

  1. abbrev OAI.GeneralMahler.Frm line 12
  2. def OAI.GeneralMahler.Frm.loc line 15
  3. def OAI.GeneralMahler.Frm.fixMat line 16
  4. def OAI.GeneralMahler.Frm.eig line 17
  5. def OAI.GeneralMahler.Frm.Dgn line 18
  6. lemma OAI.GeneralMahler.Frm.m₁ line 19
  7. lemma OAI.GeneralMahler.Frm.m₂ line 20
  8. lemma OAI.GeneralMahler.Frm.loc_fix line 22
  9. lemma OAI.GeneralMahler.Frm.fix_loc line 26
  10. lemma OAI.GeneralMahler.Frm.loc_inj line 30
  11. lemma OAI.GeneralMahler.Frm.loc_mul line 33
  12. lemma OAI.GeneralMahler.Frm.loc_star line 37
  13. lemma OAI.GeneralMahler.Frm.loc_trace line 39
  14. lemma OAI.GeneralMahler.Frm.loc_norm line 41
  15. lemma OAI.GeneralMahler.Frm.loc_one line 45
  16. lemma OAI.GeneralMahler.Frm.loc_zero line 46
  17. lemma OAI.GeneralMahler.Frm.loc_sub line 47
  18. lemma OAI.GeneralMahler.Frm.loc_add line 48
  19. lemma OAI.GeneralMahler.Frm.loc_smul line 49
  20. lemma OAI.GeneralMahler.Frm.fix_mul_cross line 51
  21. lemma OAI.GeneralMahler.Frm.fix_mul_cross' line 55
  22. lemma OAI.GeneralMahler.Frm.cross_cancel line 61
  23. def OAI.GeneralMahler.Frm.specEval line 66
  24. lemma OAI.GeneralMahler.Frm.lSpecEq line 67
  25. lemma OAI.GeneralMahler.Frm.frame_cross line 70
  26. lemma OAI.GeneralMahler.Frm.spec_unique line 76
  27. def OAI.GeneralMahler.Frm.eu line 88
  28. lemma OAI.GeneralMahler.Frm.eu_loc line 89
  29. lemma OAI.GeneralMahler.Frm.eu_eig line 95
  30. lemma OAI.GeneralMahler.Frm.eu_d line 96
  31. lemma OAI.GeneralMahler.Frm.loc_cfc line 98
  32. lemma OAI.GeneralMahler.Frm.cont_loc line 108
  33. lemma OAI.GeneralMahler.Frm.cdiag line 112
  34. lemma OAI.GeneralMahler.Frm.cdiagonal line 114
  35. lemma OAI.GeneralMahler.Frm.Dgn_closed line 116
  36. instance OAI.GeneralMahler.Frm.frame_cmp line 119
  37. abbrev OAI.GeneralMahler.Frm.SH line 136
  38. lemma OAI.GeneralMahler.Frm.selectU line 137
  39. def OAI.GeneralMahler.Frm.fr line 145
  40. lemma OAI.GeneralMahler.Frm.fr_m line 146
  41. lemma OAI.GeneralMahler.Frm.fr_d line 147