OAI/Probability/SKFluctuations/RealSKPressureL1.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Real S K Pressure L1.

  1. theorem OAI.SKFluctuations.realOrderedSKPathPressure_l1_comparison line 15
  2. theorem OAI.SKFluctuations.intervalIntegral_abs_le_unit_bound line 42
  3. theorem OAI.SKFluctuations.realOrderedSKPathPressure_uniform_comparison line 53
  4. def OAI.SKFluctuations.Hierarchy.omittedExtension line 82
  5. theorem OAI.SKFluctuations.Hierarchy.omittedExtension_before line 85
  6. theorem OAI.SKFluctuations.Hierarchy.omittedExtension_on line 89
  7. theorem OAI.SKFluctuations.Hierarchy.omittedExtension_intervalIntegrable line 93
  8. theorem OAI.SKFluctuations.Hierarchy.omittedExtension_dist line 99
  9. theorem OAI.SKFluctuations.Hierarchy.omittedExtension_integral_dist line 107
  10. theorem OAI.SKFluctuations.Hierarchy.omittedExtension_integral_continuous line 116
  11. def OAI.SKFluctuations.coordinateObjective line 132
  12. theorem OAI.SKFluctuations.coordinateObjective_continuous line 138
  13. def OAI.SKFluctuations.constrainedCoefficient line 174
  14. theorem OAI.SKFluctuations.constrainedCoefficient_continuous line 181
  15. def OAI.SKFluctuations.inverseCompensatedPressure line 205
  16. theorem OAI.SKFluctuations.inverseCompensatedPressure_eq line 212
  17. theorem OAI.SKFluctuations.inverseCompensatedPressure_continuous line 235
  18. theorem OAI.SKFluctuations.inverseCompensatedPressure_minimum line 253
  19. theorem OAI.SKFluctuations.source_coefficient_curve line 298
  20. theorem OAI.SKFluctuations.source_objective_curve_derivative line 306
  21. theorem OAI.SKFluctuations.Hierarchy.lipschitz_interval_integral_image line 390
  22. theorem OAI.SKFluctuations.Hierarchy.inverse_gradient_substitution line 447
  23. def OAI.SKFluctuations.Hierarchy.radiusComparisonGradient line 473
  24. theorem OAI.SKFluctuations.Hierarchy.omitted_interval_integral line 476
  25. theorem OAI.SKFluctuations.Hierarchy.inverseConstraint_image line 487
  26. theorem OAI.SKFluctuations.Hierarchy.comparison_gradient_substitution line 498
  27. theorem OAI.SKFluctuations.Hierarchy.right_derivative_nonneg line 536
  28. theorem OAI.SKFluctuations.source_coefficient_initial line 565
  29. theorem OAI.SKFluctuations.source_objective_initial line 572
  30. theorem OAI.SKFluctuations.source_minimum_first_variation line 585