The Lagrange formula reproduces the tabulated values

Proved

MetodosNumericos.lagrange_interpolates

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

interpolationnumerical-analysis

For pairwise distinct nodes, the Lagrange sum $P_n(t) = \\sum_i f_i L_i(t)$ satisfies $P_n(x_i) = f_i$ for every node $x_i$ .

Preamble

import Mathlib
import Definitions.Def_MetodosNumericos_interpolacaoDefs

Formal statement

namespace MetodosNumericos

theorem lagrange_interpolates {n : ℕ} (xs fs : Fin (n + 1) → ℝ)
    (hxs : Function.Injective xs) (i : Fin (n + 1)) :
    lagrangeInterp xs fs (xs i) = fs i := by sorry

end MetodosNumericos

Source

S. R. Freitas, Métodos Numéricos (UFMS, 2000), Cap. 7, §7.3, pp. 138–140.

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 $n$ , families $x$ and $f$ of $n+1$ reals with $i \\mapsto x_i$ injective, and an index $i$ , the statement asserts the equality

\\sum_{k=0}^{n} f_k \\prod_{j \\neq k} \\frac{x_i - x_j}{x_k - x_j} \\;=\\; f_i .

The injectivity hypothesis is what makes the denominators nonzero; without it the total-division convention would make some factors vanish. The claim is made for each index separately, the index being an argument of the statement.

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