OAI/Combinatorics/Progressions/Estimates/CoefficientDeckImageCongruence.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.uniformPMF_pi_map line 15
  2. theorem OAI.Erdos3.uniformPMF_map_coordinates line 38
  3. theorem OAI.Erdos3.uniformPMF_transposed_images line 50
  4. theorem OAI.Erdos3.uniformPMF_product_image line 72
  5. theorem OAI.Erdos3.boundedCoefficientJetMatrix_mulVec line 93
  6. theorem OAI.Erdos3.boundedCoefficientJetMatrix_range line 102
  7. theorem OAI.Erdos3.boundedCoefficientJetMatrix_multiplier line 120
  8. theorem OAI.Erdos3.boundedCoefficientJetMatrix_mask line 130
  9. theorem OAI.Erdos3.boundedCoefficientJetMatrix_index_le line 137
  10. theorem OAI.Erdos3.boundedCoefficientJetMatrix_residue_iff line 148
  11. def OAI.Erdos3.VectorPolynomial.canonicalCoefficientDeckSample line 186
  12. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientDeckSample_coordinate line 192
  13. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientDeckSample_projection line 205
  14. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientDeckSample_measurable line 215
  15. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientDeckSample_relabel line 222
  16. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientDeckSample_law line 259
  17. def OAI.Erdos3.VectorPolynomial.coefficientDeckJetMap line 303
  18. theorem OAI.Erdos3.VectorPolynomial.coefficientDeckJetMap_coordinate line 314
  19. theorem OAI.Erdos3.VectorPolynomial.coefficientDeckKernel_jets line 324
  20. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientDeckSample_jets line 346
  21. theorem OAI.Erdos3.VectorPolynomial.coefficientDeckJetMap_joint_mask line 373
  22. theorem OAI.Erdos3.VectorPolynomial.coefficientDeckJetMap_commonPeriod_mask line 404
  23. theorem OAI.Erdos3.VectorPolynomial.coefficientDeckJetMap_independent_source line 423
  24. theorem OAI.Erdos3.VectorPolynomial.coefficientDeckJetMap_mem_range_iff line 446
  25. theorem OAI.Erdos3.VectorPolynomial.coefficientDeckJetMap_range_eq_of_integer_range_eq line 464
  26. theorem OAI.Erdos3.VectorPolynomial.coefficientDeckJetMap_law_eq_of_integer_range_eq line 479