Reference · Lemmas behind operations-research checks

rainbow.math.lemmas.hhi-bounds

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

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

signed/positive-indicator-positive

TheoremFor all inputsNo axiomsSource

signed/positive-indicator-positive :
  (pi-s : ℚ)
  (pi-h : 1 ≤ data/Bool.rec (fun x₄ => ℚ) 1 0 (signed/decide-at-most pi-s 0))
  → 0 < pi-s

0 = signed/zero1 = signed/one< = signed/less-thanℚ = signed/SignedRational≤ = signed/at-most

signed/nested-eq-indicator-cases

TheoremFor all inputsNo axiomsSource

signed/nested-eq-indicator-cases :
  (ne-p ne-c : ℚ)
  → proposition/disjunction (data/Bool.rec (fun x₆₀ => ℚ) 0 (data/Bool.rec (fun x₆₄ => ℚ) 0 1 (signed/decide-at-most ne-c ne-p)) (signed/decide-at-most ne-p ne-c) = 0) (proposition/conjunction (data/Bool.rec (fun x₉₂ => ℚ) 0 (data/Bool.rec (fun x₉₆ => ℚ) 0 1 (signed/decide-at-most ne-c ne-p)) (signed/decide-at-most ne-p ne-c) = 1) (ne-p = ne-c))

0 = signed/zero1 = signed/one= = signed/equivalent: equality of rational valuesℚ = signed/SignedRational

signed/square-deviation-sum

TheoremFor all inputsNo axiomsSource

signed/square-deviation-sum :
  (dv-s : ℕ → ℚ) (dv-n : ℕ) (dv-h : ℚ)
  (dv-sum : signed/expr-sum-value dv-s dv-n = 1)
  (dv-hh : dv-h = signed/expr-sum-value (fun sq-i => dv-s sq-i · dv-s sq-i) dv-n)
  (dv-a : ℚ)
  → signed/expr-sum-value (fun dj => (dv-a + signed/negate (dv-s dj)) · (dv-a + signed/negate (dv-s dj))) dv-n = dv-a · dv-a · signed/from-nnrat (nnrat/make dv-n 0) + dv-h + signed/negate (dv-a + dv-a)

+ = signed/add1 = signed/one= = signed/equivalent: equality of rational values· = signed/multiplyℕ = data/Natℚ = signed/SignedRational

signed/hhi-reciprocal-bound

TheoremFor all inputsNo axiomsSource

signed/hhi-reciprocal-bound :
  (rc-s : ℕ → ℚ) (rc-n : ℕ) (rc-h : ℚ)
  (rc-sum : signed/expr-sum-value rc-s rc-n = 1)
  (rc-hh : rc-h = signed/expr-sum-value (fun sq-i => rc-s sq-i · rc-s sq-i) rc-n)
  → 1 ≤ signed/from-nnrat (nnrat/make rc-n 0) · rc-h

1 = signed/one= = signed/equivalent: equality of rational values· = signed/multiplyℕ = data/Natℚ = signed/SignedRational≤ = signed/at-most

signed/hhi-bounds

TheoremFor all inputsNo axiomsSource

signed/hhi-bounds :
  (bd-s : ℕ → ℚ) (bd-n : ℕ) (bd-h bd-m : ℚ)
  (hs : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx bd-n), 0 ≤ bd-s idx)
  (hsum : signed/expr-sum-value bd-s bd-n = 1)
  (hh : bd-h = signed/expr-sum-value (fun sq-i => bd-s sq-i · bd-s sq-i) bd-n)
  (hm : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx bd-n), bd-s idx ≤ bd-m)
  (hatt : 1 ≤ signed/expr-sum-value (fun at-i => data/Bool.rec (fun x₇ => ℚ) 0 (data/Bool.rec (fun x₁₀ => ℚ) 0 1 (signed/decide-at-most bd-m (bd-s at-i))) (signed/decide-at-most (bd-s at-i) bd-m)) bd-n)
  → proposition/conjunction (bd-m · bd-m ≤ bd-h) (conjunction)
  where conjunction := proposition/conjunction (bd-h ≤ bd-m) (proposition/conjunction (bd-m ≤ 1) (proposition/conjunction (bd-h ≤ 1) (1 ≤ signed/from-nnrat (nnrat/make bd-n 0) · bd-h)))

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