OAI/Geometry/HeilbronnTriangle/ParameterSequence.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Problem355.Parameters.PrimeParameterData line 11
  2. lemma OAI.Problem355.Parameters.exists_primeParameterData line 28
  3. def OAI.Problem355.Parameters.PrimeParameterData.h line 39
  4. def OAI.Problem355.Parameters.PrimeParameterData.M line 40
  5. def OAI.Problem355.Parameters.PrimeParameterData.N line 41
  6. def OAI.Problem355.Parameters.PrimeParameterData.tau line 42
  7. lemma OAI.Problem355.Parameters.PrimeParameterData.r_pos line 45
  8. lemma OAI.Problem355.Parameters.PrimeParameterData.base_ge_three line 50
  9. lemma OAI.Problem355.Parameters.PrimeParameterData.base_le_h line 62
  10. lemma OAI.Problem355.Parameters.PrimeParameterData.h_ge_three line 66
  11. lemma OAI.Problem355.Parameters.PrimeParameterData.h_le_M line 68
  12. lemma OAI.Problem355.Parameters.PrimeParameterData.r_le_M line 72
  13. lemma OAI.Problem355.Parameters.PrimeParameterData.M_pos line 85
  14. lemma OAI.Problem355.Parameters.PrimeParameterData.M_le_N line 87
  15. lemma OAI.Problem355.Parameters.PrimeParameterData.N_pos line 91
  16. lemma OAI.Problem355.Parameters.PrimeParameterData.tau_pos line 93
  17. lemma OAI.Problem355.Parameters.PrimeParameterData.twice_tau_lt_h line 95
  18. lemma OAI.Problem355.Parameters.PrimeParameterData.tau_lt_h line 98
  19. lemma OAI.Problem355.Parameters.PrimeParameterData.tau_le_cube line 102
  20. lemma OAI.Problem355.Parameters.PrimeParameterData.box_polynomial line 110
  21. lemma OAI.Problem355.Parameters.PrimeParameterData.ratio_polynomial line 113
  22. lemma OAI.Problem355.Parameters.PrimeParameterData.ratio_degree_thirty line 119
  23. lemma OAI.Problem355.Parameters.PrimeParameterData.modulus_degree_thirty line 129
  24. lemma OAI.Problem355.Parameters.PrimeParameterData.base_lower_original line 137
  25. lemma OAI.Problem355.Parameters.PrimeParameterData.tau_lt_q line 140
  26. lemma OAI.Problem355.Parameters.PrimeParameterData.alphabet_lt_base line 148
  27. lemma OAI.Problem355.Parameters.PrimeParameterData.digit_moment_bound line 156
  28. lemma OAI.Problem355.Parameters.PrimeParameterData.real_bounds line 161
  29. lemma OAI.Problem355.Parameters.exists_parameter_sequence line 174
  30. lemma OAI.Problem355.Parameters.exists_heilbronn_parameter_sequence line 191