OAI/Geometry/Convex/GeneralMahler/DefectIBP.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Scalar layer δ integration identities (including Eq 12).

  1. lemma OAI.GeneralMahler.rapid_ftc line 10
  2. lemma OAI.GeneralMahler.MomentF.int_test line 13
  3. lemma OAI.GeneralMahler.N2_test line 15
  4. def OAI.GeneralMahler.ProjField.pb line 20
  5. def OAI.GeneralMahler.ProjField.ab line 21
  6. def OAI.GeneralMahler.ProjField.rk line 22
  7. lemma OAI.GeneralMahler.ProjField.Bt_d line 23
  8. lemma OAI.GeneralMahler.ProjField.dB_d line 26
  9. lemma OAI.GeneralMahler.ProjField.hd_d line 29
  10. lemma OAI.GeneralMahler.ProjField.dm_eq line 30
  11. lemma OAI.GeneralMahler.ProjField.ab_d line 33
  12. lemma OAI.GeneralMahler.ProjField.pb_d line 36
  13. lemma OAI.GeneralMahler.ProjField.dB_c line 39
  14. lemma OAI.GeneralMahler.ProjField.hd_c line 40
  15. lemma OAI.GeneralMahler.ProjField.pb_m line 44
  16. lemma OAI.GeneralMahler.ProjField.ab_m line 45
  17. lemma OAI.GeneralMahler.ProjField.hd_m line 46
  18. lemma OAI.GeneralMahler.ProjField.dm_m line 47
  19. lemma OAI.GeneralMahler.ProjField.rk_m line 50
  20. lemma OAI.GeneralMahler.ProjField.mass line 52
  21. lemma OAI.GeneralMahler.ProjField.hd_test line 61
  22. lemma OAI.GeneralMahler.ProjField.eq12 line 70
  23. def OAI.GeneralMahler.ProjField.shiftD line 84
  24. lemma OAI.GeneralMahler.ProjField.delta_eq line 85
  25. lemma OAI.GeneralMahler.ProjField.delta_d line 97