OAI/Combinatorics/SquareDifference/RootModels.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LiftTheory.SquareDifference.truncatedSieveMean_bound line 17
  2. lemma OAI.LiftTheory.SquareDifference.truncatedSieveMean_complete line 33
  3. lemma OAI.LiftTheory.SquareDifference.localSieveTerm_product line 48
  4. lemma OAI.LiftTheory.SquareDifference.localSieveTerm_zero line 58
  5. lemma OAI.LiftTheory.SquareDifference.quadratic_sieve_bounds line 64
  6. lemma OAI.LiftTheory.SquareDifference.nonprime_sieve_mean_zero line 77
  7. def OAI.LiftTheory.SquareDifference.unitQuadraticMean line 87
  8. lemma OAI.LiftTheory.SquareDifference.prime_unit_quadratic line 90
  9. lemma OAI.LiftTheory.SquareDifference.prime_power_sieved_zero line 117
  10. lemma OAI.LiftTheory.SquareDifference.two_le_rpow_sixth line 137
  11. lemma OAI.LiftTheory.SquareDifference.smallPrime_product_bound line 144
  12. lemma OAI.LiftTheory.SquareDifference.truncatedSieveMean_decay line 171
  13. lemma OAI.LiftTheory.SquareDifference.prime_unit_mean_decay line 191
  14. lemma OAI.LiftTheory.SquareDifference.squareMultiplier_decay line 221
  15. lemma OAI.LiftTheory.SquareDifference.squarePair_tail_bound line 236
  16. abbrev OAI.LiftTheory.SquareDifference.OutsideModulus line 262
  17. def OAI.LiftTheory.SquareDifference.rootCharacter line 264
  18. def OAI.LiftTheory.SquareDifference.outsideCoordinate line 267
  19. lemma OAI.LiftTheory.SquareDifference.prodChar_split line 269
  20. lemma OAI.LiftTheory.SquareDifference.rootCharacter_neg line 276
  21. lemma OAI.LiftTheory.SquareDifference.rootCharacter_diff_cancel line 285
  22. lemma OAI.LiftTheory.SquareDifference.sum_outside_coordinate line 296
  23. def OAI.LiftTheory.SquareDifference.sequenceResidueFourier line 307
  24. lemma OAI.LiftTheory.SquareDifference.sequenceResidueFourier_root line 311
  25. lemma OAI.LiftTheory.SquareDifference.root_model_sum line 331
  26. lemma OAI.SquareDifference.grid_phase_char line 384
  27. lemma OAI.SquareDifference.intervalFourier_grid line 395
  28. lemma OAI.SquareDifference.intervalFourier_neg_grid line 406
  29. lemma OAI.SquareDifference.root_unit_product line 430
  30. lemma OAI.SquareDifference.outside_support_denominator line 446
  31. lemma OAI.SquareDifference.small_outside_support line 469
  32. lemma OAI.SquareDifference.kernelModelCoefficient_root line 480
  33. lemma OAI.SquareDifference.modelBilinear_grid line 512
  34. lemma OAI.SquareDifference.modelBilinear_root line 537