OAI/NumberTheory/Jacobsthal/Estimates/UniformLower.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.EulerWeightedLower.paperWeight line 16
  2. def OAI.Erdos970.EulerWeightedLower.ordinaryProduct line 18
  3. lemma OAI.Erdos970.EulerWeightedLower.eventMass_congr line 21
  4. lemma OAI.Erdos970.EulerWeightedLower.eulerMass_as_weight line 27
  5. theorem OAI.Erdos970.EulerWeightedLower.product_eq_iff_vector line 40
  6. theorem OAI.Erdos970.EulerWeightedLower.upper_integer_mass line 50
  7. theorem OAI.Erdos970.EulerWeightedLower.lower_integer_mass line 78
  8. def OAI.Erdos970.EulerWeightedLower.supportedIntegers line 104
  9. def OAI.Erdos970.EulerWeightedLower.weightedSmallSum line 106
  10. def OAI.Erdos970.EulerWeightedLower.ordinarySmallSum line 108
  11. theorem OAI.Erdos970.EulerWeightedLower.eventMass_finite_values line 111
  12. theorem OAI.Erdos970.EulerWeightedLower.product_mem_supported_iff line 124
  13. theorem OAI.Erdos970.EulerWeightedLower.weightedSmallSum_eq_event line 132
  14. theorem OAI.Erdos970.EulerWeightedLower.ordinarySmallSum_eq_event line 143
  15. theorem OAI.Erdos970.EulerWeightedLower.weightedSmallSum_coupling_lower line 158
  16. theorem OAI.Erdos970.EulerWeightedLower.finite_product_reindex line 179
  17. def OAI.Erdos970.EulerWeightedLower.restrictOutcomes line 194
  18. def OAI.Erdos970.EulerWeightedLower.retainedIndexEquiv line 197
  19. theorem OAI.Erdos970.EulerWeightedLower.eventMass_restrict line 204
  20. theorem OAI.Erdos970.EulerWeightedLower.lowerInteger_restrict_le line 235
  21. theorem OAI.Erdos970.EulerWeightedLower.ordinarySmallSum_antitone line 256
  22. def OAI.Erdos970.EulerWeightedLower.primesThrough line 281
  23. lemma OAI.Erdos970.EulerWeightedLower.primesThrough_prime line 284
  24. lemma OAI.Erdos970.EulerWeightedLower.ordinaryProduct_nonneg line 287
  25. theorem OAI.Erdos970.EulerWeightedLower.supportedIntegers_primesThrough line 293
  26. lemma OAI.Erdos970.EulerWeightedLower.harmonic_real_eq line 302
  27. theorem OAI.Erdos970.EulerWeightedLower.ordinarySmallSum_primesThrough line 306
  28. def OAI.Erdos970.EulerWeightedLower.uniformLowerEnvelope line 310
  29. theorem OAI.Erdos970.EulerWeightedLower.weightedSmallSum_uniform_lower line 314
  30. theorem OAI.Erdos970.EulerWeightedLower.uniformLowerEnvelope_limit line 330
  31. theorem OAI.Erdos970.EulerWeightedLower.weightedSmallSum_eventually_uniform line 349