OAI/NumberTheory/DirichletL/Moments/DetectorDictionaryUniformLog.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentDetectorDictionary.realInterpolatedLog line 13
2. lemma OAI.SevenEighths.CenteredMomentDetectorDictionary.realInterpolatedLog_smooth line 16
3. lemma OAI.SevenEighths.CenteredMomentDetectorDictionary.realInterpolatedLog_support line 22
4. def OAI.SevenEighths.CenteredMomentDetectorDictionary.realInterpolatedLogSchwartz line 31
5. lemma OAI.SevenEighths.CenteredMomentDetectorDictionary.realInterpolatedLogSchwartz_apply line 36
6. def OAI.SevenEighths.CenteredMomentDetectorDictionary.interpolatedProfile line 50
7. lemma OAI.SevenEighths.CenteredMomentDetectorDictionary.interpolatedProfile_apply line 55