OAI/Probability/SKFluctuations/OrderedSKRateDirection.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Ordered S K Rate Direction.

  1. theorem OAI.SKFluctuations.orderedPathPair_mul_integrable line 18
  2. theorem OAI.SKFluctuations.pathPressureRate_ordered_direction line 35
  3. theorem OAI.SKFluctuations.orderedSKPathPressure_hasDerivWithinAt_curve line 99
  4. theorem OAI.SKFluctuations.Hierarchy.curve_interval_integral_hasDerivWithinAt line 144
  5. def OAI.SKFluctuations.realOrderedSKPathPressure line 185
  6. theorem OAI.SKFluctuations.toNNReal_monotoneOn line 189
  7. theorem OAI.SKFluctuations.sampled_orderedSKPressure_eq line 194
  8. theorem OAI.SKFluctuations.orderedSKPressure_samples_tendsto line 213
  9. theorem OAI.SKFluctuations.realOrderedSKPathPressure_hasDerivWithinAt_curve line 241
  10. theorem OAI.SKFluctuations.Hierarchy.partitionSum_error line 293
  11. theorem OAI.SKFluctuations.Hierarchy.partitionSum_tendsto line 309
  12. def OAI.SKFluctuations.pathCompensatedPressure line 328
  13. theorem OAI.SKFluctuations.comp_partitionPoint_monotone line 333
  14. theorem OAI.SKFluctuations.finiteCompensatedPressure_tendsto_path line 339
  15. theorem OAI.SKFluctuations.pathCompensatedPressure_mono line 353
  16. theorem OAI.SKFluctuations.pathCompensatedPressure_lower line 386
  17. theorem OAI.SKFluctuations.compensated_curve_derivative line 412
  18. theorem OAI.SKFluctuations.comparison_gradient_algebra line 478
  19. theorem OAI.SKFluctuations.radius_curve_derivative line 494
  20. theorem OAI.SKFluctuations.Hierarchy.source_velocity_measurable line 563
  21. theorem OAI.SKFluctuations.Hierarchy.source_velocity_bound line 570
  22. theorem OAI.SKFluctuations.Hierarchy.sourceForwardCurve_initial_eq line 591