OAI/NumberTheory/DirichletL/Energy/ReferenceDeletionBudget.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.CenteredMomentEnergyReferenceDeletionBudget.product_norm_ge_one line 14
2. lemma OAI.SevenEighths.CenteredMomentEnergyReferenceDeletionBudget.weighted_inverse_sqrt line 19
3. lemma OAI.SevenEighths.CenteredMomentEnergyReferenceDeletionBudget.powerset_square_subpower line 27
4. lemma OAI.SevenEighths.CenteredMomentEnergyReferenceDeletionBudget.weighted_uniform_term line 45
5. lemma OAI.SevenEighths.CenteredMomentEnergyReferenceDeletionBudget.signed_weighted_term line 68
6. lemma OAI.SevenEighths.CenteredMomentEnergyReferenceDeletionBudget.slot_majorant_mass line 98
7. theorem OAI.SevenEighths.CenteredMomentEnergyReferenceDeletionBudget.weighted_uniform_mass_subpower line 118
8. theorem OAI.SevenEighths.CenteredMomentEnergyReferenceDeletionBudget.weighted_signed_mass_subpower line 177