Lagrange interpolation

[Julek]

No description provided.

[github-actions]

🤖 Gemini PR Summary

This PR implements a structured and computable version of Lagrange interpolation within the CompPoly library. It focuses on integrating these mathematical constructions with Mathlib and establishing the necessary algebraic foundations (module structures) and homomorphism lemmas to ensure formal correctness.

Features

• Module Structure for CPolynomial: Formally defined the module structure for CPolynomial R, including scalar multiplication and the verification of all required module axioms.
• Algebraic Lemmas for toPoly: Introduced new lemmas proving that the toPoly mapping is a homomorphism with respect to finite sums and finite products of computable polynomials.

Refactoring

• Lagrange Interpolation: Replaced the previous raw implementation of Lagrange interpolation with a more structured, computable version. This new implementation is better integrated with Mathlib's hierarchy and includes rigorous formal correctness proofs.

Fixes

• No specific bug fixes were noted in this PR.

Documentation

• No dedicated documentation files were added, though the PR enhances the formal specification of the library through its proof developments.

---

Analysis of Changes

Metric	Count
📝 Files Changed	3
✅ Lines Added	221
❌ Lines Removed	37

---

Lean Declarations

✅ **Removed:** 1 declaration(s)

• def nodal {R : Type*} [Ring R] [BEq R] (n : ℕ) (ω : R) : CPolynomial.Raw R in CompPoly/Univariate/Lagrange.lean

❌ **Added:** 18 declaration(s)

• def smul (r : R) (p : CPolynomial R) : CPolynomial R in CompPoly/Univariate/Basic.lean
• lemma zero_smul : ∀ (x : CPolynomial R), smul 0 x = 0 in CompPoly/Univariate/Basic.lean
• def basisDivisor (xᵢ xⱼ : R) : CPolynomial R in CompPoly/Univariate/Lagrange.lean
• def interpolatePow {n : ℕ} (ω : R) (r : Vector R n) : in CompPoly/Univariate/Lagrange.lean
• lemma cinterpolate_eq_interpolate in CompPoly/Univariate/Lagrange.lean
• lemma cbasisDivisor_eq_basisDivisor {xᵢ xⱼ : R} : in CompPoly/Univariate/Lagrange.lean
• lemma smul_add : ∀ (a : R) (x y : CPolynomial R), smul a (x + y) = smul a x + smul a y in CompPoly/Univariate/Basic.lean
• def basis {ι : Type*} [DecidableEq ι] (s : Finset ι) (x : ι → R) (i : ι) : in CompPoly/Univariate/Lagrange.lean
• lemma toPoly_sum.{u} {R : Type*} [BEq R] [Field R] [LawfulBEq R] {ι : Type u} [DecidableEq ι] in CompPoly/Univariate/ToPoly.lean
• lemma add_smul : ∀ (r s : R) (x : CPolynomial R), smul (r + s) x = smul r x + smul s x in CompPoly/Univariate/Basic.lean
• theorem eq_of_pow_eq_pow_of_lt_orderOf {G : Type*} [Group G] {ω : G} {n : ℕ} in CompPoly/Univariate/Lagrange.lean
• lemma one_smul : ∀ (b : CPolynomial R), smul 1 b = b in CompPoly/Univariate/Basic.lean
• lemma cbasis_eq_basis {ι : Type*} [DecidableEq ι] (s : Finset ι) (x : ι → R) (i : ι) : in CompPoly/Univariate/Lagrange.lean
• lemma coeff_C_mul [Nontrivial R] (p : CPolynomial R) (c : R) : in CompPoly/Univariate/Basic.lean
• lemma eval_interpolatePow_at_node {n : ℕ} {ω : Rˣ} {r : Vector R n} : n < orderOf ω → in CompPoly/Univariate/Lagrange.lean
• lemma smul_zero : ∀ (a : R), smul a 0 = 0 in CompPoly/Univariate/Basic.lean
• lemma mul_smul : ∀ (x y : R) (b : CPolynomial R), smul (x * y) b = smul x (smul y b) in CompPoly/Univariate/Basic.lean
• lemma toPoly_prod.{u} {R : Type*} [BEq R] [Field R] [LawfulBEq R] {ι : Type u} [DecidableEq ι] in CompPoly/Univariate/ToPoly.lean

✏️ **Affected:** 1 declaration(s) (line number changed)

• def interpolate {ι : Type*} [DecidableEq ι] (s : Finset ι) (x : ι → R) : in CompPoly/Univariate/Lagrange.lean moved from L35 to L52

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

🎨 **Style Guide Adherence**

The following lines violate the provided style guide:

• CompPoly/Univariate/Basic.lean:239: "i, j, k, ... : Integers" (The natural number index i should be m, n, or k).
• CompPoly/Univariate/Basic.lean:246: "x, y, z, ... : Elements of a generic type" (Elements a and b of ring R should be x, y, or z).
• CompPoly/Univariate/Basic.lean:803: "x, y, z, ... : Elements of a generic type" (Elements a and b should be x, y, or z).
• CompPoly/Univariate/Basic.lean:810: "x, y, z, ... : Elements of a generic type" (Polynomial element p should be x, y, or z).
• CompPoly/Univariate/Basic.lean:815: "x, y, z, ... : Elements of a generic type" (Element a should be x, y, or z).
• CompPoly/Univariate/Basic.lean:824: "x, y, z, ... : Elements of a generic type" and "p, q, r, ... : Predicates and relations" (Elements a, p, and q should be x, y, or z).
• CompPoly/Univariate/Basic.lean:830: "x, y, z, ... : Elements of a generic type" (Elements a, b, and p should be x, y, or z).
• CompPoly/Univariate/Lagrange.lean:91: "x, y, z, ... : Elements of a generic type" (Elements xᵢ, xⱼ should use standard element variables).
• CompPoly/Univariate/Lagrange.lean:96: "Standard Forms: Use established normal forms (e.g., s.Nonempty instead of s ≠ ∅) to enable dot notation and consistency." (Naming should follow the file's established toPoly_ pattern, i.e., toPoly_basisDivisor).
• CompPoly/Univariate/Lagrange.lean:104: "Line Length: Keep lines under 100 characters."
• CompPoly/Univariate/Lagrange.lean:106: "Standard Forms: Use established normal forms... to enable dot notation and consistency." (Naming should be toPoly_basis).
• CompPoly/Univariate/Lagrange.lean:114: "h, h₁, ... : Assumptions/Hypotheses" (Hypotheses h_order and h_pow should use standard naming convention).
• CompPoly/Univariate/Lagrange.lean:117-119: "Avoid parentheses where possible. Use <| (pipe left) and |> (pipe right) to reduce nesting."
• CompPoly/Univariate/Lagrange.lean:123: "Prefer placing hypotheses to the left of the colon (e.g., (h : P) : Q) rather than using arrows (: P → Q) when the proof introduces them."
• CompPoly/Univariate/Lagrange.lean:124: "m, n, k, ... : Natural numbers" (Natural index i should be m, n, or k).
• CompPoly/Univariate/Lagrange.lean:125: "h, h₁, ... : Assumptions/Hypotheses" (Descriptive name order_ω_lt_n used instead of h).
• CompPoly/Univariate/Lagrange.lean:132: "Line Length: Keep lines under 100 characters."
• CompPoly/Univariate/Lagrange.lean:144-148: "h, h₁, ... : Assumptions/Hypotheses" (Descriptive names h₁, h₂, h₃, h_le, h_eq used instead of standard convention).
• CompPoly/Univariate/ToPoly.lean:355-359: "Indentation: Use 2 spaces for indentation." (The | branches are incorrectly indented).
• CompPoly/Univariate/ToPoly.lean:364-368: "Indentation: Use 2 spaces for indentation." (The | branches are incorrectly indented).

---

📄 **Per-File Summaries**

• CompPoly/Univariate/Basic.lean: This change defines the module structure for CPolynomial R by implementing scalar multiplication and proving the required module axioms.
• CompPoly/Univariate/Lagrange.lean: Replaced the raw implementation of Lagrange interpolation with a structured, computable version integrated with Mathlib and supported by formal correctness proofs.
• CompPoly/Univariate/ToPoly.lean: This change adds lemmas proving that the toPoly mapping commutes with finite sums and products of computable polynomials.

---

Last updated: 2026-02-25 12:33 UTC.

[dhsorens]

I'm very happy with this, thank you @Julek ! I just had some stylistic notes for the sake of consistency throughout the repository. But the code is correct (proven so) and I appreciate the closeness of the syntax and function definition to Mathlib's, distinctly being a Lean style. In conversation with @alexanderlhicks we agreed that the previous version of this was more Rust-y, something we may want later but can wait to develop out properly for when we have an actual use case.

I'm happy for this to be merged, though I will likely want the stylistic notes taken into account either now or later (e.g. in a code cleanup/organisation PR I'm happy to make).

Reviewed for:

• correctness
• style consistency with the rest of CompPoly

[dhsorens]

my personal preference for readability and reuse is to pull each field proof out into named lemmas. should note here that module theory is also implemented in #88 (still WIP) and so we can address stylistic nuances there

[dhsorens]

a note here stylistically, elsewhere in CompPoly we use {R : Type*} which is ofc compatible with the .{u} notation but we may consider keeping things consistent across the board

[alexanderlhicks]

Any chance you could do a pass over the style guide adherence (cf summary workflow)? We made a bit of an effort to clean up CompPoly in this regard and it would be nice to keep it consistent moving forward.

[Julek]

Any chance you could do a pass over the style guide adherence (cf summary workflow)? We made a bit of an effort to clean up CompPoly in this regard and it would be nice to keep it consistent moving forward.

@alexanderlhicks Where can I find this style guide? 😅

[dhsorens]

our summary script uses the style guide from mathlib and what's outlined in CONTRIBUTING.md - if you scroll up there is a drop-down option where it gives feedback on the style guide :)

[dhsorens]

one last comment here - the structure of CompPoly/Univariate is such that the operations are defined e.g. in Basic, with only the necessary lemmas about the operations proved there, and their correctness wrt Mathlib is established in Univariate/ToPoly.lean. The rationale for this is so that if you just need the computable/executable side of CompPoly you only need to import the definitions, where if you want to start proving things about it you then import ToPoly and you have access to all the related theorems/lemmas you could want there from Mathlib.

so my personal preference would be to have ToPoly import Lagrange, and then the theorems such as cBasisDivisorEq, cBasisEq, lagrangeEq, etc establishing correctness move to ToPoly and live e.g. in a section Lagrange within the ImplementationCorrectness section.

wdyt @alexanderlhicks @Julek ? does that seem reasonable? I'm happy to punt this, and just make a note for future discussions