rainbow.math.lemmas.minimax-regret

Lemmas behind operations-research checks src/rainbow/math/lemmas/minimax_regret.clj0 definitions, 1 theorems

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

signed/indicator-witness-bound

TheoremFor all inputsNo axiomsSource

signed/indicator-witness-bound :
  (I F : ℕ → ℚ) (c R : ℚ) (n : ℕ)
  (hI : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), proposition/disjunction (I idx = 0) (proposition/conjunction (I idx = 1) (c ≤ F idx)))
  (hsum : 1 ≤ signed/expr-sum-value (fun si => I si) n)
  (hb : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), F idx ≤ R)
  → c ≤ R

0 = signed/zero1 = signed/one= = signed/equivalent: equality of rational valuesℕ = data/Natℚ = signed/SignedRational≤ = signed/at-most