OAI/Probability/SKFluctuations/ClockForkCost.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Clock Fork Cost.

  1. def OAI.SKFluctuations.Hierarchy.ClockTree.forkCost line 19
  2. def OAI.SKFluctuations.Hierarchy.ClockTree.edgeBudget line 26
  3. theorem OAI.SKFluctuations.Hierarchy.ClockTree.forkCost_nonneg line 30
  4. theorem OAI.SKFluctuations.Hierarchy.ClockTree.edgeBudget_nonneg line 37
  5. theorem OAI.SKFluctuations.Hierarchy.ClockTree.single_forkCost line 45
  6. theorem OAI.SKFluctuations.Hierarchy.ClockTree.split_le_forkCost line 52
  7. def OAI.SKFluctuations.Hierarchy.ClockTree.attachForkExtra line 78
  8. theorem OAI.SKFluctuations.Hierarchy.ClockTree.attachForkExtra_le line 83
  9. theorem OAI.SKFluctuations.Hierarchy.ClockTree.markedAttach_forkCost line 110
  10. theorem OAI.SKFluctuations.Hierarchy.ClockTree.markedAttach_forkCost_le line 143
  11. def OAI.SKFluctuations.Hierarchy.ClockTree.forkLedger line 163
  12. def OAI.SKFluctuations.Hierarchy.ClockTree.forkVariation line 167
  13. theorem OAI.SKFluctuations.Hierarchy.ClockTree.forkVariation_nonneg line 171
  14. theorem OAI.SKFluctuations.Hierarchy.ClockTree.forkLedger_nonneg line 176
  15. theorem OAI.SKFluctuations.Hierarchy.ClockTree.forkLedger_le line 187
  16. def OAI.SKFluctuations.Hierarchy.ClockTree.pairMean line 238
  17. theorem OAI.SKFluctuations.Hierarchy.ClockTree.pairMean_zero_symm line 248
  18. theorem OAI.SKFluctuations.Hierarchy.ClockTree.expect_pairAtSlot line 261
  19. def OAI.SKFluctuations.Hierarchy.ClockTree.pairRootMean line 316
  20. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootExpect_pairAtSlot line 322
  21. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootExpect_const line 340
  22. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootExpect_pair_envelope line 350
  23. theorem OAI.SKFluctuations.Hierarchy.ClockTree.profilePairTest_root_envelope line 372
  24. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootExpect_add line 403
  25. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootExpect_mul_sq_le line 416
  26. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootExpect_abs_mul_le line 439
  27. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootExpect_finsetSum line 465
  28. def OAI.SKFluctuations.Hierarchy.ClockTree.plantedWeight line 480
  29. theorem OAI.SKFluctuations.Hierarchy.ClockTree.plantedWeight_nonneg line 485
  30. theorem OAI.SKFluctuations.Hierarchy.ClockTree.plantedWeight_sum line 494
  31. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootExpect_eq_plantedSum line 503
  32. def OAI.SKFluctuations.Hierarchy.ClockTree.plantedPMF line 517
  33. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootExpect_eq_plantedIntegral line 526
  34. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootExpect_holder line 547
  35. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootExpect_holder_budget line 564
  36. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootExpect_rpow_from_second line 584