OAI/NumberTheory/PrimeGaps/WeightMoments.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LargePrimeGaps.weightedBlock_average_limit line 27
  2. theorem OAI.LargePrimeGaps.average_const line 44
  3. theorem OAI.LargePrimeGaps.weightedBlock_zero line 50
  4. theorem OAI.LargePrimeGaps.weightedBlock_average_converges line 61
  5. theorem OAI.LargePrimeGaps.HasBudget.tensor line 89
  6. theorem OAI.LargePrimeGaps.weightedBlock_fourth_converges line 99
  7. theorem OAI.LargePrimeGaps.fourth_power_sum_le line 124
  8. def OAI.LargePrimeGaps.subsetCoefficient line 133
  9. def OAI.LargePrimeGaps.orderedWeight line 136
  10. theorem OAI.LargePrimeGaps.blockOffset_eventually line 141
  11. theorem OAI.LargePrimeGaps.finite_sum_fourth_bound line 146
  12. theorem OAI.LargePrimeGaps.orderedWeight_fourth_bound line 166
  13. def OAI.LargePrimeGaps.matchedPattern line 180
  14. theorem OAI.LargePrimeGaps.matchedPattern_left line 183
  15. theorem OAI.LargePrimeGaps.matchedPattern_right line 190
  16. theorem OAI.LargePrimeGaps.matchedPattern_injective line 197
  17. theorem OAI.LargePrimeGaps.matchedPattern_quotient_card line 208
  18. theorem OAI.LargePrimeGaps.ker_eq_bot_iff_injective line 217
  19. theorem OAI.LargePrimeGaps.numericPattern_left_injective line 229
  20. theorem OAI.LargePrimeGaps.numericPattern_right_injective line 237
  21. theorem OAI.LargePrimeGaps.injective_ranges_card line 245
  22. theorem OAI.LargePrimeGaps.matching_pattern_eq line 251
  23. theorem OAI.LargePrimeGaps.matchedPattern_family line 272
  24. theorem OAI.LargePrimeGaps.sum_matched_patterns line 291
  25. theorem OAI.LargePrimeGaps.realEuclidean_compact line 308
  26. theorem OAI.LargePrimeGaps.realEuclidean_smooth line 313
  27. def OAI.LargePrimeGaps.cumulativePatternKernel line 317
  28. theorem OAI.LargePrimeGaps.cumulative_pair_unmatched line 324
  29. theorem OAI.LargePrimeGaps.cumulative_pair_matched line 357
  30. theorem OAI.LargePrimeGaps.cumulative_square_pattern_sum line 368
  31. theorem OAI.LargePrimeGaps.cumulative_cross_pattern_sum line 406
  32. theorem OAI.LargePrimeGaps.weightedBlock_congr_orthant line 428
  33. theorem OAI.LargePrimeGaps.weightedBlock_cumulative_mul line 436
  34. theorem OAI.LargePrimeGaps.weightedBlock_positive_limit line 454
  35. theorem OAI.LargePrimeGaps.cumulative_pair_limit line 473
  36. theorem OAI.LargePrimeGaps.cumulativeProfile_fin_zero line 499
  37. theorem OAI.LargePrimeGaps.l2Mass_fin_zero line 511