OAI/NumberTheory/DirichletL/Energy/StageReserveSchedule.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentEnergyStageReserveSchedule.stageLoss line 11
2. lemma OAI.SevenEighths.CenteredMomentEnergyStageReserveSchedule.stageLoss_pos line 13
3. lemma OAI.SevenEighths.CenteredMomentEnergyStageReserveSchedule.stageLoss_final line 19
4. lemma OAI.SevenEighths.CenteredMomentEnergyStageReserveSchedule.successor_with_references line 25
5. lemma OAI.SevenEighths.CenteredMomentEnergyStageReserveSchedule.one_time_with_new_cost line 38
6. lemma OAI.SevenEighths.CenteredMomentEnergyStageReserveSchedule.actual_one_time_with_new_cost line 47