OAI/NumberTheory/DirichletL/Descent/FirstEnergy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.InverseMoment.full_rayIdealRow_continuous line 14
2. theorem OAI.SevenEighths.InverseMoment.full_rayIdealRow_uniform_bound line 23
3. theorem OAI.SevenEighths.InverseMoment.full_rayIdealEnergy_continuous line 45
4. theorem OAI.SevenEighths.InverseMoment.full_rayIdealEnergy_uniform_bound line 57
5. theorem OAI.SevenEighths.InverseMoment.full_integrable_rayIdealEnergy line 74
6. theorem OAI.SevenEighths.InverseMoment.full_cube_integral_norm_le_energy line 86