OAI/Geometry/Convex/GeneralMahler/Qprimitive.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Eq13 mixed derivative kernel, proof via rectangle cumulative representation of a(min)B(max).

  1. lemma OAI.GeneralMahler.rightLayer.B_c line 14
  2. lemma OAI.GeneralMahler.rightLayer.K_c line 16
  3. lemma OAI.GeneralMahler.rightLayer.K_nn line 18
  4. def OAI.GeneralMahler.rightLayer.Kab line 20
  5. def OAI.GeneralMahler.rightLayer.Rect line 22
  6. lemma OAI.GeneralMahler.rightLayer.rcompact line 23
  7. lemma OAI.GeneralMahler.rightLayer.concat_m line 24
  8. def OAI.GeneralMahler.rightLayer.RectF line 33
  9. lemma OAI.GeneralMahler.rightLayer.rect_slice_i line 34
  10. lemma OAI.GeneralMahler.rightLayer.Rect_bound line 42
  11. lemma OAI.GeneralMahler.rightLayer.length_rect line 46
  12. lemma OAI.GeneralMahler.rightLayer.Rect_int line 56
  13. lemma OAI.GeneralMahler.rightLayer.slice_rect_a line 95
  14. lemma OAI.GeneralMahler.rightLayer.Kab_I line 119
  15. lemma OAI.GeneralMahler.rightLayer.R_reverse line 123
  16. lemma OAI.GeneralMahler.rightLayer.mrgMul line 131
  17. lemma OAI.GeneralMahler.rightLayer.R_identity line 138