OAI/NumberTheory/DirichletL/Descent/SecondSharpPuncture.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.InverseMoment.actual_second_radical_puncture_q0_norm line 17
2. theorem OAI.SevenEighths.InverseMoment.actual_second_inherited_puncture_q0_norm line 43
3. theorem OAI.SevenEighths.InverseMoment.actual_second_q0_cube_bound line 67
4. theorem OAI.SevenEighths.InverseMoment.actual_second_puncture_power_from_cubes line 79
5. theorem OAI.SevenEighths.InverseMoment.actual_second_puncture_width_from_cubes line 105
6. theorem OAI.SevenEighths.InverseMoment.actual_second_child_margins_from_cubes line 128