OAI/Combinatorics/Progressions/Dynamics/AllocatedMixedSiteBudget.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedMixedPointCapLog line 9
  2. def OAI.Erdos3.VectorPolynomial.allocatedMixedSiteOutputLog line 12
  3. def OAI.Erdos3.VectorPolynomial.allocatedMixedAccuracyLog line 15
  4. def OAI.Erdos3.VectorPolynomial.allocatedMixedJointSiteLog line 18
  5. def OAI.Erdos3.VectorPolynomial.allocatedMixedJointPrimitiveLog line 21
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedMixedPointCapLog_bounds line 24
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedMixedSiteOutputLog_bounds line 34
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedMixedJointLogs_nonneg line 44
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedActiveSiteOutputLog_eval line 54
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedInactiveSiteOutputLog_eval line 67
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedMixedPointCapLog_eval line 81
  12. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedMixedJointPrimitiveLog_bound line 96