OAI/NumberTheory/Jacobsthal/Estimates/ProductRestriction.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Erdos970.EulerWeightedLower.hasSum_mul_nonneg line 13
  2. theorem OAI.Erdos970.EulerWeightedLower.hasSum_fin_product line 19
  3. theorem OAI.Erdos970.EulerWeightedLower.hasSum_finite_product line 40
  4. theorem OAI.Erdos970.EulerWeightedLower.product_coordinate_hasSum line 57
  5. abbrev OAI.Erdos970.EulerWeightedLower.Outcomes line 81
  6. def OAI.Erdos970.EulerWeightedLower.productMass line 82
  7. def OAI.Erdos970.EulerWeightedLower.excessLog line 84
  8. def OAI.Erdos970.EulerWeightedLower.eventMass line 86
  9. lemma OAI.Erdos970.EulerWeightedLower.productMass_nonneg line 92
  10. theorem OAI.Erdos970.EulerWeightedLower.productMass_hasSum line 97
  11. lemma OAI.Erdos970.EulerWeightedLower.product_event_summable line 104
  12. lemma OAI.Erdos970.EulerWeightedLower.excessLog_nonneg line 110
  13. theorem OAI.Erdos970.EulerWeightedLower.product_excess_hasSum line 115
  14. theorem OAI.Erdos970.EulerWeightedLower.product_excess_mean_le line 139
  15. theorem OAI.Erdos970.EulerWeightedLower.excess_tail_le line 144
  16. theorem OAI.Erdos970.EulerWeightedLower.finite_product_restrict line 166