OAI/Combinatorics/Progressions/Lattices/AllocatedAffinePhysicalTerminalReset.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedCertifiedAffineControlledGlobalTerminal line 15
2. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedCertifiedAffineGlobalPhysicalTerminal line 156
3. def OAI.Erdos3.VectorPolynomial.allocatedEarlyAffineLeftExponent line 310
4. def OAI.Erdos3.VectorPolynomial.allocatedEarlyAffineRightExponent line 313
5. theorem OAI.Erdos3.VectorPolynomial.allocatedEarlyAffine_exponent_bounds line 316
6. structure OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.AffinePhysicalTerminalData line 362
7. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.exists_affinePhysicalTerminalData line 409
8. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.exists_affinePhysicalTerminal_nativeReset_of_zero_restriction line 546
9. def OAI.Erdos3.VectorPolynomial.affineResetNativeBudget line 649
10. theorem OAI.Erdos3.VectorPolynomial.affineResetNativeBudget_bounds line 652
11. theorem OAI.Erdos3.VectorPolynomial.affineResetNativeBudget_exp_bounds line 677
12. def OAI.Erdos3.VectorPolynomial.allocatedAffineResetNativeBudget line 690
13. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineResetNativeBudget_exp_bounds line 693
14. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedAffinePhysicalTerminalReset line 719