OAI/Combinatorics/Progressions/Probability/AllocatedFixedPathSlicedRationalDensityComparison.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPath_sliced_density_residue_comparison line 38
2. def OAI.Erdos3.VectorPolynomial.allocatedFixedPathSlicedForecastDensity line 223
3. def OAI.Erdos3.VectorPolynomial.allocatedFixedPathSlicedRationalFiniteMean line 233
4. def OAI.Erdos3.VectorPolynomial.allocatedFixedPathSlicedRationalReferenceMean line 252
5. def OAI.Erdos3.VectorPolynomial.allocatedFixedPathSlicedResidueReferenceMean line 269
6. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPathSlicedResidueReferenceMean_eq line 284
7. def OAI.Erdos3.VectorPolynomial.allocatedFixedPathSlicedComparisonError line 297
8. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPath_sliced_finite_reference_comparison line 308
9. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPath_sliced_rational_density_comparison line 330