OAI/Probability/SKBarriers/Locking/NarrowScheduleEndpoint.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SK.Analytic.narrowClockPerturbed_zero line 15
2. def OAI.SK.Analytic.narrowCrossPenalty line 19
3. def OAI.SK.Analytic.narrowQuarticPenalty line 22
4. theorem OAI.SK.Analytic.narrowSchedule_covariance line 25
5. theorem OAI.SK.Analytic.narrowSchedule_penalty line 43
6. theorem OAI.SK.Analytic.narrowNoisePenalty_nonneg line 65
7. theorem OAI.SK.Analytic.narrowQuarticPenalty_nonneg line 76
8. theorem OAI.SK.Analytic.narrowConstrainedPressure_schedule line 89