OAI/Probability/SKFluctuations/RadiusGridCount.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Radius Grid Count.

  1. def OAI.SKFluctuations.Hierarchy.radiusGridCount line 21
  2. theorem OAI.SKFluctuations.Hierarchy.lt_radiusGridCount line 24
  3. theorem OAI.SKFluctuations.Hierarchy.radiusGridCount_le line 35
  4. theorem OAI.SKFluctuations.Hierarchy.radiusGridCount_endpoint line 41
  5. theorem OAI.SKFluctuations.Hierarchy.radiusGridCount_sum line 52
  6. def OAI.SKFluctuations.Hierarchy.radiusSquareIntegral line 76
  7. theorem OAI.SKFluctuations.Hierarchy.boundedMartingale_radiusSquareIntegral_moment line 82
  8. theorem OAI.SKFluctuations.Hierarchy.radiusSquareIntegral_ae_nonneg line 175
  9. theorem OAI.SKFluctuations.Hierarchy.boundedMartingale_radiusSquareIntegral_Lp line 185
  10. def OAI.SKFluctuations.actualRadiusSquareIntegral line 210
  11. theorem OAI.SKFluctuations.actualRadiusSquareIntegral_Lp line 221
  12. theorem OAI.SKFluctuations.Hierarchy.radiusSquareIntegral_measurable line 247
  13. theorem OAI.SKFluctuations.Hierarchy.radiusSquareIntegral_ae_bound line 258
  14. theorem OAI.SKFluctuations.Hierarchy.radiusSquareIntegral_power_integrable line 266
  15. def OAI.SKFluctuations.Hierarchy.nearPairMomentConstant line 277
  16. theorem OAI.SKFluctuations.Hierarchy.nearPairMomentConstant_nonneg line 279
  17. theorem OAI.SKFluctuations.Hierarchy.boundedMartingale_nearPairProduct_moment line 285
  18. theorem OAI.SKFluctuations.Hierarchy.boundedMartingale_nearPairProduct_Lp line 341
  19. theorem OAI.SKFluctuations.actualNearPairProduct_Lp line 375