OAI/Combinatorics/Progressions/Estimates/AllocatedFrozenPrefixStageData.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedCandidateStageBaseExponent line 11
  2. def OAI.Erdos3.VectorPolynomial.allocatedCandidateStageSliceExponent line 15
  3. def OAI.Erdos3.VectorPolynomial.allocatedCandidateStageBase line 19
  4. def OAI.Erdos3.VectorPolynomial.allocatedCandidateStageSlice line 23
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedCandidateStageBaseExponent_bounds line 27
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedCandidateStageBase_bounds line 38
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedCandidateStage_primitive_le_base line 50
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedCandidateStage_control_le_base line 62
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedCandidateStageSlice_bounds line 71
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedCandidateStageBase_le_forwardWork line 79
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedCandidateStageSlice_forward_bounds line 95
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedCandidateStage_cost_lt_slice line 119
  13. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.exists_axisFreezing_of_side_bounds line 164
  14. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.exists_forward_axisFreezing line 181
  15. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.historyStageData_of_prefix_bounds line 257
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedCandidateStage_keep_subset_initialLong line 365
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedCandidateStage_canonical_masks line 382
  18. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.expLongAxes_subset_keep line 442
  19. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.exists_common_scalar_long_axis line 450
  20. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.expLongAxes_nonempty line 460
  21. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.AxisFreezing.historyStageData_of_original_factors line 526