OAI/Probability/SKFluctuations/PhysicalRetainedCut.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Physical Retained Cut.

  1. theorem OAI.SKFluctuations.sampled_split_mass line 15
  2. theorem OAI.SKFluctuations.sampled_retained_mass line 29
  3. theorem OAI.SKFluctuations.splitClockSteps_length_le line 36
  4. def OAI.SKFluctuations.physicalRetainedIndex line 42
  5. theorem OAI.SKFluctuations.physicalRetainedIndex_mono line 46
  6. theorem OAI.SKFluctuations.physicalRetainedIndex_mass line 50
  7. theorem OAI.SKFluctuations.physicalRetainedIndex_after line 56
  8. theorem OAI.SKFluctuations.physicalQuantileGrid_retained line 76
  9. theorem OAI.SKFluctuations.physical_retained_interval_after line 92
  10. theorem OAI.SKFluctuations.retainedConstrainedWindow line 109
  11. theorem OAI.SKFluctuations.sampledFieldDuration_radius line 174
  12. theorem OAI.SKFluctuations.sampledFieldClock_radius_difference line 188
  13. theorem OAI.SKFluctuations.radiusSampledStrength_growth line 216
  14. theorem OAI.SKFluctuations.radiusPrecedingClocks line 233
  15. theorem OAI.SKFluctuations.physicalConstrainedClockLengths line 298
  16. theorem OAI.SKFluctuations.PhysicalBandWindow.nearCoefficient_bound line 367
  17. theorem OAI.SKFluctuations.PhysicalBandWindow.farCoefficient_bound line 405
  18. theorem OAI.SKFluctuations.geometric_mean_balance line 435
  19. def OAI.SKFluctuations.PhysicalBandWindow.nearScaleConstant line 452
  20. def OAI.SKFluctuations.PhysicalBandWindow.farScaleConstant line 454
  21. def OAI.SKFluctuations.PhysicalBandWindow.scaleFactor line 456
  22. theorem OAI.SKFluctuations.PhysicalBandWindow.coefficient_balanced line 459
  23. theorem OAI.SKFluctuations.PhysicalBandWindow.loss_bound line 489
  24. theorem OAI.SKFluctuations.PhysicalBandWindow.nearCoefficient_general line 523
  25. theorem OAI.SKFluctuations.PhysicalBandWindow.farCoefficient_general line 562
  26. def OAI.SKFluctuations.PhysicalBandWindow.generalNearScaleConstant line 593
  27. def OAI.SKFluctuations.PhysicalBandWindow.generalFarScaleConstant line 595
  28. def OAI.SKFluctuations.PhysicalBandWindow.generalScaleFactor line 597
  29. theorem OAI.SKFluctuations.PhysicalBandWindow.coefficient_balanced_general line 600