OAI/Probability/SKFluctuations/InverseConstraintNonempty.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Inverse Constraint Nonempty.

  1. def OAI.SKFluctuations.Hierarchy.affineInverse line 15
  2. theorem OAI.SKFluctuations.Hierarchy.affineInverse_on line 18
  3. theorem OAI.SKFluctuations.Hierarchy.affineInverse_monotone line 22
  4. theorem OAI.SKFluctuations.Hierarchy.affineInverse_range line 29
  5. def OAI.SKFluctuations.Hierarchy.affineInverseProfile line 42
  6. theorem OAI.SKFluctuations.Hierarchy.affineInverseProfile_feasible line 46
  7. theorem OAI.SKFluctuations.Hierarchy.inverseIntegralConstraints_nonempty_of_affine line 84
  8. theorem OAI.SKFluctuations.Hierarchy.comparisonFloor_le_inv_cube line 102
  9. theorem OAI.SKFluctuations.Hierarchy.comparisonFloor_le_half line 117
  10. theorem OAI.SKFluctuations.Hierarchy.comparisonCap_ge line 125
  11. theorem OAI.SKFluctuations.Hierarchy.comparisonConstraints_nonempty line 133
  12. theorem OAI.SKFluctuations.Hierarchy.comparisonFloor_lower_on line 164
  13. theorem OAI.SKFluctuations.Hierarchy.comparisonFloor_measurable line 184
  14. theorem OAI.SKFluctuations.Hierarchy.comparisonCapSlope_continuous line 188
  15. theorem OAI.SKFluctuations.Hierarchy.comparisonCapSlope_nonneg line 193
  16. theorem OAI.SKFluctuations.Hierarchy.comparisonCapSlope_bound line 199
  17. theorem OAI.SKFluctuations.Hierarchy.comparisonCapSlope_times_le line 207
  18. theorem OAI.SKFluctuations.Hierarchy.comparison_control_bounds line 217
  19. theorem OAI.SKFluctuations.comparison_minimum_potential line 240
  20. theorem OAI.SKFluctuations.cumulativePair_SK_bounds line 323
  21. theorem OAI.SKFluctuations.stepPairDisorder_SK_bounds line 339
  22. theorem OAI.SKFluctuations.pathPairMoment_SK_bounds line 358
  23. theorem OAI.SKFluctuations.orderedPath_SK_bounds line 390
  24. def OAI.SKFluctuations.comparisonStrength line 408
  25. def OAI.SKFluctuations.comparisonLogSlope line 409
  26. def OAI.SKFluctuations.comparisonRadiusField line 410
  27. theorem OAI.SKFluctuations.hasDerivAt_radius_strength line 412
  28. theorem OAI.SKFluctuations.radius_strength_growth line 422
  29. theorem OAI.SKFluctuations.comparisonRadiusField_growth line 439
  30. theorem OAI.SKFluctuations.radius_clock_growth_of_approx line 451
  31. theorem OAI.SKFluctuations.comparison_gradient_slope line 474
  32. theorem OAI.SKFluctuations.comparison_gradient_identity line 483
  33. theorem OAI.SKFluctuations.comparison_gradient_nonneg_geometry line 489
  34. theorem OAI.SKFluctuations.comparison_gradient_contact_mismatch line 515
  35. theorem OAI.SKFluctuations.comparison_minimum_contact_potential line 544