OAI/NumberTheory/Jacobsthal/Estimates/DisjointBlockExpansion.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.blockChoices line 15
  2. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.mem_blockChoices line 20
  3. def OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.selectedUnion line 26
  4. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.selectedUnion_subset line 30
  5. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.selectedUnion_inter_block line 38
  6. def OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.intersectionChoices line 57
  7. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.intersectionChoices_mem line 60
  8. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.selectedUnion_intersectionChoices line 66
  9. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.sum_subsets_product line 79
  10. def OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.truncatedCoefficient line 103
  11. def OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.layerCoefficient line 106
  12. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.truncatedCoefficient_sum line 109
  13. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.truncatedCoefficient_evaluation line 145
  14. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.layerCoefficient_evaluation line 150
  15. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.intersectionValue_eq_product line 163
  16. def OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.globalCoefficient line 188
  17. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.globalCoefficient_evaluation line 192
  18. def OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.upperCoefficient line 208
  19. def OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.correctionCoefficient line 212
  20. def OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.lowerCoefficient line 218
  21. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.upperCoefficient_evaluation line 222
  22. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.correctionCoefficient_evaluation line 233
  23. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.lowerCoefficient_evaluation line 254
  24. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.truncatedCoefficient_ne_zero_iff line 269
  25. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.layerCoefficient_ne_zero_iff line 274
  26. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.truncatedCoefficient_abs_le line 279
  27. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.layerCoefficient_abs_le line 284
  28. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.globalCoefficient_abs_le line 289
  29. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.upperCoefficient_abs_le line 297
  30. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.correctionCoefficient_abs_le line 301
  31. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.correctionCoefficient_own_card line 309
  32. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.correctionCoefficient_other_card line 316
  33. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.correctionCoefficient_disjoint line 323
  34. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.upperCoefficient_zero_of_correction line 332
  35. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.lowerCoefficient_abs_le line 340
  36. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.prod_inter_blocks line 360
  37. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.globalCoefficient_density line 374
  38. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.upperCoefficient_density line 388
  39. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.weighted_coefficient_expansion line 397
  40. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.global_main_remainder line 410
  41. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.supported_remainder_bound line 421
  42. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.weighted_global_coefficient_bounds line 442
  43. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.layerCoefficient_density line 457
  44. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.correctionCoefficient_density line 468
  45. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.lowerCoefficient_density line 487
  46. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.upperCoefficient_card line 502
  47. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.lowerCoefficient_card line 508
  48. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.prime_product_support line 530
  49. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.lowerCoefficient_prime_support line 552
  50. theorem OAI.Erdos970.NumberTheoryLean.DisjointBlockExpansion.prime_product_injective line 562