The linear fit: the classical two-equation normal system

Proved

MetodosNumericos.mmq_linear_case

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

least-squaresnumerical-analysis

For the base functions $\\varphi_0 = 1$ and $\\varphi_1(t) = t$ , a coefficient pair $(c_0,c_1)$ minimizes the sum of squared residuals if and only if

c_0(m+1) + c_1\\sum_i x_i = \\sum_i f_i, \\qquad c_0\\sum_i x_i + c_1\\sum_i x_i^2 = \\sum_i x_i f_i,

the normal system of the straight-line fit of §6.1–6.3.

Preamble

import Mathlib
import Definitions.Def_MetodosNumericos_ajusteDefs

Formal statement

namespace MetodosNumericos

theorem mmq_linear_case {m : ℕ} (x f : Fin (m + 1) → ℝ) (c : Fin 2 → ℝ)
    (phi : Fin 2 → ℝ → ℝ) (hphi0 : phi 0 = fun _ => 1) (hphi1 : phi 1 = fun t => t) :
    (∀ d : Fin 2 → ℝ, sqError phi x f c ≤ sqError phi x f d) ↔
      (c 0 * (m + 1 : ℝ) + c 1 * ∑ i : Fin (m + 1), x i = ∑ i : Fin (m + 1), f i ∧
        c 0 * (∑ i : Fin (m + 1), x i) + c 1 * ∑ i : Fin (m + 1), x i ^ 2 =
          ∑ i : Fin (m + 1), x i * f i) := by sorry

end MetodosNumericos

Source

S. R. Freitas, Métodos Numéricos (UFMS, 2000), Cap. 6, §6.1 Caso Linear, pp. 119–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 a natural number $m$ , families $x, f$ of $m+1$ reals, a pair of coefficients $(c_0, c_1)$ and a family $\\varphi$ of two real functions, under the hypotheses that $\\varphi_0$ is the constant function with value $1$ and $\\varphi_1$ is the identity function, the statement is an if-and-only-if between:

for every pair $d = (d_0,d_1)$ of reals, $\\sum_{i=0}^{m}(c_0\\varphi_0(x_i) + c_1\\varphi_1(x_i) - f_i)^2 \\le \\sum_{i=0}^{m}(d_0\\varphi_0(x_i)+d_1\\varphi_1(x_i)-f_i)^2$ ; and
the conjunction of the two equations

c_0\\,(m+1) + c_1\\sum_{i=0}^{m} x_i = \\sum_{i=0}^{m} f_i, \\qquad c_0\\sum_{i=0}^{m} x_i + c_1\\sum_{i=0}^{m} x_i^{2} = \\sum_{i=0}^{m} x_i f_i,

where $m+1$ is the natural number $m+1$ cast into $\\mathbb{R}$ , that is, the number of data points.

No assumption is made that the nodes are distinct; if all $x_i$ coincide the two equations become dependent and both sides of the equivalence are still meaningful.

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