OAI/Combinatorics/UniformKServer/AdaptiveAlphaLinear.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exact affine old-state alpha coefficients on changing active domains. These are computed from the genuine regular/marked improper primitives. Their uniform bound is used before, not after, testing refresh events.

  1. def OAI.UniformKServer.ProportionParameters.coefficient line 19
  2. theorem OAI.UniformKServer.ProportionParameters.affine line 28
  3. def OAI.UniformKServer.AdaptiveAlphaLinear.coefficient line 74
  4. theorem OAI.UniformKServer.AdaptiveAlphaLinear.affine line 77
  5. theorem OAI.UniformKServer.AdaptiveAlphaLinear.bound line 88
  6. theorem OAI.UniformKServer.AdaptiveAlphaLinear.filtering line 98