OAI/Combinatorics/Progressions/Lattices/AffineCoefficientSubspace.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.integerContractedRow line 13
  2. theorem OAI.Erdos3.VectorPolynomial.integerContractedRow_cast line 17
  3. theorem OAI.Erdos3.VectorPolynomial.integerContractedRow_coefficientFunctional line 34
  4. theorem OAI.Erdos3.BooleanCubeKernel.integer_cube_root_bound line 52
  5. theorem OAI.Erdos3.BooleanCubeKernel.integer_cube_difference_bound line 59
  6. theorem OAI.Erdos3.BooleanCubeKernel.integerCubeWitnessBound_le_polynomial line 80
  7. theorem OAI.Erdos3.BooleanCubeKernel.exists_bounded_integer_mode_witness line 128
  8. theorem OAI.Erdos3.rowPolynomial_homogeneous line 171
  9. theorem OAI.Erdos3.VectorPolynomial.integerContractedRow_apply line 175
  10. theorem OAI.Erdos3.BooleanCubeKernel.exists_bounded_integer_mode_rows line 186
  11. def OAI.Erdos3.VectorPolynomial.affineParameterSubstitution line 236
  12. theorem OAI.Erdos3.VectorPolynomial.dehomogenize_rowPolynomial line 240
  13. theorem OAI.Erdos3.VectorPolynomial.affineParameterSubstitution_degree line 245
  14. theorem OAI.Erdos3.VectorPolynomial.affineParameterSubstitution_eval line 250
  15. def OAI.Erdos3.VectorPolynomial.affineModeLift line 257
  16. theorem OAI.Erdos3.VectorPolynomial.affineModeLift_substitute line 261
  17. theorem OAI.Erdos3.VectorPolynomial.coefficientModePolynomial_affine_eval line 271
  18. theorem OAI.Erdos3.VectorPolynomial.coefficientModePolynomial_degreeLE line 279
  19. theorem OAI.Erdos3.VectorPolynomial.rowPolynomial_integer_site line 305
  20. theorem OAI.Erdos3.VectorPolynomial.exists_absorbed_integer_site_tests line 319
  21. def OAI.Erdos3.BooleanCubeKernel.cubeModePolynomialBudget line 359
  22. theorem OAI.Erdos3.BooleanCubeKernel.integerCubeWitnessBound_le_vertex_budget line 362
  23. theorem OAI.Erdos3.BooleanCubeKernel.exists_vertex_bounded_integer_mode line 368
  24. theorem OAI.Erdos3.VectorPolynomial.degreeLE_dehomogenize line 405
  25. theorem OAI.Erdos3.VectorPolynomial.affineModeLift_factorization_iff line 413
  26. theorem OAI.Erdos3.VectorPolynomial.affineModeLift_exists_factorization_iff line 429
  27. theorem OAI.Erdos3.VectorPolynomial.exists_highest_affine_nonfactor line 438
  28. theorem OAI.Erdos3.VectorPolynomial.exists_absorbed_affine_site_tests line 466
  29. def OAI.Erdos3.FiniteSitePhaseRemoval line 500
  30. theorem OAI.Erdos3.finiteSitePhaseRemoval_of_annihilates line 510
  31. theorem OAI.Erdos3.BooleanCubeKernel.exists_vertex_mode_with_phase_removal line 520
  32. theorem OAI.Erdos3.VectorPolynomial.affineModeLift_comp_map line 554
  33. theorem OAI.Erdos3.VectorPolynomial.exists_highest_affine_subspace_nonfactor line 562