OAI/Combinatorics/Progressions/Sampling/AllocatedExternalCandidateForecastComparisonSource.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion.forecast_noise_mem line 138
2. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion.forecast_base_mem line 146
3. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion.forecast_density_ne_zero line 153
4. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion.forecast_sample_eq line 164
5. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion.forecast_read_eq line 170
6. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion.denseSliceInput_physical_complexMean line 177
7. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion.forecast_source_facts line 190
8. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Conclusion.forecastFiber_ambient_bounded_original_twist_precision line 210