diff --git a/Complexity.lean b/Complexity.lean index 51608e7cb..e1ae2c26f 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2685,6 +2685,7 @@ public import Complexity.Foundations.Data.Polynomial.ParityAmplifier public import Complexity.Foundations.Data.Polynomial.ParityAmplifierDegree public import Complexity.Foundations.Data.Polynomial.SignQueries public import Complexity.Foundations.Data.Polynomial.StagedJetArithmetic +public import Complexity.Foundations.Data.Polynomial.TaperedHermite public import Complexity.Foundations.Data.Rat.Basic public import Complexity.Foundations.Data.Seq.Computation public import Complexity.Foundations.Data.Set.Card diff --git a/Complexity/Foundations/Data/Polynomial/HermiteInterpolation.lean b/Complexity/Foundations/Data/Polynomial/HermiteInterpolation.lean index 7c42d723f..6ee65b63d 100644 --- a/Complexity/Foundations/Data/Polynomial/HermiteInterpolation.lean +++ b/Complexity/Foundations/Data/Polynomial/HermiteInterpolation.lean @@ -11,45 +11,73 @@ public import Complexity.Init public import Mathlib.Algebra.Algebra.Rat public import Mathlib.Algebra.Polynomial.Taylor public import Mathlib.LinearAlgebra.Matrix.Determinant.Basic +public import Mathlib.RingTheory.PowerSeries.Inverse +public import Mathlib.RingTheory.PowerSeries.Trunc import Mathlib.LinearAlgebra.Matrix.ToLinearEquiv import Mathlib.RingTheory.Polynomial.Basic /-! -# Confluent Hermite interpolation from Taylor jets - -A polynomial of degree less than `Q * J` is determined by its first `J` Taylor coefficients at each -of `Q` nodes, provided the nodes differ by units. Over a commutative ring `R`, the order-`J` Taylor -jet of `p` at nodes `t : Fin Q → R` is the family of coefficients -`(Polynomial.taylor (t i) p).coeff j = [z ^ j] p (t i + z)`, for `i < Q` and `j < J` -(`Polynomial.taylorJet`). This file proves - -* uniqueness: a polynomial of degree less than `Q * J` whose jet vanishes is zero, over any - commutative ring whose nodes have unit differences (`Polynomial.eq_zero_of_taylorJet_eq_zero`); -* reconstruction: for integer nodes, the integer confluent Vandermonde matrix - `Polynomial.hermiteMatrix` maps the coefficient vector to the jet, it is nonsingular when the - nodes are distinct, and Cramer's rule expresses each coefficient through two determinants - (`Polynomial.det_hermiteMatrix_mul_coeff`). Over a `ℚ`-algebra this recovers every coefficient, - and in particular the value at `0`, as a rational combination of the jet - (`Polynomial.eval_zero_eq_of_taylorJet`). +# Confluent Hermite interpolation + +A polynomial of degree less than `∑ i, J i` is determined by its first `J i` Taylor coefficients +at each node `t i`, provided the nodes differ by units. This file proves this with node-varying +multiplicities `J : ι → ℕ` over a finite set of nodes `s`, in two forms, over any commutative ring +whose nodes have unit differences: + +* uniqueness: a polynomial of degree less than `∑ i ∈ s, J i` divisible by every `(X - t i) ^ J i` + is zero (`Polynomial.eq_zero_of_forall_X_sub_C_pow_dvd`); +* the Chinese-remainder form: such a polynomial is `p = ∑ i ∈ s, E_i * r_i`, where the Hermite + basis polynomial `E_i = ∏_{j ≠ i} ((X - t j) / (t i - t j)) ^ J j` (`Polynomial.hermiteBasis`) is + `1` at `t i` and vanishes to order `J j` at the other nodes, and `r_i` is the truncation below + order `J i` of the local quotient `p / E_i` at `t i` + (`Polynomial.eq_sum_hermiteBasis_mul_of_dvd`). The local quotient is taken in the scaled + coordinate `T = t i + α z` for a unit `α` (`Polynomial.hermiteQuotient`), so `r_i` depends only on + the first `J i` coefficients of `p (t i + α z)` + (`Polynomial.eq_sum_hermiteBasis_mul_hermiteQuotient`, + `Polynomial.eval_eq_sum_hermiteBasis_mul_hermiteQuotient`). + +For a uniform multiplicity `J` at `Q` nodes `t : Fin Q → R`, the order-`J` Taylor jet is the +family of coefficients `(Polynomial.taylor (t i) p).coeff j = [z ^ j] p (t i + z)`, for `i < Q` +and `j < J` (`Polynomial.taylorJet`), and uniqueness specializes to +`Polynomial.eq_zero_of_taylorJet_eq_zero`. For integer nodes, the integer confluent Vandermonde +matrix `Polynomial.hermiteMatrix` maps the coefficient vector to the jet, it is nonsingular when the +nodes are distinct, and Cramer's rule expresses each coefficient through two determinants +(`Polynomial.det_hermiteMatrix_mul_coeff`). Over a `ℚ`-algebra this recovers every coefficient, +and in particular the value at `0`, as a rational combination of the jet +(`Polynomial.eval_zero_eq_of_taylorJet`). The coefficient of `X ^ u` is indexed by `c : Fin Q × Fin J` with `u = finProdFinEquiv c`, so the Hermite matrix is square over `Fin Q × Fin J`. Its entry in row `(i, j)` and column `c` is `(u choose j) * t i ^ (u - j)`, the coefficient of `z ^ j` in `(t i + z) ^ u`; it vanishes for `u < j` because the binomial does. -This is the interpolation step of the subexponential counting algorithm of [OpenAI2026ETH] -(§3.4 and Appendix B.3): the count is the value at `0` of a polynomial `H` of degree less than -`Q * J`, and only Taylor coefficients of `H` at the nodes `1, …, Q` are computed. Ordinary -Lagrange interpolation (`Lagrange.interpolate`) is the case `J = 1`. +This is the interpolation step of the subexponential counting algorithms of [OpenAI2026ETH]. In +§3.4 and Appendix B.3 the count is the value at `0` of a polynomial `H` of degree less than `Q * J`, +and only Taylor coefficients of `H` at the nodes `1, …, Q` are computed. The tapered recovery of +Lemma D.5 (§D.4.4, pp. 60–61) uses node-varying multiplicities and the Chinese-remainder form, +equation (D.9), with `α = 2 ^ (a + 1)`. Ordinary Lagrange interpolation (`Lagrange.interpolate`) +is the case of multiplicity `1`. ## Main definitions +* `Polynomial.hermiteBasis`: the Hermite basis polynomial `E_i` of node-varying multiplicities. +* `Polynomial.hermiteQuotient`: the truncated local quotient `(P / E_i (t i + α z)) mod z ^ J i`. * `Polynomial.taylorJet`: the order-`J` Taylor jet at `Q` nodes, as a linear map. * `Polynomial.hermiteMatrix`: the integer confluent Vandermonde matrix of integer nodes. ## Main results -* `Polynomial.eq_zero_of_taylorJet_eq_zero`, `Polynomial.eq_of_taylorJet_eq`: uniqueness. +* `Polynomial.eq_zero_of_forall_X_sub_C_pow_dvd`: uniqueness with node-varying multiplicities. +* `Polynomial.eq_sum_hermiteBasis_mul_of_dvd`: the Chinese-remainder form for any local factors + satisfying the local congruences. +* `Polynomial.hermiteQuotient_eq_of_X_pow_dvd`, `Polynomial.X_pow_dvd_sub_mul_hermiteQuotient`: the + Hermite quotient is the unique polynomial of degree less than `J i` satisfying the local + congruence. +* `Polynomial.eq_sum_hermiteBasis_mul_hermiteQuotient`, + `Polynomial.eval_eq_sum_hermiteBasis_mul_hermiteQuotient`: reconstruction from scaled local + jets, equation (D.9) of [OpenAI2026ETH] at `0`. +* `Polynomial.eq_zero_of_taylorJet_eq_zero`, `Polynomial.eq_of_taylorJet_eq`: uniqueness for a + uniform multiplicity. * `Polynomial.hermiteMatrix_mulVec`: the Hermite matrix maps coefficients to the jet. * `Polynomial.det_hermiteMatrix_ne_zero`: it is nonsingular at distinct integer nodes. * `Polynomial.det_hermiteMatrix_mul_coeff`: Cramer's rule for the coefficients, over any @@ -70,7 +98,234 @@ open Finset Matrix variable {R : Type*} [CommRing R] {Q J : ℕ} -/-! ### Taylor jets and uniqueness -/ +/-! ### Node-varying multiplicities -/ + +section Multiplicities + +variable {ι : Type*} {s : Finset ι} {t : ι → R} {J : ι → ℕ} + +/-- `(X - r) ^ n` divides `p` exactly when the first `n` Taylor coefficients of `p` at `r` +vanish. -/ +theorem X_sub_C_pow_dvd_iff_taylor_coeff {r : R} {n : ℕ} {p : R[X]} : + (X - C r) ^ n ∣ p ↔ ∀ j < n, (taylor r p).coeff j = 0 := by + rw [X_sub_C_pow_dvd_iff, ← taylor_apply, X_pow_dvd_iff] + +/-- `(X - r) ^ n` divides `p` exactly when `z ^ n` divides `p (r + α z)`, for a unit `α`. -/ +theorem X_sub_C_pow_dvd_iff_X_pow_dvd_comp (α : Rˣ) {r : R} {n : ℕ} {p : R[X]} : + (X - C r) ^ n ∣ p ↔ X ^ n ∣ p.comp (C r + C (α : R) * X) := by + have hσ : (C r + C (α : R) * X).comp (C (↑α⁻¹ : R) * (X - C r)) = X := by + simp only [add_comp, C_comp, mul_comp, X_comp] + rw [← mul_assoc, ← C_mul, Units.mul_inv, C_1, one_mul, add_sub_cancel] + have hτ : (X - C r).comp (C r + C (α : R) * X) = C (α : R) * X := by + simp only [sub_comp, X_comp, C_comp, add_sub_cancel_left] + constructor + · rintro ⟨q, rfl⟩ + rw [mul_comp, pow_comp, hτ, mul_pow, mul_comm (C _ ^ n), mul_assoc] + exact dvd_mul_right _ _ + · rintro ⟨q, hq⟩ + have hp : p = (p.comp (C r + C (α : R) * X)).comp (C (↑α⁻¹ : R) * (X - C r)) := by + rw [comp_assoc, hσ, comp_X] + rw [hp, hq, mul_comp, pow_comp, X_comp, mul_pow, mul_comm (C _ ^ n), mul_assoc] + exact dvd_mul_right _ _ + +/-- **Uniqueness of Hermite interpolation.** A polynomial of degree less than `∑ i ∈ s, J i` that +vanishes to order `J i` at each node `t i`, for nodes with unit differences, is zero. -/ +theorem eq_zero_of_forall_X_sub_C_pow_dvd (ht : (s : Set ι).Pairwise fun i j => IsUnit (t i - t j)) + {p : R[X]} (hp : p.degree < ↑(∑ i ∈ s, J i)) (h : ∀ i ∈ s, (X - C (t i)) ^ J i ∣ p) : + p = 0 := by + nontriviality R + by_contra h0 + have hcop : (s : Set ι).Pairwise (Function.onFun IsCoprime fun i => (X - C (t i)) ^ J i) := + fun i hi j hj hij => (isCoprime_X_sub_C_of_isUnit_sub (ht hi hj hij)).pow + have hmon : ∀ i ∈ s, ((X - C (t i)) ^ J i).Monic := fun i _ => (monic_X_sub_C _).pow _ + refine (monic_prod_of_monic _ _ hmon).not_dvd_of_natDegree_lt h0 ?_ + (Finset.prod_dvd_of_coprime hcop h) + rw [natDegree_prod_of_monic _ _ hmon] + simpa only [(monic_X_sub_C _).natDegree_pow, natDegree_X_sub_C, mul_one] using + (natDegree_lt_iff_degree_lt h0).mpr hp + +variable [DecidableEq ι] + +/-- The *Hermite basis polynomial* of node `i`, +`E_i = ∏_{j ∈ s, j ≠ i} ((X - t j) / (t i - t j)) ^ J j`, dividing by `Ring.inverse`. At nodes with +unit differences it is `1` at `t i` (`eval_hermiteBasis_self`) and vanishes to order `J k` at +every other node `t k` (`X_sub_C_pow_dvd_hermiteBasis`). With every `J j = 1` it is the Lagrange +basis polynomial. -/ +noncomputable def hermiteBasis (s : Finset ι) (t : ι → R) (J : ι → ℕ) (i : ι) : R[X] := + ∏ j ∈ s.erase i, (C (Ring.inverse (t i - t j)) * (X - C (t j))) ^ J j + +theorem eval_hermiteBasis (s : Finset ι) (t : ι → R) (J : ι → ℕ) (i : ι) (x : R) : + (hermiteBasis s t J i).eval x = + ∏ j ∈ s.erase i, (Ring.inverse (t i - t j) * (x - t j)) ^ J j := by + simp only [hermiteBasis, eval_prod, eval_pow, eval_mul, eval_C, eval_sub, eval_X] + +/-- The Hermite basis polynomial of a node is `1` at that node. -/ +theorem eval_hermiteBasis_self (ht : (s : Set ι).Pairwise fun i j => IsUnit (t i - t j)) {i : ι} + (hi : i ∈ s) : (hermiteBasis s t J i).eval (t i) = 1 := by + rw [eval_hermiteBasis] + refine Finset.prod_eq_one fun j hj => ?_ + rw [Ring.inverse_mul_cancel _ + (ht hi (Finset.mem_of_mem_erase hj) (Finset.ne_of_mem_erase hj).symm), one_pow] + +/-- The Hermite basis polynomial of `i` vanishes to order `J k` at every other node `t k`. -/ +theorem X_sub_C_pow_dvd_hermiteBasis {i k : ι} (hk : k ∈ s) (hki : k ≠ i) : + (X - C (t k)) ^ J k ∣ hermiteBasis s t J i := by + refine (Dvd.intro_left (C (Ring.inverse (t i - t k)) ^ J k) ?_).trans + (Finset.dvd_prod_of_mem _ (Finset.mem_erase.mpr ⟨hki, hk⟩)) + rw [mul_pow] + +theorem natDegree_hermiteBasis_le (s : Finset ι) (t : ι → R) (J : ι → ℕ) (i : ι) : + (hermiteBasis s t J i).natDegree ≤ ∑ j ∈ s.erase i, J j := by + refine (natDegree_prod_le _ _).trans (Finset.sum_le_sum fun j _ => natDegree_pow_le.trans ?_) + calc J j * (C (Ring.inverse (t i - t j)) * (X - C (t j))).natDegree ≤ J j * 1 := + Nat.mul_le_mul_left _ ((natDegree_C_mul_le _ _).trans (natDegree_X_sub_C_le _)) + _ = J j := mul_one _ + +/-- The Hermite basis commutes with ring homomorphisms, at nodes with unit differences. -/ +theorem map_hermiteBasis {S : Type*} [CommRing S] (f : R →+* S) + (ht : (s : Set ι).Pairwise fun i j => IsUnit (t i - t j)) {i : ι} (hi : i ∈ s) : + (hermiteBasis s t J i).map f = hermiteBasis s (fun j => f (t j)) J i := by + simp only [hermiteBasis, Polynomial.map_prod, Polynomial.map_pow, Polynomial.map_mul, map_C, + Polynomial.map_sub, map_X] + refine Finset.prod_congr rfl fun j hj => ?_ + obtain ⟨u, hu⟩ := ht hi (Finset.mem_of_mem_erase hj) (Finset.ne_of_mem_erase hj).symm + rw [← map_sub f, ← hu, Ring.inverse_unit] + exact congrArg (fun x => (C x * (X - C (f (t j)))) ^ J j) + (Ring.inverse_unit (Units.map (f : R →* S) u)).symm + +/-- **The Chinese-remainder form of Hermite interpolation.** Let `p` have degree less than +`∑ i ∈ s, J i`, at nodes with unit differences. If at every node `r i` has degree less than `J i` +and `E_i * r i` agrees with `p` to order `J i` at `t i`, then `p = ∑ i ∈ s, E_i * r i`. -/ +theorem eq_sum_hermiteBasis_mul_of_dvd (ht : (s : Set ι).Pairwise fun i j => IsUnit (t i - t j)) + {p : R[X]} (hp : p.degree < ↑(∑ i ∈ s, J i)) (r : ι → R[X]) + (hr : ∀ i ∈ s, (r i).degree < J i) + (hdvd : ∀ i ∈ s, (X - C (t i)) ^ J i ∣ p - hermiteBasis s t J i * r i) : + p = ∑ i ∈ s, hermiteBasis s t J i * r i := by + refine sub_eq_zero.mp (eq_zero_of_forall_X_sub_C_pow_dvd (J := J) ht ?_ fun k hk => ?_) + · refine (degree_sub_le _ _).trans_lt (max_lt hp ((degree_sum_le _ _).trans_lt ?_)) + refine (Finset.sup_lt_iff (WithBot.bot_lt_coe _)).mpr fun i hi => ?_ + by_cases hri : r i = 0 + · rw [hri, mul_zero, degree_zero] + exact WithBot.bot_lt_coe _ + refine degree_le_natDegree.trans_lt ?_ + rw [← Finset.add_sum_erase s J hi, Nat.cast_lt] + have hri' := (natDegree_lt_iff_degree_lt hri).mpr (hr i hi) + have hE := natDegree_hermiteBasis_le s t J i + have hmul := natDegree_mul_le (p := hermiteBasis s t J i) (q := r i) + omega + · rw [← Finset.add_sum_erase s _ hk, ← sub_sub] + exact dvd_sub (hdvd k hk) (Finset.dvd_sum fun i hi => + (X_sub_C_pow_dvd_hermiteBasis hk (Finset.ne_of_mem_erase hi).symm).mul_right _) + +/-- The *Hermite quotient* at node `i` with scale `α` of a power series `P`: the truncation below +`z ^ J i` of `P(z) / E_i(t i + α z)`, using the power-series inverse of `E_i(t i + α z)`, whose +constant term `E_i(t i)` is `1` at nodes with unit differences. For `P(z) = p(t i + α z)` it is +the local factor of `p` at `t i` in the Chinese-remainder form of Hermite interpolation +(`eq_sum_hermiteBasis_mul_hermiteQuotient`). -/ +noncomputable def hermiteQuotient (s : Finset ι) (t : ι → R) (J : ι → ℕ) (α : R) (i : ι) + (P : PowerSeries R) : R[X] := + PowerSeries.trunc (J i) + (P * PowerSeries.invOfUnit ((hermiteBasis s t J i).comp (C (t i) + C α * X) : PowerSeries R) 1) + +/-- The Hermite quotient at node `i` depends only on the first `J i` coefficients. -/ +@[simp] +theorem hermiteQuotient_trunc (s : Finset ι) (t : ι → R) (J : ι → ℕ) (α : R) (i : ι) + (P : PowerSeries R) : + hermiteQuotient s t J α i (PowerSeries.trunc (J i) P) = hermiteQuotient s t J α i P := + PowerSeries.trunc_trunc_mul _ _ + +theorem degree_hermiteQuotient_lt (s : Finset ι) (t : ι → R) (J : ι → ℕ) (α : R) (i : ι) + (P : PowerSeries R) : (hermiteQuotient s t J α i P).degree < J i := + PowerSeries.degree_trunc_lt _ _ + +/-- The constant term of `E_i(t i + α z)` is `1`. -/ +private theorem coeff_zero_hermiteBasis_comp + (ht : (s : Set ι).Pairwise fun i j => IsUnit (t i - t j)) (α : R) {i : ι} (hi : i ∈ s) : + ((hermiteBasis s t J i).comp (C (t i) + C α * X)).coeff 0 = 1 := by + rw [coeff_zero_eq_eval_zero, eval_comp, eval_add, eval_C, eval_mul, eval_C, eval_X, mul_zero, + add_zero, eval_hermiteBasis_self ht hi] + +/-- **The defining congruence of the Hermite quotient.** For a polynomial `P`, the product +`E_i(t i + α z)` times the Hermite quotient of `P` agrees with `P` below `z ^ J i`. -/ +theorem X_pow_dvd_sub_mul_hermiteQuotient + (ht : (s : Set ι).Pairwise fun i j => IsUnit (t i - t j)) (α : R) {i : ι} (hi : i ∈ s) + (P : R[X]) : + X ^ J i ∣ + P - (hermiteBasis s t J i).comp (C (t i) + C α * X) * hermiteQuotient s t J α i P := by + rw [X_pow_dvd_iff] + intro d hd + rw [coeff_sub, ← coeff_coe, ← coeff_coe, coe_mul, hermiteQuotient, + PowerSeries.coeff_mul_eq_coeff_trunc_mul_trunc _ _ hd, PowerSeries.trunc_trunc, + ← PowerSeries.coeff_mul_eq_coeff_trunc_mul_trunc _ _ hd, mul_left_comm, + PowerSeries.mul_invOfUnit _ _ (by + rw [constantCoeff_coe, coeff_zero_hermiteBasis_comp ht α hi, Units.val_one]), + mul_one, sub_self] + +/-- **The Hermite quotient is characterized by its congruence**: a polynomial of degree less than +`J i` whose product with `E_i(t i + α z)` agrees with `P` below `z ^ J i` is the Hermite +quotient of `P`. -/ +theorem hermiteQuotient_eq_of_X_pow_dvd + (ht : (s : Set ι).Pairwise fun i j => IsUnit (t i - t j)) (α : R) {i : ι} (hi : i ∈ s) + {P q : R[X]} (hq : q.degree < J i) + (h : X ^ J i ∣ P - (hermiteBasis s t J i).comp (C (t i) + C α * X) * q) : + hermiteQuotient s t J α i P = q := by + obtain ⟨g, hg⟩ := h + have hP : (P : PowerSeries R) = + ((hermiteBasis s t J i).comp (C (t i) + C α * X) : PowerSeries R) * (q : PowerSeries R) + + PowerSeries.X ^ J i * (g : PowerSeries R) := by + rw [← coe_X, ← coe_pow, ← coe_mul, ← coe_mul, ← coe_add, ← hg, add_sub_cancel] + rw [hermiteQuotient, hP, add_mul, mul_comm _ (q : PowerSeries R), mul_assoc, + PowerSeries.mul_invOfUnit _ _ (by + rw [constantCoeff_coe, coeff_zero_hermiteBasis_comp ht α hi, Units.val_one]), + mul_one, mul_assoc, map_add, PowerSeries.trunc_X_pow_self_mul, add_zero] + by_cases hq0 : q = 0 + · rw [hq0, coe_zero, map_zero] + exact PowerSeries.trunc_coe_eq_self ((natDegree_lt_iff_degree_lt hq0).mpr hq) + +/-- **The Chinese-remainder form of Hermite interpolation, in scaled local coordinates.** Let `p` +have degree less than `∑ i ∈ s, J i`, at nodes with unit differences, and let `α` be a unit. Then +`p(T)` is the sum over the nodes of `E_i(T)` times the Hermite quotient of `p(t i + α z)` at +`z = (T - t i) / α`. Each summand uses only the first `J i` coefficients of `p(t i + α z)` +(`hermiteQuotient_trunc`). With `α = 1` the local coordinate is `z = T - t i`. -/ +theorem eq_sum_hermiteBasis_mul_hermiteQuotient + (ht : (s : Set ι).Pairwise fun i j => IsUnit (t i - t j)) (α : Rˣ) {p : R[X]} + (hp : p.degree < ↑(∑ i ∈ s, J i)) : + p = ∑ i ∈ s, hermiteBasis s t J i * + (hermiteQuotient s t J α i (p.comp (C (t i) + C (α : R) * X))).comp + (C (↑α⁻¹ : R) * (X - C (t i))) := by + have hτσ : ∀ r : R, (C (↑α⁻¹ : R) * (X - C r)).comp (C r + C (α : R) * X) = X := fun r => by + simp only [mul_comp, sub_comp, C_comp, X_comp, add_sub_cancel_left] + rw [← mul_assoc, ← C_mul, Units.inv_mul, C_1, one_mul] + refine eq_sum_hermiteBasis_mul_of_dvd ht hp _ (fun i _ => ?_) fun i hi => ?_ + · set q := hermiteQuotient s t J α i (p.comp (C (t i) + C (α : R) * X)) + by_cases hq : q = 0 + · rw [hq, zero_comp, degree_zero] + exact WithBot.bot_lt_coe _ + refine (degree_le_natDegree.trans (Nat.cast_le.mpr natDegree_comp_le)).trans_lt ?_ + have hlin : (C (↑α⁻¹ : R) * (X - C (t i))).natDegree ≤ 1 := + (natDegree_C_mul_le _ _).trans (natDegree_X_sub_C_le _) + refine lt_of_le_of_lt (Nat.cast_le.mpr ((Nat.mul_le_mul_left _ hlin).trans (mul_one _).le)) ?_ + exact Nat.cast_lt.mpr + ((natDegree_lt_iff_degree_lt hq).mpr (degree_hermiteQuotient_lt _ _ _ _ _ _)) + · rw [X_sub_C_pow_dvd_iff_X_pow_dvd_comp α, sub_comp, mul_comp, comp_assoc, hτσ, comp_X] + exact X_pow_dvd_sub_mul_hermiteQuotient ht _ hi _ + +/-- **Hermite reconstruction of a value (D.9).** Under the hypotheses of +`eq_sum_hermiteBasis_mul_hermiteQuotient`, `p(x) = ∑ i ∈ s, E_i(x) * Q_i((x - t i) / α)`, where +`Q_i` is the Hermite quotient of `p(t i + α z)`. At `x = 0` this is equation (D.9) of +[OpenAI2026ETH, §D.4.4, p. 60]. -/ +theorem eval_eq_sum_hermiteBasis_mul_hermiteQuotient + (ht : (s : Set ι).Pairwise fun i j => IsUnit (t i - t j)) (α : Rˣ) {p : R[X]} + (hp : p.degree < ↑(∑ i ∈ s, J i)) (x : R) : + p.eval x = ∑ i ∈ s, (hermiteBasis s t J i).eval x * + (hermiteQuotient s t J α i (p.comp (C (t i) + C (α : R) * X))).eval + ((↑α⁻¹ : R) * (x - t i)) := by + conv_lhs => rw [eq_sum_hermiteBasis_mul_hermiteQuotient ht α hp] + simp only [eval_finsetSum, eval_mul, eval_comp, eval_C, eval_sub, eval_X] + +end Multiplicities + +/-! ### Uniform multiplicity: Taylor jets -/ /-- The order-`J` Taylor jet of a polynomial at the nodes `t`: the coefficient of `z ^ j` in `p (t i + z)`, for `i < Q` and `j < J`. -/ @@ -85,22 +340,10 @@ theorem taylorJet_apply (t : Fin Q → R) (J : ℕ) (p : R[X]) (r : Fin Q × Fin /-- **Uniqueness of confluent Hermite interpolation.** A polynomial of degree less than `Q * J` whose order-`J` Taylor jet vanishes at `Q` nodes with unit differences is zero. -/ theorem eq_zero_of_taylorJet_eq_zero {t : Fin Q → R} (ht : Pairwise fun i j => IsUnit (t i - t j)) - {p : R[X]} (hp : p.degree < ↑(Q * J)) (h : taylorJet t J p = 0) : p = 0 := by - nontriviality R - by_contra h0 - have hdvd : ∀ i ∈ (univ : Finset (Fin Q)), (X - C (t i)) ^ J ∣ p := fun i _ => by - rw [X_sub_C_pow_dvd_iff, ← taylor_apply, X_pow_dvd_iff] - exact fun d hd => congrFun h (i, ⟨d, hd⟩) - have hcop : ((univ : Finset (Fin Q)) : Set (Fin Q)).Pairwise - (Function.onFun IsCoprime fun i => (X - C (t i)) ^ J) := fun i _ j _ hij => - (isCoprime_X_sub_C_of_isUnit_sub (ht hij)).pow - have hmon : ∀ i ∈ (univ : Finset (Fin Q)), ((X - C (t i)) ^ J).Monic := fun i _ => - (monic_X_sub_C _).pow J - refine (monic_prod_of_monic _ _ hmon).not_dvd_of_natDegree_lt h0 ?_ - (Finset.prod_dvd_of_coprime hcop hdvd) - rw [natDegree_prod_of_monic _ _ hmon] - simpa only [(monic_X_sub_C _).natDegree_pow, natDegree_X_sub_C, mul_one, sum_const, card_univ, - Fintype.card_fin, smul_eq_mul] using (natDegree_lt_iff_degree_lt h0).mpr hp + {p : R[X]} (hp : p.degree < ↑(Q * J)) (h : taylorJet t J p = 0) : p = 0 := + eq_zero_of_forall_X_sub_C_pow_dvd (s := univ) (J := fun _ => J) (fun i _ j _ hij => ht hij) + (by rwa [sum_const, card_univ, Fintype.card_fin, smul_eq_mul]) + fun i _ => X_sub_C_pow_dvd_iff_taylor_coeff.mpr fun j hj => congrFun h (i, ⟨j, hj⟩) /-- Two polynomials of degree less than `Q * J` with the same order-`J` Taylor jet at `Q` nodes with unit differences are equal. -/ diff --git a/Complexity/Foundations/Data/Polynomial/TaperedHermite.lean b/Complexity/Foundations/Data/Polynomial/TaperedHermite.lean new file mode 100644 index 000000000..8a5a5188c --- /dev/null +++ b/Complexity/Foundations/Data/Polynomial/TaperedHermite.lean @@ -0,0 +1,465 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Foundations.Data.Polynomial.HermiteInterpolation +public import Mathlib.Data.Int.Interval +public import Mathlib.NumberTheory.Padics.PadicVal.Basic +import Mathlib.Algebra.BigOperators.Intervals +import Mathlib.Order.Interval.Finset.Nat + +/-! +# Two-adic size of tapered Hermite basis values + +The tapered Hermite recovery of [OpenAI2026ETH, Lemma D.5, §D.4.4, pp. 60–61] interpolates on the +dyadic grid `S = [-2 ^ a, 2 ^ a)`, a complete residue system modulo `2 ^ (a + 1)`. The nodes are +the points `q ≠ 0` of `S`, and the multiplicity of `q` depends only on its 2-adic valuation, +`q_q = m (v₂ q)`. Its precision analysis needs a lower bound on the 2-adic valuation of the +Hermite basis values `E_t(0) = ∏_{q ∈ S \ {0, t}} (-q / (t - q)) ^ m (v₂ q)` of the +Chinese-remainder form (D.9) (`Polynomial.eval_eq_sum_hermiteBasis_mul_hermiteQuotient`). + +For a node `t` of valuation `i`, +`v₂ (E_t(0)) = ∑_{i < j ≤ a} 2 ^ (a - j) (j - i) (m j - m i)` +(`Polynomial.padicValRat_eval_zero_hermiteBasis_dyadic`), the middle expression of (D.10). The +proof pairs `q` with the reflection of `t - q` into the grid: points of valuation below `i` +contribute `0`, and the points of valuation `i` cancel the `i`-part of those above `i`. Counting +the points of each valuation on the grid (`sum_Ico_erase_zero_padicValInt_two`) gives +the closed form. If `m` drops by at most `h` per level, as the taper `m i = h * max(0, u - i)` +does, then `v₂ (E_t(0)) ≥ -6 h 2 ^ (a - i)`, since `∑_{j ≥ 1} j ^ 2 / 2 ^ j = 6` +(`Polynomial.neg_le_padicValRat_eval_zero_hermiteBasis_dyadic`, +`Polynomial.neg_le_padicValRat_eval_zero_hermiteBasis_taper`). This is (D.10), with +`D = 2 ^ (a - i) = L / 2 ^ i` for `L = 2 ^ a`. + +`E_t(0)` is rational, so this uses `padicValRat` and needs no valuation on the coefficient ring of +Lemma D.5. + +## Main results + +* `padicValRat.prod`: the `p`-adic valuation of a product of nonzero rationals. +* `sum_Ico_erase_zero_padicValInt_two`: the valuation `j ≤ a` occurs `2 ^ (a - j)` + times on the nonzero points of `[-2 ^ a, 2 ^ a)`. +* `Polynomial.padicValRat_eval_zero_hermiteBasis_dyadic`: the exact valuation of `E_t(0)`. +* `Polynomial.neg_le_padicValRat_eval_zero_hermiteBasis_dyadic`, + `Polynomial.neg_le_padicValRat_eval_zero_hermiteBasis_taper`: the bound (D.10). + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH] +-/ + +public section + +open Finset + +/-- The `p`-adic valuation of a finite product of nonzero rationals is the sum of the +valuations. -/ +theorem padicValRat.prod {p : ℕ} [Fact p.Prime] {ι : Type*} (s : Finset ι) {f : ι → ℚ} + (hf : ∀ i ∈ s, f i ≠ 0) : padicValRat p (∏ i ∈ s, f i) = ∑ i ∈ s, padicValRat p (f i) := by + classical + induction s using Finset.induction_on with + | empty => simp + | insert j s hj ih => + rw [prod_insert hj, sum_insert hj, + padicValRat.mul (hf j (mem_insert_self j s)) + (prod_ne_zero_iff.mpr fun i hi => hf i (mem_insert_of_mem hi)), + ih fun i hi => hf i (mem_insert_of_mem hi)] + +namespace Polynomial + +/-! ### Two-adic valuations of integers -/ + +/-- The 2-adic valuation of `x` is `n` when `2 ^ n`, but not `2 ^ (n + 1)`, divides `x`. -/ +private theorem padicValInt_two_eq {x : ℤ} {n : ℕ} (h1 : (2 : ℤ) ^ n ∣ x) + (h2 : ¬(2 : ℤ) ^ (n + 1) ∣ x) : padicValInt 2 x = n := by + have hx : x ≠ 0 := by rintro rfl; exact h2 (dvd_zero _) + have hle : n ≤ padicValInt 2 x := + ((padicValInt_dvd_iff (p := 2) n x).mp (by exact_mod_cast h1)).resolve_left hx + have hlt : ¬n + 1 ≤ padicValInt 2 x := fun h => + h2 (by exact_mod_cast (padicValInt_dvd_iff (p := 2) (n + 1) x).mpr (Or.inr h)) + omega + +private theorem two_pow_padicValInt_dvd (x : ℤ) : (2 : ℤ) ^ padicValInt 2 x ∣ x := by + exact_mod_cast padicValInt_dvd (p := 2) x + +private theorem not_two_pow_succ_padicValInt_dvd {x : ℤ} (hx : x ≠ 0) : + ¬(2 : ℤ) ^ (padicValInt 2 x + 1) ∣ x := fun h => by + have := ((padicValInt_dvd_iff (p := 2) (padicValInt 2 x + 1) x).mp + (by exact_mod_cast h)).resolve_left hx + omega + +private theorem le_padicValInt_two {x : ℤ} {n : ℕ} (hx : x ≠ 0) (h : (2 : ℤ) ^ n ∣ x) : + n ≤ padicValInt 2 x := + ((padicValInt_dvd_iff (p := 2) n x).mp (by exact_mod_cast h)).resolve_left hx + +/-- A nonzero integer of absolute value less than `2 ^ n` has 2-adic valuation less than `n`. -/ +private theorem padicValInt_two_lt {x : ℤ} {n : ℕ} (hx : x ≠ 0) (h : x.natAbs < 2 ^ n) : + padicValInt 2 x < n := by + have h2 : 2 ^ padicValInt 2 x ∣ x.natAbs := by + have := Int.natAbs_dvd_natAbs.mpr (two_pow_padicValInt_dvd x) + rwa [Int.natAbs_pow] at this + exact (pow_lt_pow_iff_right₀ (by norm_num : 1 < 2)).mp + ((Nat.le_of_dvd (Int.natAbs_pos.mpr hx) h2).trans_lt h) + +/-- Adding a multiple of `2 ^ n` to a nonzero integer of absolute value less than `2 ^ n` keeps +its 2-adic valuation. -/ +private theorem padicValInt_two_add_mul {x : ℤ} {n : ℕ} (hx : x ≠ 0) (h : x.natAbs < 2 ^ n) + (c : ℤ) : padicValInt 2 (x + 2 ^ n * c) = padicValInt 2 x := by + have hlt := padicValInt_two_lt hx h + refine padicValInt_two_eq (dvd_add (two_pow_padicValInt_dvd x) + (dvd_mul_of_dvd_left (pow_dvd_pow 2 hlt.le) c)) fun hd => ?_ + refine not_two_pow_succ_padicValInt_dvd hx ?_ + have := dvd_sub hd (dvd_mul_of_dvd_left (pow_dvd_pow 2 (Nat.succ_le_of_lt hlt)) c) + rwa [add_sub_cancel_right] at this + +/-- If `v₂ x < v₂ y` then `x - y` and `y - x` have the valuation of `x`. -/ +private theorem padicValInt_two_sub_of_lt {x y : ℤ} (hx : x ≠ 0) + (h : padicValInt 2 x < padicValInt 2 y) : + padicValInt 2 (x - y) = padicValInt 2 x ∧ padicValInt 2 (y - x) = padicValInt 2 x := by + have hy : (2 : ℤ) ^ (padicValInt 2 x + 1) ∣ y := + (pow_dvd_pow 2 (Nat.succ_le_of_lt h)).trans (two_pow_padicValInt_dvd y) + have hx1 := two_pow_padicValInt_dvd x + have hx2 := not_two_pow_succ_padicValInt_dvd hx + refine ⟨padicValInt_two_eq (dvd_sub hx1 ((pow_dvd_pow 2 (Nat.le_succ _)).trans hy)) + fun hd => hx2 ?_, padicValInt_two_eq (dvd_sub ((pow_dvd_pow 2 (Nat.le_succ _)).trans hy) hx1) + fun hd => hx2 ?_⟩ + · have := dvd_add hd hy; rwa [sub_add_cancel] at this + · have := dvd_sub hy hd; rwa [sub_sub_cancel] at this + +/-- Two integers of the same 2-adic valuation `i` differ by a multiple of `2 ^ (i + 1)`. -/ +private theorem two_pow_succ_dvd_sub {x y : ℤ} (hx : x ≠ 0) (hy : y ≠ 0) + (h : padicValInt 2 x = padicValInt 2 y) : (2 : ℤ) ^ (padicValInt 2 x + 1) ∣ x - y := by + have hdx := two_pow_padicValInt_dvd x + have hdy := two_pow_padicValInt_dvd y + have hnx := not_two_pow_succ_padicValInt_dvd hx + have hny := not_two_pow_succ_padicValInt_dvd hy + rw [← h] at hdy hny + generalize padicValInt 2 x = i at hdx hnx hdy hny ⊢ + obtain ⟨x', rfl⟩ := hdx + obtain ⟨y', rfl⟩ := hdy + have hox : ¬(2 : ℤ) ∣ x' := fun ⟨c, hc⟩ => hnx ⟨c, by rw [hc, pow_succ]; ring⟩ + have hoy : ¬(2 : ℤ) ∣ y' := fun ⟨c, hc⟩ => hny ⟨c, by rw [hc, pow_succ]; ring⟩ + obtain ⟨c, hc⟩ : (2 : ℤ) ∣ x' - y' := by omega + exact ⟨c, by rw [pow_succ, mul_assoc, ← hc, mul_sub]⟩ + +/-! ### The dyadic grid -/ + +/-- The 2-adic valuation of `2 x` is one more than that of a nonzero `x`. -/ +private theorem padicValInt_two_mul {x : ℤ} (hx : x ≠ 0) : + padicValInt 2 (2 * x) = padicValInt 2 x + 1 := by + rw [padicValInt.mul two_ne_zero hx, add_comm, show (2 : ℤ) = ((2 : ℕ) : ℤ) from rfl, + padicValInt.self (by norm_num)] + +private theorem natAbs_sub_lt {a : ℕ} {t q : ℤ} (ht : t ∈ Ico (-(2 : ℤ) ^ a) (2 ^ a)) + (hq : q ∈ Ico (-(2 : ℤ) ^ a) (2 ^ a)) : (t - q).natAbs < 2 ^ (a + 1) := by + rw [mem_Ico] at ht hq + have : |t - q| < (2 : ℤ) ^ (a + 1) := by + rw [abs_lt, pow_succ] + constructor <;> omega + rw [← Int.natCast_natAbs] at this + exact_mod_cast this + +/-- **The distribution of 2-adic valuations on the dyadic grid.** On the nonzero points of +`[-2 ^ a, 2 ^ a)`, the valuation `j ≤ a` occurs `2 ^ (a - j)` times. -/ +theorem _root_.sum_Ico_erase_zero_padicValInt_two (a : ℕ) (f : ℕ → ℤ) : + ∑ q ∈ (Ico (-(2 : ℤ) ^ a) (2 ^ a)).erase 0, f (padicValInt 2 q) = + ∑ j ∈ range (a + 1), 2 ^ (a - j) * f j := by + induction a generalizing f with + | zero => + rw [show (Ico (-(2 : ℤ) ^ 0) (2 ^ 0)).erase 0 = {-1} by + ext q; simp only [mem_erase, mem_Ico, mem_singleton]; omega, sum_singleton, + padicValInt.eq_zero_of_not_dvd (by norm_num), sum_range_one, pow_zero, one_mul] + | succ a ih => + have hpow : (2 : ℤ) ^ (a + 1) = 2 * 2 ^ a := by rw [pow_succ, mul_comm] + rw [← sum_filter_add_sum_filter_not _ (fun q : ℤ => (2 : ℤ) ∣ q)] + -- even points are `2 q` for nonzero `q ∈ [-2 ^ a, 2 ^ a)` + have heven : ∑ q ∈ ((Ico (-(2 : ℤ) ^ (a + 1)) (2 ^ (a + 1))).erase 0).filter + (fun q : ℤ => (2 : ℤ) ∣ q), f (padicValInt 2 q) = + ∑ q ∈ (Ico (-(2 : ℤ) ^ a) (2 ^ a)).erase 0, f (padicValInt 2 q + 1) := by + refine sum_nbij' (fun q => q / 2) (fun q => 2 * q) (fun q hq => ?_) (fun q hq => ?_) + (fun q hq => ?_) (fun q hq => ?_) (fun q hq => ?_) + all_goals simp only [mem_filter, mem_erase, mem_Ico, hpow] at hq ⊢ + · omega + · omega + · omega + · omega + · obtain ⟨⟨hq0, -⟩, hq2⟩ := hq + rw [← padicValInt_two_mul (by omega), Int.mul_ediv_cancel' hq2] + -- odd points have valuation `0`; there are `2 ^ (a + 1)` of them + have hodd : ∑ q ∈ ((Ico (-(2 : ℤ) ^ (a + 1)) (2 ^ (a + 1))).erase 0).filter + (fun q : ℤ => ¬(2 : ℤ) ∣ q), f (padicValInt 2 q) = 2 ^ (a + 1) * f 0 := by + rw [sum_congr rfl fun q hq => by + rw [padicValInt.eq_zero_of_not_dvd (by exact_mod_cast (mem_filter.mp hq).2)], sum_const, + nsmul_eq_mul] + congr 1 + have hcard : #(((Ico (-(2 : ℤ) ^ (a + 1)) (2 ^ (a + 1))).erase 0).filter + (fun q : ℤ => ¬(2 : ℤ) ∣ q)) = #(Ico (-(2 : ℤ) ^ a) (2 ^ a)) := by + refine card_nbij' (fun q => (q - 1) / 2) (fun q => 2 * q + 1) (fun q hq => ?_) + (fun q hq => ?_) (fun q hq => ?_) (fun q hq => ?_) + all_goals simp only [coe_filter, mem_erase, mem_Ico, Set.mem_ofPred_eq, coe_Ico, + Set.mem_Ico, hpow] at hq ⊢ + all_goals omega + rw [hcard, Int.card_Ico, show (2 : ℤ) ^ a - -2 ^ a = ((2 ^ (a + 1) : ℕ) : ℤ) by + push_cast; ring, Int.toNat_natCast] + push_cast + rfl + rw [heven, hodd, ih fun j => f (j + 1), sum_range_succ' _ (a + 1), Nat.sub_zero] + simp only [Nat.add_sub_add_right] + +/-- The reflection `q ↦ t - q` of the grid `[-L, L)`, reduced modulo `2 L` back into the grid. -/ +private def gridFlip (L t q : ℤ) : ℤ := + if t - q < -L then t - q + 2 * L else if t - q < L then t - q else t - q - 2 * L + +section gridFlip + +variable {L t q : ℤ} + +private theorem gridFlip_mem (ht : t ∈ Ico (-L) L) (hq : q ∈ Ico (-L) L) : + gridFlip L t q ∈ Ico (-L) L := by + rw [mem_Ico] at ht hq ⊢ + unfold gridFlip + split_ifs <;> omega + +private theorem gridFlip_gridFlip (ht : t ∈ Ico (-L) L) (hq : q ∈ Ico (-L) L) : + gridFlip L t (gridFlip L t q) = q := by + rw [mem_Ico] at ht hq + unfold gridFlip + split_ifs <;> omega + +private theorem gridFlip_eq_zero_iff (ht : t ∈ Ico (-L) L) (hq : q ∈ Ico (-L) L) : + gridFlip L t q = 0 ↔ q = t := by + rw [mem_Ico] at ht hq + unfold gridFlip + split_ifs <;> omega + +private theorem gridFlip_eq_self_iff (ht : t ∈ Ico (-L) L) (hq : q ∈ Ico (-L) L) : + gridFlip L t q = t ↔ q = 0 := by + rw [mem_Ico] at ht hq + unfold gridFlip + split_ifs <;> omega + +private theorem exists_gridFlip_eq (L t q : ℤ) : ∃ c : ℤ, gridFlip L t q = t - q + 2 * L * c := by + unfold gridFlip + split_ifs + · exact ⟨1, by ring⟩ + · exact ⟨0, by ring⟩ + · exact ⟨-1, by ring⟩ + +end gridFlip + +section Dyadic + +variable {a : ℕ} {t q : ℤ} + +/-- On the dyadic grid, the reflection of `q ≠ t` has the valuation of `t - q`. -/ +private theorem padicValInt_gridFlip (ht : t ∈ Ico (-(2 : ℤ) ^ a) (2 ^ a)) + (hq : q ∈ Ico (-(2 : ℤ) ^ a) (2 ^ a)) (hqt : q ≠ t) : + padicValInt 2 (gridFlip (2 ^ a) t q) = padicValInt 2 (t - q) := by + obtain ⟨c, hc⟩ := exists_gridFlip_eq (2 ^ a) t q + rw [hc, show 2 * (2 : ℤ) ^ a * c = 2 ^ (a + 1) * c by ring] + exact padicValInt_two_add_mul (sub_ne_zero.mpr hqt.symm) (natAbs_sub_lt ht hq) c + +/-- On the dyadic grid, `t` minus the reflection of `q ≠ 0` has the valuation of `q`. -/ +private theorem padicValInt_sub_gridFlip (ht : t ∈ Ico (-(2 : ℤ) ^ a) (2 ^ a)) + (hq : q ∈ Ico (-(2 : ℤ) ^ a) (2 ^ a)) (hq0 : q ≠ 0) : + padicValInt 2 (t - gridFlip (2 ^ a) t q) = padicValInt 2 q := by + have h := padicValInt_gridFlip ht (gridFlip_mem ht hq) + (fun h => hq0 ((gridFlip_eq_self_iff ht hq).mp h)) + rwa [gridFlip_gridFlip ht hq, eq_comm] at h + +/-- **The tapered sum on the dyadic grid.** For a nonzero grid point `t` of valuation `i` and any +multiplicities `m` by valuation, `∑_{q ≠ 0, t} m(v₂ q) (v₂ q - v₂ (t - q))` is +`∑_{q ≠ 0, v₂ q > i} (v₂ q - i) (m (v₂ q) - m i)`: pairing `q` with the reflection of `t - q` +into the grid cancels the points of valuation `i` against those of valuation above `i`. -/ +private theorem sum_tapered_eq (m : ℕ → ℕ) (ht : t ∈ Ico (-(2 : ℤ) ^ a) (2 ^ a)) (ht0 : t ≠ 0) : + ∑ q ∈ ((Ico (-(2 : ℤ) ^ a) (2 ^ a)).erase 0).erase t, + (m (padicValInt 2 q) : ℤ) * ((padicValInt 2 q : ℤ) - padicValInt 2 (t - q)) = + ∑ q ∈ (Ico (-(2 : ℤ) ^ a) (2 ^ a)).erase 0, + if padicValInt 2 t < padicValInt 2 q then + ((padicValInt 2 q : ℤ) - padicValInt 2 t) * + ((m (padicValInt 2 q) : ℤ) - m (padicValInt 2 t)) + else 0 := by + set S := Ico (-(2 : ℤ) ^ a) (2 ^ a) + set v : ℤ → ℕ := padicValInt 2 + set i := v t + set φ := gridFlip (2 ^ a) t + have hmem : ∀ {q}, q ∈ (S.erase 0).erase t ↔ q ∈ S ∧ q ≠ 0 ∧ q ≠ t := fun {q} => by + simp only [mem_erase]; tauto + have hφ : ∀ {q}, q ∈ (S.erase 0).erase t → φ q ∈ (S.erase 0).erase t := fun {q} hq => by + rw [hmem] at hq ⊢ + exact ⟨gridFlip_mem ht hq.1, fun h => hq.2.2 ((gridFlip_eq_zero_iff ht hq.1).mp h), + fun h => hq.2.1 ((gridFlip_eq_self_iff ht hq.1).mp h)⟩ + have hφφ : ∀ {q}, q ∈ (S.erase 0).erase t → φ (φ q) = q := fun {q} hq => + gridFlip_gridFlip ht (hmem.mp hq).1 + have hvφ : ∀ {q}, q ∈ (S.erase 0).erase t → v (φ q) = v (t - q) := fun {q} hq => + padicValInt_gridFlip ht (hmem.mp hq).1 (hmem.mp hq).2.2 + have hvsubφ : ∀ {q}, q ∈ (S.erase 0).erase t → v (t - φ q) = v q := fun {q} hq => + padicValInt_sub_gridFlip ht (hmem.mp hq).1 (hmem.mp hq).2.1 + -- a point of valuation above `i` has `v₂ (t - q) = i`, and one of valuation `i` has more + have hgt : ∀ {q}, i < v q → v (t - q) = i := fun h => (padicValInt_two_sub_of_lt ht0 h).1 + have hlt : ∀ {q}, q ≠ 0 → v q < i → v (t - q) = v q := fun hq0 h => + (padicValInt_two_sub_of_lt hq0 h).2 + have heq : ∀ {q}, q ≠ 0 → q ≠ t → v q = i → i < v (t - q) := fun hq0 hqt h => + le_padicValInt_two (sub_ne_zero.mpr hqt.symm) (two_pow_succ_dvd_sub ht0 hq0 h.symm) + set g : ℤ → ℤ := fun q => (v q : ℤ) * ((m (v q) : ℤ) - m (v (t - q))) + -- reflect the second half of the sum + have h1 : ∑ q ∈ (S.erase 0).erase t, (m (v q) : ℤ) * ((v q : ℤ) - v (t - q)) = + ∑ q ∈ (S.erase 0).erase t, g q := by + have hrefl : ∑ q ∈ (S.erase 0).erase t, (m (v q) : ℤ) * (v (t - q) : ℤ) = + ∑ q ∈ (S.erase 0).erase t, (m (v (t - q)) : ℤ) * (v q : ℤ) := + sum_nbij' φ φ (fun q hq => hφ hq) (fun q hq => hφ hq) (fun q hq => hφφ hq) + (fun q hq => hφφ hq) fun q hq => by rw [hvφ hq, hvsubφ hq] + simp only [g, mul_sub, sum_sub_distrib, hrefl] + congr 1 + · exact sum_congr rfl fun q _ => mul_comm _ _ + · exact sum_congr rfl fun q _ => mul_comm _ _ + -- points of valuation `i` are reflections of points of valuation above `i` + have h2 : ∑ q ∈ ((S.erase 0).erase t).filter (fun q => ¬i < v q), g q = + ∑ q ∈ ((S.erase 0).erase t).filter (fun q => i < v q), g (φ q) := by + rw [← sum_subset (s₁ := ((S.erase 0).erase t).filter (fun q => v q = i)) + (fun q hq => by + simp only [mem_filter] at hq ⊢ + exact ⟨hq.1, by omega⟩) + fun q hq hq' => by + simp only [mem_filter, not_and, not_lt] at hq hq' + have hlt' : v q < i := lt_of_le_of_ne hq.2 (hq' hq.1) + simp only [g, hlt (hmem.mp hq.1).2.1 hlt', sub_self, mul_zero]] + refine sum_nbij' φ φ (fun q hq => ?_) (fun q hq => ?_) (fun q hq => hφφ (mem_filter.mp hq).1) + (fun q hq => hφφ (mem_filter.mp hq).1) fun q hq => by rw [hφφ (mem_filter.mp hq).1] + · rw [mem_filter] at hq ⊢ + refine ⟨hφ hq.1, ?_⟩ + rw [hvφ hq.1] + exact heq (hmem.mp hq.1).2.1 (hmem.mp hq.1).2.2 hq.2 + · rw [mem_filter] at hq ⊢ + exact ⟨hφ hq.1, by rw [hvφ hq.1, hgt hq.2]⟩ + rw [h1, ← sum_filter_add_sum_filter_not _ (fun q => i < v q), h2, ← sum_add_distrib, + ← sum_erase (S.erase 0) (a := t) (by simp only [i, lt_irrefl, ite_false]), sum_filter] + refine sum_congr rfl fun q hq => ?_ + split_ifs with hiq + · simp only [g, hgt hiq, hvφ hq, hvsubφ hq] + ring + · rfl + +/-- **The two-adic valuation of a tapered Hermite basis value, exactly (D.10).** On the grid +`S = [-2 ^ a, 2 ^ a)`, take the nodes `S \ {0}`, a node `q` having multiplicity `m (v₂ q)`. For a +node `t` of valuation `i`, the value at `0` of its Hermite basis polynomial +`E_t(T) = ∏_{q ∈ S \ {0, t}} ((T - q) / (t - q)) ^ m (v₂ q)` has valuation +`∑_{i < j ≤ a} 2 ^ (a - j) (j - i) (m j - m i)`. This is the middle expression of (D.10) in +[OpenAI2026ETH, §D.4.4, p. 61] with `j = i + j'` and `D = 2 ^ (a - i)`. -/ +theorem padicValRat_eval_zero_hermiteBasis_dyadic (m : ℕ → ℕ) + (ht : t ∈ Ico (-(2 : ℤ) ^ a) (2 ^ a)) (ht0 : t ≠ 0) : + padicValRat 2 ((hermiteBasis ((Ico (-(2 : ℤ) ^ a) (2 ^ a)).erase 0) (fun q : ℤ => (q : ℚ)) + (fun q => m (padicValInt 2 q)) t).eval 0) = + ∑ j ∈ Ioc (padicValInt 2 t) a, + 2 ^ (a - j) * (((j : ℤ) - padicValInt 2 t) * ((m j : ℤ) - m (padicValInt 2 t))) := by + have hfac : ∀ q ∈ ((Ico (-(2 : ℤ) ^ a) (2 ^ a)).erase 0).erase t, + (Ring.inverse ((t : ℚ) - q) * (0 - q)) ^ m (padicValInt 2 q) ≠ 0 ∧ + padicValRat 2 ((Ring.inverse ((t : ℚ) - q) * (0 - q)) ^ m (padicValInt 2 q)) = + (m (padicValInt 2 q) : ℤ) * ((padicValInt 2 q : ℤ) - padicValInt 2 (t - q)) := by + intro q hq + simp only [mem_erase] at hq + have hq0 : (q : ℚ) ≠ 0 := by exact_mod_cast hq.2.1 + have htq : ((t : ℚ) - q) ≠ 0 := sub_ne_zero.mpr (by exact_mod_cast hq.1.symm) + have hx : Ring.inverse ((t : ℚ) - q) * (0 - q) ≠ 0 := by + rw [Ring.inverse_eq_inv, zero_sub] + exact mul_ne_zero (inv_ne_zero htq) (neg_ne_zero.mpr hq0) + refine ⟨pow_ne_zero _ hx, ?_⟩ + rw [padicValRat.pow, Ring.inverse_eq_inv, zero_sub, + padicValRat.mul (inv_ne_zero htq) (neg_ne_zero.mpr hq0), padicValRat.inv, padicValRat.neg, + show (t : ℚ) - q = ((t - q : ℤ) : ℚ) by push_cast; ring, padicValRat.of_int, + padicValRat.of_int] + ring + rw [eval_hermiteBasis, padicValRat.prod _ fun q hq => (hfac q hq).1, + sum_congr rfl fun q hq => (hfac q hq).2, sum_tapered_eq m ht ht0, + sum_Ico_erase_zero_padicValInt_two a fun j => if padicValInt 2 t < j then + ((j : ℤ) - padicValInt 2 t) * ((m j : ℤ) - m (padicValInt 2 t)) else 0] + simp only [mul_ite, mul_zero] + rw [← sum_filter] + refine sum_congr (Finset.ext fun j => ?_) fun _ _ => rfl + simp only [mem_filter, mem_range, mem_Ioc] + omega + +/-- `∑_{k < n} 2 ^ (n - 1 - k) (k + 1) ^ 2 + n ^ 2 + 4 n + 6 = 6 * 2 ^ n`, so the sum is at most +`6 * 2 ^ n`: the finite form of `∑_{j ≥ 1} j ^ 2 / 2 ^ j = 6`. -/ +private theorem sum_two_pow_mul_sq (n : ℕ) : + ∑ k ∈ range n, 2 ^ (n - 1 - k) * (k + 1) ^ 2 + n ^ 2 + 4 * n + 6 = 6 * 2 ^ n := by + induction n with + | zero => simp + | succ n ih => + rw [sum_range_succ, Nat.add_sub_cancel, Nat.sub_self, pow_zero, one_mul, + sum_congr rfl fun k hk => by + rw [show n - k = n - 1 - k + 1 by have := mem_range.mp hk; omega, pow_succ, mul_comm _ 2, + mul_assoc], + ← mul_sum, pow_succ 2 n] + ring_nf + ring_nf at ih + omega + +/-- **The valuation bound (D.10).** If the multiplicity by valuation `m` drops by at most `h` per +level, `m k ≤ m (k + 1) + h`, then the Hermite basis value at `0` of a nonzero grid node `t` +satisfies `v₂ (E_t(0)) ≥ -6 h D` with `D = 2 ^ (a - v₂ t)` +([OpenAI2026ETH, Lemma D.5, (D.10), p. 61]). -/ +theorem neg_le_padicValRat_eval_zero_hermiteBasis_dyadic {h : ℕ} {m : ℕ → ℕ} + (hm : ∀ k, m k ≤ m (k + 1) + h) (ht : t ∈ Ico (-(2 : ℤ) ^ a) (2 ^ a)) (ht0 : t ≠ 0) : + -(6 * (h : ℤ) * 2 ^ (a - padicValInt 2 t)) ≤ + padicValRat 2 ((hermiteBasis ((Ico (-(2 : ℤ) ^ a) (2 ^ a)).erase 0) + (fun q : ℤ => (q : ℚ)) (fun q => m (padicValInt 2 q)) t).eval 0) := by + rw [padicValRat_eval_zero_hermiteBasis_dyadic m ht ht0] + set i := padicValInt 2 t + have hdrop : ∀ k j, m k ≤ m (k + j) + h * j := fun k j => by + induction j with + | zero => simp + | succ j ih => have := hm (k + j); rw [← add_assoc]; nlinarith + -- each level loses at most `h (j - i) ^ 2` times its count + have hterm : ∀ j ∈ Ioc i a, -((h : ℤ) * (2 ^ (a - j) * ((j : ℤ) - i) ^ 2)) ≤ + 2 ^ (a - j) * (((j : ℤ) - i) * ((m j : ℤ) - m i)) := fun j hj => by + have hij : i ≤ j := (mem_Ioc.mp hj).1.le + have hd := hdrop i (j - i) + rw [Nat.add_sub_cancel' hij] at hd + have hd' : (m i : ℤ) ≤ m j + h * ((j : ℤ) - i) := by + have := (Nat.cast_le (α := ℤ)).mpr hd + push_cast [Nat.cast_sub hij] at this + exact this + have hji : (0 : ℤ) ≤ (j : ℤ) - i := sub_nonneg.mpr (by exact_mod_cast hij) + have key : 0 ≤ (2 : ℤ) ^ (a - j) * ((j : ℤ) - i) * ((m j : ℤ) - m i + h * ((j : ℤ) - i)) := + mul_nonneg (mul_nonneg (by positivity) hji) (by linarith) + nlinarith [key] + refine le_trans ?_ (sum_le_sum hterm) + rw [sum_neg_distrib, neg_le_neg_iff, ← mul_sum, + show (6 : ℤ) * h * 2 ^ (a - i) = h * (6 * 2 ^ (a - i)) by ring] + refine mul_le_mul_of_nonneg_left ?_ (Nat.cast_nonneg (α := ℤ) h) + -- reindex `j = i + 1 + k` and use `∑ j ^ 2 / 2 ^ j ≤ 6` + have hreindex : ∑ j ∈ Ioc i a, (2 : ℤ) ^ (a - j) * ((j : ℤ) - i) ^ 2 = + ((∑ k ∈ range (a - i), 2 ^ (a - i - 1 - k) * (k + 1) ^ 2 : ℕ) : ℤ) := by + rw [show Ioc i a = Ico (i + 1) (a + 1) by ext; simp only [mem_Ioc, mem_Ico]; omega, + sum_Ico_eq_sum_range] + push_cast + refine sum_congr (by congr 1) fun k hk => ?_ + rw [show a - (i + 1 + k) = a - i - 1 - k by omega] + ring + rw [hreindex] + have := sum_two_pow_mul_sq (a - i) + exact_mod_cast (by omega : ∑ k ∈ range (a - i), 2 ^ (a - i - 1 - k) * (k + 1) ^ 2 ≤ + 6 * 2 ^ (a - i)) + +/-- **The tapered multiplicities of Lemma D.5.** With `q(i) = h * max(0, u - i)` (natural +subtraction), the Hermite basis value at `0` of a nonzero grid node `t` satisfies +`v₂ (E_t(0)) ≥ -6 h D` with `D = 2 ^ (a - v₂ t)`: (D.10) of +[OpenAI2026ETH, Lemma D.5, p. 61]. -/ +theorem neg_le_padicValRat_eval_zero_hermiteBasis_taper (u h : ℕ) + (ht : t ∈ Ico (-(2 : ℤ) ^ a) (2 ^ a)) (ht0 : t ≠ 0) : + -(6 * (h : ℤ) * 2 ^ (a - padicValInt 2 t)) ≤ + padicValRat 2 ((hermiteBasis ((Ico (-(2 : ℤ) ^ a) (2 ^ a)).erase 0) + (fun q : ℤ => (q : ℚ)) (fun q => h * (u - padicValInt 2 q)) t).eval 0) := + neg_le_padicValRat_eval_zero_hermiteBasis_dyadic (m := fun k => h * (u - k)) + (fun k => by + rw [← mul_add_one] + exact Nat.mul_le_mul_left h (by omega)) ht ht0 + +end Dyadic + +end Polynomial diff --git a/ComplexityTests/Foundations/Data/Polynomial/TaperedHermite.lean b/ComplexityTests/Foundations/Data/Polynomial/TaperedHermite.lean new file mode 100644 index 000000000..2651abc88 --- /dev/null +++ b/ComplexityTests/Foundations/Data/Polynomial/TaperedHermite.lean @@ -0,0 +1,86 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: local-only (tests of Complexity.Foundations.Data.Polynomial.TaperedHermite) + +import Complexity.Foundations.Data.Polynomial.TaperedHermite + +-- Regression tests intentionally export no declarations. +set_option linter.privateModule false + +/-! Tests for the two-adic size of tapered Hermite basis values on the dyadic grid. -/ + +namespace ComplexityTests.TaperedHermite + +open Finset Polynomial + +/-! ### Valuations on the grid `[-4, 4)` + +The nonzero points `-4, -3, -2, -1, 1, 2, 3` have 2-adic valuations `2, 0, 1, 0, 0, 1, 0`: the +valuation `j ≤ 2` occurs `2 ^ (2 - j)` times. -/ + +example : ∑ q ∈ (Ico (-(2 : ℤ) ^ 2) (2 ^ 2)).erase 0, (padicValInt 2 q : ℤ) = 4 := by + rw [sum_Ico_erase_zero_padicValInt_two 2 fun j => (j : ℤ)] + decide + +example : ∑ q ∈ (Ico (-(2 : ℤ) ^ 2) (2 ^ 2)).erase 0, ((padicValInt 2 q : ℤ) - 1) ^ 2 = 5 := by + rw [sum_Ico_erase_zero_padicValInt_two 2 fun j => ((j : ℤ) - 1) ^ 2] + decide + +/-! ### A tapered basis value + +On `[-4, 4)`, give a node of valuation `j` the multiplicity `2 - j` (the taper `h = 1`, `u = 2`). +For the node `t = 1`, +`E_1(0) = (3/4) ^ 2 (2/3) (1/2) ^ 2 (2) (3/2) ^ 2 = 27 / 64`, from the factors +`-q / (1 - q)` at `q = -3, -2, -1, 2, 3` (the node `-4` has multiplicity `0`). So +`v₂ (E_1(0)) = -6`, which the closed form gives as `2 ^ 1 * 1 * (1 - 2) + 2 ^ 0 * 2 * (0 - 2)`. -/ + +private theorem padicValInt_two_neg_four : padicValInt 2 (-4) = 2 := by + rw [padicValInt, Int.natAbs_neg, show Int.natAbs 4 = 2 ^ 2 from rfl, padicValNat.prime_pow] + +private theorem padicValInt_two_two : padicValInt 2 2 = 1 := + padicValInt.self (by norm_num) + +private theorem padicValInt_two_neg_two : padicValInt 2 (-2) = 1 := by + rw [padicValInt, Int.natAbs_neg] + exact padicValInt_two_two + +private theorem padicValInt_two_odd {z : ℤ} (hz : ¬(2 : ℤ) ∣ z) : padicValInt 2 z = 0 := + padicValInt.eq_zero_of_not_dvd (p := 2) (by exact_mod_cast hz) + +/-- The basis value, computed directly from the product. -/ +example : (hermiteBasis ((Ico (-(2 : ℤ) ^ 2) (2 ^ 2)).erase 0) (fun q : ℤ => (q : ℚ)) + (fun q => 2 - padicValInt 2 q) 1).eval 0 = 27 / 64 := by + rw [eval_hermiteBasis, show ((Ico (-(2 : ℤ) ^ 2) (2 ^ 2)).erase 0).erase 1 = + {-4, -3, -2, -1, 2, 3} by decide] + rw [prod_insert (by decide), prod_insert (by decide), prod_insert (by decide), + prod_insert (by decide), prod_insert (by decide), prod_singleton, padicValInt_two_neg_four, + padicValInt_two_neg_two, padicValInt_two_two, padicValInt_two_odd (z := -3) (by decide), + padicValInt_two_odd (z := -1) (by decide), padicValInt_two_odd (z := 3) (by decide)] + norm_num [Ring.inverse_eq_inv] + +example : padicValRat 2 (27 / 64) = -6 := by + rw [padicValRat.div (by norm_num) (by norm_num), show (27 : ℚ) = ((27 : ℕ) : ℚ) by norm_num, + show (64 : ℚ) = ((2 ^ 6 : ℕ) : ℚ) by norm_num, padicValRat.of_nat, padicValRat.of_nat, + padicValNat.eq_zero_of_not_dvd (by decide), padicValNat.prime_pow] + norm_num + +/-- The closed form of (D.10) gives the same valuation. -/ +example : padicValRat 2 ((hermiteBasis ((Ico (-(2 : ℤ) ^ 2) (2 ^ 2)).erase 0) + (fun q : ℤ => (q : ℚ)) (fun q => 2 - padicValInt 2 q) 1).eval 0) = -6 := by + rw [padicValRat_eval_zero_hermiteBasis_dyadic (fun j => 2 - j) (by decide) one_ne_zero, + padicValInt.one] + decide + +/-- The bound (D.10) for the taper `h = 1`, `u = 2`: `-6 * 1 * 2 ^ 2 ≤ v₂ (E_1(0)) = -6`. -/ +example : -(6 * (1 : ℤ) * 2 ^ 2) ≤ + padicValRat 2 ((hermiteBasis ((Ico (-(2 : ℤ) ^ 2) (2 ^ 2)).erase 0) + (fun q : ℤ => (q : ℚ)) (fun q => 1 * (2 - padicValInt 2 q)) 1).eval 0) := by + have := neg_le_padicValRat_eval_zero_hermiteBasis_taper (a := 2) 2 1 (by decide) one_ne_zero + rwa [padicValInt.one] at this + +end ComplexityTests.TaperedHermite diff --git a/ComplexityTests/HermiteInterpolation.lean b/ComplexityTests/HermiteInterpolation.lean index 1f6af7fa2..f07801579 100644 --- a/ComplexityTests/HermiteInterpolation.lean +++ b/ComplexityTests/HermiteInterpolation.lean @@ -12,7 +12,11 @@ import Mathlib.Data.ZMod.Defs import Mathlib.Tactic.ComputeDegree import Mathlib.Tactic.FinCases -/-! Tests for confluent Hermite interpolation from Taylor jets. -/ +-- Regression tests intentionally export no declarations. +set_option linter.privateModule false + +/-! Tests for confluent Hermite interpolation: Taylor jets, node-varying multiplicities and the +Chinese-remainder form. -/ namespace ComplexityTests.HermiteInterpolation @@ -90,4 +94,72 @@ example : (3 : ℚ) = ((hermiteMatrix ![1, 2] 2).det : ℚ)⁻¹ • rw [← h] simp + +/-! ### Node-varying multiplicities + +Two nodes `1, 2` with multiplicities `1, 2`, and polynomials of degree less than `1 + 2 = 3`. The +Hermite basis polynomials are `E₀ = ((X - 2) / (1 - 2)) ^ 2 = (X - 2) ^ 2` and +`E₁ = (X - 1) / (2 - 1) = X - 1`, so `E₀ (0) = 4` and `E₁ (0) = -1`. For `p = X ^ 2 + 3`, at node +`1`, `p (1 + z) / E₀ (1 + z) = (4 + 2 z + z ^ 2) / (1 - z) ^ 2 ≡ 4 (mod z)`; at node `2`, +`p (2 + z) / E₁ (2 + z) = (7 + 4 z + z ^ 2) / (1 + z) ≡ 7 - 3 z (mod z ^ 2)`. Hence +`p = 4 (X - 2) ^ 2 + (X - 1) (7 - 3 (X - 2))`, and at `0`, `3 = 4 * 4 + (-1) * 13`. -/ + +/-- The nodes `1, 2`. -/ +private abbrev node : Fin 2 → ℚ := ![1, 2] + +/-- The multiplicities `1, 2`. -/ +private abbrev mult : Fin 2 → ℕ := ![1, 2] + +private theorem node_pairwise : + ((Finset.univ : Finset (Fin 2)) : Set (Fin 2)).Pairwise fun i j => IsUnit (node i - node j) := + fun i _ j _ hij => isUnit_iff_ne_zero.mpr <| by + fin_cases i <;> fin_cases j <;> first | exact absurd rfl hij | norm_num + +private theorem hermiteBasis_zero : hermiteBasis Finset.univ node mult 0 = (X - C 2) ^ 2 := by + rw [hermiteBasis, show (Finset.univ : Finset (Fin 2)).erase 0 = {1} by decide, + Finset.prod_singleton] + norm_num [Ring.inverse_eq_inv'] + ring + +private theorem hermiteBasis_one : hermiteBasis Finset.univ node mult 1 = X - C 1 := by + rw [hermiteBasis, show (Finset.univ : Finset (Fin 2)).erase 1 = {0} by decide, + Finset.prod_singleton] + norm_num [Ring.inverse_eq_inv'] + +/-- The Hermite quotient of `X ^ 2 + 3` at the node `1` of multiplicity `1` is `4`. -/ +example : hermiteQuotient Finset.univ node mult 1 0 ((X ^ 2 + C 3 : ℚ[X]).comp (C 1 + C 1 * X)) = + C 4 := by + refine hermiteQuotient_eq_of_X_pow_dvd node_pairwise 1 (Finset.mem_univ 0) + ((degree_C_le).trans_lt (by decide)) ⟨C 10 - C 3 * X, ?_⟩ + rw [hermiteBasis_zero] + simp only [node, Matrix.cons_val_zero, add_comp, pow_comp, sub_comp, X_comp, C_comp] + simp only [map_ofNat, map_one] + ring + +/-- The Hermite quotient of `X ^ 2 + 3` at the node `2` of multiplicity `2` is `7 - 3 z`. -/ +example : hermiteQuotient Finset.univ node mult 1 1 ((X ^ 2 + C 3 : ℚ[X]).comp (C 2 + C 1 * X)) = + C 7 - C 3 * X := by + refine hermiteQuotient_eq_of_X_pow_dvd node_pairwise 1 (Finset.mem_univ 1) ?_ ⟨C 4, ?_⟩ + · refine (degree_sub_le _ _).trans_lt (max_lt ((degree_C_le).trans_lt (by decide)) ?_) + exact (degree_C_mul_X_le _).trans_lt (by decide) + · rw [hermiteBasis_one] + simp only [node, Matrix.cons_val_one, Matrix.cons_val_zero, add_comp, pow_comp, sub_comp, + X_comp, C_comp] + simp only [map_ofNat, map_one] + ring + +/-- **(D.9) at two nodes of multiplicities `1, 2`.** Every polynomial of degree less than `3` has +`p (0) = E₀ (0) Q₀ (-1) + E₁ (0) Q₁ (-2) = 4 Q₀ (-1) - Q₁ (-2)`, where `Q_i` is the Hermite quotient +of `p` at the node `i`. -/ +example (p : ℚ[X]) (hp : p.degree < 3) : + p.eval 0 = + 4 * (hermiteQuotient Finset.univ node mult 1 0 (p.comp (C 1 + C 1 * X))).eval (-1) - + (hermiteQuotient Finset.univ node mult 1 1 (p.comp (C 2 + C 1 * X))).eval (-2) := by + have h3 : ∑ i ∈ Finset.univ, mult i = 3 := by decide + rw [eval_eq_sum_hermiteBasis_mul_hermiteQuotient (J := mult) node_pairwise 1 + (by rw [h3]; exact_mod_cast hp) 0, + Fin.sum_univ_two, hermiteBasis_zero, hermiteBasis_one] + norm_num + ring + end ComplexityTests.HermiteInterpolation