OAI/Probability/SKFluctuations/PhysicalDyadicClock.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Physical Dyadic Clock.

  1. theorem OAI.SKFluctuations.physicalProjectionClock_of_field_cuts line 15
  2. theorem OAI.SKFluctuations.physicalProjectionClock_of_field_terminal line 27
  3. theorem OAI.SKFluctuations.physicalDyadicLayer_clock line 39
  4. theorem OAI.SKFluctuations.hasFarPairClock_of_layer_scales line 150
  5. theorem OAI.SKFluctuations.physicalDyadic_hasFarPairClock line 192
  6. theorem OAI.SKFluctuations.eventually_physical_dyadic_band line 251
  7. structure OAI.SKFluctuations.PhysicalBandWindow line 353
  8. def OAI.SKFluctuations.PhysicalBandWindow.mass line 393
  9. def OAI.SKFluctuations.PhysicalBandWindow.measure line 395
  10. instance OAI.SKFluctuations.PhysicalBandWindow.(instance at line 399) line 399
  11. def OAI.SKFluctuations.PhysicalBandWindow.nearCoefficient line 403
  12. def OAI.SKFluctuations.PhysicalBandWindow.farCoefficient line 407
  13. def OAI.SKFluctuations.PhysicalBandWindow.coefficient line 410
  14. def OAI.SKFluctuations.PhysicalBandWindow.loss line 413
  15. theorem OAI.SKFluctuations.PhysicalBandWindow.measure_mass line 416
  16. theorem OAI.SKFluctuations.PhysicalBandWindow.measure_cap line 420
  17. theorem OAI.SKFluctuations.PhysicalBandWindow.nearCoefficient_nonneg line 425
  18. theorem OAI.SKFluctuations.PhysicalBandWindow.farCoefficient_nonneg line 435
  19. theorem OAI.SKFluctuations.PhysicalBandWindow.coefficient_nonneg line 441
  20. def OAI.SKFluctuations.physicalIntervalCells line 457
  21. theorem OAI.SKFluctuations.mem_physicalIntervalCells line 460
  22. theorem OAI.SKFluctuations.physicalIntervalMass line 465
  23. theorem OAI.SKFluctuations.physicalIntervalCell_band line 484
  24. theorem OAI.SKFluctuations.physicalIntervalCell_cap line 497
  25. theorem OAI.SKFluctuations.physicalCell_pos_of_cap line 518
  26. theorem OAI.SKFluctuations.Hierarchy.inverseConstraint_local_cap line 543
  27. theorem OAI.SKFluctuations.Hierarchy.inverseConstraint_window_cap line 558
  28. def OAI.SKFluctuations.constrainedPhysicalWindow line 579