OAI/Geometry/Convex/GeneralMahler/Edge.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Deterministic-endcut layer of PSD contractions. Carries the precise data needed for log-Jacobian estimate.

  1. structure OAI.GeneralMahler.Edge line 14
  2. lemma OAI.GeneralMahler.ProjField.Field_tend line 27
  3. def OAI.GeneralMahler.ProjField.edge line 42
  4. def OAI.GeneralMahler.Edge.ref line 56
  5. def OAI.GeneralMahler.Edge.radius line 66
  6. lemma OAI.GeneralMahler.Edge.r_meas line 68
  7. lemma OAI.GeneralMahler.Edge.r_poly line 70
  8. lemma OAI.GeneralMahler.Edge.r_pos line 73
  9. lemma OAI.GeneralMahler.Edge.Pcont line 75
  10. lemma OAI.GeneralMahler.Edge.P_poly line 82
  11. def OAI.GeneralMahler.Edge.EP line 84
  12. lemma OAI.GeneralMahler.Edge.st_poly line 85
  13. lemma OAI.GeneralMahler.Edge.EP_mixed line 87
  14. def OAI.GeneralMahler.Edge.WP line 96
  15. lemma OAI.GeneralMahler.Edge.wp_meas line 98
  16. lemma OAI.GeneralMahler.Edge.wp_psd line 101
  17. lemma OAI.GeneralMahler.Edge.wp_le line 104
  18. lemma OAI.GeneralMahler.Edge.WP_mixed line 106
  19. lemma OAI.GeneralMahler.Edge.wp_slice_SM line 119
  20. lemma OAI.GeneralMahler.Edge.wp_slice_i line 121
  21. lemma OAI.GeneralMahler.Edge.wp_int line 123
  22. def OAI.GeneralMahler.Edge.Jedge line 126
  23. lemma OAI.GeneralMahler.Edge.Jedge_SM line 128
  24. lemma OAI.GeneralMahler.Edge.Jedge_poly line 129
  25. lemma OAI.GeneralMahler.Edge.Jedge_bound line 130
  26. lemma OAI.GeneralMahler.Edge.Jedge_pd line 141