OAI/Probability/SKFluctuations/InverseConstraintQuantile.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Inverse Constraint Quantile.

  1. theorem OAI.SKFluctuations.Hierarchy.inverseConstraint_lower_slope line 15
  2. theorem OAI.SKFluctuations.Hierarchy.inverseConstraint_strictMonoOn line 28
  3. theorem OAI.SKFluctuations.Hierarchy.inverseConstraint_coSlope line 37
  4. def OAI.SKFluctuations.Hierarchy.inverseConstraintMap line 50
  5. theorem OAI.SKFluctuations.Hierarchy.inverseConstraintMap_surjective line 55
  6. def OAI.SKFluctuations.Hierarchy.inverseConstraintOrderIso line 65
  7. def OAI.SKFluctuations.Hierarchy.constrainedQuantile line 74
  8. theorem OAI.SKFluctuations.Hierarchy.constrainedQuantile_spec line 81
  9. theorem OAI.SKFluctuations.Hierarchy.constrainedQuantile_lipschitz line 89
  10. theorem OAI.SKFluctuations.Hierarchy.constrainedQuantile_joint_continuous line 116
  11. def OAI.SKFluctuations.Hierarchy.constrainedQuantileMap line 145
  12. theorem OAI.SKFluctuations.Hierarchy.constrainedQuantileMap_continuous line 153
  13. theorem OAI.SKFluctuations.Hierarchy.constrainedQuantileMap_compact line 161
  14. theorem OAI.SKFluctuations.Hierarchy.inverse_perturbation_quotient line 180
  15. theorem OAI.SKFluctuations.Hierarchy.inverse_affine_displacement line 211
  16. theorem OAI.SKFluctuations.Hierarchy.inverse_affine_hasDerivWithinAt line 224
  17. theorem OAI.SKFluctuations.Hierarchy.ae_inverse_pullback line 260
  18. theorem OAI.SKFluctuations.Hierarchy.inverse_affine_ae_derivative line 288
  19. def OAI.SKFluctuations.Hierarchy.sourceInverseConstraints line 328
  20. theorem OAI.SKFluctuations.Hierarchy.sourceInverseConstraints_monotone line 332
  21. def OAI.SKFluctuations.Hierarchy.sourceInverseExtension line 344
  22. theorem OAI.SKFluctuations.Hierarchy.sourceInverseExtension_on line 366
  23. theorem OAI.SKFluctuations.Hierarchy.sourceInverseExtension_mem line 373
  24. def OAI.SKFluctuations.Hierarchy.sourceInverseCurve line 416
  25. theorem OAI.SKFluctuations.Hierarchy.sourceInverseCurve_on line 423
  26. def OAI.SKFluctuations.Hierarchy.sourceForwardCurve line 428
  27. theorem OAI.SKFluctuations.Hierarchy.sourceForwardCurve_mem line 432
  28. theorem OAI.SKFluctuations.Hierarchy.sourceForwardCurve_equation line 437
  29. theorem OAI.SKFluctuations.Hierarchy.sourceForwardCurve_initial line 466
  30. theorem OAI.SKFluctuations.Hierarchy.sourceForwardCurve_continuous line 470
  31. theorem OAI.SKFluctuations.Hierarchy.sourceForwardCurve_displacement line 475
  32. theorem OAI.SKFluctuations.Hierarchy.sourceForwardCurve_ae_derivative line 487
  33. theorem OAI.SKFluctuations.Hierarchy.inverse_velocity_measurable line 519
  34. theorem OAI.SKFluctuations.Hierarchy.inverse_velocity_bound line 525
  35. theorem OAI.SKFluctuations.Hierarchy.bounded_measurable_intervalIntegrable line 539
  36. def OAI.SKFluctuations.Hierarchy.omittedCurve line 557
  37. theorem OAI.SKFluctuations.Hierarchy.omittedCurve_measurable line 560
  38. theorem OAI.SKFluctuations.Hierarchy.omittedCurve_bound line 565
  39. theorem OAI.SKFluctuations.Hierarchy.omittedCurve_integrable line 572
  40. theorem OAI.SKFluctuations.Hierarchy.omittedCurve_displacement line 582
  41. theorem OAI.SKFluctuations.Hierarchy.omittedCurve_hasDerivWithinAt line 596
  42. theorem OAI.SKFluctuations.Hierarchy.omittedCurve_rate_integrable line 610