OAI/NumberTheory/DirichletL/Energy/BackwardSourceRanges.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentEnergyBackwardSourceRanges.lengthAt line 14
2. def OAI.SevenEighths.CenteredMomentEnergyBackwardSourceRanges.lowerAt line 15
3. lemma OAI.SevenEighths.CenteredMomentEnergyBackwardSourceRanges.previous_length line 17
4. lemma OAI.SevenEighths.CenteredMomentEnergyBackwardSourceRanges.previous_lower line 23
5. lemma OAI.SevenEighths.CenteredMomentEnergyBackwardSourceRanges.length_nonneg line 28
6. lemma OAI.SevenEighths.CenteredMomentEnergyBackwardSourceRanges.original_length line 31
7. lemma OAI.SevenEighths.CenteredMomentEnergyBackwardSourceRanges.lower_positive line 34
8. theorem OAI.SevenEighths.CenteredMomentEnergyBackwardSourceRanges.profile_step_support line 37
9. theorem OAI.SevenEighths.CenteredMomentEnergyBackwardSourceRanges.previous_admits line 45
10. lemma OAI.SevenEighths.CenteredMomentEnergyBackwardSourceRanges.paired_contours line 64
11. lemma OAI.SevenEighths.CenteredMomentEnergyBackwardSourceRanges.source_cap_uniform line 72
12. lemma OAI.SevenEighths.CenteredMomentEnergyBackwardSourceRanges.scheduled_source_cap line 78
13. theorem OAI.SevenEighths.CenteredMomentEnergyBackwardSourceRanges.actual_reference_reserve_previous line 82