OAI/Combinatorics/Progressions/Dynamics/AllocatedExternalCandidateSourcePhysicalBudgetBounds.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.candidateSourceBackendPolynomial line 12
  2. theorem OAI.Erdos3.VectorPolynomial.candidateSourceBackendPolynomial_eval line 15
  3. theorem OAI.Erdos3.VectorPolynomial.candidateSourceBackendPolynomial_bounds line 23
  4. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.InnerSourceProfile.physicalBudget line 50
  5. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.InnerSourceProfile.ordinaryBudget line 53
  6. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.InnerSourceProfile.recursiveParameter line 55
  7. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.InnerSourceProfile.separation line 59
  8. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.InnerSourceProfile.physicalBudget_nonneg line 63
  9. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.InnerSourceProfile.ordinaryBudget_nonneg line 67
  10. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.InnerSourceProfile.recursiveParameter_nonneg line 70
  11. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.InnerSourceProfile.physicalBudget_le_recursiveParameter line 76
  12. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.InnerSourceProfile.input_le_physicalBudget line 88
  13. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.InnerSourceProfile.input_le_recursiveParameter line 94
  14. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.InnerSourceProfile.recursiveParameter_polynomial line 97
  15. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.InnerSourceProfile.affine_floor line 101
  16. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.InnerSourceProfile.physicalBudget_bounds line 142
  17. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.InnerSourceProfile.physicalBudget_ge_primitive line 162
  18. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.InnerSourceProfile.affineCenter_le_physicalBudget line 166
  19. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.InnerSourceProfile.affineBudget_le_physicalBudget line 172
  20. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.InnerSourceProfile.affineMassLog_le_ordinaryBudget line 180
  21. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.InnerSourceProfile.factorMass_lower line 200
  22. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.InnerSourceProfile.affineMass_lower line 213
  23. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.InnerSourceProfile.affineFactorMass_lower line 224