OAI/NumberTheory/DirichletL/Descent/SecondNormalizedEnergy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.InverseMoment.child_ball_neg line 13
2. lemma OAI.SevenEighths.InverseMoment.child_ball_sum_neg line 17
3. def OAI.SevenEighths.InverseMoment.secondLabelWeight line 35
4. theorem OAI.SevenEighths.InverseMoment.second_left_normalized_energy line 37
5. theorem OAI.SevenEighths.InverseMoment.second_right_normalized_energy line 50
6. theorem OAI.SevenEighths.InverseMoment.normalized_child_energy_radical_puncture line 80