OAI/NumberTheory/Jacobsthal/Harmonic/AuxiliaryPolynomialLifting.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosAuxiliaryPolynomial.constraintVolume line 13
  2. def OAI.Erdos970.ErdosAuxiliaryPolynomial.logarithmicCost line 16
  3. theorem OAI.Erdos970.ErdosAuxiliaryPolynomial.constraintVolume_pos line 19
  4. theorem OAI.Erdos970.ErdosAuxiliaryPolynomial.constraintVolume_log line 25
  5. theorem OAI.Erdos970.ErdosAuxiliaryPolynomial.dimension_pos line 40
  6. theorem OAI.Erdos970.ErdosAuxiliaryPolynomial.dimension_ratio line 42
  7. theorem OAI.Erdos970.ErdosAuxiliaryPolynomial.exists_small_line_polynomial line 50
  8. def OAI.Erdos970.ErdosAuxiliaryPolynomial.valueBudget line 82
  9. def OAI.Erdos970.ErdosAuxiliaryPolynomial.logarithmicValueBudget line 85
  10. theorem OAI.Erdos970.ErdosAuxiliaryPolynomial.valueBudget_pos line 88
  11. theorem OAI.Erdos970.ErdosAuxiliaryPolynomial.valueBudget_log line 94
  12. theorem OAI.Erdos970.ErdosAuxiliaryPolynomial.prime_product_log line 103
  13. theorem OAI.Erdos970.ErdosAuxiliaryPolynomial.polynomial_log_value_bound line 108
  14. theorem OAI.Erdos970.ErdosAuxiliaryPolynomial.value_zero_of_log_prime_budget line 119
  15. def OAI.Erdos970.ErdosAuxiliaryPolynomial.LineIncidence line 142
  16. theorem OAI.Erdos970.ErdosAuxiliaryPolynomial.exists_auxiliary_polynomial_lifting line 146
  17. theorem OAI.Erdos970.ErdosAuxiliaryPolynomial.logarithmicCost_le_budget line 172