OAI/NumberTheory/DirichletL/CubicSieve/ChildTransfer.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SecondPassArithmetic.fixedSecondMode line 89
  2. theorem OAI.SecondPassArithmetic.fixed_second_mode_transfer line 95
  3. theorem OAI.SecondPassArithmetic.secondInputCoefficient_union line 154
  4. def OAI.SecondPassArithmetic.inputConjugateRow line 164
  5. theorem OAI.SecondPassArithmetic.supportMobius_disjoint_mul line 169
  6. theorem OAI.SecondPassArithmetic.inputConjugateRow_sq_overlap line 179
  7. theorem OAI.SecondPassArithmetic.commonProduct_mask line 254
  8. theorem OAI.SecondPassArithmetic.sum_remove_common_pool line 274
  9. theorem OAI.SecondPassArithmetic.secondInputCoefficient_fixed_mask line 301
  10. theorem OAI.SecondPassArithmetic.inputConjugateRow_fixed_pool line 309
  11. theorem OAI.SecondPassArithmetic.sum_pair_remove_common_pool line 332
  12. lemma OAI.SecondPassArithmetic.star_mask line 348
  13. theorem OAI.SecondPassArithmetic.input_pair_fixed_pool line 353
  14. theorem OAI.SecondPassArithmetic.poisson_mask_generator_dvd line 384
  15. def OAI.SecondPassArithmetic.secondMaskQuotient line 394
  16. theorem OAI.SecondPassArithmetic.secondMaskQuotient_spec line 398
  17. theorem OAI.SecondPassArithmetic.secondMaskQuotient_span line 407
  18. theorem OAI.SecondPassArithmetic.secondMaskQuotient_norm line 426
  19. def OAI.SecondPassArithmetic.maskedSecondSource line 447
  20. def OAI.SecondPassArithmetic.overlapPairWeight line 452
  21. theorem OAI.SecondPassArithmetic.maskedSecondSource_summable line 460
  22. theorem OAI.SecondPassArithmetic.inputConjugateRow_smoothed_overlap line 476
  23. def OAI.SecondPassArithmetic.maskedSecondDual line 527
  24. theorem OAI.SecondPassArithmetic.inputConjugateRow_smoothed_second_poisson line 540
  25. abbrev OAI.SecondPassArithmetic.FirstCoreIndex line 573
  26. def OAI.SecondPassArithmetic.sideRayMonoid line 575
  27. def OAI.SecondPassArithmetic.multiplicativeCoreColumn line 583
  28. def OAI.SecondPassArithmetic.firstCoreTest line 586
  29. def OAI.SecondPassArithmetic.firstCoreOuter line 592
  30. def OAI.SecondPassArithmetic.firstCoreTwist line 599
  31. theorem OAI.SecondPassArithmetic.cubeCoreCoefficient_ray_family line 603
  32. theorem OAI.SecondPassArithmetic.dilatedCoreRow_eq_input_family line 626