OAI/NumberTheory/DirichletL/CubicSieve/RayExpansion.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FirstPassCubeLabels.fixedRayExpansion line 83
  2. theorem OAI.FirstPassCubeLabels.fixedRayExpansion_eq_cross line 87
  3. def OAI.FirstPassCubeLabels.cubeMinusCoefficient line 96
  4. def OAI.FirstPassCubeLabels.cubePlusCoefficient line 104
  5. def OAI.FirstPassCubeLabels.idealPairReindex line 112
  6. theorem OAI.FirstPassCubeLabels.threeGaussRowFactor_eq_ray_columns line 129
  7. theorem OAI.FirstPassCubeLabels.sum_threeGaussRowFactor_eq_ideal_rows line 154
  8. theorem OAI.FirstPassCubeLabels.two_variable_radial_separation line 208
  9. def OAI.FirstPassCubeLabels.logTwistMinus line 235
  10. def OAI.FirstPassCubeLabels.logTwistPlus line 239
  11. theorem OAI.FirstPassCubeLabels.threeGaussRowFactor_log_twist line 243
  12. theorem OAI.FirstPassCubeLabels.integrable_log_pair line 256
  13. theorem OAI.FirstPassCubeLabels.smooth_cube_pairs_to_ideal_rows line 262
  14. def OAI.FirstPassCubeLabels.primeProductNorm line 359
  15. theorem OAI.FirstPassCubeLabels.primeProductNorm_pos line 362
  16. theorem OAI.FirstPassCubeLabels.primeProductNorm_union line 366
  17. def OAI.FirstPassCubeLabels.columnLog line 371
  18. def OAI.FirstPassCubeLabels.firstDualScale line 374
  19. theorem OAI.FirstPassCubeLabels.actual_radial_argument line 379
  20. def OAI.FirstPassCubeLabels.normalizedColumn line 394
  21. theorem OAI.FirstPassCubeLabels.threeGaussRowFactor_normalized line 397
  22. theorem OAI.FirstPassCubeLabels.actual_pair_prefactor line 411
  23. theorem OAI.FirstPassCubeLabels.cube_integral_of_radial_separation line 429
  24. theorem OAI.FirstPassCubeLabels.actual_first_kernel_to_ideal_rows line 512
  25. abbrev OAI.QuadraticDivisorSplit.O line 590
  26. theorem OAI.QuadraticDivisorSplit.exists_unique_split line 592
  27. theorem OAI.QuadraticDivisorSplit.split_product_injective line 616
  28. theorem OAI.QuadraticDivisorSplit.divisors_coprime_product line 628
  29. theorem OAI.QuadraticDivisorSplit.sum_divisors_coprime_product line 643
  30. theorem OAI.QuadraticDivisorSplit.residual_norm_le line 660