OAI/Combinatorics/Progressions/Dynamics/PreparedFiniteNestedFrontNativeBudget.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.FrontSourceProfile.familyCap line 34
2. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.FrontSourceProfile.familyParameter line 39
3. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.FrontSourceProfile.familyCap_bounds line 41
4. structure OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.FrontSourceProfile.FamilyBudget line 61
5. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.FrontSourceProfile.familyBudget line 75
6. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.FrontSourceProfile.frontModelBudget line 121
7. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.FrontSourceProfile.frontTermLog line 124
8. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.FrontSourceProfile.frontCorrelationLoss line 127
9. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.FrontSourceProfile.frontRawMassLoss line 132
10. structure OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.FrontSourceProfile.LossBudget line 137
11. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.FrontSourceProfile.lossBudget line 152
12. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.FrontSourceProfile.primitiveFrontLoss_bounds line 179
13. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.FrontSourceProfile.exp_neg_familyParameter_le_rawMassLoss line 192
14. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.FrontSourceProfile.exp_neg_familyParameter_le_correlationLoss line 196
15. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteForwardFrontFamilyScalar_budget line 210
16. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteForwardFrontFamily_budget line 247
17. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteForwardFrontFamily_polynomial_later_work_budget line 285
18. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.FrontSourceProfile.geometryBudget line 342
19. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.FrontSourceProfile.factorBudget line 347
20. structure OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.FrontSourceProfile.FactorGeometryBudget line 351
21. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.FrontSourceProfile.factorGeometryBudget line 370
22. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteNestedSourceNative_front_mem line 409
23. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteNestedFrontFamily_polynomial_next_seed line 439