OAI/NumberTheory/DirichletL/Moments/RadialCenteredEnergy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentRadialCenteredEnergy.centeredChildEnergy line 17
2. lemma OAI.SevenEighths.CenteredMomentRadialCenteredEnergy.centered_child_summable line 22
3. lemma OAI.SevenEighths.CenteredMomentRadialCenteredEnergy.centered_child_nonneg line 50
4. def OAI.SevenEighths.CenteredMomentRadialCenteredEnergy.restrict line 54
5. theorem OAI.SevenEighths.CenteredMomentRadialCenteredEnergy.centered_child_split line 56
6. theorem OAI.SevenEighths.CenteredMomentRadialCenteredEnergy.actual_source_centered line 67
7. theorem OAI.SevenEighths.CenteredMomentRadialCenteredEnergy.actual_source_from_centered_children line 110