OAI/Combinatorics/Progressions/Dynamics/PreparedRelativeEndpointComparisonBudget.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointTestLog line 9
  2. def OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointComparisonLog line 12
  3. theorem OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointTestLog_nonneg line 17
  4. theorem OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointTestLog_local line 22
  5. theorem OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointTestLog_native line 26
  6. theorem OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointComparisonLog_nonneg line 30
  7. theorem OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointComparisonLog_test_precision line 40
  8. theorem OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointComparisonLog_model_precision line 48
  9. theorem OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointComparisonLog_forecast_accuracy line 64
  10. theorem OAI.Erdos3.VectorPolynomial.exists_preparedRelativeEndpointComparisonLog_budget line 74
  11. def OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointSourceLog line 104
  12. def OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointCoarseLog line 107
  13. def OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointSigmaLog line 110
  14. theorem OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointSourceLog_nonneg line 116
  15. theorem OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointCoarseLog_nonneg line 121
  16. theorem OAI.Erdos3.VectorPolynomial.preparedRelativeEndpointSigmaLog_nonneg line 128
  17. theorem OAI.Erdos3.VectorPolynomial.exists_preparedRelativeEndpointPerturbationLog_budget line 135