OAI/Geometry/Convex/GeneralMahler/TraceOrder.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.GeneralMahler.mat_meas line 11

   Source comment

   Use actual Borel measurable structure

   instance mat_meas (m:ℕ) : MeasurableSpace (Mat m) := borel _

   Mentions: OAI.GeneralMahler.Mat

2. instance OAI.GeneralMahler.mat_borel line 12
3. lemma OAI.GeneralMahler.trN_cyclic line 13
4. lemma OAI.GeneralMahler.trN_add line 15
5. lemma OAI.GeneralMahler.trN_sub line 16
6. lemma OAI.GeneralMahler.trN_smul line 17
7. lemma OAI.GeneralMahler.trN_mono line 19
8. lemma OAI.GeneralMahler.sand_nonneg line 25
9. lemma OAI.GeneralMahler.trN_mul_nonneg line 29
10. lemma OAI.GeneralMahler.trN_mul_mono line 37
11. lemma OAI.GeneralMahler.trN_j line 41
12. lemma OAI.GeneralMahler.trN_one line 44
13. lemma OAI.GeneralMahler.trN_unit line 45
14. lemma OAI.GeneralMahler.trN_prod_unit line 49
15. lemma OAI.GeneralMahler.thresh_pd line 56
16. lemma OAI.GeneralMahler.inv_mul' line 58
17. lemma OAI.GeneralMahler.mul_inv' line 59
18. lemma OAI.GeneralMahler.inv_rev line 62

    Source documentation

    Order reversal under inversion: prove by nonnegative remainder.

    lemma inv_rev {A B:Mat m} (ha:A.PosDef) (hb:B.PosDef) (hh:A≤B) : B⁻¹≤A⁻¹ := by
    …

    Mentions: OAI.GeneralMahler.Mat

19. def OAI.GeneralMahler.thresh line 72
20. lemma OAI.GeneralMahler.thresh_mono line 73
21. lemma OAI.GeneralMahler.thresh_unit line 75
22. lemma OAI.GeneralMahler.thresh_eq line 80
23. lemma OAI.GeneralMahler.mul_comm_nonneg line 86

    Source comment

    b > 0 upper bound on I+A gives b⁻¹ A ≤ thresh A via eigenvectors or product of commuting

    lemma mul_comm_nonneg {A B:Mat m} (ha:0≤A) (hb:0≤B) (hh:Commute A B) :
        0 ≤ A*B := by
    …

    Mentions: OAI.GeneralMahler.Mat

24. lemma OAI.GeneralMahler.thresh_low line 97