OAI/Combinatorics/Progressions/Dynamics/CandidatePhysicalOrdinaryBudget.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.allocatedCandidateTerminalFullInput line 10
2. theorem OAI.Erdos3.VectorPolynomial.terminal_affine_budget_arithmetic line 16
3. theorem OAI.Erdos3.VectorPolynomial.terminal_affine_budget_bounds line 21
4. theorem OAI.Erdos3.VectorPolynomial.allocatedCandidateTerminalFullInput_bounds line 29
5. theorem OAI.Erdos3.VectorPolynomial.allocatedCandidateTerminalFullInput_denominator_bound line 51
6. theorem OAI.Erdos3.VectorPolynomial.terminal_mass_budget_bound line 61
7. theorem OAI.Erdos3.VectorPolynomial.actualCandidateSlowProjectionMassBudget_terminal_bound line 101
8. theorem OAI.Erdos3.VectorPolynomial.allocatedCandidateTerminalFullInput_mass_bound line 135
9. def OAI.Erdos3.VectorPolynomial.candidatePhysicalOrdinaryBudget line 157
10. theorem OAI.Erdos3.VectorPolynomial.candidatePhysicalOrdinaryBudget_bounds line 160
11. theorem OAI.Erdos3.VectorPolynomial.candidatePhysicalOrdinaryBudget_observable line 180
12. theorem OAI.Erdos3.VectorPolynomial.certifiedAffine_budget_lower_arithmetic line 188
13. theorem OAI.Erdos3.VectorPolynomial.certifiedAffineCenterBudget_primitive_bounds line 201
14. theorem OAI.Erdos3.VectorPolynomial.candidatePhysicalOrdinaryBudget_mass line 207
15. theorem OAI.Erdos3.VectorPolynomial.candidatePhysicalOrdinaryBudget_separation line 227