OAI/Combinatorics/Progressions/Estimates/ModularMultilinearAmbientSublevel.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.degreeOf_polynomialTranslate_le line 18
  2. theorem OAI.Erdos3.top_coeff_polynomialTranslate line 34
  3. theorem OAI.Erdos3.degreeOf_killCompl_le line 48
  4. def OAI.Erdos3.conditionPolynomial line 58
  5. theorem OAI.Erdos3.degreeOf_conditionPolynomial_le line 62
  6. theorem OAI.Erdos3.coeff_conditionPolynomial_top line 67
  7. theorem OAI.Erdos3.eval_conditionPolynomial line 75
  8. theorem OAI.Erdos3.conditionPolynomial_fullSquarefree line 95
  9. theorem OAI.Erdos3.fullShiftExponent_mapDomain line 108
  10. theorem OAI.Erdos3.expect_eval_conditionPolynomial line 123
  11. theorem OAI.Erdos3.modularPolynomial_zero_reduction line 140
  12. theorem OAI.Erdos3.modularAffine_zero_split line 163
  13. theorem OAI.Erdos3.multiaffine_map line 196
  14. theorem OAI.Erdos3.modularMultilinear_full_sublevel line 204
  15. theorem OAI.Erdos3.modularMultilinear_sublevel line 296
  16. theorem OAI.Erdos3.modularMultilinear_sublevel_of_pos line 320