OAI/Geometry/Convex/GeneralMahler/Variation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Inverse-kernel and variation identity Eq14.

  1. def OAI.GeneralMahler.Nr line 10
  2. lemma OAI.GeneralMahler.nr_test line 11
  3. lemma OAI.GeneralMahler.rightLayer.std_hb line 15
  4. lemma OAI.GeneralMahler.rightLayer.Qpos_id line 16
  5. def OAI.GeneralMahler.rightLayer.stdL line 19
  6. lemma OAI.GeneralMahler.rightLayer.Ileft line 32
  7. lemma OAI.GeneralMahler.rightLayer.pleft line 45
  8. lemma OAI.GeneralMahler.rightLayer.right_i line 61
  9. lemma OAI.GeneralMahler.rightLayer.pright line 72
  10. lemma OAI.GeneralMahler.rightLayer.Q0_cov line 90
  11. lemma OAI.GeneralMahler.rightLayer.arM line 110
  12. lemma OAI.GeneralMahler.rightLayer.prM line 117
  13. def OAI.GeneralMahler.rightLayer.variationK line 122
  14. lemma OAI.GeneralMahler.rightLayer.varI line 124
  15. lemma OAI.GeneralMahler.rightLayer.Q_var line 128