OAI/NumberTheory/DirichletL/Moments/AmplificationEnergy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentAmplificationEnergy.eligiblePairs line 13
2. def OAI.SevenEighths.CenteredMomentAmplificationEnergy.outputRow line 16
3. theorem OAI.SevenEighths.CenteredMomentAmplificationEnergy.outputRow_norm line 18
4. theorem OAI.SevenEighths.CenteredMomentAmplificationEnergy.amplified_energy_pushforward line 34
5. theorem OAI.SevenEighths.CenteredMomentAmplificationEnergy.sum_eligiblePairs line 65
6. def OAI.SevenEighths.CenteredMomentAmplificationEnergy.errorEnergy line 71
7. theorem OAI.SevenEighths.CenteredMomentAmplificationEnergy.gauss_energy_amplification line 77