Reference · Lemmas behind operations-research checks

rainbow.math.lemmas.lsq-optimal

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

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

signed/lsq-row-difference

TheoremFor all inputsNo axiomsSource

signed/lsq-row-difference :
  (A : ℕ → ℕ → ℚ) (z x : ℕ → ℚ) (n i : ℕ)
  → signed/expr-sum-value (fun j => A i j · (fun dj => z dj + signed/negate (x dj)) j) n = signed/expr-sum-value (fun j => A i j · z j) n + signed/negate (signed/expr-sum-value (fun j => A i j · x j) n)

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

signed/lsq-residual-change

TheoremFor all inputsNo axiomsSource

signed/lsq-residual-change :
  (A : ℕ → ℕ → ℚ) (b x r z : ℕ → ℚ) (n i : ℕ)
  (hr : r i = signed/expr-sum-value (fun j => A i j · x j) n + signed/negate (b i))
  → signed/expr-sum-value (fun j => A i j · z j) n + signed/negate (b i) = r i + signed/expr-sum-value (fun j => A i j · (fun dj => z dj + signed/negate (x dj)) j) n

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

signed/lsq-square-expansion

TheoremFor all inputsNo axiomsSource

signed/lsq-square-expansion :
  (x y : ℚ)
  → (x + y) · (x + y) = x · x + y · y + (1 + 1) · (x · y)

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

signed/expr-sum-norm-add-expansion

TheoremFor all inputsNo axiomsSource

signed/expr-sum-norm-add-expansion :
  (r d : ℕ → ℚ) (m : ℕ)
  → signed/expr-sum-value (fun i => (r i + d i) · (r i + d i)) m = signed/expr-sum-value (fun sq-i => r sq-i · r sq-i) m + signed/expr-sum-value (fun sq-i => d sq-i · d sq-i) m + (1 + 1) · signed/expr-sum-value (fun dot-i => r dot-i · d dot-i) m

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

signed/lsq-cross-normal

TheoremFor all inputsNo axiomsSource

signed/lsq-cross-normal :
  (A : ℕ → ℕ → ℚ) (r d : ℕ → ℚ) (m n : ℕ)
  → signed/expr-sum-value (fun dot-i => r dot-i · (fun ai => signed/expr-sum-value (fun j => A ai j · d j) n) dot-i) m = signed/expr-sum-value (fun dot-i => d dot-i · (fun nj => signed/expr-sum-value (fun ni => A ni nj · r ni) m) dot-i) n

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

signed/expr-sum-lsq-decomposition

TheoremFor all inputsNo axiomsSource

signed/expr-sum-lsq-decomposition :
  (A : ℕ → ℕ → ℚ) (b x r z : ℕ → ℚ) (m n : ℕ)
  (hr : ∀ (ri : ℕ), ∀ (ri-lt : nat/strict-below ri m), r ri = (fun ri₁ => signed/expr-sum-value (fun j => A ri₁ j · x j) n + signed/negate (b ri₁)) ri)
  → signed/expr-sum-value (fun sq-i => (fun ri => signed/expr-sum-value (fun j => A ri j · z j) n + signed/negate (b ri)) sq-i · (fun ri => signed/expr-sum-value (fun j => A ri j · z j) n + signed/negate (b ri)) sq-i) m = signed/expr-sum-value (fun sq-i => r sq-i · r sq-i) m + signed/expr-sum-value (fun sq-i => (fun ai => signed/expr-sum-value (fun j => A ai j · (fun dj => …⟨1⟩ …⟨1⟩ + …⟨1⟩ …⟨3⟩) j) n) sq-i · (fun ai => signed/expr-sum-value (fun j => A ai j · (fun dj => …⟨1⟩ …⟨1⟩ + …⟨1⟩ …⟨3⟩) j) n) sq-i) m + (1 + 1) · signed/expr-sum-value (fun dot-i => (fun dj => z dj + signed/negate (x dj)) dot-i · (fun nj => signed/expr-sum-value (fun ni => A ni nj · r ni) m) dot-i) n

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

signed/lsq-normal-dot-zero

TheoremFor all inputsNo axiomsSource

signed/lsq-normal-dot-zero :
  (A : ℕ → ℕ → ℚ) (r d : ℕ → ℚ) (m n : ℕ)
  (hn : ∀ (nj : ℕ), ∀ (nj-lt : nat/strict-below nj n), (fun nj₁ => signed/expr-sum-value (fun ni => A ni nj₁ · r ni) m) nj = 0)
  → signed/expr-sum-value (fun dot-i => d dot-i · (fun nj => signed/expr-sum-value (fun ni => A ni nj · r ni) m) dot-i) n = 0

0 = signed/zero= = signed/equivalent: equality of rational values· = signed/multiplyℕ = data/Natℚ = signed/SignedRational

signed/expr-sum-lsq-optimal

TheoremFor all inputsNo axiomsSource

signed/expr-sum-lsq-optimal :
  (A : ℕ → ℕ → ℚ) (b x r z : ℕ → ℚ) (m n : ℕ)
  (hr : ∀ (ri : ℕ), ∀ (ri-lt : nat/strict-below ri m), r ri = (fun ri₁ => signed/expr-sum-value (fun j => A ri₁ j · x j) n + signed/negate (b ri₁)) ri)
  (hn : ∀ (nj : ℕ), ∀ (nj-lt : nat/strict-below nj n), (fun nj₁ => signed/expr-sum-value (fun ni => A ni nj₁ · r ni) m) nj = 0)
  → signed/expr-sum-value (fun sq-i => r sq-i · r sq-i) m ≤ signed/expr-sum-value (fun sq-i => (fun ri => signed/expr-sum-value (fun j => A ri j · z j) n + signed/negate (b ri)) sq-i · (fun ri => signed/expr-sum-value (fun j => A ri j · z j) n + signed/negate (b ri)) sq-i) m

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