OAI/Combinatorics/Progressions/Estimates/DenseProductApproximation.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.nearInteger_mono line 11
  2. theorem OAI.Erdos3.nearInteger_of_pos_density_const line 16
  3. theorem OAI.Erdos3.expect_dependent_fin_cons line 21
  4. theorem OAI.Erdos3.nearIntegerDensity_product_cons line 35
  5. theorem OAI.Erdos3.dense_product_step_tolerance line 59
  6. theorem OAI.Erdos3.dense_product_error_composition line 70
  7. theorem OAI.Erdos3.exists_common_rational_approximations line 88
  8. theorem OAI.Erdos3.sum_dependent_fin_cons line 126
  9. theorem OAI.Erdos3.dependent_fin_cons_map line 138
  10. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_const line 146
  11. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_pi_fin_cons line 151
  12. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_empty_tuple line 163
  13. theorem OAI.Erdos3.dense_product_fiber line 183
  14. theorem OAI.Erdos3.independent_rational_frequencies line 239
  15. theorem OAI.Erdos3.exists_common_rational_approximations_varying line 278
  16. theorem OAI.Erdos3.dense_product_approximation line 315