OAI/Geometry/Convex/GeneralMahler/Update.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

§02 covariance equation from scalar inequalities of §01.

  1. def OAI.GeneralMahler.lam line 11
  2. def OAI.GeneralMahler.mstar line 12
  3. def OAI.GeneralMahler.ell0 line 13
  4. def OAI.GeneralMahler.cupper line 14
  5. structure OAI.GeneralMahler.UpdatesOK line 17

    Source documentation

    Regularity and scalar bounds for the covariance update.

    structure UpdatesOK (C K : ℝ → ℝ) : Prop where
…
  6. def OAI.GeneralMahler.jprod line 29
  7. def OAI.GeneralMahler.updEq line 30
  8. def OAI.GeneralMahler.updGap line 31
  9. lemma OAI.GeneralMahler.jordan_sym line 33
  10. lemma OAI.GeneralMahler.sqPSD line 38
  11. lemma OAI.GeneralMahler.upd_sym line 42
  12. lemma OAI.GeneralMahler.upd_form line 46
  13. lemma OAI.GeneralMahler.gap_from_cov line 58
  14. def OAI.GeneralMahler.ProjField.expL line 90
  15. theorem OAI.GeneralMahler.ProjField.intL line 93
  16. lemma OAI.GeneralMahler.ProjField.expL_sym line 106
  17. lemma OAI.GeneralMahler.ProjField.expL_affine_pos line 110
  18. lemma OAI.GeneralMahler.ProjField.expL_bounds line 138