OAI/Geometry/Convex/GeneralMahler/Field.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

§02, Gaussian field notation and mean equations.

  1. structure OAI.GeneralMahler.ProjField line 12
  2. abbrev OAI.GeneralMahler.ProjField.D line 28
  3. def OAI.GeneralMahler.ProjField.covMat line 29
  4. def OAI.GeneralMahler.ProjField.shift line 30
  5. def OAI.GeneralMahler.ProjField.XT line 31
  6. def OAI.GeneralMahler.ProjField.Z line 32
  7. def OAI.GeneralMahler.ProjField.YT line 33
  8. def OAI.GeneralMahler.ProjField.Pmat line 34
  9. lemma OAI.GeneralMahler.ProjField.Pmat_psd line 36
  10. lemma OAI.GeneralMahler.ProjField.Pmat_le line 37
  11. lemma OAI.GeneralMahler.ProjField.Pmat_herm line 38
  12. lemma OAI.GeneralMahler.ProjField.scaled_interior line 40
  13. lemma OAI.GeneralMahler.ProjField.contDiff_a line 50
  14. theorem OAI.GeneralMahler.ProjField.shift_cd line 53
  15. lemma OAI.GeneralMahler.ProjField.XT_mean line 59
  16. lemma OAI.GeneralMahler.ProjField.YT_sub line 62
  17. lemma OAI.GeneralMahler.ProjField.Y_mean line 65
  18. lemma OAI.GeneralMahler.ProjField.XP line 71
  19. lemma OAI.GeneralMahler.ProjField.deriv_shift_mean line 76
  20. def OAI.GeneralMahler.ProjField.Bt line 84
  21. def OAI.GeneralMahler.ProjField.r1 line 85
  22. lemma OAI.GeneralMahler.ProjField.Bt_hasDeriv line 87
  23. lemma OAI.GeneralMahler.ProjField.r1_eq line 95
  24. lemma OAI.GeneralMahler.ProjField.Bt_nonneg line 99
  25. lemma OAI.GeneralMahler.ProjField.r1_pos line 112