OAI/Probability/SKFluctuations/PowerTraceRelativeAbsLe.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Power Trace Relative Abs Le.

  1. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.powerTrace_relative_abs_le line 20
  2. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.clock_nonneg line 43
  3. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.clock_powerTrace_relative_abs_le line 52
  4. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.clockResponse_relative_abs_le line 66
  5. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.clock_exp_comparison line 87
  6. structure OAI.SKFluctuations.Hierarchy.ExpClose line 110
  7. theorem OAI.SKFluctuations.Hierarchy.ExpClose.refl line 117
  8. theorem OAI.SKFluctuations.Hierarchy.ExpClose.symm line 119
  9. theorem OAI.SKFluctuations.Hierarchy.ExpClose.mono line 121
  10. theorem OAI.SKFluctuations.Hierarchy.ExpClose.trans line 125
  11. theorem OAI.SKFluctuations.Hierarchy.ExpClose.mul line 135
  12. theorem OAI.SKFluctuations.Hierarchy.ExpClose.of_bounds line 146
  13. theorem OAI.SKFluctuations.Hierarchy.ExpClose.finset_sum line 151
  14. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.clock_close line 166
  15. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.finite_close line 178
  16. def OAI.SKFluctuations.Hierarchy.ClockTree.rootForks line 206
  17. def OAI.SKFluctuations.Hierarchy.ClockTree.atomicHead line 211
  18. theorem OAI.SKFluctuations.Hierarchy.ClockTree.atomicHead_eq_clock line 219
  19. theorem OAI.SKFluctuations.Hierarchy.ClockTree.atomicHead_variation line 233
  20. theorem OAI.SKFluctuations.Hierarchy.ClockTree.atomicHead_crossing line 262
  21. theorem OAI.SKFluctuations.Hierarchy.massOrdered_bounds line 307
  22. theorem OAI.SKFluctuations.Hierarchy.ClockTree.atomicHead_mass_difference line 313
  23. theorem OAI.SKFluctuations.Hierarchy.ClockTree.atomicHead_transfer line 338
  24. theorem OAI.SKFluctuations.Hierarchy.ClockTree.atomicHead_smooth line 359
  25. theorem OAI.SKFluctuations.Hierarchy.ClockTree.atomicHead_probability line 368
  26. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.head_transfer line 383
  27. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.budget_add line 442
  28. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.budget_mul line 449
  29. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.budget_mono line 456
  30. def OAI.SKFluctuations.Hierarchy.ClockTree.forksAt line 464
  31. theorem OAI.SKFluctuations.Hierarchy.ClockTree.forksAt_zero line 470
  32. theorem OAI.SKFluctuations.Hierarchy.ClockTree.leaves_pos line 477
  33. theorem OAI.SKFluctuations.Hierarchy.ClockTree.forks_total line 483
  34. theorem OAI.SKFluctuations.Hierarchy.ClockTree.cut_budget_leaves line 498
  35. theorem OAI.SKFluctuations.Hierarchy.ClockTree.cut_budget_forks line 521
  36. theorem OAI.SKFluctuations.Hierarchy.ClockTree.atomicHead_close line 553
  37. theorem OAI.SKFluctuations.Hierarchy.ClockTree.addHead_close line 576
  38. theorem OAI.SKFluctuations.Hierarchy.ClockTree.atomicHead_crossing_close line 602