OAI/Geometry/Convex/GeneralMahler/Threshold.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Thresholds of arbitrary moderate-growth random Hermitian fields (in particular A and L) §04.

  1. structure OAI.GeneralMahler.FieldMat line 14
  2. def OAI.GeneralMahler.ProjField.FA line 21
  3. def OAI.GeneralMahler.ProjField.FL line 26
  4. lemma OAI.GeneralMahler.FieldMat.reg line 35
  5. def OAI.GeneralMahler.FieldMat.Fr line 37
  6. lemma OAI.GeneralMahler.FieldMat.Fr_D line 38
  7. lemma OAI.GeneralMahler.FieldMat.fr_m line 39
  8. def OAI.GeneralMahler.FieldMat.ev line 40
  9. lemma OAI.GeneralMahler.FieldMat.ev_m line 41
  10. def OAI.GeneralMahler.FieldMat.eval line 45
  11. lemma OAI.GeneralMahler.FieldMat.evfrm line 46
  12. lemma OAI.GeneralMahler.FieldMat.evfrm' line 49
  13. lemma OAI.GeneralMahler.FieldMat.theta_gen_meas line 52
  14. lemma OAI.GeneralMahler.FieldMat.eval_reg line 62
  15. def OAI.GeneralMahler.FieldMat.Θ line 72
  16. lemma OAI.GeneralMahler.FieldMat.thetaM line 73
  17. lemma OAI.GeneralMahler.FieldMat.theta_nn line 74
  18. lemma OAI.GeneralMahler.FieldMat.theta_le line 78
  19. lemma OAI.GeneralMahler.FieldMat.theta_norm line 82
  20. def OAI.GeneralMahler.FieldMat.QP line 89
  21. lemma OAI.GeneralMahler.FieldMat.theta_exact line 90
  22. lemma OAI.GeneralMahler.FieldMat.qp_mixed line 103
  23. def OAI.GeneralMahler.ProjField.EZ line 113
  24. lemma OAI.GeneralMahler.ProjField.eM line 114
  25. lemma OAI.GeneralMahler.ProjField.eSM line 117
  26. def OAI.GeneralMahler.ProjField.zE line 120
  27. lemma OAI.GeneralMahler.ProjField.zm line 121
  28. lemma OAI.GeneralMahler.ProjField.zSM line 125
  29. lemma OAI.GeneralMahler.ProjField.zi line 127
  30. def OAI.GeneralMahler.ProjField.MB line 131
  31. lemma OAI.GeneralMahler.ProjField.mb_eq line 132