OAI/Combinatorics/Progressions/Probability/AllocatedFixedPositiveDensity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.canonicalMixedDensity_continuous_of_ambient line 18
2. theorem OAI.Erdos3.canonicalMixedDensity_continuous line 41
3. theorem OAI.Erdos3.canonicalArrayDensity_continuous line 57
4. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientDensity_continuous line 79
5. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientDensity_continuous line 133
6. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientDensity_bounds line 144
7. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientDensity_positive_spec line 163
8. theorem OAI.Erdos3.BooleanCubeKernel.exists_allocated_covered_euclidean_density line 189
9. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientDensity_fixedScale_le_exp line 282
10. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_fixed_positive_density line 313