OAI/Combinatorics/Progressions/Sampling/NormalizedTwistRationalForecast.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.frozenAmbientCoefficientLip line 11
2. def OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.frozenAmbientObservable line 19
3. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.frozenAmbientObservable_lipschitz line 25
4. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.norm_frozenAmbientObservable_le line 32
5. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.frozenAmbientObservable_sample line 39
6. theorem OAI.Erdos3.VectorPolynomial.exists_normalizedTwist_frozen_cover_sampling line 61
7. def OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.vertexResidue line 112
8. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.selected_frozenSpatialEval_eq line 117
9. theorem OAI.Erdos3.VectorPolynomial.exists_normalizedTwist_residue_frozen_sampling line 149
10. def OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.frozenHaarReference line 206
11. theorem OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.norm_frozenHaarReference_le line 216
12. def OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.frozenResidueSamplerMean line 227
13. def OAI.Erdos3.VectorPolynomial.NormalizedPolynomialTwist.residueSamplerMean line 238
14. theorem OAI.Erdos3.VectorPolynomial.rational_forecast_sample_error line 250
15. structure OAI.Erdos3.VectorPolynomial.FrozenSamplerComparison line 288
16. theorem OAI.Erdos3.VectorPolynomial.exists_normalizedTwist_frozen_samplerComparison line 304
17. theorem OAI.Erdos3.VectorPolynomial.FrozenSamplerComparison.rational_forecast line 342
18. theorem OAI.Erdos3.VectorPolynomial.FrozenSamplerComparison.rational_forecast_eval line 378