OAI/Combinatorics/Progressions/Estimates/AllocatedPlateauSiteApproximation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.allocatedNaturalGridSpectrum_character line 37
2. theorem OAI.Erdos3.VectorPolynomial.allocatedConstantPlateauApproximation_expansion line 63
3. theorem OAI.Erdos3.VectorPolynomial.allocatedNaturalGridSpectrum_modes line 119
4. def OAI.Erdos3.VectorPolynomial.allocatedPlateauModeModel line 146
5. theorem OAI.Erdos3.VectorPolynomial.allocatedPlateauModeModel_grid_value line 154
6. theorem OAI.Erdos3.VectorPolynomial.allocatedPlateauModeModel_norm line 168
7. theorem OAI.Erdos3.VectorPolynomial.allocatedPlateauModeModel_lipschitz line 194
8. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_physical_site_approximation line 264