Reference · Lemmas behind operations-research checks

rainbow.math.lemmas.game-value

Lemmas behind operations-research checkssrc/rainbow/math/lemmas/game_value.clj0 definitions, 5 theorems

General lemmas: game value. The mathematical facts the corresponding checks rest on, each checked by the kernel.

signed/game-payoff-at-most-value :
  (A : ℕ → ℕ → ℚ) (x y : ℕ → ℚ) (v : ℚ) (m n : ℕ)
  (rows : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx m), signed/expr-sum-value (fun j => A idx j · y j) n ≤ v)
  (xn : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx m), 0 ≤ x idx)
  (xs : signed/expr-sum-value x m = 1)
  → signed/expr-sum-value (fun i => x i · signed/expr-sum-value (fun j => A i j · y j) n) m ≤ v

signed/game-value-at-most-column-form :
  (A : ℕ → ℕ → ℚ) (x y : ℕ → ℚ) (v : ℚ) (m n : ℕ)
  (columns : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), v ≤ signed/expr-sum-value (fun i => x i · A i idx) m)
  (yn : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), 0 ≤ y idx)
  (ys : signed/expr-sum-value y n = 1)
  → v ≤ signed/expr-sum-value (fun j => signed/expr-sum-value (fun i => x i · A i j) m · y j) n

signed/game-payoff-column-form :
  (A : ℕ → ℕ → ℚ) (x y : ℕ → ℚ) (m n : ℕ)
  → signed/expr-sum-value (fun i => x i · signed/expr-sum-value (fun j => A i j · y j) n) m = signed/expr-sum-value (fun j => signed/expr-sum-value (fun i => x i · A i j) m · y j) n

signed/game-value-at-most-payoff :
  (A : ℕ → ℕ → ℚ) (x y : ℕ → ℚ) (v : ℚ) (m n : ℕ)
  (columns : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), v ≤ signed/expr-sum-value (fun i => x i · A i idx) m)
  (yn : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), 0 ≤ y idx)
  (ys : signed/expr-sum-value y n = 1)
  → v ≤ signed/expr-sum-value (fun i => x i · signed/expr-sum-value (fun j => A i j · y j) n) m

signed/game-payoff-equivalent-value :
  (A : ℕ → ℕ → ℚ) (x y : ℕ → ℚ) (v : ℚ) (m n : ℕ)
  (xn : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx m), 0 ≤ x idx)
  (xs : signed/expr-sum-value x m = 1)
  (yn : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), 0 ≤ y idx)
  (ys : signed/expr-sum-value y n = 1)
  (columns : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), v ≤ signed/expr-sum-value (fun i => x i · A i idx) m)
  (rows : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx m), signed/expr-sum-value (fun j => A idx j · y j) n ≤ v)
  → signed/expr-sum-value (fun i => x i · signed/expr-sum-value (fun j => A i j · y j) n) m = v