OAI/NumberTheory/DirichletL/Energy/Bands.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentEnergyBands.length line 15
2. lemma OAI.SevenEighths.CenteredMomentEnergyBands.length_nonneg line 17
3. def OAI.SevenEighths.CenteredMomentEnergyBands.ZeroAt line 20
4. lemma OAI.SevenEighths.CenteredMomentEnergyBands.zeroAt_of_zeroBound line 27
5. def OAI.SevenEighths.CenteredMomentEnergyBands.PositiveAt line 39
6. theorem OAI.SevenEighths.CenteredMomentEnergyBands.exists_positive_bottom line 55