OAI/Combinatorics/Progressions/Sampling/ForecastLawCenteredRecoveredKernel.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.centeredTagCoordinates_lipschitz line 57
2. def OAI.Erdos3.VectorPolynomial.centeredTagPullback line 66
3. theorem OAI.Erdos3.VectorPolynomial.centeredTagPullback_lipschitz line 69
4. def OAI.Erdos3.VectorPolynomial.forecastLawCenteredRecoveredKernel line 79
5. theorem OAI.Erdos3.VectorPolynomial.forecastLawCenteredRecoveredKernel_lift_lipschitz line 86
6. theorem OAI.Erdos3.VectorPolynomial.forecastLawCenteredRecoveredKernel_spatial_lipschitz line 100
7. theorem OAI.Erdos3.VectorPolynomial.forecastLawCenteredRecoveredKernel_mem_Icc line 110
8. theorem OAI.Erdos3.VectorPolynomial.forecastLawCenteredRecoveredKernel_recovered_invariant line 119