OAI/NumberTheory/DirichletL/Energy/ReferenceDeletionCapacity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.CenteredMomentEnergyReferenceDeletionCapacity.deleted_short_length line 15
2. theorem OAI.SevenEighths.CenteredMomentEnergyReferenceDeletionCapacity.deleted_reflection_excess line 27
3. theorem OAI.SevenEighths.CenteredMomentEnergyReferenceDeletionCapacity.deleted_reflection_removal line 57
4. lemma OAI.SevenEighths.CenteredMomentEnergyReferenceDeletionCapacity.plain_kappa_eq line 77
5. lemma OAI.SevenEighths.CenteredMomentEnergyReferenceDeletionCapacity.plain_kappa_lower line 80
6. lemma OAI.SevenEighths.CenteredMomentEnergyReferenceDeletionCapacity.paid_divisor_power line 83