OAI/NumberTheory/DirichletL/CubicSieve/CrossFactorization.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FirstPassCubeLabels.blockCross_union_left line 79
  2. def OAI.FirstPassCubeLabels.threeBlockExponent line 86
  3. theorem OAI.FirstPassCubeLabels.gaussBlock_three_cube_partition line 91
  4. theorem OAI.FirstPassCubeLabels.canonicalProductGauss_three_cube_partition line 147
  5. theorem OAI.FirstPassCubeLabels.gaussBlock_eq_mobius_converted line 182
  6. theorem OAI.FirstPassCubeLabels.a_weighted_three_cube_gauss line 213
  7. theorem OAI.QuadraticGaussRay.quadraticRayValue_square line 267
  8. theorem OAI.QuadraticGaussRay.quadraticRayValue_same_residue_product line 289
  9. abbrev OAI.QuadraticMainBoundaryFibers.O line 298
  10. def OAI.QuadraticMainBoundaryFibers.productIdeal line 301
  11. theorem OAI.QuadraticMainBoundaryFibers.product_fiber_card_le line 303
  12. theorem OAI.QuadraticMainBoundaryFibers.product_fiber_small_power line 326
  13. def OAI.QuadraticMainBoundaryFibers.boundaryCoefficient line 347
  14. theorem OAI.QuadraticMainBoundaryFibers.norm_cutoffDifference_le line 352
  15. theorem OAI.QuadraticMainBoundaryFibers.boundaryCoefficient_norm_le_card line 357
  16. theorem OAI.QuadraticMainBoundaryFibers.boundaryCoefficient_small_power line 373
  17. theorem OAI.QuadraticMainBoundaryFibers.boundaryCoefficient_eq_zero_below line 381
  18. theorem OAI.CoprimeSieveOperator.square_norm_sum line 399
  19. theorem OAI.CoprimeSieveOperator.disjoint_gram_expansion line 405
  20. theorem OAI.CoprimeSieveOperator.masked_coefficient_energy line 446
  21. theorem OAI.CoprimeSieveOperator.weighted_energy_bound line 463
  22. theorem OAI.CoprimeSieveOperator.coprime_gram_operator_bound line 480
  23. abbrev OAI.IdealCoprimeSieveOperator.O line 523
  24. theorem OAI.IdealCoprimeSieveOperator.primeSupport_disjoint_iff line 527
  25. def OAI.IdealCoprimeSieveOperator.supportConstant line 545
  26. theorem OAI.IdealCoprimeSieveOperator.supportConstant_pos line 548
  27. theorem OAI.IdealCoprimeSieveOperator.support_card_bound line 551
  28. theorem OAI.IdealCoprimeSieveOperator.ideal_coprime_gram_operator_bound line 555
  29. theorem OAI.IdealCoprimeSieveOperator.actual_quadratic_coprime_gram_bound line 586
  30. abbrev OAI.QuadraticMainOperatorBound.O line 607
  31. def OAI.QuadraticMainOperatorBound.mainWeight line 610
  32. theorem OAI.QuadraticMainOperatorBound.mainWeight_eq_zero_of_row_gt line 613
  33. theorem OAI.QuadraticMainOperatorBound.mainWeight_norm_le line 620
  34. theorem OAI.QuadraticMainOperatorBound.main_difference_operator_bound line 633
  35. theorem OAI.QuadraticMainOperatorBound.ideal_quadraticRow_norm_le_one line 700
  36. theorem OAI.QuadraticMainOperatorBound.actual_quadratic_main_difference_bound line 710