OAI/NumberTheory/Jacobsthal/Sieve/CoprimePositionSieve.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosVarianceMoments.divisorJoint line 14
  2. def OAI.Erdos970.ErdosVarianceMoments.coprimeJoint line 18
  3. theorem OAI.Erdos970.ErdosVarianceMoments.jointCondition_coordinates line 23
  4. theorem OAI.Erdos970.ErdosVarianceMoments.divisorJoint_card line 29
  5. theorem OAI.Erdos970.ErdosVarianceMoments.divisorJoint_card_real line 51
  6. theorem OAI.Erdos970.ErdosVarianceMoments.conditional_pattern_card line 59
  7. def OAI.Erdos970.ErdosVarianceMoments.patternPrimeUnit line 82
  8. theorem OAI.Erdos970.ErdosVarianceMoments.patternPrimeUnit_coe line 86
  9. theorem OAI.Erdos970.ErdosVarianceMoments.unit_mul_eq_iff line 95
  10. def OAI.Erdos970.ErdosVarianceMoments.coprimeCoefficientUnit line 104
  11. def OAI.Erdos970.ErdosVarianceMoments.coprimeShiftUnit line 109
  12. def OAI.Erdos970.ErdosVarianceMoments.coprimeForbidden line 112
  13. theorem OAI.Erdos970.ErdosVarianceMoments.mem_coprimeForbidden line 118
  14. theorem OAI.Erdos970.ErdosVarianceMoments.coprimeForbidden_card line 138
  15. def OAI.Erdos970.ErdosVarianceMoments.coprimeForbiddenFamily line 153
  16. theorem OAI.Erdos970.ErdosVarianceMoments.coprimeForbiddenFamily_card line 158
  17. theorem OAI.Erdos970.ErdosVarianceMoments.coprimeJoint_avoidance line 164
  18. theorem OAI.Erdos970.ErdosVarianceMoments.nonzero_positionDensity_two line 176
  19. def OAI.Erdos970.ErdosVarianceMoments.coprimePositionSurvivors line 188
  20. theorem OAI.Erdos970.ErdosVarianceMoments.coprimePositionSurvivors_sieve_sum line 192
  21. theorem OAI.Erdos970.ErdosVarianceMoments.coprimePositionSurvivors_estimate line 205