OAI/NumberTheory/DirichletL/CubicSieve/DivisorTargets.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SecondPassArithmetic.parity_pair_norm_bounds line 82
  2. lemma OAI.SecondPassArithmetic.parity_pair_fiber_count line 98
  3. theorem OAI.SecondPassArithmetic.parity_ideal_pair_count line 122
  4. theorem OAI.SecondPassArithmetic.cubeParityKey_norm_product line 170
  5. theorem OAI.SecondPassArithmetic.cubeParityKey_active_bound line 180
  6. theorem OAI.SecondPassArithmetic.cube_coordinates_parity_count line 194
  7. theorem OAI.SecondPassArithmetic.parity_ideal_pair_inverse_sqrt_sum line 280
  8. theorem OAI.SecondPassArithmetic.cube_coordinates_inverse_active_sum line 319
  9. theorem OAI.SecondPassArithmetic.globalFirst_diagonal_scalar line 426
  10. def OAI.SecondPassArithmetic.globalFirstCountKey line 494
  11. def OAI.SecondPassArithmetic.globalFirstDivisorTarget line 497
  12. theorem OAI.SecondPassArithmetic.globalFirstDivisorTarget_ne_zero line 500
  13. theorem OAI.SecondPassArithmetic.globalFirst_divisor_dvd_target line 505
  14. theorem OAI.SecondPassArithmetic.globalFirst_divisor_fiber_card line 513
  15. theorem OAI.SecondPassArithmetic.globalFirstDivisorTarget_norm_bound line 532
  16. theorem OAI.SecondPassArithmetic.primeSupport_inverse_sum line 543
  17. theorem OAI.SecondPassArithmetic.globalFirstData_harmonic_sum line 562