OAI/NumberTheory/DirichletL/Descent/FirstBalancedSource.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.InverseMoment.first_fresh_physical_profile line 11
2. theorem OAI.SevenEighths.InverseMoment.first_balanced_density_integrable line 76
3. theorem OAI.SevenEighths.InverseMoment.firstCommonNorms_pos line 89
4. theorem OAI.SevenEighths.InverseMoment.actual_first_balanced_block line 106