OAI/NumberTheory/DirichletL/Moments/SourceZeroEnergy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.CenteredMomentSourceZeroEnergy.profileCoefficient_norm_le line 17
2. theorem OAI.SevenEighths.CenteredMomentSourceZeroEnergy.profileCoefficient_product_bound line 53
3. theorem OAI.SevenEighths.CenteredMomentSourceZeroEnergy.zeroEnergy_eq_zero_of_subunit line 89
4. theorem OAI.SevenEighths.CenteredMomentSourceZeroEnergy.smooth_source_zero_energy line 106
5. theorem OAI.SevenEighths.CenteredMomentSourceZeroEnergy.smooth_source_zero_energy_at_radius line 187
6. theorem OAI.SevenEighths.CenteredMomentSourceZeroEnergy.smooth_subset_source_zero_energy line 244