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

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GeneralMahler.Veven line 11
2. lemma OAI.GeneralMahler.trace_star_r line 13
3. lemma OAI.GeneralMahler.pj_cyc3 line 14
4. lemma OAI.GeneralMahler.ipN_ent line 24
5. lemma OAI.GeneralMahler.ipN_comm line 26
6. lemma OAI.GeneralMahler.young_H line 27
7. lemma OAI.GeneralMahler.hsN_mul_bdd line 39
8. lemma OAI.GeneralMahler.log_low line 60

   Source comment

   logarithm bound by derivative sign

   lemma log_low (x:ℝ) (hx:tmin≤x):
       x- Real.log (1+x) ≤ x^2/(2*(1+tmin)) := by
   …

   Mentions: OAI.GeneralMahler.tmin

9. lemma OAI.GeneralMahler.logSigma line 92
10. lemma OAI.GeneralMahler.ProjField.residual_odd line 123
11. lemma OAI.GeneralMahler.ProjField.RoH line 147
12. lemma OAI.GeneralMahler.ProjField.end_cost line 149