OAI/Probability/SKFluctuations/Chain.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Chain.

  1. theorem OAI.SKFluctuations.Hierarchy.ExpClose.chain line 19
  2. theorem OAI.SKFluctuations.Hierarchy.ClockTree.cumulative_lowering_close line 33
  3. theorem OAI.SKFluctuations.Hierarchy.ClockTree.cumulative_uniform_close line 78
  4. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.linearClock_mass_close line 116
  5. theorem OAI.SKFluctuations.Hierarchy.ClockTree.atomicHead_mass_close_nonneg line 139
  6. theorem OAI.SKFluctuations.Hierarchy.ClockTree.atomicHead_root_transfer_close line 162
  7. theorem OAI.SKFluctuations.Hierarchy.ExpClose.integral line 184
  8. theorem OAI.SKFluctuations.Hierarchy.ClockTree.expect_close line 198
  9. theorem OAI.SKFluctuations.Hierarchy.ClockTree.root_close line 210
  10. theorem OAI.SKFluctuations.Hierarchy.ClockTree.cumulative_uniform_expect_close line 220
  11. theorem OAI.SKFluctuations.Hierarchy.ExpClose.limit_cost line 241
  12. theorem OAI.SKFluctuations.Hierarchy.MassOrdered.exists_positive_lower line 249
  13. def OAI.SKFluctuations.Hierarchy.ClockTree.rootWeight line 259
  14. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootCumulative_uniform_close line 267
  15. theorem OAI.SKFluctuations.Hierarchy.shiftedMean_add_const line 317
  16. theorem OAI.SKFluctuations.Hierarchy.spinWeight_mass_one line 325
  17. def OAI.SKFluctuations.Hierarchy.terminalMass line 356
  18. def OAI.SKFluctuations.Hierarchy.ClockTree.extendOne line 359
  19. def OAI.SKFluctuations.Hierarchy.ClockTree.extendOneEquiv line 364
  20. theorem OAI.SKFluctuations.Hierarchy.ClockTree.extendOne_leaves line 370
  21. theorem OAI.SKFluctuations.Hierarchy.MassOrdered.append_one line 377
  22. theorem OAI.SKFluctuations.Hierarchy.ClockTree.weight_extendOne line 387
  23. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootWeight_congr line 421
  24. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootWeight_extendOne line 431
  25. theorem OAI.SKFluctuations.Hierarchy.ClockTree.rootCumulative_close line 445
  26. def OAI.SKFluctuations.Hierarchy.ReplicaTree.Slot line 488
  27. def OAI.SKFluctuations.Hierarchy.ReplicaTree.atSlot line 493
  28. def OAI.SKFluctuations.Hierarchy.ReplicaTree.singleSlot line 498
  29. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.atSlot_single line 502
  30. structure OAI.SKFluctuations.Hierarchy.ReplicaTree.MarkedPlacement line 510
  31. def OAI.SKFluctuations.Hierarchy.ReplicaTree.MarkedPlacement.fresh line 518
  32. def OAI.SKFluctuations.Hierarchy.ReplicaTree.MarkedPlacement.coincide line 525
  33. def OAI.SKFluctuations.Hierarchy.ReplicaTree.MarkedPlacement.step line 532
  34. def OAI.SKFluctuations.Hierarchy.ReplicaTree.MarkedPlacement.left line 540
  35. def OAI.SKFluctuations.Hierarchy.ReplicaTree.MarkedPlacement.right line 550
  36. def OAI.SKFluctuations.Hierarchy.ReplicaTree.markedAttach line 561
  37. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.markedAttach_forget line 568
  38. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.markedAttach_mass line 581
  39. def OAI.SKFluctuations.Hierarchy.ReplicaTree.MarkedPlacement.hit line 587
  40. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.MarkedPlacement.hit_fresh line 592
  41. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.MarkedPlacement.hit_step line 600
  42. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.MarkedPlacement.coeff_step line 603
  43. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.markedAttach_hit line 608
  44. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.markedAttach_diagonal line 635