OAI/Probability/SKFluctuations/SegmentTest.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Segment Test.

  1. theorem OAI.SKFluctuations.Hierarchy.OrderedSteps.mem_pos line 22
  2. theorem OAI.SKFluctuations.Hierarchy.integral_scaledTransition_test line 33
  3. theorem OAI.SKFluctuations.Hierarchy.integral_segmentLaw_test line 63
  4. theorem OAI.SKFluctuations.Hierarchy.integral_segmentLaw_append line 91
  5. theorem OAI.SKFluctuations.Hierarchy.OrderedSteps.suffix line 123
  6. theorem OAI.SKFluctuations.Hierarchy.prefixTest_mono line 129
  7. def OAI.SKFluctuations.Hierarchy.AlignedFieldClock line 145
  8. def OAI.SKFluctuations.Hierarchy.projectionBlockConstant line 149
  9. theorem OAI.SKFluctuations.Hierarchy.projection_aligned_block line 153
  10. theorem OAI.SKFluctuations.Hierarchy.projection_aligned_blocks_prefix line 169
  11. theorem OAI.SKFluctuations.Hierarchy.prefixContinuation_reindex_steps line 227
  12. theorem OAI.SKFluctuations.Hierarchy.prefixTest_reindex_steps line 240
  13. theorem OAI.SKFluctuations.Hierarchy.hierarchyCenteredEvenMoment_reindex line 255
  14. theorem OAI.SKFluctuations.Hierarchy.AlignedFieldClock.reindex line 263
  15. theorem OAI.SKFluctuations.Hierarchy.reindexSteps_append line 289
  16. theorem OAI.SKFluctuations.Hierarchy.reindexSteps_flatten line 294
  17. theorem OAI.SKFluctuations.Hierarchy.projection_aligned_blocks_finite line 302
  18. def OAI.SKFluctuations.fieldProjectionDirection line 347
  19. def OAI.SKFluctuations.spinProjection line 351
  20. def OAI.SKFluctuations.projectionEuclideanNorm line 354
  21. theorem OAI.SKFluctuations.finiteFeature_fieldProjectionDirection line 357
  22. theorem OAI.SKFluctuations.fieldProjectionDirection_sqsum line 365
  23. theorem OAI.SKFluctuations.spinProjection_abs_le line 370
  24. theorem OAI.SKFluctuations.Hierarchy.hierarchyCenteredEvenMoment_bound line 389
  25. def OAI.SKFluctuations.Hierarchy.projectionOrderConstant line 404
  26. theorem OAI.SKFluctuations.Hierarchy.projectionBlockConstant_eq line 408
  27. theorem OAI.SKFluctuations.finiteSK_projection_blocks line 425
  28. def OAI.SKFluctuations.projectionLogBlocks line 465
  29. theorem OAI.SKFluctuations.projectionLogBlocks_ge line 467
  30. theorem OAI.SKFluctuations.projectionLogBlocks_le line 470
  31. theorem OAI.SKFluctuations.projectionLogBlocks_pos line 478
  32. theorem OAI.SKFluctuations.projectionLogBlocks_suppression line 484
  33. theorem OAI.SKFluctuations.eventually_projectionLogBlocks line 504
  34. theorem OAI.SKFluctuations.eventually_finiteSK_projection_log line 531