OAI/NumberTheory/DirichletL/CubicSieve/FirstPassage.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FirstPassCubeLabels.firstColumnEnergy_eq_sum_integrals line 81
2. theorem OAI.FirstPassCubeLabels.first_column_energy_integral line 112
3. def OAI.FirstPassCubeLabels.firstOutputEnergy line 155
4. theorem OAI.FirstPassCubeLabels.firstOutputEnergy_nonneg line 166
5. theorem OAI.FirstPassCubeLabels.first_passage_transfer line 182
6. def OAI.FirstPassCubeLabels.dilatedIdealCoefficient line 289
7. theorem OAI.FirstPassCubeLabels.dilatedCoreRow_eq_ideal line 300
8. theorem OAI.FirstPassCubeLabels.supportFamily_primePool_char line 315
9. theorem OAI.FirstPassCubeLabels.dilatedCoreRow_smoothed_summable line 334
10. theorem OAI.FirstPassCubeLabels.dilatedCoreRow_second_poisson line 347
11. abbrev OAI.SecondPassArithmetic.O line 372
12. theorem OAI.SecondPassArithmetic.columnCoefficient_norm_one line 378
13. theorem OAI.SecondPassArithmetic.columnCoefficient_mul_star line 390
14. theorem OAI.SecondPassArithmetic.convertedColumnBlock_restore line 399
15. def OAI.SecondPassArithmetic.secondColumnMinus line 425
16. def OAI.SecondPassArithmetic.secondColumnPlus line 433
17. theorem OAI.SecondPassArithmetic.mobius_second_gauss_restore line 442
18. theorem OAI.SecondPassArithmetic.mask_star_row line 498
19. theorem OAI.SecondPassArithmetic.second_child_masked line 507
20. def OAI.SecondPassArithmetic.secondPreColumn line 535
21. def OAI.SecondPassArithmetic.secondChildColumn line 544
22. theorem OAI.SecondPassArithmetic.secondPreColumn_union line 551
23. def OAI.SecondPassArithmetic.secondSeparatedPair line 593
24. def OAI.SecondPassArithmetic.secondCommonWeight line 601
25. def OAI.SecondPassArithmetic.secondChildSum line 606
26. theorem OAI.SecondPassArithmetic.secondSeparatedPair_eq_children line 612
27. def OAI.SecondPassArithmetic.secondChildEnergy line 643
28. theorem OAI.SecondPassArithmetic.secondSeparatedPair_norm_le line 649