Every solution of the normal system is a global least-squares minimizer

Proved

MetodosNumericos.mmq_normal_system_minimizer

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

least-squaresnumerical-analysis

If the coefficients $c$ satisfy the normal system, then $S(c) \\le S(d)$ for every coefficient vector $d$ . This converse of the source's derivation is what makes the normal system a characterization of the least-squares fit and not merely a necessary condition.

Preamble

import Mathlib
import Definitions.Def_MetodosNumericos_ajusteDefs

Formal statement

namespace MetodosNumericos

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

end MetodosNumericos

Source

S. R. Freitas, Métodos Numéricos (UFMS, 2000), Cap. 6, §6.3, pp. 122–124 (converse of the stated necessary condition).

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$ of $n+1$ real functions, node and data families $x, f$ of $m+1$ reals each, and a coefficient family $c$ of $n+1$ reals, the hypothesis is that for every index $k$ ,

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

The conclusion is that for every coefficient family $d$ of $n+1$ reals,

\\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}.

The comparison is with all coefficient vectors (a global statement), the inequality is non-strict, and no uniqueness is claimed.

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