OAI/NumberTheory/Jacobsthal/Sieve/AdmittedExponentMarginal.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.NumberTheoryLean.HarmonicExponentMeasure.nextExponent_measurable line 18
  2. theorem OAI.Erdos970.NumberTheoryLean.HarmonicExponentMeasure.exponent_image_Ici line 21
  3. theorem OAI.Erdos970.NumberTheoryLean.HarmonicExponentMeasure.nextExponent_injOn line 39
  4. theorem OAI.Erdos970.NumberTheoryLean.HarmonicExponentMeasure.harmonic_lintegral_substitution line 45
  5. def OAI.Erdos970.NumberTheoryLean.HarmonicExponentMeasure.ratioMeasure line 67
  6. def OAI.Erdos970.NumberTheoryLean.HarmonicExponentMeasure.exponentMeasure line 70
  7. theorem OAI.Erdos970.NumberTheoryLean.HarmonicExponentMeasure.ratioMeasure_map line 73
  8. def OAI.Erdos970.NumberTheoryLean.HarmonicExponentMeasure.inverseRatio line 85
  9. theorem OAI.Erdos970.NumberTheoryLean.HarmonicExponentMeasure.inverseRatio_measurable line 87
  10. theorem OAI.Erdos970.NumberTheoryLean.HarmonicExponentMeasure.inverse_lintegral_substitution line 90
  11. theorem OAI.Erdos970.NumberTheoryLean.HarmonicExponentMeasure.exponentMeasure_map line 103
  12. theorem OAI.Erdos970.NumberTheoryLean.HarmonicExponentMeasure.ratioMeasure_map_update line 115
  13. theorem OAI.Erdos970.NumberTheoryLean.HarmonicExponentMeasure.accepted_exponent_measure line 122
  14. theorem OAI.Erdos970.NumberTheoryLean.HarmonicExponentRows.exponentMeasure_restrict line 153
  15. theorem OAI.Erdos970.NumberTheoryLean.HarmonicExponentRows.exponentMeasure_ae_interval line 165
  16. theorem OAI.Erdos970.NumberTheoryLean.HarmonicExponentRows.accepted_update_measure line 173
  17. theorem OAI.Erdos970.NumberTheoryLean.HarmonicExponentRows.harmonic_even_ratioMeasure line 191
  18. theorem OAI.Erdos970.NumberTheoryLean.HarmonicExponentRows.harmonic_odd_ratioMeasure line 198
  19. theorem OAI.Erdos970.NumberTheoryLean.HarmonicExponentRows.evenUpdate_exponent line 205
  20. theorem OAI.Erdos970.NumberTheoryLean.HarmonicExponentRows.oddUpdate_exponent line 214
  21. theorem OAI.Erdos970.NumberTheoryLean.HarmonicExponentRows.admitted_even_exponent_row line 223
  22. theorem OAI.Erdos970.NumberTheoryLean.HarmonicExponentRows.admitted_odd_exponent_row line 236
  23. theorem OAI.Erdos970.NumberTheoryLean.AdmittedExponentMarginal.inverse_update_marginal line 263
  24. theorem OAI.Erdos970.NumberTheoryLean.AdmittedExponentMarginal.admitted_even_exponent_marginal line 283
  25. theorem OAI.Erdos970.NumberTheoryLean.AdmittedExponentMarginal.admitted_odd_exponent_marginal line 293
  26. theorem OAI.Erdos970.NumberTheoryLean.AdmittedExponentMarginal.harmonic_cutoff_mono line 303
  27. theorem OAI.Erdos970.NumberTheoryLean.AdmittedExponentMarginal.admitted_exponent_marginal_le line 318