OAI/Combinatorics/Progressions/Probability/CanonicalCoverLaw.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.coefficientCover_measurePreserving line 17
  2. theorem OAI.Erdos3.VectorPolynomial.coefficientCover_integrable line 33
  3. theorem OAI.Erdos3.VectorPolynomial.coefficientCover_integral line 43
  4. instance OAI.Erdos3.subspaceArrayIntegerLattice_closed line 67
  5. def OAI.Erdos3.euclideanSubspaceTorusMeasurableEquiv line 84
  6. def OAI.Erdos3.euclideanSubspaceTorusMeasure line 96
  7. theorem OAI.Erdos3.euclideanSubspaceTorusMeasure_probability line 99
  8. theorem OAI.Erdos3.euclideanSubspaceTorusMeasure_invariant line 104
  9. theorem OAI.Erdos3.euclideanSubspaceTorusMeasure_mass line 109
  10. theorem OAI.Erdos3.VectorPolynomial.coefficientCover_density_integral line 136
  11. theorem OAI.Erdos3.VectorPolynomial.coefficientCover_density_sample line 148
  12. theorem OAI.Erdos3.VectorPolynomial.coefficientCover_density_approximation line 156
  13. theorem OAI.Erdos3.VectorPolynomial.exists_covered_coefficient_density line 178
  14. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientCoverLaw line 282