OAI/Probability/SKFluctuations/ClockZeroRefinement.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

Clock Zero Refinement.

  1. theorem OAI.SKFluctuations.Hierarchy.shiftedContinuation_zero_clock line 16
  2. theorem OAI.SKFluctuations.Hierarchy.shiftedMean_zero_clock line 22
  3. theorem OAI.SKFluctuations.Hierarchy.prefixContinuation_zero_insert line 28
  4. theorem OAI.SKFluctuations.Hierarchy.prefixTest_zero_insert line 34
  5. inductive OAI.SKFluctuations.Hierarchy.ZeroClockRefinement line 43
  6. theorem OAI.SKFluctuations.Hierarchy.ZeroClockRefinement.continuation_test line 49
  7. theorem OAI.SKFluctuations.Hierarchy.ZeroClockRefinement.hierarchy line 59
  8. theorem OAI.SKFluctuations.Hierarchy.ZeroClockRefinement.cons line 77
  9. abbrev OAI.SKFluctuations.Hierarchy.PairedClockStep line 86
  10. def OAI.SKFluctuations.Hierarchy.commonClockSteps line 88
  11. def OAI.SKFluctuations.Hierarchy.leftClockSteps line 95
  12. def OAI.SKFluctuations.Hierarchy.rightClockSteps line 98
  13. theorem OAI.SKFluctuations.Hierarchy.zeroClockSteps_refines line 101
  14. theorem OAI.SKFluctuations.Hierarchy.commonClockSteps_refines line 110
  15. theorem OAI.SKFluctuations.Hierarchy.commonClockSteps_same_masses line 142
  16. theorem OAI.SKFluctuations.Hierarchy.OrderedSteps.map_variance line 147
  17. theorem OAI.SKFluctuations.Hierarchy.commonClockSteps_ordered line 154
  18. def OAI.SKFluctuations.Hierarchy.positiveStepMasses line 193
  19. theorem OAI.SKFluctuations.Hierarchy.positiveStepMasses_length line 198
  20. theorem OAI.SKFluctuations.Hierarchy.positiveStepMasses_ordered line 204
  21. def OAI.SKFluctuations.Hierarchy.stepClockValues line 211
  22. theorem OAI.SKFluctuations.Hierarchy.stepClockValues_zero line 216
  23. theorem OAI.SKFluctuations.Hierarchy.stepClockValues_mono line 219
  24. theorem OAI.SKFluctuations.Hierarchy.stepClockValues_initial_le line 230
  25. theorem OAI.SKFluctuations.Hierarchy.diagonalBoundarySteps_stepClockValues line 235
  26. theorem OAI.SKFluctuations.Hierarchy.stepClockValues_terminal line 248
  27. theorem OAI.SKFluctuations.Hierarchy.ZeroClockRefinement.total_variance line 254
  28. theorem OAI.SKFluctuations.Hierarchy.ClockTree.singleMean_eq_hierarchy line 273
  29. def OAI.SKFluctuations.Hierarchy.stepPairMean line 287
  30. theorem OAI.SKFluctuations.Hierarchy.ClockTree.pairMean_prefix line 293
  31. theorem OAI.SKFluctuations.Hierarchy.ZeroClockRefinement.pairMean line 326
  32. theorem OAI.SKFluctuations.Hierarchy.ClockTree.disorderExpect_integral line 336
  33. theorem OAI.SKFluctuations.Hierarchy.length_clockSteps line 361
  34. theorem OAI.SKFluctuations.Hierarchy.positiveStepMasses_append line 368
  35. theorem OAI.SKFluctuations.Hierarchy.clockSteps_stepClockValues line 377
  36. def OAI.SKFluctuations.Hierarchy.stepPairDisorder line 383
  37. theorem OAI.SKFluctuations.Hierarchy.ClockTree.pairDisorder_coordinates line 389
  38. theorem OAI.SKFluctuations.Hierarchy.ZeroClockRefinement.pairDisorder line 430
  39. theorem OAI.SKFluctuations.Hierarchy.ClockTree.disorderProfileJets_oneError_pointwise line 448
  40. theorem OAI.SKFluctuations.Hierarchy.ClockTree.disorderProfileJets_l1_comparison line 481
  41. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.coordinateProfile_abs_le_sum line 513
  42. theorem OAI.SKFluctuations.Hierarchy.ClockTree.single_leaves_exact line 538
  43. theorem OAI.SKFluctuations.Hierarchy.ClockTree.pairClock_leaves line 545
  44. theorem OAI.SKFluctuations.Hierarchy.ClockTree.pairClock_forkCost line 555
  45. theorem OAI.SKFluctuations.Hierarchy.ClockTree.pairDisorder_l1_comparison line 568
  46. def OAI.SKFluctuations.Hierarchy.stepDisorderPressure line 603
  47. theorem OAI.SKFluctuations.Hierarchy.stepDisorderPressure_eq line 608
  48. theorem OAI.SKFluctuations.Hierarchy.ZeroClockRefinement.pressure line 617
  49. theorem OAI.SKFluctuations.Hierarchy.positiveStepMasses_values line 626
  50. theorem OAI.SKFluctuations.Hierarchy.positiveStepMasses_eq line 633
  51. theorem OAI.SKFluctuations.Hierarchy.stepDisorderPressure_comparison line 639