OAI/Probability/SKFluctuations/ClockSplitSteps.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

Clock Split Steps.

  1. def OAI.SKFluctuations.Hierarchy.splitClockSteps line 17
  2. theorem OAI.SKFluctuations.Hierarchy.splitClockSteps_append line 22
  3. theorem OAI.SKFluctuations.Hierarchy.splitClockSteps_ordered line 29
  4. theorem OAI.SKFluctuations.Hierarchy.massStepFunction_split_index line 45
  5. theorem OAI.SKFluctuations.Hierarchy.stepClockFunction_split line 59
  6. def OAI.SKFluctuations.Hierarchy.stepPairMoment line 73
  7. theorem OAI.SKFluctuations.Hierarchy.stepPairMoment_eq_split line 79
  8. theorem OAI.SKFluctuations.Hierarchy.stepPairMoment_intervalIntegrable line 103
  9. def OAI.SKFluctuations.Hierarchy.partitionValues line 119
  10. def OAI.SKFluctuations.Hierarchy.partitionSample line 124
  11. theorem OAI.SKFluctuations.Hierarchy.partitionSample_nil line 127
  12. theorem OAI.SKFluctuations.Hierarchy.partitionSample_cons line 130
  13. theorem OAI.SKFluctuations.Hierarchy.partitionSample_intervalIntegrable line 134
  14. def OAI.SKFluctuations.Hierarchy.PartitionMesh line 138
  15. theorem OAI.SKFluctuations.Hierarchy.partition_error_on_cell line 142
  16. theorem OAI.SKFluctuations.Hierarchy.partitionSample_l1_error line 159
  17. def OAI.SKFluctuations.Hierarchy.uniformMassTail line 209
  18. theorem OAI.SKFluctuations.Hierarchy.uniformMassTail_ordered line 213
  19. theorem OAI.SKFluctuations.Hierarchy.uniformMassTail_mesh line 224
  20. def OAI.SKFluctuations.Hierarchy.uniformMasses line 239
  21. theorem OAI.SKFluctuations.Hierarchy.uniformMasses_ordered line 242
  22. theorem OAI.SKFluctuations.Hierarchy.uniformMasses_mesh line 247
  23. def OAI.SKFluctuations.Hierarchy.sampleClockSteps line 263
  24. theorem OAI.SKFluctuations.Hierarchy.sampleClockSteps_ordered line 267
  25. theorem OAI.SKFluctuations.Hierarchy.sampleClockSteps_masses line 273
  26. theorem OAI.SKFluctuations.Hierarchy.sampleClockSteps_values line 280
  27. theorem OAI.SKFluctuations.Hierarchy.sampleClockSteps_function line 301
  28. def OAI.SKFluctuations.Hierarchy.partitionEnd line 320
  29. def OAI.SKFluctuations.Hierarchy.splitMassPartition line 324
  30. theorem OAI.SKFluctuations.Hierarchy.splitMassPartition_end line 331
  31. theorem OAI.SKFluctuations.Hierarchy.splitMassPartition_bounds line 341
  32. theorem OAI.SKFluctuations.Hierarchy.splitMassPartition_ordered line 354
  33. theorem OAI.SKFluctuations.Hierarchy.splitMassPartition_mesh line 366
  34. theorem OAI.SKFluctuations.Hierarchy.partitionEnd_append line 382
  35. theorem OAI.SKFluctuations.Hierarchy.partitionValues_terminal line 388
  36. theorem OAI.SKFluctuations.Hierarchy.sampleClockSteps_append line 394
  37. theorem OAI.SKFluctuations.Hierarchy.MassOrdered.append_end line 401
  38. theorem OAI.SKFluctuations.Hierarchy.MassOrdered.end_bounds line 407
  39. theorem OAI.SKFluctuations.Hierarchy.PartitionMesh.append_one line 413
  40. theorem OAI.SKFluctuations.Hierarchy.partitionSample_pair_error line 431
  41. def OAI.SKFluctuations.Hierarchy.sampledDisorderPressure line 452
  42. def OAI.SKFluctuations.Hierarchy.clockVariationBound line 456
  43. theorem OAI.SKFluctuations.Hierarchy.clockVariationBound_nonneg line 459
  44. theorem OAI.SKFluctuations.Hierarchy.sampledDisorderPressure_mesh_comparison line 468
  45. theorem OAI.SKFluctuations.Hierarchy.sampleClockSteps_length line 510
  46. theorem OAI.SKFluctuations.Hierarchy.sampleClockSteps_terminal line 517
  47. theorem OAI.SKFluctuations.Hierarchy.sampleClockSteps_mass_le line 526
  48. theorem OAI.SKFluctuations.Hierarchy.sampleClock_distance_integral line 538
  49. def OAI.SKFluctuations.Hierarchy.sampledPairDisorder line 567
  50. theorem OAI.SKFluctuations.Hierarchy.sampledPairDisorder_mesh_comparison line 571
  51. theorem OAI.SKFluctuations.Hierarchy.uniformMasses_mesh_tendsto line 617
  52. theorem OAI.SKFluctuations.Hierarchy.sampledDisorderPressure_cauchy line 622
  53. def OAI.SKFluctuations.Hierarchy.pathDisorderPressure line 642
  54. theorem OAI.SKFluctuations.Hierarchy.sampledDisorderPressure_tendsto line 646
  55. theorem OAI.SKFluctuations.Hierarchy.sampledDisorderPressure_path_error line 656