OAI/Combinatorics/UniformKServer/FlexEstimates.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Persistent endpoint interpolation of the noncore ranks and its true parameter error. The endpoints and the tolerance are the manuscript's ones.

  1. def OAI.UniformKServer.FlexEstimates.mix line 18
  2. theorem OAI.UniformKServer.FlexEstimates.mix_range line 20
  3. theorem OAI.UniformKServer.FlexEstimates.rank_mix line 24
  4. def OAI.UniformKServer.FlexEstimates.term line 30
  5. def OAI.UniformKServer.FlexEstimates.estimateFlex line 34
  6. def OAI.UniformKServer.FlexEstimates.trueFlex line 37
  7. theorem OAI.UniformKServer.FlexEstimates.endpoint_range line 40
  8. theorem OAI.UniformKServer.FlexEstimates.term_range line 44
  9. theorem OAI.UniformKServer.FlexEstimates.term_comparison line 57
  10. theorem OAI.UniformKServer.FlexEstimates.flex_comparison line 66
  11. def OAI.UniformKServer.FlexEstimates.flexGap line 85
  12. theorem OAI.UniformKServer.FlexEstimates.flex_nonneg line 88
  13. theorem OAI.UniformKServer.FlexEstimates.gap_bounds line 96
  14. theorem OAI.UniformKServer.FlexEstimates.flex_affine line 116
  15. theorem OAI.UniformKServer.FlexEstimates.relative_error line 127
  16. theorem OAI.UniformKServer.FlexEstimates.parameter_error line 136
  17. theorem OAI.UniformKServer.FlexEstimates.child_slack line 159