OAI/NumberTheory/PrimeGaps/OrthantIntegrals.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LargePrimeGaps.integral_eq_orthant_integral line 13
  2. theorem OAI.LargePrimeGaps.l2Mass_eq_orthant_integral line 31
  3. theorem OAI.LargePrimeGaps.deleteCoordinate_eq_orthant_integral line 39
  4. def OAI.LargePrimeGaps.squareDimension line 54
  5. theorem OAI.LargePrimeGaps.squareDimension_pos line 56
  6. theorem OAI.LargePrimeGaps.active_length_le_squareDimension line 60
  7. theorem OAI.LargePrimeGaps.squareDimension_strictMono line 64
  8. theorem OAI.LargePrimeGaps.tendsto_squareDimension line 69
  9. theorem OAI.LargePrimeGaps.tendsto_inverse_squareDimension line 72
  10. theorem OAI.LargePrimeGaps.tendsto_inverse_active_length line 76
  11. theorem OAI.LargePrimeGaps.rectangle_error_tendsto_zero line 80
  12. theorem OAI.LargePrimeGaps.square_ratio_eq_inverse line 85
  13. theorem OAI.LargePrimeGaps.cancellation_bound_tendsto_zero line 92
  14. theorem OAI.LargePrimeGaps.cancellationFamily_W_tendsto line 103
  15. theorem OAI.LargePrimeGaps.cancellationFamily_V_tendsto line 122
  16. def OAI.LargePrimeGaps.AdmissibleFamily line 143
  17. theorem OAI.LargePrimeGaps.exists_canceling_families line 149
  18. theorem OAI.LargePrimeGaps.exists_family_small_marked_ratio line 184
  19. def OAI.LargePrimeGaps.divisorMultiplicity line 201
  20. theorem OAI.LargePrimeGaps.divisorMultiplicity_one line 203
  21. theorem OAI.LargePrimeGaps.divisorMultiplicity_succ line 206
  22. theorem OAI.LargePrimeGaps.divisorMultiplicity_prime line 210
  23. theorem OAI.LargePrimeGaps.divisorMultiplicity_squarefree line 218
  24. theorem OAI.LargePrimeGaps.reciprocal_divisor_sum_le line 227
  25. theorem OAI.LargePrimeGaps.sum_divisorMultiplicity_reciprocal_le line 281
  26. theorem OAI.LargePrimeGaps.squarefree_reciprocal_weight_bound line 300
  27. theorem OAI.LargePrimeGaps.squarefree_totient_lower line 311
  28. theorem OAI.LargePrimeGaps.weighted_error_square_bound line 324
  29. theorem OAI.LargePrimeGaps.markedClassError_trivial line 375
  30. theorem OAI.LargePrimeGaps.markedError_trivial line 418
  31. def OAI.LargePrimeGaps.residueSlice line 437
  32. def OAI.LargePrimeGaps.residuePrefix line 440
  33. theorem OAI.LargePrimeGaps.residuePrefix_sub line 443
  34. theorem OAI.LargePrimeGaps.shifted_sum_eq_residueSlice line 460