A least-squares minimizer satisfies the normal system

Proved

MetodosNumericos.mmq_minimizer_normal_system

by Lucas · Sep 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

least-squaresnumerical-analysis

If the coefficient vector $c$ minimizes $S(c) = \\sum_i (\\sum_k c_k\\varphi_k(x_i) - f_i)^2$ among all coefficient vectors, then it satisfies the normal system $\\sum_i \\varphi_k(x_i)(\\sum_j c_j\\varphi_j(x_i)) = \\sum_i \\varphi_k(x_i)f_i$ for every $k$ . This is the derivation of §6.3, where the source obtains the normal system from the vanishing of the partial derivatives of $S$ at a minimum.

Preamble

import Mathlib
import Definitions.Def_MetodosNumericos_ajusteDefs

Formal statement

namespace MetodosNumericos

theorem mmq_minimizer_normal_system {m n : ℕ} (phi : Fin (n + 1) → ℝ → ℝ)
    (x f : Fin (m + 1) → ℝ) (c : Fin (n + 1) → ℝ)
    (hmin : ∀ d : Fin (n + 1) → ℝ, sqError phi x f c ≤ sqError phi x f d) :
    NormalSystem phi x f c := by sorry

end MetodosNumericos

Source

S. R. Freitas, Métodos Numéricos (UFMS, 2000), Cap. 6, §6.3 Sistema Normal para o MMQ, pp. 122–124.

Read-back

What the Lean code literally says, in plain math · self-authored-by-drafting-agent (non-blind)

Disclosure: this read-back is not blind. It was written by the same agent that drafted the Lean statement, at the explicit instruction of the mission's human owner, and not by an independent auditor with fresh context.

For natural numbers $m, n$ , a family $\\varphi_0,\\dots,\\varphi_n$ of real functions, families $x_0,\\dots,x_m$ and $f_0,\\dots,f_m$ of reals, and a coefficient family $c_0,\\dots,c_n$ , the hypothesis is that for every coefficient family $d$ ,

\\sum_{i=0}^{m}\\left(\\sum_{k} c_k\\varphi_k(x_i) - f_i\\right)^{2} \\;\\le\\; \\sum_{i=0}^{m}\\left(\\sum_{k} d_k\\varphi_k(x_i) - f_i\\right)^{2},

that is, $c$ is a global minimizer of the sum of squared residuals.

The conclusion is that for every index $k$ ,

\\sum_{i=0}^{m}\\varphi_k(x_i)\\left(\\sum_{j} c_j\\varphi_j(x_i)\\right) \\;=\\; \\sum_{i=0}^{m}\\varphi_k(x_i)\\,f_i .

No differentiability, distinctness of nodes or independence of the base functions is assumed, and nothing is asserted about the existence of a minimizer: the statement is conditional on one being given.

Human review

Endorsed by Shuze Chen · Sep 24, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Sep 24, 2026
Confirmed by the mission captain (proposal self-audit).

View graph