OAI/Probability/SKBarriers/Replicas/TripleTimeBlocks.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SK.Analytic.TripleTimeBlocks line 15
  2. def OAI.SK.Analytic.TripleTimeBlocks.front line 25
  3. def OAI.SK.Analytic.TripleTimeBlocks.full line 26
  4. def OAI.SK.Analytic.TripleTimeBlocks.early line 27
  5. def OAI.SK.Analytic.TripleTimeBlocks.c line 29
  6. def OAI.SK.Analytic.TripleTimeBlocks.b line 30
  7. def OAI.SK.Analytic.TripleTimeBlocks.a line 31
  8. def OAI.SK.Analytic.TripleTimeBlocks.d line 32
  9. def OAI.SK.Analytic.TripleTimeBlocks.t line 33
  10. def OAI.SK.Analytic.TripleTimeBlocks.w line 34
  11. theorem OAI.SK.Analytic.TripleTimeBlocks.w_underlying line 36
  12. theorem OAI.SK.Analytic.TripleTimeBlocks.prefix_raw line 39
  13. theorem OAI.SK.Analytic.TripleTimeBlocks.full_raw line 42
  14. theorem OAI.SK.Analytic.TripleTimeBlocks.early_raw line 45
  15. theorem OAI.SK.Analytic.TripleTimeBlocks.c_variance line 48
  16. theorem OAI.SK.Analytic.TripleTimeBlocks.a_variance line 49
  17. theorem OAI.SK.Analytic.TripleTimeBlocks.prefix_variance line 50
  18. theorem OAI.SK.Analytic.TripleTimeBlocks.full_variance line 52
  19. theorem OAI.SK.Analytic.TripleTimeBlocks.early_variance line 54
  20. theorem OAI.SK.Analytic.TripleTimeBlocks.w_variance line 57
  21. theorem OAI.SK.Analytic.TripleTimeBlocks.w_cross line 58
  22. theorem OAI.SK.Analytic.TripleTimeBlocks.w_absCross line 59
  23. theorem OAI.SK.Analytic.TripleTimeBlocks.w_penalty line 61
  24. theorem OAI.SK.Analytic.TripleTimeBlocks.normalized_stats line 64
  25. theorem OAI.SK.Analytic.TripleTimeBlocks.normalized_penalty line 72