OAI/Combinatorics/Progressions/Polynomial/RationalPolynomialForecastBoxError.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.tupleResidueReduction line 11
  2. theorem OAI.Erdos3.tupleResidueReduction_surjective line 20
  3. theorem OAI.Erdos3.uniform_residue_reduction_complexMean line 26
  4. def OAI.Erdos3.integerLongPolynomialOutput line 44
  5. theorem OAI.Erdos3.integerLongPolynomialOutput_reduce line 48
  6. theorem OAI.Erdos3.rationalPolynomialForecast_marginal line 65
  7. theorem OAI.Erdos3.rationalInactivePolynomialForecast_marginal line 80
  8. theorem OAI.Erdos3.norm_complexMean_sub_uniform_of_relative_error line 113
  9. theorem OAI.Erdos3.integerBox_residue_test_error line 137
  10. theorem OAI.Erdos3.rationalPolynomialForecast_box_error line 151
  11. theorem OAI.Erdos3.rationalInactivePolynomialForecast_box_error line 183