OAI/Probability/SKBarriers/Locking/NarrowSchedule.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SK.Analytic.NarrowMiddleIncrement line 14
2. def OAI.SK.Analytic.narrowCommonSchedule line 16
3. def OAI.SK.Analytic.narrowMiddleVector line 19
4. def OAI.SK.Analytic.narrowMiddleSchedule line 23
5. def OAI.SK.Analytic.narrowMiddleNoise line 26
6. def OAI.SK.Analytic.narrowNoisePenalty line 30
7. theorem OAI.SK.Analytic.narrowCommonSchedule_covariance line 33
8. theorem OAI.SK.Analytic.narrowCommonSchedule_penalty line 49
9. theorem OAI.SK.Analytic.narrowMiddleSchedule_covariance line 67
10. theorem OAI.SK.Analytic.narrowMiddleSchedule_penalty line 94