OAI/Probability/SKFluctuations/ComparisonPolynomialRoom.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Comparison Polynomial Room.

  1. theorem OAI.SKFluctuations.comparisonCap_cubic_ratio line 15
  2. theorem OAI.SKFluctuations.eventually_comparisonCap_room line 35
  3. theorem OAI.SKFluctuations.comparison_strength_denominator line 70
  4. theorem OAI.SKFluctuations.comparisonCap_ge_rpow line 80
  5. theorem OAI.SKFluctuations.comparisonCap_strength_ratio line 98
  6. theorem OAI.SKFluctuations.eventually_comparisonBalancedRawParameters line 124
  7. theorem OAI.SKFluctuations.comparisonTravel_log_bound line 176
  8. theorem OAI.SKFluctuations.comparisonTravel_ratio_bound line 200
  9. theorem OAI.SKFluctuations.eventually_comparisonTravel_small line 236
  10. theorem OAI.SKFluctuations.eventually_comparisonSmallMass_small line 269
  11. theorem OAI.SKFluctuations.eventually_comparisonLowerScale_depth line 284
  12. theorem OAI.SKFluctuations.eventually_comparison_regular_band_margins line 320
  13. theorem OAI.SKFluctuations.finite_dyadic_small_cover line 455
  14. structure OAI.SKFluctuations.RawFutureCutFamily line 498
  15. theorem OAI.SKFluctuations.rawFutureCutFamily_nonempty line 512