OAI/NumberTheory/DirichletL/CubicSieve/RayCoefficients.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SecondPassArithmetic.rayMonoid line 81
  2. def OAI.SecondPassArithmetic.conjugateRayMonoid line 86
  3. theorem OAI.SecondPassArithmetic.rayMonoid_apply line 89
  4. theorem OAI.SecondPassArithmetic.conjugateRayMonoid_apply line 91
  5. theorem OAI.SecondPassArithmetic.columnG_eq_ray_sum line 99
  6. def OAI.SecondPassArithmetic.secondInputCoefficient line 108
  7. theorem OAI.SecondPassArithmetic.secondColumnMinus_ray_expansion line 114
  8. theorem OAI.SecondPassArithmetic.secondColumnPlus_ray_expansion line 128
  9. theorem OAI.SecondPassArithmetic.second_gauss_ray_expansion line 146
  10. abbrev OAI.SecondPassArithmetic.SecondRayIndex line 185
  11. def OAI.SecondPassArithmetic.secondRayCoefficient line 187
  12. def OAI.SecondPassArithmetic.secondRayMinus line 190
  13. def OAI.SecondPassArithmetic.secondRayPlus line 193
  14. def OAI.SecondPassArithmetic.secondActualPair line 201
  15. theorem OAI.SecondPassArithmetic.secondActualPair_eq_separated line 211
  16. def OAI.SecondPassArithmetic.secondTotalWeight line 258
  17. def OAI.SecondPassArithmetic.secondTotalEnergy line 264
  18. theorem OAI.SecondPassArithmetic.secondActualPair_eq_children line 272
  19. theorem OAI.SecondPassArithmetic.weighted_star_cauchy line 287
  20. theorem OAI.SecondPassArithmetic.secondActualPair_norm_le line 295
  21. theorem OAI.SecondPassArithmetic.secondChildColumn_zero_of_overlap line 322
  22. theorem OAI.SecondPassArithmetic.secondChildSum_fixed_pool line 337
  23. theorem OAI.CubicJacobiGlobal.symbol_ne_zero_of_isCoprime line 360
  24. theorem OAI.CubicJacobiGlobal.primary_mul line 384
  25. theorem OAI.CubicJacobiGlobal.primary_add_multiple_three line 389
  26. theorem OAI.CubicJacobiGlobal.kubota_mul_of_isCoprime line 394
  27. lemma OAI.CubicJacobiGlobal.three_dvd_primary_sub_one line 439
  28. theorem OAI.CubicJacobiGlobal.exists_coprime_three_shift line 444
  29. lemma OAI.CubicJacobiGlobal.symbol_three_shift line 490
  30. theorem OAI.CubicJacobiGlobal.kubota_mul line 499
  31. theorem OAI.CubicJacobiGlobal.symbol_cube_of_isCoprime line 538
  32. abbrev OAI.CubicKubota.O line 564
  33. def OAI.CubicKubota.levelThree line 567
  34. lemma OAI.CubicKubota.levelThree_entry line 571
  35. lemma OAI.CubicKubota.levelThree_primary line 582
  36. lemma OAI.CubicKubota.levelThree_upper line 585
  37. lemma OAI.CubicKubota.levelThree_lower line 587
  38. def OAI.CubicKubota.value line 590
  39. theorem OAI.CubicKubota.value_mul line 593
  40. theorem OAI.CubicKubota.value_one line 610
  41. def OAI.CubicKubota.character line 614
  42. theorem OAI.CubicKubota.value_isUnit line 619
  43. theorem OAI.CubicKubota.value_zero_lower_left line 622
  44. theorem OAI.CubicKubota.value_cube line 630
  45. def OAI.CubicKubota.complexCharacter line 638
  46. theorem OAI.CubicKubota.complexCharacter_cube line 641
  47. theorem OAI.CubicKubota.norm_complexCharacter line 645