OAI/NumberTheory/DirichletL/MeanSquare/CanonicalTailBounds.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.InitialMeanSquare.outside_mean_square_of_canonical_density line 81
2. lemma OAI.SecondPassArithmetic.firstTail_inverse_scale_bound line 160
3. lemma OAI.SecondPassArithmetic.firstTail_scalar_bound line 170
4. lemma OAI.SecondPassArithmetic.cubeCoordinates_radical_bound line 203
5. lemma OAI.SecondPassArithmetic.cubeSourceDivisor_norm_bound line 219
6. lemma OAI.SecondPassArithmetic.cubeSourceDivisors_card line 233
7. lemma OAI.SecondPassArithmetic.sourceMobiusDivisor_norm_le_one line 249
8. theorem OAI.SecondPassArithmetic.canonicalCubeDualTail_support line 271
9. theorem OAI.SecondPassArithmetic.full_uniform_canonicalSourceTail_bound line 290
10. theorem OAI.SecondPassArithmetic.globalBin_canonical_child_bound line 442
11. theorem OAI.SecondPassArithmetic.globalSelected_canonical_child_bound line 493
12. theorem OAI.SecondPassArithmetic.globalPooled_mass_le_parent line 558
13. theorem OAI.SecondPassArithmetic.globalArithmeticTargets_nonzero line 579
14. theorem OAI.SecondPassArithmetic.globalRetained_canonical_geometry line 590