OAI/Geometry/Convex/GeneralMahler/DefectLayer.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

μ functionals and integrable density algebra for Section §03-04.

  1. lemma OAI.GeneralMahler.rapid.rfadd line 15
  2. lemma OAI.GeneralMahler.rapid.rfneg line 22
  3. lemma OAI.GeneralMahler.rapid.rfsub line 23
  4. lemma OAI.GeneralMahler.poly_st line 26
  5. lemma OAI.GeneralMahler.poly_p line 27
  6. lemma OAI.GeneralMahler.rapid_half_a line 29
  7. lemma OAI.GeneralMahler.rapid_ar line 37
  8. def OAI.GeneralMahler.MomentF line 46

    Source comment

    integrable densities with polynomial weights
    def MomentF (f:ℝ→ℝ) :=
…
  9. lemma OAI.GeneralMahler.MomentF.of_rapid line 50
  10. lemma OAI.GeneralMahler.MomentF.inte line 52
  11. lemma OAI.GeneralMahler.MomentF.add line 53
  12. lemma OAI.GeneralMahler.MomentF.neg line 56
  13. lemma OAI.GeneralMahler.MomentF.sub line 59
  14. lemma OAI.GeneralMahler.MomentF.mul line 60
  15. lemma OAI.GeneralMahler.MomentF.mono line 63
  16. def OAI.GeneralMahler.ProjField.dB line 74

    Source comment

    deltas
    def dB (x:ℝ) := q.Bt x-q.s0*a (-x)
  17. def OAI.GeneralMahler.ProjField.dr line 75
  18. def OAI.GeneralMahler.ProjField.hDel line 76
  19. def OAI.GeneralMahler.ProjField.dm line 77
  20. def OAI.GeneralMahler.ProjField.delt line 78
  21. lemma OAI.GeneralMahler.ProjField.Bt_poly line 81
  22. lemma OAI.GeneralMahler.ProjField.B_tail line 89
  23. lemma OAI.GeneralMahler.ProjField.dB_poly line 127
  24. lemma OAI.GeneralMahler.ProjField.dB_tail line 130
  25. lemma OAI.GeneralMahler.ProjField.pB_tail line 133
  26. lemma OAI.GeneralMahler.ProjField.aB_tail line 136
  27. lemma OAI.GeneralMahler.ProjField.hd_tail line 139
  28. lemma OAI.GeneralMahler.ProjField.moment_w line 143
  29. lemma OAI.GeneralMahler.ProjField.ar_moment line 152
  30. lemma OAI.GeneralMahler.ProjField.a0_id line 157
  31. lemma OAI.GeneralMahler.ProjField.arDelta_moment line 159
  32. lemma OAI.GeneralMahler.ProjField.prDelta_moment line 168