OAI/Combinatorics/Progressions/Geometry/AllocatedProductChartRadius.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.finiteRowChartRadius_support_le_inv line 9
2. def OAI.Erdos3.VectorPolynomial.allocatedProductChartLog line 20
3. theorem OAI.Erdos3.VectorPolynomial.allocatedProductChartLog_bounds line 23
4. theorem OAI.Erdos3.VectorPolynomial.allocatedProductChartLog_mono line 42
5. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedProductChartLog_bound line 48
6. def OAI.Erdos3.VectorPolynomial.allocatedProductChartRadius line 60
7. theorem OAI.Erdos3.VectorPolynomial.allocatedProductChartRadius_bounds line 63
8. theorem OAI.Erdos3.VectorPolynomial.allocatedProductIdealSiteRadius_exp_bound line 97
9. theorem OAI.Erdos3.VectorPolynomial.allocatedProductGridRadius_inv_exp_bound line 130
10. theorem OAI.Erdos3.VectorPolynomial.allocatedProductChartRadius_le_charts line 157
11. theorem OAI.Erdos3.VectorPolynomial.allocatedProductChartRadius_recovery_budget line 184