OAI/Combinatorics/UniformKServer/AnchorRamp.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Exact clipped ramp and retained-heavy-anchor release. All integrals here are finite weighted sums on the original finite metric.

  1. def OAI.UniformKServer.AnchorRamp.ramp line 16
  2. theorem OAI.UniformKServer.AnchorRamp.range line 18
  3. theorem OAI.UniformKServer.AnchorRamp.zero line 23
  4. theorem OAI.UniformKServer.AnchorRamp.one line 28
  5. theorem OAI.UniformKServer.AnchorRamp.lipschitz line 33
  6. def OAI.UniformKServer.AnchorRamp.value line 44
  7. theorem OAI.UniformKServer.AnchorRamp.value_range line 46
  8. theorem OAI.UniformKServer.AnchorRamp.change line 48
  9. def OAI.UniformKServer.AnchorRamp.ball line 73
  10. def OAI.UniformKServer.AnchorRamp.mass line 74
  11. theorem OAI.UniformKServer.AnchorRamp.inner_change line 77
  12. theorem OAI.UniformKServer.AnchorRamp.integral_drop line 89
  13. theorem OAI.UniformKServer.AnchorRamp.payment line 113