OAI/Geometry/Convex/GeneralMahler/Packet.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Fixed profiles supplementing Profile.d,v,g, exact constants and layered profiles.

  1. def OAI.GeneralMahler.Profile.bb line 10
  2. def OAI.GeneralMahler.Profile.cc line 11
  3. def OAI.GeneralMahler.Profile.r line 12
  4. def OAI.GeneralMahler.Profile.omegaP line 13
  5. def OAI.GeneralMahler.Profile.sb line 14
  6. def OAI.GeneralMahler.Profile.eta line 15
  7. def OAI.GeneralMahler.Profile.kk line 16
  8. def OAI.GeneralMahler.Profile.kar line 17
  9. def OAI.GeneralMahler.Profile.ar line 18
  10. def OAI.GeneralMahler.Profile.tc line 19
  11. def OAI.GeneralMahler.Profile.tr line 20
  12. def OAI.GeneralMahler.Profile.bm line 21
  13. def OAI.GeneralMahler.Profile.eâ‚€ line 22
  14. def OAI.GeneralMahler.Profile.alpha line 23
  15. def OAI.GeneralMahler.Profile.hâ‚€ line 24
  16. def OAI.GeneralMahler.Profile.rad line 26
  17. def OAI.GeneralMahler.Profile.qu line 27
  18. def OAI.GeneralMahler.Profile.angle line 28
  19. def OAI.GeneralMahler.Profile.uc line 29
  20. def OAI.GeneralMahler.Profile.us line 30
  21. def OAI.GeneralMahler.Profile.FF line 31
  22. def OAI.GeneralMahler.Profile.Cp line 32
  23. def OAI.GeneralMahler.Profile.Kp line 33
  24. def OAI.GeneralMahler.Profile.HH line 35
  25. def OAI.GeneralMahler.Profile.Hh line 37
  26. lemma OAI.GeneralMahler.Profile.k_pos line 39
  27. lemma OAI.GeneralMahler.Profile.k_sq line 40
  28. lemma OAI.GeneralMahler.Profile.u_eq line 41
  29. structure OAI.GeneralMahler.Profile.LayerOK line 50

    Source comment

    Properties proved later in the scalar estimates and used in abstract layer lemmas
    structure LayerOK : Prop where
…
  30. lemma OAI.GeneralMahler.Profile.LayerOK.f_test line 66
  31. lemma OAI.GeneralMahler.Profile.LayerOK.fN line 67