OAI/NumberTheory/DirichletL/Energy/State.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SevenEighths.CenteredMomentEnergyState.NaturalState line 15
2. def OAI.SevenEighths.CenteredMomentEnergyState.NaturalState.width line 37
3. lemma OAI.SevenEighths.CenteredMomentEnergyState.NaturalState.width_nonneg line 38
4. def OAI.SevenEighths.CenteredMomentEnergyState.NaturalState.mask line 41
5. def OAI.SevenEighths.CenteredMomentEnergyState.NaturalState.plainEnergy line 44
6. lemma OAI.SevenEighths.CenteredMomentEnergyState.NaturalState.plainEnergy_eq_zero line 50
7. lemma OAI.SevenEighths.CenteredMomentEnergyState.NaturalState.radical_bound line 56
8. def OAI.SevenEighths.CenteredMomentEnergyState.ZeroBound line 64