OAI/Geometry/Convex/GeneralMahler/Budget/Parity.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Parity of Gaussian fields and coefficient projections.

  1. lemma OAI.GeneralMahler.map_deriv_odd line 12
  2. lemma OAI.GeneralMahler.map_deriv_even line 20
  3. lemma OAI.GeneralMahler.pl_odd line 28
  4. lemma OAI.GeneralMahler.fl_odd line 46
  5. lemma OAI.GeneralMahler.Hneg line 54
  6. lemma OAI.GeneralMahler.MMneg line 66
  7. lemma OAI.GeneralMahler.ProjField.Lneg line 73
  8. lemma OAI.GeneralMahler.ProjField.BoEval line 78
  9. lemma OAI.GeneralMahler.ProjField.cf_ref line 104
  10. lemma OAI.GeneralMahler.ProjField.cf_s line 108
  11. lemma OAI.GeneralMahler.ProjField.cof_odd_zero line 111
  12. def OAI.GeneralMahler.ProjField.Ro line 123
  13. lemma OAI.GeneralMahler.ProjField.re_ref line 124
  14. lemma OAI.GeneralMahler.ProjField.Ro_reg line 127
  15. lemma OAI.GeneralMahler.ProjField.coRo line 130
  16. lemma OAI.GeneralMahler.ProjField.bal_cf line 139