OAI/Geometry/Convex/GeneralMahler/GradientLayer.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

The centered fields W_f from §02,04. We use coefficient derivatives (Hermite) as justified by differentiation by parts: rather than interchanging weak derivatives, integrate the coefficient identity using the layer cutoff bounds.

  1. def OAI.GeneralMahler.ProjField.Xb line 17
  2. def OAI.GeneralMahler.ProjField.Yb line 18
  3. lemma OAI.GeneralMahler.ProjField.XPbound line 19
  4. lemma OAI.GeneralMahler.ProjField.YPbound line 22
  5. lemma OAI.GeneralMahler.ProjField.XbM line 29
  6. lemma OAI.GeneralMahler.ProjField.YbM line 42
  7. def OAI.GeneralMahler.ProjField.WW line 56
  8. lemma OAI.GeneralMahler.ProjField.WW_mean line 60
  9. lemma OAI.GeneralMahler.ProjField.WW_eq line 75
  10. lemma OAI.GeneralMahler.ProjField.WW_m line 81
  11. lemma OAI.GeneralMahler.ProjField.WW_c line 94
  12. def OAI.GeneralMahler.ProjField.WK line 97
  13. def OAI.GeneralMahler.ProjField.WH line 98
  14. lemma OAI.GeneralMahler.ProjField.WK_SM line 101
  15. lemma OAI.GeneralMahler.ProjField.WK_m line 103
  16. lemma OAI.GeneralMahler.ProjField.WH_reg line 108
  17. lemma OAI.GeneralMahler.ProjField.WH_mean line 112
  18. def OAI.GeneralMahler.ProjField.act line 119
  19. lemma OAI.GeneralMahler.ProjField.act_eq line 122
  20. lemma OAI.GeneralMahler.ProjField.WWd line 125
  21. lemma OAI.GeneralMahler.ProjField.WW_lip line 137
  22. lemma OAI.GeneralMahler.ProjField.WDer_p line 140
  23. lemma OAI.GeneralMahler.ProjField.WW_recur line 145
  24. lemma OAI.GeneralMahler.ProjField.cof_layer line 159
  25. lemma OAI.GeneralMahler.ProjField.WH_rec line 171