OAI/Combinatorics/UniformKServer/AlphaEmptyLinear.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The true affine potential extended to empty domains.

  1. def OAI.UniformKServer.AlphaEmptyLinear.coefficient line 17
  2. theorem OAI.UniformKServer.AlphaEmptyLinear.affine line 21
  3. theorem OAI.UniformKServer.AlphaEmptyLinear.bound line 28
  4. theorem OAI.UniformKServer.AlphaEmptyLinear.difference line 34