OAI/NumberTheory/DirichletL/Moments/RadialEligibleEnergy.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SevenEighths.CenteredMomentRadialEligibleEnergy.Radial line 15
2. def OAI.SevenEighths.CenteredMomentRadialEligibleEnergy.Radial.weight line 22
3. lemma OAI.SevenEighths.CenteredMomentRadialEligibleEnergy.Radial.weight_nonneg line 25
4. def OAI.SevenEighths.CenteredMomentRadialEligibleEnergy.finiteData line 31
5. def OAI.SevenEighths.CenteredMomentRadialEligibleEnergy.energy line 34
6. def OAI.SevenEighths.CenteredMomentRadialEligibleEnergy.childEnergy line 39
7. lemma OAI.SevenEighths.CenteredMomentRadialEligibleEnergy.child_summable line 45
8. lemma OAI.SevenEighths.CenteredMomentRadialEligibleEnergy.finite_child_le line 61
9. lemma OAI.SevenEighths.CenteredMomentRadialEligibleEnergy.energy_nonneg line 67
10. lemma OAI.SevenEighths.CenteredMomentRadialEligibleEnergy.child_nonneg line 70
11. theorem OAI.SevenEighths.CenteredMomentRadialEligibleEnergy.actual_source_from_children line 74
12. theorem OAI.SevenEighths.CenteredMomentRadialEligibleEnergy.actual_source_root_from_children line 87