OAI/Geometry/Convex/GeneralMahler/Lift.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.GeneralMahler.Body line 12

   Source documentation

   Paper K is a real convex body with interior.

   structure Body (n : ℕ) extends ConvexBody (Rn n) where
   …

   Mentions: OAI.GeneralMahler.Rn

2. instance OAI.GeneralMahler.Body.(instance at line 17) line 17
3. theorem OAI.GeneralMahler.Body.isCompact line 20
4. theorem OAI.GeneralMahler.Body.isClosed line 21
5. theorem OAI.GeneralMahler.Body.convex line 22
6. theorem OAI.GeneralMahler.Body.has_interior line 23
7. theorem OAI.GeneralMahler.Body.nonempty line 24
8. abbrev OAI.GeneralMahler.LiftSpace line 27
9. def OAI.GeneralMahler.pair line 30
10. def OAI.GeneralMahler.hgt line 31
11. def OAI.GeneralMahler.horiz line 32
12. theorem OAI.GeneralMahler.pair_hgt line 33
13. theorem OAI.GeneralMahler.pair_horiz line 34
14. theorem OAI.GeneralMahler.hgt_horiz_pair line 35
15. theorem OAI.GeneralMahler.pair_zero line 36
16. theorem OAI.GeneralMahler.pair_inner line 37
17. theorem OAI.GeneralMahler.hgt_add line 39
18. theorem OAI.GeneralMahler.horiz_add line 40
19. theorem OAI.GeneralMahler.hgt_smul line 41
20. theorem OAI.GeneralMahler.horiz_smul line 42
21. theorem OAI.GeneralMahler.smul_pair line 44
22. theorem OAI.GeneralMahler.continuous_pair line 46
23. theorem OAI.GeneralMahler.continuous_pair' line 48
24. theorem OAI.GeneralMahler.continuous_hgt line 51
25. theorem OAI.GeneralMahler.continuous_horiz line 53
26. def OAI.GeneralMahler.Body.cone line 59

    Source documentation

    The solid pointed cone generated by (1,K).

    def cone (K : Body n) : ProperCone ℝ (LiftSpace n) where
    …

    Mentions: OAI.GeneralMahler.Body, OAI.GeneralMahler.LiftSpace

27. theorem OAI.GeneralMahler.Body.pair_mem_cone line 95
28. theorem OAI.GeneralMahler.Body.pair_mem_interior_cone_iff line 98
29. theorem OAI.GeneralMahler.Body.solid_cone line 126
30. theorem OAI.GeneralMahler.Body.axis_dual_interior line 131