OAI/Geometry/Convex/GeneralMahler/Kernel.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Kernel integrations for §04. Plane is Euclidean pair (with product volume), split along diagonal.

  1. def OAI.GeneralMahler.Rlo line 13
  2. lemma OAI.GeneralMahler.Rlo_m line 14
  3. lemma OAI.GeneralMahler.upper1 line 15
  4. lemma OAI.GeneralMahler.upper2 line 24
  5. lemma OAI.GeneralMahler.off_diag line 31
  6. lemma OAI.GeneralMahler.split_plane line 35
  7. lemma OAI.GeneralMahler.real_slice line 56
  8. lemma OAI.GeneralMahler.pairMoment line 69
  9. structure OAI.GeneralMahler.rightLayer line 91

    Source comment

    One-dimensional with right/left densities r=r1 or q0. Base p/a fixed.
    structure rightLayer where
…
  10. def OAI.GeneralMahler.rightLayer.Km line 103
  11. def OAI.GeneralMahler.rightLayer.mrg line 104
  12. lemma OAI.GeneralMahler.rightLayer.p_slice line 106
  13. lemma OAI.GeneralMahler.rightLayer.r_slice line 122
  14. lemma OAI.GeneralMahler.rightLayer.marg line 132
  15. lemma OAI.GeneralMahler.rightLayer.K_pair line 151
  16. def OAI.GeneralMahler.rightLayer.Q line 157
  17. lemma OAI.GeneralMahler.rightLayer.Q_int line 159
  18. lemma OAI.GeneralMahler.rightLayer.Q_split line 164