OAI/Combinatorics/UniformKServer/OfflineDynamic.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact rational minimization used by uniform-computation Section 02, Proposition prop:finite-table, paragraph "Exact rational attainment". An affine row is constrained to be ≤ 0. The last coordinate is the nonnegative objective a; all other coordinates are eliminated in order. The algorithm is executable rational arithmetic; no real optimization oracle.

  1. def OAI.UniformKServer.OfflineDynamic.minimum line 9
  2. def OAI.UniformKServer.OfflineDynamic.optRat line 12
  3. theorem OAI.UniformKServer.OfflineDynamic.minimum_le line 16
  4. theorem OAI.UniformKServer.OfflineDynamic.minimum_attained line 19
  5. theorem OAI.UniformKServer.OfflineDynamic.optRat_attained line 24
  6. theorem OAI.UniformKServer.OfflineDynamic.optRat_lower line 34
  7. theorem OAI.UniformKServer.OfflineDynamic.offline_eq_optRat line 45