OAI/Geometry/Convex/GeneralMahler/Budget/Blocks.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Algebra of the positive layer blocks (with no commutation assumptions). All entries here are in a fixed spectral frame.

  1. def OAI.GeneralMahler.hsN line 13
  2. def OAI.GeneralMahler.ipN line 14
  3. def OAI.GeneralMahler.cmu line 15
  4. lemma OAI.GeneralMahler.symm_entry line 16
  5. def OAI.GeneralMahler.mats line 18
  6. lemma OAI.GeneralMahler.trace_pair line 19
  7. lemma OAI.GeneralMahler.traceDiag line 21
  8. lemma OAI.GeneralMahler.hsN_eq line 24
  9. lemma OAI.GeneralMahler.hsN_pos line 26
  10. lemma OAI.GeneralMahler.hsN_loc line 27
  11. lemma OAI.GeneralMahler.Frm.loc_psd line 29
  12. lemma OAI.GeneralMahler.Frm.loc_le line 32
  13. lemma OAI.GeneralMahler.cmu_eig line 36
  14. lemma OAI.GeneralMahler.mats_add line 45
  15. lemma OAI.GeneralMahler.mats_s line 47
  16. lemma OAI.GeneralMahler.mats_le line 49
  17. structure OAI.GeneralMahler.block line 52

    Source comment

    entries in frame of A, eigenvalues x_i
    structure block (m:ℕ) where
…
  18. def OAI.GeneralMahler.block.E line 61
  19. def OAI.GeneralMahler.block.L line 62
  20. def OAI.GeneralMahler.block.a line 63
  21. def OAI.GeneralMahler.block.S line 64
  22. lemma OAI.GeneralMahler.block.az line 66
  23. lemma OAI.GeneralMahler.block.Sspec line 70
  24. lemma OAI.GeneralMahler.block.Ediag line 72
  25. lemma OAI.GeneralMahler.block.Her line 73
  26. lemma OAI.GeneralMahler.block.Spar line 75
  27. lemma OAI.GeneralMahler.block.Sdiag line 98
  28. lemma OAI.GeneralMahler.block.Ed2 line 102
  29. lemma OAI.GeneralMahler.block.tr_blk line 115