OAI/NumberTheory/Ostmann/Characters/RichShellSelectionMass.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Characters.harmonicIntervalMass line 11
2. lemma OAI.Ostmann.Characters.harmonicIntervalMass_nonneg line 14
3. lemma OAI.Ostmann.Characters.harmonicIntervalMass_mono line 18
4. lemma OAI.Ostmann.Characters.harmonicIntervalMass_self line 27
5. lemma OAI.Ostmann.Characters.harmonicIntervalMass_add line 34
6. lemma OAI.Ostmann.Characters.harmonicIntervalMass_grid line 41
7. lemma OAI.Ostmann.Characters.harmonicIntervalMass_eq_of_support line 52
8. theorem OAI.Ostmann.Characters.harmonicIntervalMass_mertens line 58