OAI/Combinatorics/Progressions/Probability/LocalLayerOneSiteLaw.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_local_subspace_density line 16
  2. def OAI.Erdos3.VectorPolynomial.oneSiteCoefficientSample line 71
  3. theorem OAI.Erdos3.VectorPolynomial.oneSiteCoefficientSample_eq line 78
  4. theorem OAI.Erdos3.VectorPolynomial.oneSiteCoefficientSample_measurable line 91
  5. theorem OAI.Erdos3.VectorPolynomial.oneSiteCoefficientSample_image line 97
  6. theorem OAI.Erdos3.VectorPolynomial.oneSiteCoefficientSample_image_le line 110
  7. theorem OAI.Erdos3.VectorPolynomial.oneSiteCoefficientSample_mixed_center line 122
  8. def OAI.Erdos3.VectorPolynomial.layerOneSiteSample line 159
  9. theorem OAI.Erdos3.VectorPolynomial.layerOneSiteSample_eq line 165
  10. theorem OAI.Erdos3.VectorPolynomial.layerOneSiteSample_image_le line 181
  11. theorem OAI.Erdos3.VectorPolynomial.layerOneSiteSample_mixed_center line 192
  12. theorem OAI.Erdos3.VectorPolynomial.exists_local_one_site_coefficient_law line 227
  13. theorem OAI.Erdos3.VectorPolynomial.exists_local_layer_one_site_law line 275