OAI/Combinatorics/Progressions/Sampling/ForecastPhysicalTargetReal.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.forecastDensityPhysicalChartSource_real line 65
2. theorem OAI.Erdos3.VectorPolynomial.forecastDensityPhysicalTarget_real line 70
3. theorem OAI.Erdos3.VectorPolynomial.forecastDensityPhysicalTarget_star line 82
4. theorem OAI.Erdos3.VectorPolynomial.forecastDensityPhysicalTarget_scaled_real line 89
5. theorem OAI.Erdos3.VectorPolynomial.forecastDensityPhysicalTarget_scaled_star line 95
6. theorem OAI.Erdos3.VectorPolynomial.forecastDensityPhysicalChartSource_nonneg line 102
7. theorem OAI.Erdos3.VectorPolynomial.forecastDensityPhysicalTarget_nonneg line 110
8. theorem OAI.Erdos3.VectorPolynomial.forecastDensityPhysicalTarget_scaled_nonneg line 127