Documentation

LeanPool.MatrixMultiplicationAllFields.LinearAlgebra.MatrixMultiplication.AuxiliarySeparation.Polynomial.Interpolation

Exact interpolation away from zero #

The coefficient-extraction theorem already proved for matrix multiplication is used here with D + 1 pairwise distinct nonzero elements of K, chosen using an embedding of the naturals (interpolationNode). In particular a polynomial degeneration can be recovered by a finite sum of its ordinary restrictions at nonzero parameters, with the leading power divided out at each parameter.

source
theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.infinite_nonzero {K : Type} [Field K] [Infinite K] :
Infinite ↑{0}ᶜ

The nonzero elements of an infinite field form an infinite set.

source
noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.interpolationNode (K : Type) [Field K] [IsAlgClosed K] (D : ℕ) (i : Fin (D + 1)) :
K

A choice of D + 1 distinct nonzero interpolation parameters. Over ℂ the paper uses 1, ..., D + 1; here any infinite field suffices (an algebraically closed field is infinite), so the parameters are taken from an embedding of ℕ into the nonzero elements.

Equations
Instances For
    source
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.interpolationNode_injective {K : Type} [Field K] [IsAlgClosed K] (D : ℕ) :
    Function.Injective (interpolationNode K D)
    source
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.interpolationNode_ne_zero {K : Type} [Field K] [IsAlgClosed K] (D : ℕ) (i : Fin (D + 1)) :
    interpolationNode K D i ≠ 0
    source
    noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.constantInterpolationWeight {K : Type} [Field K] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (nodes : ι → K) (i : ι) :
    K

    The constant-coefficient functional expressed in the Lagrange basis.

    Equations
    Instances For
      source
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.constant_eq_sum_eval {K : Type} [Field K] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (nodes : ι → K) (hinj : Function.Injective nodes) (p : Polynomial K) (hdegree : p.degree < ↑(Fintype.card ι)) :
      p.coeff 0 = ∑ i : ι, constantInterpolationWeight nodes i * Polynomial.eval (nodes i) p

      Exact constant recovery; this specializes the existing coefficient theorem.

      source
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.constant_eq_sum_nonzero_eval {K : Type} [Field K] [IsAlgClosed K] (D : ℕ) (p : Polynomial K) (hdegree : p.degree ≤ ↑D) :
      p.coeff 0 = ∑ i : Fin (D + 1), constantInterpolationWeight (interpolationNode K D) i * Polynomial.eval (interpolationNode K D i) p

      A degree-D polynomial is recovered at zero using only nonzero parameters.

      source
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.leading_eq_sum_normalized_eval {K : Type} [Field K] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (nodes : ι → K) (hinj : Function.Injective nodes) (hnonzero : ∀ (i : ι), nodes i ≠ 0) (p q : Polynomial K) (d : ℕ) (hp : p = Polynomial.X ^ d * q) (hdegree : q.degree < ↑(Fintype.card ι)) :
      p.coeff d = ∑ i : ι, constantInterpolationWeight nodes i * (nodes i ^ d)⁻¹ * Polynomial.eval (nodes i) p

      Removing a leading power before interpolation only requires evaluations at nonzero nodes. The degree bound is on the normalized polynomial.

      source
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.leading_eq_sum_nonzero_eval {K : Type} [Field K] [IsAlgClosed K] (D d : ℕ) (p : Polynomial K) (hvanish : ∀ j < d, p.coeff j = 0) (hdegree : p.degree ≤ ↑D) :
      p.coeff d = ∑ i : Fin (D + 1), constantInterpolationWeight (interpolationNode K D) i * (interpolationNode K D i ^ d)⁻¹ * Polynomial.eval (interpolationNode K D i) p

      A leading coefficient is a finite linear combination of normalized evaluations, assuming all lower coefficients vanish.

      source
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.restrictionDegeneration_eval {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {X' : Type u_4} {Y' : Type u_5} {Z' : Type u_6} [Fintype X] [Fintype Y] [Fintype Z] {T : Foundation.Tensor K X Y Z} {U : Foundation.Tensor K X' Y' Z'} {k Lx Ly Lz : ℕ} (L : T.PolynomialRestrictionDegeneration U k Lx Ly Lz) (t : K) (x' : X') (y' : Y') (z' : Z') :
      Polynomial.eval t (L.basePolynomial x' y' z') = Foundation.Tensor.restrict (fun (a : X') (x : X) => Polynomial.eval t (L.leftMap a x)) (fun (b : Y') (y : Y) => Polynomial.eval t (L.middleMap b y)) (fun (c : Z') (z : Z) => Polynomial.eval t (L.rightMap c z)) T x' y' z'

      Evaluating the polynomial restriction evaluates its three local maps.

      source
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.restrictionDegeneration_degree {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {X' : Type u_4} {Y' : Type u_5} {Z' : Type u_6} [Fintype X] [Fintype Y] [Fintype Z] {T : Foundation.Tensor K X Y Z} {U : Foundation.Tensor K X' Y' Z'} {k Lx Ly Lz : ℕ} (L : T.PolynomialRestrictionDegeneration U k Lx Ly Lz) (x' : X') (y' : Y') (z' : Z') :
      (L.basePolynomial x' y' z').degree ≤ ↑(Lx + Ly + Lz)

      The degree of a polynomial restriction is bounded by the sum of the degrees of its three local maps.

      source
      noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.restrictionDegenerationApproximation {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {X' : Type u_4} {Y' : Type u_5} {Z' : Type u_6} [Fintype X] [Fintype Y] [Fintype Z] {T : Foundation.Tensor K X Y Z} {U : Foundation.Tensor K X' Y' Z'} {k Lx Ly Lz : ℕ} (L : T.PolynomialRestrictionDegeneration U k Lx Ly Lz) {r : ℕ} (hT : T.RankAtMost r) :
      U.PolynomialApproximation r k (Lx + Ly + Lz)

      The existing polynomial-approximation API applies to a polynomial restriction as soon as the source tensor has a rank bound.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.restrictionDegeneration_recovery {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {X' : Type u_4} {Y' : Type u_5} {Z' : Type u_6} [Fintype X] [Fintype Y] [Fintype Z] {T : Foundation.Tensor K X Y Z} {U : Foundation.Tensor K X' Y' Z'} {k Lx Ly Lz : ℕ} [IsAlgClosed K] (L : T.PolynomialRestrictionDegeneration U k Lx Ly Lz) (x' : X') (y' : Y') (z' : Z') :
        U x' y' z' = ∑ i : Fin (Lx + Ly + Lz + 1), constantInterpolationWeight (interpolationNode K (Lx + Ly + Lz)) i * (interpolationNode K (Lx + Ly + Lz) i ^ k)⁻¹ * Foundation.Tensor.restrict (fun (a : X') (x : X) => Polynomial.eval (interpolationNode K (Lx + Ly + Lz) i) (L.leftMap a x)) (fun (b : Y') (y : Y) => Polynomial.eval (interpolationNode K (Lx + Ly + Lz) i) (L.middleMap b y)) (fun (c : Z') (z : Z) => Polynomial.eval (interpolationNode K (Lx + Ly + Lz) i) (L.rightMap c z)) T x' y' z'

        A polynomial degeneration yields an exact finite sum of ordinary restrictions at nonzero parameters. There are Lx + Ly + Lz + 1 terms.

        source
        theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.restrictionDegeneration_rankAtMost {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {X' : Type u_4} {Y' : Type u_5} {Z' : Type u_6} [Fintype X] [Fintype Y] [Fintype Z] {T : Foundation.Tensor K X Y Z} {U : Foundation.Tensor K X' Y' Z'} {k Lx Ly Lz : ℕ} [IsAlgClosed K] (L : T.PolynomialRestrictionDegeneration U k Lx Ly Lz) {r : ℕ} (hT : T.RankAtMost r) :
        U.RankAtMost ((Lx + Ly + Lz + 1) * r)

        Finite interpolation converts a polynomial degeneration into an exact rank bound with its explicit number of evaluation parameters.