OAI/Combinatorics/UniformKServer/StarActualJumps.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Parameter jumps of the two actual causal minimizers.

  1. def OAI.UniformKServer.StarActualJumps.alphaScale line 19
  2. def OAI.UniformKServer.StarActualJumps.sideSlope line 20
  3. theorem OAI.UniformKServer.StarActualJumps.scale_nonneg line 22
  4. theorem OAI.UniformKServer.StarActualJumps.slope_nonneg line 25
  5. theorem OAI.UniformKServer.StarActualJumps.alpha_scale line 30
  6. theorem OAI.UniformKServer.StarActualJumps.side_slope line 35
  7. theorem OAI.UniformKServer.StarActualJumps.alpha_star_bound line 38
  8. theorem OAI.UniformKServer.StarActualJumps.side_star_bound line 44
  9. theorem OAI.UniformKServer.StarActualJumps.alpha_jump line 50
  10. theorem OAI.UniformKServer.StarActualJumps.side_jump line 67