OAI/Probability/SKFluctuations/PhysicalIncrementMoment.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Physical Increment Moment.

  1. theorem OAI.SKFluctuations.physicalCutNormPower_integrable line 15
  2. theorem OAI.SKFluctuations.physicalCutIncrementNormPower_integrable line 29
  3. theorem OAI.SKFluctuations.physicalRawRatio_increment_moment line 43
  4. theorem OAI.SKFluctuations.projectionEuclideanNorm_coe line 120
  5. theorem OAI.SKFluctuations.physicalCutIncrement_coe_measurable line 125
  6. theorem OAI.SKFluctuations.physicalCutPairSquare_futurePair line 132
  7. theorem OAI.SKFluctuations.root_le_of_even_projection line 148
  8. theorem OAI.SKFluctuations.eventually_cut_pair_moment line 161
  9. theorem OAI.SKFluctuations.physicalCutPairSquare_futureTerminal line 213
  10. theorem OAI.SKFluctuations.eventually_cut_pair_terminal_moment line 231
  11. theorem OAI.SKFluctuations.physicalCutPairSquare_futurePair_observed line 283
  12. theorem OAI.SKFluctuations.eventually_cut_pair_observed_moment line 299
  13. theorem OAI.SKFluctuations.physicalCutPairSquare_futureTerminal_observed line 351
  14. theorem OAI.SKFluctuations.eventually_cut_pair_terminal_observed_moment line 369
  15. inductive OAI.SKFluctuations.PhysicalProjectionClock line 423
  16. theorem OAI.SKFluctuations.eventually_physical_clock_pair_moment line 436
  17. theorem OAI.SKFluctuations.eventually_physical_clock_pair_observed_moment line 457
  18. def OAI.SKFluctuations.Hierarchy.cutSlice line 489
  19. theorem OAI.SKFluctuations.Hierarchy.cutSlice_append_drop line 491
  20. theorem OAI.SKFluctuations.Hierarchy.length_cutSlice line 496
  21. theorem OAI.SKFluctuations.Hierarchy.take_append_slices line 501
  22. theorem OAI.SKFluctuations.orderedSteps_drop_cutMass line 512
  23. theorem OAI.SKFluctuations.physicalProjectionClock_of_gaussian_cuts line 522
  24. theorem OAI.SKFluctuations.physicalProjectionClock_of_terminal_cuts line 541
  25. def OAI.SKFluctuations.physicalFieldDuration line 573
  26. theorem OAI.SKFluctuations.physicalFieldDuration_nonneg line 576
  27. theorem OAI.SKFluctuations.physicalFieldDuration_append line 579
  28. theorem OAI.SKFluctuations.physicalFieldDuration_take_le line 584
  29. theorem OAI.SKFluctuations.physicalFieldDuration_drop_le line 591
  30. theorem OAI.SKFluctuations.physicalFieldDuration_slice_le line 598
  31. theorem OAI.SKFluctuations.physicalFieldDuration_slice_eq line 603
  32. theorem OAI.SKFluctuations.physicalFieldDuration_prefix_monotone line 612
  33. theorem OAI.SKFluctuations.alignedFieldClock_slice line 618