OAI/NumberTheory/DirichletL/CubicSieve/ArithmeticBins.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SecondPassArithmetic.globalArithmeticBin line 88
  2. def OAI.SecondPassArithmetic.globalSquarefreeBin line 92
  3. def OAI.SecondPassArithmetic.globalArithmeticTargets line 96
  4. theorem OAI.SecondPassArithmetic.globalArithmeticTargets_squarefree line 101
  5. theorem OAI.SecondPassArithmetic.globalArithmeticTargets_bounds line 109
  6. def OAI.SecondPassArithmetic.globalBinZ line 125
  7. def OAI.SecondPassArithmetic.globalBinUd line 129
  8. def OAI.SecondPassArithmetic.globalBinUe line 132
  9. def OAI.SecondPassArithmetic.globalBinUv line 135
  10. def OAI.SecondPassArithmetic.globalBinKap line 138
  11. def OAI.SecondPassArithmetic.globalBinRadial line 141
  12. theorem OAI.SecondPassArithmetic.globalBinRadial_pos line 144
  13. def OAI.SecondPassArithmetic.globalArithmeticBinSource line 154
  14. theorem OAI.SecondPassArithmetic.globalArithmeticBinSource_squarefree line 164
  15. theorem OAI.SecondPassArithmetic.globalArithmeticBin_transfer line 188
  16. def OAI.SecondPassArithmetic.fixedDepthRank line 246
  17. theorem OAI.SecondPassArithmetic.fixedDepthRank_initial line 248
  18. theorem OAI.SecondPassArithmetic.fixedDepthRank_step line 259
  19. theorem OAI.SecondPassArithmetic.fixedDepthRank_path line 277
  20. theorem OAI.SecondPassArithmetic.globalPooledDelta_pos line 297
  21. theorem OAI.SecondPassArithmetic.globalPooledDelta_ge line 303
  22. theorem OAI.SecondPassArithmetic.globalPooledNaturalRow_pos line 313
  23. theorem OAI.SecondPassArithmetic.globalPooledNaturalRow_bound line 319
  24. theorem OAI.SecondPassArithmetic.globalPooledRow_contraction line 329
  25. theorem OAI.SecondPassArithmetic.globalPooled_J_bound line 350
  26. theorem OAI.SecondPassArithmetic.globalActualBin_fixed_depth line 361
  27. def OAI.CanonicalQuadraticSieve.activeGcdColumns line 393
  28. def OAI.CanonicalQuadraticSieve.activeGcdCoefficient line 397
  29. theorem OAI.CanonicalQuadraticSieve.originalHigh_gcd_eq_maskedPoissonDifference line 400
  30. theorem OAI.CanonicalQuadraticSieve.annularRayGcdBlock_eq_active_difference line 415
  31. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.annular_small_gcd_complete line 438
  32. def OAI.CanonicalQuadraticSieve.selectedPoissonT line 470
  33. def OAI.CanonicalQuadraticSieve.selectedPoissonK line 471
  34. theorem OAI.CanonicalQuadraticSieve.selectedPoisson_bounds line 473
  35. theorem OAI.CanonicalQuadraticSieve.selectedPoisson_radial_identity line 499
  36. theorem OAI.CanonicalQuadraticSieve.cutoff_middle_identity line 506
  37. theorem OAI.CanonicalQuadraticSieve.selectedPoisson_middle_bound line 525
  38. abbrev OAI.CubicEisenstein.EuclideanSpatial line 569
  39. def OAI.CubicEisenstein.euclideanUpperHalf line 571
  40. def OAI.CubicEisenstein.hyperbolicDensity line 572
  41. def OAI.CubicEisenstein.hyperbolicEuclideanVolume line 574
  42. lemma OAI.CubicEisenstein.euclideanUpperHalf_measurable line 577
  43. lemma OAI.CubicEisenstein.hyperbolicDensity_measurable line 580
  44. lemma OAI.CubicEisenstein.hyperbolic_volume_map_of_jacobian line 584
  45. def OAI.CubicEisenstein.euclideanInversion line 612
  46. def OAI.CubicEisenstein.euclideanInversionDeriv line 614
  47. lemma OAI.CubicEisenstein.euclideanInversion_apply line 617
  48. lemma OAI.CubicEisenstein.euclideanInversion_measurable line 621
  49. lemma OAI.CubicEisenstein.euclideanUpperHalf_ne_zero line 625
  50. lemma OAI.CubicEisenstein.euclideanInversion_mem line 629
  51. lemma OAI.CubicEisenstein.euclideanInversion_image line 635
  52. lemma OAI.CubicEisenstein.euclideanInversion_hasFDerivAt line 643
  53. lemma OAI.CubicEisenstein.euclideanInversion_abs_det line 648
  54. lemma OAI.CubicEisenstein.euclideanInversion_jacobian_density line 658
  55. theorem OAI.CubicEisenstein.euclideanInversion_preserves_hyperbolicVolume line 667