OAI/NumberTheory/DirichletL/CubicSieve/DualZeroMode.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.FirstPassCubeLabels.threeGaussRowFactor_empty line 87
  2. lemma OAI.SecondPassArithmetic.canonicalCubeResidual_empty line 114
  3. def OAI.SecondPassArithmetic.canonicalCubeDualZero line 121
  4. theorem OAI.SecondPassArithmetic.canonicalCubeDualZero_eq_density line 134
  5. theorem OAI.SecondPassArithmetic.canonicalCubeDualZero_norm_le line 163
  6. theorem OAI.SecondPassArithmetic.boundedPrimeSupports_card_positive line 203
  7. theorem OAI.FirstPassCubeLabels.actualFirstKernel_complement_eq_pairs line 232
  8. theorem OAI.FirstPassCubeLabels.full_uniform_actualFirstKernel_disk_remainder line 259
  9. theorem OAI.SecondPassArithmetic.canonicalCubeDualZero_support line 407
  10. theorem OAI.SecondPassArithmetic.canonicalCubeDualZero_fixed_bound line 423
  11. theorem OAI.SecondPassArithmetic.canonicalCubeZero_common_sum_bound line 439
  12. theorem OAI.SecondPassArithmetic.full_uniform_canonicalFirstZero_bound line 493
  13. lemma OAI.SecondPassArithmetic.originalLabelColumn_core_norm_le line 563
  14. lemma OAI.SecondPassArithmetic.originalLabelColumn_core_test_ne_zero line 586
  15. theorem OAI.SecondPassArithmetic.canonicalFirstFrequencyRadius_eq_global line 597
  16. theorem OAI.SecondPassArithmetic.full_uniform_canonicalSource_kernel_tail line 624