OAI/Combinatorics/Progressions/Lattices/AffineCoefficientCoverTilt.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_integer_cover_threshold line 16
  2. theorem OAI.Erdos3.VectorPolynomial.affineSampleCoefficientArray_smul line 40
  3. def OAI.Erdos3.VectorPolynomial.affineCoefficientCoverSample line 54
  4. theorem OAI.Erdos3.VectorPolynomial.affineCoefficientCoverSample_eq_scaled line 60
  5. theorem OAI.Erdos3.VectorPolynomial.affineCoefficientCoverSample_projection line 70
  6. theorem OAI.Erdos3.VectorPolynomial.exists_affine_coefficient_haar_comparison line 92
  7. theorem OAI.Erdos3.VectorPolynomial.exists_affine_coefficient_haar_approximation line 144
  8. theorem OAI.Erdos3.VectorPolynomial.exists_affine_coefficient_cover_haar_approximation line 213
  9. theorem OAI.Erdos3.VectorPolynomial.exists_affine_coefficient_density_mass line 281
  10. theorem OAI.Erdos3.VectorPolynomial.exists_affine_coefficient_cover_tilted_family_comparison line 340
  11. theorem OAI.Erdos3.VectorPolynomial.exists_affine_coefficient_tilted_comparison line 433
  12. theorem OAI.Erdos3.VectorPolynomial.exists_affine_coefficient_cover_tilted_comparison line 525