OAI/NumberTheory/PrimeGaps/EqualityPatterns.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LargePrimeGaps.index_density_from_weight_estimates line 27
  2. def OAI.LargePrimeGaps.PatternMaps line 68
  3. def OAI.LargePrimeGaps.patternLift line 71
  4. theorem OAI.LargePrimeGaps.patternLift_mk line 78
  5. theorem OAI.LargePrimeGaps.patternLift_injective line 81
  6. theorem OAI.LargePrimeGaps.patternLift_map_injective line 91
  7. def OAI.LargePrimeGaps.patternClass line 98
  8. theorem OAI.LargePrimeGaps.mem_patternClass line 101
  9. theorem OAI.LargePrimeGaps.patternClass_card_le line 105
  10. theorem OAI.LargePrimeGaps.patternClass_pairwise_disjoint line 118
  11. instance OAI.LargePrimeGaps.finiteSetoidFintype line 126
  12. theorem OAI.LargePrimeGaps.sum_patterns line 129
  13. theorem OAI.LargePrimeGaps.fiberSubsetFamily_image_eq_of_kernel line 136
  14. theorem OAI.LargePrimeGaps.append_fiber_card line 146
  15. theorem OAI.LargePrimeGaps.append_fiber_card_le_two line 152
  16. theorem OAI.LargePrimeGaps.append_left_singleton line 167
  17. theorem OAI.LargePrimeGaps.append_right_singleton line 187
  18. theorem OAI.LargePrimeGaps.cumulative_tensor_unmatched_kernel_zero line 207
  19. theorem OAI.LargePrimeGaps.duplicateLabels_image line 237
  20. theorem OAI.LargePrimeGaps.duplicate_shiftFamily line 243
  21. def OAI.LargePrimeGaps.patternEmbedding line 260
  22. def OAI.LargePrimeGaps.embeddingPattern line 263
  23. def OAI.LargePrimeGaps.patternEquivEmbedding line 270
  24. def OAI.LargePrimeGaps.patternClassEquiv line 280
  25. theorem OAI.LargePrimeGaps.patternClass_sum_norm_le line 284
  26. theorem OAI.LargePrimeGaps.patternClass_scaled_sum_norm_le line 294
  27. theorem OAI.LargePrimeGaps.pattern_errors_tendsto_zero line 314
  28. theorem OAI.LargePrimeGaps.all_pattern_errors_tendsto_zero line 334
  29. theorem OAI.LargePrimeGaps.blockLength_ratio_tendsto line 348
  30. theorem OAI.LargePrimeGaps.blockLength_tendsto line 368
  31. theorem OAI.LargePrimeGaps.blockLength_densityCutoff_eventually line 372
  32. theorem OAI.LargePrimeGaps.uniform_singularBoxMean_tendsto line 383
  33. theorem OAI.LargePrimeGaps.constant_boxDiameterBound line 393
  34. theorem OAI.LargePrimeGaps.quotient_ker_card line 402
  35. def OAI.LargePrimeGaps.numericPattern line 419
  36. theorem OAI.LargePrimeGaps.numericPattern_ker line 422
  37. theorem OAI.LargePrimeGaps.constant_boxTuple_injective_iff line 430
  38. def OAI.LargePrimeGaps.patternTupleEquiv line 442
  39. theorem OAI.LargePrimeGaps.patternTupleEquiv_apply line 452
  40. theorem OAI.LargePrimeGaps.patternTupleEquiv_image line 458