OAI/Combinatorics/Progressions/Probability/EmptyCoefficientDensity.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.canonicalArrayDensity line 17
  2. theorem OAI.Erdos3.canonicalArrayDensity_measurable line 21
  3. theorem OAI.Erdos3.canonicalArrayDensity_recover line 26
  4. theorem OAI.Erdos3.canonicalArrayDensity_recover_unique line 50
  5. theorem OAI.Erdos3.canonicalArrayDensity_apply line 60
  6. theorem OAI.Erdos3.canonicalArrayDensity_nonzero_iff line 70
  7. theorem OAI.Erdos3.canonicalArrayDensity_nonneg line 85
  8. theorem OAI.Erdos3.canonicalArrayDensity_mass line 91
  9. theorem OAI.Erdos3.canonicalArrayDensity_law line 106
  10. abbrev OAI.Erdos3.VectorPolynomial.CoefficientSamplerArrays line 145
  11. def OAI.Erdos3.VectorPolynomial.canonicalCoefficientSample line 150
  12. def OAI.Erdos3.VectorPolynomial.canonicalCoefficientDensity line 158
  13. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientDensity_recover_unique line 162
  14. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientDensity_measurable line 182
  15. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientSample_measurable line 190
  16. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientDensity_nonneg line 200
  17. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientDensity_nonzero_iff line 205
  18. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientDensity_mass line 235
  19. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientLayers_law line 257
  20. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientDensity_law line 280
  21. theorem OAI.Erdos3.canonicalMixedDensity_empty line 309
  22. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientDensity_empty line 339