OAI/NumberTheory/DirichletL/Moments/AbsoluteEnergy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.CenteredMomentAbsoluteEnergy.rowWeight_norm_le_one_all line 16
2. theorem OAI.SevenEighths.CenteredMomentAbsoluteEnergy.radial_norm_summable line 24
3. theorem OAI.SevenEighths.CenteredMomentAbsoluteEnergy.radial_weight_lattice_bound_all line 29
4. theorem OAI.SevenEighths.CenteredMomentAbsoluteEnergy.finite_hecke_polynomial_norm line 64
5. theorem OAI.SevenEighths.CenteredMomentAbsoluteEnergy.finite_hecke_energy_summable line 73
6. theorem OAI.SevenEighths.CenteredMomentAbsoluteEnergy.finite_hecke_energy_absolute line 87
7. theorem OAI.SevenEighths.CenteredMomentAbsoluteEnergy.smooth_subset_source_absolute_energy line 107