OAI/Combinatorics/Progressions/Sampling/ForecastLawPhysicalTargetReal.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.forecastLawDensityPhysicalChartSource_real line 65
2. theorem OAI.Erdos3.VectorPolynomial.forecastLawDensityPhysicalTarget_real line 70
3. theorem OAI.Erdos3.VectorPolynomial.forecastLawDensityPhysicalTarget_star line 82
4. theorem OAI.Erdos3.VectorPolynomial.forecastLawDensityPhysicalTarget_scaled_real line 89
5. theorem OAI.Erdos3.VectorPolynomial.forecastLawDensityPhysicalTarget_scaled_star line 95
6. theorem OAI.Erdos3.VectorPolynomial.forecastLawDensityPhysicalChartSource_nonneg line 102
7. theorem OAI.Erdos3.VectorPolynomial.forecastLawDensityPhysicalTarget_nonneg line 110
8. theorem OAI.Erdos3.VectorPolynomial.forecastLawDensityPhysicalTarget_scaled_nonneg line 127