OAI/Combinatorics/SquareDifference/PrimaryKernel.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SquareDifference.prime_power_sieved_zero line 10
  2. lemma OAI.SquareDifference.two_le_rpow_sixth line 30
  3. lemma OAI.SquareDifference.smallPrime_product_bound line 37
  4. lemma OAI.SquareDifference.truncatedSieveMean_decay line 64
  5. lemma OAI.SquareDifference.truncatedSieveMean_restrict line 78
  6. lemma OAI.SquareDifference.product_sieve_coefficient line 108
  7. lemma OAI.SquareDifference.localSieveTerm_factor line 138
  8. lemma OAI.SquareDifference.truncatedSieveMean_factor line 160
  9. lemma OAI.SquareDifference.truncatedSieveMean_congr_active line 184
  10. lemma OAI.SquareDifference.residueDensity_nonneg line 201
  11. lemma OAI.SquareDifference.residueDensity_quadratic_norm line 204
  12. lemma OAI.SquareDifference.smallPrime_product_bound_inj line 215
  13. lemma OAI.SquareDifference.truncatedSieveMean_decay_inj line 249
  14. def OAI.SquareDifference.rootSieveA line 271
  15. def OAI.SquareDifference.rootSieveB line 275
  16. lemma OAI.SquareDifference.rootSieveA_trivial line 279
  17. lemma OAI.SquareDifference.rootSieveB_trivial line 286
  18. lemma OAI.SquareDifference.rootSieveA_root_bound line 293
  19. lemma OAI.SquareDifference.rootSieveB_root line 297
  20. lemma OAI.SquareDifference.rootSieve_factor line 300
  21. lemma OAI.SquareDifference.rootSieve_decay line 317
  22. lemma OAI.SquareDifference.residueDensity_quadratic_zero_dvd line 341
  23. lemma OAI.SquareDifference.odd_prime_power_root_zero line 352
  24. lemma OAI.SquareDifference.odd_root_quadratic_large_dvd line 359
  25. lemma OAI.SquareDifference.two_prime_power_root_zero line 373
  26. lemma OAI.SquareDifference.two_prime_power_root_small line 379
  27. lemma OAI.SquareDifference.prime_power_sieved_zero_dvd line 387
  28. lemma OAI.SquareDifference.prime_power_sieve_complete_zero line 398
  29. lemma OAI.SquareDifference.residueDensity_quadratic_phase line 405
  30. lemma OAI.SquareDifference.prime_unit_quadratic_of_eq line 417
  31. lemma OAI.SquareDifference.rootSieve_complete line 434
  32. lemma OAI.SquareDifference.rootSieve_complete_phase line 444
  33. lemma OAI.SquareDifference.rootSieve_zero_of_root line 461
  34. lemma OAI.SquareDifference.rootSieve_zero_of_squarefactor line 469
  35. lemma OAI.SquareDifference.zmod_equiv_coordinate line 481
  36. lemma OAI.SquareDifference.coordinateChar_inflation_primitive line 488