OAI/Combinatorics/Progressions/Dynamics/AllocatedCandidateStageScalarBudget.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedCandidateStageResetInput line 11
  2. def OAI.Erdos3.VectorPolynomial.allocatedCandidateStageResetLog line 15
  3. def OAI.Erdos3.VectorPolynomial.allocatedCandidateStageLocalInput line 19
  4. def OAI.Erdos3.VectorPolynomial.allocatedCandidateStageSliceLog line 22
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedCandidateStage_reset_lower line 29
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedCandidateStage_reset_bounds line 37
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedCandidateStage_allowance line 45
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedCandidateStage_common_bound line 87
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedCandidateStage_mapSlow_bound line 95
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedCandidateStage_resetLog_nonneg line 104
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedCandidateStage_local_bounds line 110
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedCandidateStage_localSize_bound line 120
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedCandidateStage_localDen_bound line 137
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedCandidateStage_localCost_le_slice line 155
  15. theorem OAI.Erdos3.VectorPolynomial.stageSlice_addition_bounds line 175
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedCandidateStage_slice_bounds line 189
  17. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedCandidateStageSliceLog_budget line 208