OAI/NumberTheory/DirichletL/Moments/SecondWidthDrop.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SevenEighths.CenteredMomentSecondWidthDrop.amplificationIncrementline 16 - def
OAI.SevenEighths.CenteredMomentSecondWidthDrop.nominalLengthline 19 - lemma
OAI.SevenEighths.CenteredMomentSecondWidthDrop.physical_frequency_scaleline 21 - lemma
OAI.SevenEighths.CenteredMomentSecondWidthDrop.actual_nominal_dropline 33 - theorem
OAI.SevenEighths.CenteredMomentSecondWidthDrop.exists_physical_width_familyline 41