OAI/Probability/SKBarriers/Locking/NarrowTimeBlocks.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SK.Analytic.NarrowTimeBlocks line 18
  2. def OAI.SK.Analytic.NarrowTimeBlocks.common line 28
  3. def OAI.SK.Analytic.NarrowTimeBlocks.middle line 29
  4. def OAI.SK.Analytic.NarrowTimeBlocks.front line 30
  5. def OAI.SK.Analytic.NarrowTimeBlocks.full line 31
  6. def OAI.SK.Analytic.NarrowTimeBlocks.b line 33
  7. def OAI.SK.Analytic.NarrowTimeBlocks.l line 34
  8. def OAI.SK.Analytic.NarrowTimeBlocks.j line 35
  9. def OAI.SK.Analytic.NarrowTimeBlocks.k line 36
  10. def OAI.SK.Analytic.NarrowTimeBlocks.t line 37
  11. def OAI.SK.Analytic.NarrowTimeBlocks.c line 39
  12. def OAI.SK.Analytic.NarrowTimeBlocks.v line 40
  13. def OAI.SK.Analytic.NarrowTimeBlocks.w line 41
  14. theorem OAI.SK.Analytic.NarrowTimeBlocks.c_underlying line 43
  15. theorem OAI.SK.Analytic.NarrowTimeBlocks.v_underlying line 45
  16. theorem OAI.SK.Analytic.NarrowTimeBlocks.w_underlying line 47
  17. theorem OAI.SK.Analytic.NarrowTimeBlocks.common_raw line 50
  18. theorem OAI.SK.Analytic.NarrowTimeBlocks.middle_raw line 52
  19. theorem OAI.SK.Analytic.NarrowTimeBlocks.front_raw line 54
  20. theorem OAI.SK.Analytic.NarrowTimeBlocks.full_raw line 56
  21. theorem OAI.SK.Analytic.NarrowTimeBlocks.l_variance line 59
  22. theorem OAI.SK.Analytic.NarrowTimeBlocks.j_variance line 61
  23. theorem OAI.SK.Analytic.NarrowTimeBlocks.common_variance line 63
  24. theorem OAI.SK.Analytic.NarrowTimeBlocks.front_variance line 65
  25. theorem OAI.SK.Analytic.NarrowTimeBlocks.full_variance line 67
  26. theorem OAI.SK.Analytic.NarrowTimeBlocks.cross_stats line 70
  27. theorem OAI.SK.Analytic.NarrowTimeBlocks.variance_stats line 76
  28. theorem OAI.SK.Analytic.NarrowTimeBlocks.absCross_stats line 82
  29. theorem OAI.SK.Analytic.NarrowTimeBlocks.v_mean line 89