OAI/NumberTheory/DirichletL/Moments/FirstAmplifiedCapacityCommon.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentFirstAmplifiedCapacityCommon.envelopeRef line 25
2. def OAI.SevenEighths.CenteredMomentFirstAmplifiedCapacityCommon.ratioPenalty line 29
3. lemma OAI.SevenEighths.CenteredMomentFirstAmplifiedCapacityCommon.envelope_pos line 32
4. lemma OAI.SevenEighths.CenteredMomentFirstAmplifiedCapacityCommon.adjusted_log line 42
5. theorem OAI.SevenEighths.CenteredMomentFirstAmplifiedCapacityCommon.common_raw_reference_shift line 49
6. theorem OAI.SevenEighths.CenteredMomentFirstAmplifiedCapacityCommon.common_raw_reference_shift_right line 76
7. theorem OAI.SevenEighths.CenteredMomentFirstAmplifiedCapacityCommon.actual_width_le_reference line 103