OAI/Combinatorics/Progressions/Sampling/AllocatedOriginalSampleForecastMeasurable.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.canonicalZeroSpatialJointDensity_measurable line 12
2. theorem OAI.Erdos3.binaryDensity_measurable_family line 29
3. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPathPrincipal_measurable_family line 48
4. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPathShift_measurable_family line 59
5. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPathLiftDensity_measurable_family line 69
6. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPathForecastDensity_measurable_family line 87
7. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleLiftDensity_measurable line 134
8. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleForecastDensity_measurable line 144
9. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleNormalizedForecast_measurable line 153