OAI/Combinatorics/Progressions/Dynamics/AllocatedCommonCoarseBudget.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedCommonRefinedSourceLog line 10
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonRefinedSourceLog_bounds line 15
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonRefinedSourceLog_mono line 33
  4. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedCommonRefinedSourceLog_bound line 49
  5. def OAI.Erdos3.VectorPolynomial.allocatedCommonCoverEarlyLog line 89
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonCoverEarlyLog_bounds line 97
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonCoverEarlyLog_mono line 118
  8. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedCommonCoverEarlyLog_bound line 152
  9. def OAI.Erdos3.VectorPolynomial.coarseProfileConstant line 185
  10. def OAI.Erdos3.VectorPolynomial.allocatedCommonCoarseSourceLog line 187
  11. def OAI.Erdos3.VectorPolynomial.allocatedCommonCoarseMassLog line 192
  12. def OAI.Erdos3.VectorPolynomial.allocatedCommonCoarseMass line 198
  13. def OAI.Erdos3.VectorPolynomial.allocatedCommonCoarseMesh line 204
  14. def OAI.Erdos3.VectorPolynomial.allocatedCoarseSourceEnvelope line 210
  15. def OAI.Erdos3.VectorPolynomial.allocatedCoarseMassEnvelope line 214
  16. def OAI.Erdos3.VectorPolynomial.allocatedCoarseMassBudget line 220
  17. def OAI.Erdos3.VectorPolynomial.allocatedCoarseInputEnvelope line 224
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonCoarseSourceLog_nonneg line 229
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonCoarseEnvelope_bounds line 238
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonCoarseMass_nonneg line 281
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedCoarseMassBudget_nonneg line 287
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedCommonCoarseMass_le_exp line 295