Reference · Lemmas behind operations-research checks
rainbow.math.lemmas.knn-reading
General lemmas: knn reading. The mathematical facts the corresponding checks rest on, each checked by the kernel.
signed/knn-selected-nearer
signed/knn-selected-nearer : (kn-d kn-z : ℕ → ℚ) (kn-n : ℕ) (kn-01 : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx kn-n), kn-z idx · (1 + signed/negate (kn-z idx)) = 0) (kn-top : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx kn-n), kn-z idx · signed/expr-sum-value (fun kn-j => (1 + signed/negate (kn-z kn-j)) · data/Bool.rec (fun x₃ => ℚ) 1 0 (signed/decide-at-most (kn-d idx) (kn-d kn-j))) kn-n = 0) (kn-i : ℕ) (kn-hi : nat/strict-below kn-i kn-n) (kn-j : ℕ) (kn-hj : nat/strict-below kn-j kn-n) (kn-zi : kn-z kn-i = 1) (kn-zj : kn-z kn-j = 0) → kn-d kn-i ≤ kn-d kn-j
+ = signed/add0 = signed/zero1 = signed/one= = signed/equivalent: equality of rational values· = signed/multiplyℕ = data/Natℚ = signed/SignedRational≤ = signed/at-most
signed/knn-majority
signed/knn-majority : (mj-y mj-k mj-c : ℚ) (mj-1 : mj-y · (mj-k + signed/negate mj-c) ≤ 0) (mj-0 : (1 + signed/negate mj-y) · (mj-c + signed/negate mj-k) ≤ 0) → proposition/conjunction (mj-y = 1 → mj-k ≤ mj-c) (mj-y = 0 → mj-c ≤ mj-k)
+ = signed/add0 = signed/zero1 = signed/one= = signed/equivalent: equality of rational values· = signed/multiplyℚ = signed/SignedRational≤ = signed/at-most