Polynomial tensor restrictions and exact coefficient extraction.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.coeff_eq_sum_eval {F : Type u_1} [Field F] {ι : Type u_5} [Fintype ι] [DecidableEq ι] (nodes : ι → F) (hnodes : Function.Injective nodes) (p : Polynomial F) (d : ℕ) (hdegree : p.degree < ↑(Fintype.card ι)) : p.coeff d = ∑ i : ι, Polynomial.eval (nodes i) p * (Lagrange.basis Finset.univ nodes i).coeff d

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.coeff {F : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [Field F] {ι : Type u_5} [Fintype ι] (nodes : ι → F) (hnodes : Function.Injective nodes) {P : Tensor (Polynomial F) X Y Z} {r : ℕ} (hP : P.RankAtMost r) (d : ℕ) (hdegree : ∀ (x : X) (y : Y) (z : Z), (P x y z).degree < ↑(Fintype.card ι)) : RankAtMost (fun (x : X) (y : Y) (z : Z) => (P x y z).coeff d) (Fintype.card ι * r)

structure MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation {F : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [Field F] (T : Tensor F X Y Z) (r d D : ℕ) : Type (max (max (max u_1 u_2) u_3) u_4)

A bounded-degree, bounded-rank polynomial tensor with specified leading tensor and vanishing order.

• polynomial : Tensor (Polynomial F) X Y Z

  Polynomial coefficients of the approximating tensor family.

• rank_bound : self.polynomial.RankAtMost r
• vanishes (x : X) (y : Y) (z : Z) (k : ℕ) : k < d → (self.polynomial x y z).coeff k = 0
• leading (x : X) (y : Y) (z : Z) : (self.polynomial x y z).coeff d = T x y z
• degree_bound (x : X) (y : Y) (z : Z) : (self.polynomial x y z).degree ≤ ↑D

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.normalized {F : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [Field F] {T : Tensor F X Y Z} {r d D : ℕ} (A : T.PolynomialApproximation r d D) : Tensor (Polynomial F) X Y Z

Remove the common power of the polynomial variable from an approximation.

Equations

• A.normalized x y z = Classical.choose ⋯

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.polynomial_eq {F : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [Field F] {T : Tensor F X Y Z} {r d D : ℕ} (A : T.PolynomialApproximation r d D) (x : X) (y : Y) (z : Z) : A.polynomial x y z = Polynomial.X ^ d * A.normalized x y z

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.normalized_constant {F : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [Field F] {T : Tensor F X Y Z} {r d D : ℕ} (A : T.PolynomialApproximation r d D) (x : X) (y : Y) (z : Z) : (A.normalized x y z).coeff 0 = T x y z

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.power_polynomial_eq {F : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [Field F] {T : Tensor F X Y Z} {r d D : ℕ} (A : T.PolynomialApproximation r d D) (n : ℕ) (x : Fin n → X) (y : Fin n → Y) (z : Fin n → Z) : A.polynomial.power n x y z = Polynomial.X ^ (d * n) * A.normalized.power n x y z

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.power {F : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [Field F] {T : Tensor F X Y Z} {r d D : ℕ} (A : T.PolynomialApproximation r d D) (n : ℕ) : (T.power n).PolynomialApproximation (r ^ n) (d * n) (D * n)

Tensor-power a polynomial approximation, multiplying rank bounds and adding degrees.

Equations

• A.power n = { polynomial := A.polynomial.power n, rank_bound := ⋯, vanishes := ⋯, leading := ⋯, degree_bound := ⋯ }

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.rank_power {F : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [Field F] {T : Tensor F X Y Z} {r d D : ℕ} [CharZero F] (A : T.PolynomialApproximation r d D) (n : ℕ) : (T.power n).RankAtMost ((D * n + 1) * r ^ n)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.rank_normalized_eval {F : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [Field F] {T : Tensor F X Y Z} {r d D : ℕ} (A : T.PolynomialApproximation r d D) (t : F) (ht : t ≠ 0) : RankAtMost (fun (x : X) (y : Y) (z : Z) => Polynomial.eval t (A.normalized x y z)) r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.borderRankAtMost {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {r d D : ℕ} {S : Tensor ℂ X Y Z} (A : S.PolynomialApproximation r d D) : S.BorderRankAtMost r