OAI/Probability/SKFluctuations/PhysicalFiniteRawCover.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Physical Finite Raw Cover.

  1. def OAI.SKFluctuations.PhysicalRawWindowAt line 15
  2. theorem OAI.SKFluctuations.partitionPoint_length line 31
  3. theorem OAI.SKFluctuations.sampledFieldDuration_total line 37
  4. theorem OAI.SKFluctuations.physicalRawWindowCover_of_finite line 49
  5. theorem OAI.SKFluctuations.eventually_physicalRawWindowCover_of_finite line 67
  6. theorem OAI.SKFluctuations.comparison_minimum_retained_raw_band line 107
  7. theorem OAI.SKFluctuations.eventually_comparison_minimum_raw_moment_of_finite_margins line 252
  8. theorem OAI.SKFluctuations.exists_rawWindowDepth line 394
  9. theorem OAI.SKFluctuations.rawWindowLogFactor line 432
  10. theorem OAI.SKFluctuations.eventually_rawWindow_scalar_margin line 451
  11. theorem OAI.SKFluctuations.balanced_first_layer line 479
  12. theorem OAI.SKFluctuations.eventually_balancedRawParameters line 492
  13. theorem OAI.SKFluctuations.comparisonLowerScale_pos line 539
  14. theorem OAI.SKFluctuations.comparisonSmallMass_pos line 542
  15. theorem OAI.SKFluctuations.comparison_scale_ratios line 545
  16. theorem OAI.SKFluctuations.comparison_cubic_margin line 566
  17. theorem OAI.SKFluctuations.comparisonCap_ratio line 604