OAI/Combinatorics/Progressions/Linear/PreparedFiniteNestedSourceProjectionBudget.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardFrontProjectionPrecision line 10
  2. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardFrontProjectionPrecision_nonneg line 13
  3. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteForwardFrontProjectionPrecision_budget line 21
  4. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteForwardFrontProjection_budget line 43
  5. def OAI.Erdos3.VectorPolynomial.preparedFiniteForwardFrontProjectionExponent line 70
  6. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardFrontProjectionExponent_two_le line 73
  7. def OAI.Erdos3.VectorPolynomial.preparedFiniteScheduleLocalDegreeRequired line 87
  8. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteScheduleRequiredRank_power_budget line 97
  9. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteScheduleUniformRequiredRank_power_budget line 172
  10. def OAI.Erdos3.VectorPolynomial.preparedConditionalExcessRequired line 222
  11. theorem OAI.Erdos3.VectorPolynomial.preparedConditionalExcessRequired_le_preparedFiniteScheduleLocalDegreeRequired line 226
  12. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteScheduleConditionalExcess_exp_le line 234
  13. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteScheduleConditionalExcess_size_rank line 246
  14. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteScheduleConditionalExcess_power_budget line 263
  15. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteScheduleUniformConditionalExcess_power_budget line 292
  16. def OAI.Erdos3.VectorPolynomial.preparedNestedFrontProjectionEnvelope line 325
  17. theorem OAI.Erdos3.VectorPolynomial.exists_preparedNestedFrontProjectionEnvelope_budget line 335
  18. def OAI.Erdos3.VectorPolynomial.preparedFiniteNestedSourceProjectionPrecision line 434
  19. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteNestedSourceProjection_budget line 445