OAI/Geometry/Convex/GeneralMahler/Spectral.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Order and functional calculus for real symmetric matrices.

  1. lemma OAI.GeneralMahler.op_eigen line 11
  2. theorem OAI.GeneralMahler.cfc_eigen' line 18
  3. lemma OAI.GeneralMahler.neg_eigen line 29
  4. lemma OAI.GeneralMahler.sq_order_cancel line 39

    Source documentation

    Square root order, by testing an eigenvector of A-B.

    lemma sq_order_cancel (ha : 0 ≤ A) (hb : 0 ≤ B)
    (hh : A*A ≤ B*B) : A ≤ B := by
…
  5. lemma OAI.GeneralMahler.sqrt_monotone line 65
  6. abbrev OAI.GeneralMahler.scalar line 72
  7. lemma OAI.GeneralMahler.scalar_eq line 73
  8. lemma OAI.GeneralMahler.scalar_sym line 74
  9. lemma OAI.GeneralMahler.cfc_herm line 77
  10. lemma OAI.GeneralMahler.scalar_cfc_order line 80
  11. lemma OAI.GeneralMahler.spectrum_order line 88
  12. lemma OAI.GeneralMahler.spectrum_norm_box line 96
  13. lemma OAI.GeneralMahler.spectrum_poly_le line 105
  14. lemma OAI.GeneralMahler.cfc_continuous_herm line 117