OAI/Geometry/Convex/GeneralMahler/Budget/Extract.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Frame decomposition of layer functionals.

  1. lemma OAI.GeneralMahler.bjdiag line 11
  2. lemma OAI.GeneralMahler.bjdiag' line 21
  3. lemma OAI.GeneralMahler.Frm.trNL line 27
  4. lemma OAI.GeneralMahler.Frm.pjL line 28
  5. lemma OAI.GeneralMahler.Frm.HL line 32
  6. def OAI.GeneralMahler.ProjField.BL line 39
  7. lemma OAI.GeneralMahler.ProjField.BLe line 48
  8. def OAI.GeneralMahler.ProjField.linW line 53

    Source comment

    densities of β integrals at a fixed x,z
    def linW (f:Plane→ℝ) (u:Plane):=(u.2-u.1)*f u

    Mentions: OAI.GeneralMahler.Plane

  9. def OAI.GeneralMahler.ProjField.bmZ line 54
  10. def OAI.GeneralMahler.ProjField.BB line 56
  11. lemma OAI.GeneralMahler.ProjField.lin_w line 58
  12. lemma OAI.GeneralMahler.ProjField.bmMS line 63
  13. lemma OAI.GeneralMahler.ProjField.bmh line 68
  14. lemma OAI.GeneralMahler.ProjField.bmah line 72
  15. lemma OAI.GeneralMahler.ProjField.bm_trace line 78
  16. lemma OAI.GeneralMahler.ProjField.LL_Bw line 91
  17. lemma OAI.GeneralMahler.ProjField.bm_pos line 100
  18. lemma OAI.GeneralMahler.ProjField.pairing_layer line 112
  19. lemma OAI.GeneralMahler.ProjField.bm_add line 132
  20. lemma OAI.GeneralMahler.ProjField.bm_scale line 136