OAI/NumberTheory/DirichletL/Moments/SourceSecondZeroEnergy.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentSourceSecondZeroEnergy.sourceSecondZero line 17
2. lemma OAI.SevenEighths.CenteredMomentSourceSecondZeroEnergy.heightCoeff_norm_le_one line 21
3. theorem OAI.SevenEighths.CenteredMomentSourceSecondZeroEnergy.secondZeroEnergy_filter line 32
4. lemma OAI.SevenEighths.CenteredMomentSourceSecondZeroEnergy.sourceGenerator_span line 49
5. lemma OAI.SevenEighths.CenteredMomentSourceSecondZeroEnergy.sourceGenerator_primary line 52
6. lemma OAI.SevenEighths.CenteredMomentSourceSecondZeroEnergy.sourceGenerator_injective line 55
7. theorem OAI.SevenEighths.CenteredMomentSourceSecondZeroEnergy.sourceSecondZero_divisor_bound line 60
8. theorem OAI.SevenEighths.CenteredMomentSourceSecondZeroEnergy.sourceSecondZero_eq_zero_of_subunit line 85
9. theorem OAI.SevenEighths.CenteredMomentSourceSecondZeroEnergy.tuple_second_zero_bound line 97
10. theorem OAI.SevenEighths.CenteredMomentSourceSecondZeroEnergy.normalized_tuple_second_zero_bound line 154
11. lemma OAI.SevenEighths.CenteredMomentSourceSecondZeroEnergy.profileCoefficient_dvd line 184
12. theorem OAI.SevenEighths.CenteredMomentSourceSecondZeroEnergy.profile_second_zero_energy line 192
13. theorem OAI.SevenEighths.CenteredMomentSourceSecondZeroEnergy.bounded_profile_second_zero_energy line 241
14. theorem OAI.SevenEighths.CenteredMomentSourceSecondZeroEnergy.smooth_subset_source_second_zero_energy line 300