OAI/Probability/SKFluctuations/ComparisonMinimumRegularRawRatio.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Comparison Minimum Regular Raw Ratio.

  1. theorem OAI.SKFluctuations.eventually_comparison_minimum_raw_ratio_regular line 15
  2. theorem OAI.SKFluctuations.comparison_minimum_finite_raw_ratio line 170
  3. def OAI.SKFluctuations.physicalCutPairPower line 249
  4. theorem OAI.SKFluctuations.physicalCutPairPower_nonneg line 256
  5. theorem OAI.SKFluctuations.physicalCutPairPower_futurePair line 261
  6. theorem OAI.SKFluctuations.eventually_cut_pair_full_moment line 277
  7. theorem OAI.SKFluctuations.physicalCutPairPower_test_measurable line 332
  8. theorem OAI.SKFluctuations.physicalCutPairPower_test_le line 342
  9. theorem OAI.SKFluctuations.physicalCutPairPower_measurable line 358
  10. theorem OAI.SKFluctuations.physicalCutPairPower_swap line 365
  11. def OAI.SKFluctuations.physicalOverlapComponent line 388
  12. theorem OAI.SKFluctuations.sum_physicalOverlapComponent line 394
  13. theorem OAI.SKFluctuations.physicalOverlapComponent_measurable line 406
  14. theorem OAI.SKFluctuations.physicalOverlapComponent_norm_le line 415
  15. theorem OAI.SKFluctuations.normalizedSpin_inner_eq_overlap line 424
  16. def OAI.SKFluctuations.physicalOverlapLayerTerm line 431
  17. theorem OAI.SKFluctuations.physicalOverlapLayerTerm_measurable line 438
  18. theorem OAI.SKFluctuations.physicalOverlapLayerTerm_abs_le line 446
  19. theorem OAI.SKFluctuations.sum_physicalOverlapLayerTerm line 461
  20. def OAI.SKFluctuations.physicalOverlapResidualPairs line 471
  21. theorem OAI.SKFluctuations.physicalOverlap_core_add_residual line 474
  22. theorem OAI.SKFluctuations.Hierarchy.conditionalPathAverage_add_bounded line 498
  23. theorem OAI.SKFluctuations.Hierarchy.integral_conditionalForkTest_add line 531
  24. theorem OAI.SKFluctuations.Hierarchy.integral_conditionalForkTest_fst line 554
  25. theorem OAI.SKFluctuations.Hierarchy.integral_conditionalForkTest_snd line 564
  26. def OAI.SKFluctuations.physicalProjectedOverlapMoment line 587
  27. theorem OAI.SKFluctuations.physicalProjectedOverlapMoment_le line 594