OAI/Combinatorics/UniformKServer/SideLinear.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exact affine side-potential coefficients. Their boundedness holds at every compact-domain state, not only at states feasible for the fresh posteriors.

  1. def OAI.UniformKServer.SideLinear.bCoefficient line 17
  2. def OAI.UniformKServer.SideLinear.dCoefficient line 19
  3. theorem OAI.UniformKServer.SideLinear.affine line 22
  4. theorem OAI.UniformKServer.SideLinear.zero line 31
  5. theorem OAI.UniformKServer.SideLinear.bBound line 35
  6. theorem OAI.UniformKServer.SideLinear.dBound line 42