OAI/Combinatorics/Progressions/Estimates/PreparedCanonicalRelativeEndpointBounds.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.RankPreparationFamily.pad_rank_sum line 16
2. theorem OAI.Erdos3.RankPreparationFamily.PreparedHeights.padded_preparation_data line 20
3. theorem OAI.Erdos3.RankPreparationFamily.PreparedHeights.exists_padded_early_late_sampler_geometry line 36
4. def OAI.Erdos3.preparedRelativeLateHeight line 75
5. theorem OAI.Erdos3.preparedRelative_padded_input line 79
6. def OAI.Erdos3.VectorPolynomial.preparedFiniteNestedSourceRequiredLog line 142
7. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteNestedSourceRequiredLog_power_budget line 201
8. def OAI.Erdos3.VectorPolynomial.preparedCanonicalRelativeSourceRequired line 238
9. structure OAI.Erdos3.VectorPolynomial.PreparedCanonicalRelativeScalarInputs line 254
10. theorem OAI.Erdos3.VectorPolynomial.preparedCanonicalRelative_scalarInputs line 279
11. theorem OAI.Erdos3.VectorPolynomial.preparedCanonicalRelativeSourceRequired_physicalSize line 330
12. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteNestedCanonicalRequired_power_budget line 355
13. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteNestedCanonicalRequired_power_budget_of_inputPower line 414
14. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteNestedSourceProjectionPrecision_endpoint_le line 479
15. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteNestedSourceRequiredLog_endpoint_le line 491
16. theorem OAI.Erdos3.VectorPolynomial.preparedCanonicalRelativeSourceRequired_endpoint_le line 504
17. theorem OAI.Erdos3.VectorPolynomial.preparedCanonicalRelativeProjection_endpoint_le line 518