Existence and uniqueness of the fit when the Gram matrix is invertible

Proved

MetodosNumericos.mmq_unique_minimizer

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

least-squaresnumerical-analysis

If the Gram matrix $a_{kj} = \\sum_i \\varphi_k(x_i)\\varphi_j(x_i)$ has nonzero determinant, then there is exactly one coefficient vector minimizing the sum of squared residuals. This supplies the hypothesis under which the source's assumption that $S$ attains a minimum is justified.

Preamble

import Mathlib
import Definitions.Def_MetodosNumericos_ajusteDefs

Formal statement

namespace MetodosNumericos

theorem mmq_unique_minimizer {m n : ℕ} (phi : Fin (n + 1) → ℝ → ℝ)
    (x f : Fin (m + 1) → ℝ) (hgram : IsUnit (gramMatrix phi x).det) :
    ∃! c : Fin (n + 1) → ℝ, ∀ 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, p. 122 ("Vamos supor que a função S tenha um ponto de mínimo").

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 and node and data families $x, f$ of $m+1$ reals, the hypothesis is that the determinant of the $(n+1)\\times(n+1)$ matrix with entries $\\sum_{i=0}^{m}\\varphi_k(x_i)\\varphi_j(x_i)$ is invertible in $\\mathbb{R}$ , which for real numbers means nonzero.

The conclusion is that there exists exactly one coefficient family $c$ of $n+1$ reals with the property 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 .

Uniqueness is uniqueness of the minimizing coefficient vector itself, not of the fitted function; existence is asserted, not merely uniqueness.

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