OAI/Geometry/Convex/GeneralMahler/Segment/Small.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GeneralMahler.SCal.SE.wp line 12
2. def OAI.GeneralMahler.SCal.SE.ubase line 13
3. def OAI.GeneralMahler.SCal.SE.qsmall line 14
4. lemma OAI.GeneralMahler.SCal.SE.wp_pos line 15
5. lemma OAI.GeneralMahler.SCal.SE.omega_pos line 16
6. lemma OAI.GeneralMahler.SCal.SE.ubP line 18
7. lemma OAI.GeneralMahler.SCal.SE.sfL line 20
8. lemma OAI.GeneralMahler.SCal.SE.smallD line 38
9. lemma OAI.GeneralMahler.SCal.SE.shr16 line 70

   Source comment

   exact relaxed constants for W and cosh/s

   lemma shr16 (hh:0<h)(he:h≤16/100):
       shv h ≤ 10044/10000 ∧ cosh h ≤ 1014/1000:= by
   …

   Mentions: OAI.GeneralMahler.SCal.SE.shv

10. lemma OAI.GeneralMahler.SCal.SE.mean_beta2 line 81
11. lemma OAI.GeneralMahler.SCal.SE.mean_beta4 line 83
12. lemma OAI.GeneralMahler.SCal.SE.Wshr line 86
13. lemma OAI.GeneralMahler.SCal.SE.mβ line 101