OAI/Probability/SKFluctuations/CumulativeIncrements.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Cumulative Increments.

  1. def OAI.SKFluctuations.Hierarchy.cumulativeIncrements line 22
  2. theorem OAI.SKFluctuations.Hierarchy.cumulativeIncrements_shift line 26
  3. theorem OAI.SKFluctuations.Hierarchy.clockSteps_cumulative line 32
  4. theorem OAI.SKFluctuations.Hierarchy.clockSteps_congr line 40
  5. theorem OAI.SKFluctuations.Hierarchy.ClockTree.weight_congr line 50
  6. theorem OAI.SKFluctuations.Hierarchy.ClockTree.cumulative_weight_congr line 66
  7. def OAI.SKFluctuations.Hierarchy.previousBoundary line 89
  8. theorem OAI.SKFluctuations.Hierarchy.cumulativeIncrements_eq line 93
  9. theorem OAI.SKFluctuations.Hierarchy.previousBoundary_le line 97
  10. theorem OAI.SKFluctuations.Hierarchy.cumulativeIncrements_split line 104
  11. theorem OAI.SKFluctuations.Hierarchy.cumulativeIncrements_update line 128
  12. theorem OAI.SKFluctuations.Hierarchy.MassOrdered.pairwise line 184
  13. theorem OAI.SKFluctuations.Hierarchy.MassOrdered.members_le_one line 199
  14. theorem OAI.SKFluctuations.Hierarchy.MassOrdered.of_pairwise line 209
  15. theorem OAI.SKFluctuations.Hierarchy.MassOrdered.tail_at line 219
  16. theorem OAI.SKFluctuations.Hierarchy.MassOrdered.prefix line 229
  17. def OAI.SKFluctuations.Hierarchy.massGap line 239
  18. theorem OAI.SKFluctuations.Hierarchy.massGap_nonneg line 245
  19. theorem OAI.SKFluctuations.Hierarchy.massGap_drop line 255
  20. theorem OAI.SKFluctuations.Hierarchy.massGap_sum line 266
  21. theorem OAI.SKFluctuations.Hierarchy.massGap_sum_le_one line 280
  22. theorem OAI.SKFluctuations.Hierarchy.ClockTree.cumulative_boundary_move line 294
  23. theorem OAI.SKFluctuations.Hierarchy.ClockTree.cumulative_boundary_move_at line 322
  24. def OAI.SKFluctuations.Hierarchy.loweredBoundary line 350
  25. theorem OAI.SKFluctuations.Hierarchy.loweredBoundary_zero line 353
  26. theorem OAI.SKFluctuations.Hierarchy.loweredBoundary_mono line 357
  27. theorem OAI.SKFluctuations.Hierarchy.loweredBoundary_initial line 368
  28. theorem OAI.SKFluctuations.Hierarchy.loweredBoundary_update line 376
  29. theorem OAI.SKFluctuations.Hierarchy.loweredBoundary_previous line 387
  30. theorem OAI.SKFluctuations.Hierarchy.loweredBoundary_difference line 398
  31. theorem OAI.SKFluctuations.Hierarchy.finite_law_triangle_chain line 412
  32. theorem OAI.SKFluctuations.Hierarchy.ClockTree.forks_sum_shift_le line 426
  33. theorem OAI.SKFluctuations.Hierarchy.massGap_sum_prefix_le_one line 438
  34. theorem OAI.SKFluctuations.Hierarchy.ClockTree.cumulative_lowering line 447
  35. theorem OAI.SKFluctuations.Hierarchy.ClockTree.cumulative_uniform line 492
  36. theorem OAI.SKFluctuations.Hierarchy.ClockTree.cut_mix_close line 539
  37. theorem OAI.SKFluctuations.Hierarchy.ClockTree.cut_boundary_close line 566
  38. theorem OAI.SKFluctuations.Hierarchy.ClockTree.cumulative_boundary_close line 636
  39. theorem OAI.SKFluctuations.Hierarchy.ClockTree.cumulative_boundary_close_at line 664