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

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Per Gaussian degree proof of the form estimate Eq19.

  1. lemma OAI.GeneralMahler.j_same line 13
  2. lemma OAI.GeneralMahler.pj_positive line 15
  3. lemma OAI.GeneralMahler.p_le_p line 19
  4. lemma OAI.GeneralMahler.p_ladd line 22
  5. lemma OAI.GeneralMahler.p_square_diff line 25
  6. lemma OAI.GeneralMahler.pos_cov line 30
  7. lemma OAI.GeneralMahler.Cf_sym line 32
  8. lemma OAI.GeneralMahler.rho_pos line 37
  9. lemma OAI.GeneralMahler.rho_inv line 39
  10. lemma OAI.GeneralMahler.ProjField.DD_sym line 42
  11. lemma OAI.GeneralMahler.ProjField.r_sym line 47
  12. lemma OAI.GeneralMahler.ProjField.P_mb_sym line 50
  13. lemma OAI.GeneralMahler.ProjField.D_pos line 52
  14. lemma OAI.GeneralMahler.ProjField.pl_scale line 56

    Source comment

    linearity of D in test l
    lemma pl_scale {l} (_hl:TestF l) (a:ℝ) :
    pl (fun t=>a*l t)=fun t=>a*pl l t := by
…

    Mentions: OAI.GeneralMahler.TestF

  15. lemma OAI.GeneralMahler.ProjField.d_cmul line 61
  16. lemma OAI.GeneralMahler.ProjField.fl_s line 64
  17. lemma OAI.GeneralMahler.ProjField.D_s line 69
  18. lemma OAI.GeneralMahler.ProjField.Hd_sub line 77
  19. lemma OAI.GeneralMahler.ProjField.D_sub line 83
  20. lemma OAI.GeneralMahler.ProjField.D_c1 line 94
  21. lemma OAI.GeneralMahler.ProjField.D_F line 114
  22. lemma OAI.GeneralMahler.ProjField.D_e line 120