OAI/Probability/SKBarriers/Replicas/TripleSchedule.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SK.Analytic.TripleMiddleIncrement line 14
  2. def OAI.SK.Analytic.rawVariance line 16
  3. def OAI.SK.Analytic.rawPenalty line 18
  4. def OAI.SK.Analytic.rawArea line 21
  5. def OAI.SK.Analytic.weightedCross line 23
  6. def OAI.SK.Analytic.weightedVariance line 25
  7. def OAI.SK.Analytic.weightedCrossPenalty line 27
  8. def OAI.SK.Analytic.weightedVariancePenalty line 30
  9. def OAI.SK.Analytic.weightedUnderlying line 33
  10. def OAI.SK.Analytic.tripleCommonSchedule line 35
  11. def OAI.SK.Analytic.tripleMiddleVector line 38
  12. def OAI.SK.Analytic.tripleMiddleSchedule line 42
  13. def OAI.SK.Analytic.tripleTailBlock line 45
  14. def OAI.SK.Analytic.tripleTailSchedule line 48
  15. theorem OAI.SK.Analytic.matrixChainCovariance_nil line 50
  16. theorem OAI.SK.Analytic.matrixChainCovariance_cons line 51
  17. theorem OAI.SK.Analytic.matrixChainCovariance_append line 54
  18. theorem OAI.SK.Analytic.matrixChainPenalty_nil line 58
  19. theorem OAI.SK.Analytic.matrixChainPenalty_cons line 60
  20. theorem OAI.SK.Analytic.matrixChainPenalty_append line 64
  21. theorem OAI.SK.Analytic.tripleCommonSchedule_covariance line 68
  22. theorem OAI.SK.Analytic.tripleCommonSchedule_penalty line 80
  23. theorem OAI.SK.Analytic.tripleMiddleSchedule_covariance line 93
  24. theorem OAI.SK.Analytic.tripleMiddleSchedule_penalty line 116