OAI/Probability/SKFluctuations/InverseMomentIntegrability.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Inverse Moment Integrability.

  1. theorem OAI.SKFluctuations.Hierarchy.inverse_bounded_integrable line 15
  2. theorem OAI.SKFluctuations.Hierarchy.constrained_inverse_bounded_integrable line 35
  3. theorem OAI.SKFluctuations.Hierarchy.pathPairMoment_bounded line 64
  4. theorem OAI.SKFluctuations.orderedPathPair_inverse_integrable line 93
  5. theorem OAI.SKFluctuations.source_radius_gradient_integrable line 109
  6. def OAI.SKFluctuations.Hierarchy.comparisonCapSlope line 143
  7. theorem OAI.SKFluctuations.Hierarchy.comparisonCap_tangent line 146
  8. theorem OAI.SKFluctuations.Hierarchy.control_cone_bounds line 158
  9. theorem OAI.SKFluctuations.Hierarchy.control_cone_small line 177
  10. theorem OAI.SKFluctuations.Hierarchy.inverse_control_feasible line 203
  11. theorem OAI.SKFluctuations.Hierarchy.integral_primitive_lipschitz line 252
  12. theorem OAI.SKFluctuations.Hierarchy.lipschitzOn_real_mul line 271
  13. theorem OAI.SKFluctuations.Hierarchy.lipschitzOn_exp_primitive line 290
  14. def OAI.SKFluctuations.Hierarchy.inverseControlFactor line 317
  15. def OAI.SKFluctuations.Hierarchy.inverseControlTangent line 319
  16. theorem OAI.SKFluctuations.Hierarchy.inverseControlFactor_pos line 322
  17. theorem OAI.SKFluctuations.Hierarchy.inverseControlTangent_initial line 325
  18. theorem OAI.SKFluctuations.Hierarchy.inverseControlTangent_terminal line 328
  19. theorem OAI.SKFluctuations.Hierarchy.inverseControlTangent_ae_derivative line 334
  20. theorem OAI.SKFluctuations.Hierarchy.inverseControlTangent_lipschitz line 357
  21. theorem OAI.SKFluctuations.Hierarchy.control_difference_bound line 396
  22. theorem OAI.SKFluctuations.Hierarchy.bounded_control_competitors line 407
  23. theorem OAI.SKFluctuations.Hierarchy.control_support_order line 484
  24. theorem OAI.SKFluctuations.Hierarchy.control_scalar_multiplier line 516
  25. theorem OAI.SKFluctuations.Hierarchy.control_indicator_optimality line 547
  26. def OAI.SKFluctuations.Hierarchy.controlPlusMeasure line 601
  27. def OAI.SKFluctuations.Hierarchy.controlMinusMeasure line 603
  28. theorem OAI.SKFluctuations.Hierarchy.control_bang_bang line 606