OAI/NumberTheory/DirichletL/Energy/OriginalProfileControl.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.CenteredMomentEnergyOriginalProfileControl.slot_product_le line 19
2. lemma OAI.SevenEighths.CenteredMomentEnergyOriginalProfileControl.plain_control_le line 27
3. lemma OAI.SevenEighths.CenteredMomentEnergyOriginalProfileControl.plain_control_sq_le line 40
4. lemma OAI.SevenEighths.CenteredMomentEnergyOriginalProfileControl.zero_plain_control line 47
5. lemma OAI.SevenEighths.CenteredMomentEnergyOriginalProfileControl.lower_product line 51
6. lemma OAI.SevenEighths.CenteredMomentEnergyOriginalProfileControl.source_factor_le line 61
7. theorem OAI.SevenEighths.CenteredMomentEnergyOriginalProfileControl.natural_plain_control line 96
8. theorem OAI.SevenEighths.CenteredMomentEnergyOriginalProfileControl.natural_zero_plain_control line 103
9. theorem OAI.SevenEighths.CenteredMomentEnergyOriginalProfileControl.natural_source_factor line 111
10. theorem OAI.SevenEighths.CenteredMomentEnergyOriginalProfileControl.natural_zero_source_factor line 117