Polynomial tensor restrictions and exact coefficient extraction.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.product_polynomial_eq {F : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {U : Type u_5} {V : Type u_6} {W : Type u_7} [Field F] {T : Tensor F X Y Z} {S : Tensor F U V W} {r s d e D E : ℕ} (A : T.PolynomialApproximation r d D) (B : S.PolynomialApproximation s e E) (x : X × U) (y : Y × V) (z : Z × W) : A.polynomial.product B.polynomial x y z = Polynomial.X ^ (d + e) * A.normalized.product B.normalized x y z

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.product {F : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {U : Type u_5} {V : Type u_6} {W : Type u_7} [Field F] {T : Tensor F X Y Z} {S : Tensor F U V W} {r s d e D E : ℕ} (A : T.PolynomialApproximation r d D) (B : S.PolynomialApproximation s e E) : (T.product S).PolynomialApproximation (r * s) (d + e) (D + E)

Tensor-product two approximations, multiplying their rank bounds and adding their degrees.

Equations

• A.product B = { polynomial := A.polynomial.product B.polynomial, rank_bound := ⋯, vanishes := ⋯, leading := ⋯, degree_bound := ⋯ }

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.product_polynomial {F : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {U : Type u_5} {V : Type u_6} {W : Type u_7} [Field F] {T : Tensor F X Y Z} {S : Tensor F U V W} {r s d e D E : ℕ} (A : T.PolynomialApproximation r d D) (B : S.PolynomialApproximation s e E) : (A.product B).polynomial = A.polynomial.product B.polynomial

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.productExact {F : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {U : Type u_5} {V : Type u_6} {W : Type u_7} [Field F] {T : Tensor F X Y Z} {r d D : ℕ} (A : T.PolynomialApproximation r d D) (S : Tensor F U V W) (s : ℕ) (hS : S.RankAtMost s) : (T.product S).PolynomialApproximation (r * s) d D

Tensor-product an approximation with an exactly rank-bounded tensor.

Equations

• A.productExact S s hS = A.product (MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.ofRankAtMost S s hS)

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.pullback {F : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {X' : Type u_8} {Y' : Type u_9} {Z' : Type u_10} [Field F] {T : Tensor F X Y Z} {r d D : ℕ} (A : T.PolynomialApproximation r d D) (fx : X' → X) (fy : Y' → Y) (fz : Z' → Z) : (Tensor.pullback fx fy fz T).PolynomialApproximation r d D

Pull a polynomial approximation back along maps of its coordinate sets.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.pullback_polynomial {F : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {X' : Type u_8} {Y' : Type u_9} {Z' : Type u_10} [Field F] {T : Tensor F X Y Z} {r d D : ℕ} (A : T.PolynomialApproximation r d D) (fx : X' → X) (fy : Y' → Y) (fz : Z' → Z) : (A.pullback fx fy fz).polynomial = Tensor.pullback fx fy fz A.polynomial

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.cyclic {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.cyclic.PolynomialApproximation r d D

Cyclically permute the three coordinate sets of a polynomial approximation.

Equations

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

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.cyclic_polynomial {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) : A.cyclic.polynomial = A.polynomial.cyclic

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.directSumProduct {F : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {U : Type u_5} {V : Type u_6} {W : Type u_7} [Field F] {r s d e D E : ℕ} {ι : Type u_11} {κ : Type u_12} [DecidableEq ι] [DecidableEq κ] {T : ι → Tensor F X Y Z} {S : κ → Tensor F U V W} (A : (directSum T).PolynomialApproximation r d D) (B : (directSum S).PolynomialApproximation s e E) : (directSum fun (i : ι × κ) => (T i.1).product (S i.2)).PolynomialApproximation (r * s) (d + e) (D + E)

Form the approximation for all pairwise products of two direct-sum families.

Equations

• One or more equations did not get rendered due to their size.

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.directSumPullback {F : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {X' : Type u_8} {Y' : Type u_9} {Z' : Type u_10} [Field F] {r d D : ℕ} {ι : Type u_11} [DecidableEq ι] {T : ι → Tensor F X Y Z} (A : (directSum T).PolynomialApproximation r d D) (fx : X' → X) (fy : Y' → Y) (fz : Z' → Z) : (directSum fun (i : ι) => Tensor.pullback fx fy fz (T i)).PolynomialApproximation r d D

Apply the same coordinate pullback to every direct-sum summand of an approximation.

Equations

• A.directSumPullback fx fy fz = A.pullback (fun (x : ι × X') => (x.1, fx x.2)) (fun (y : ι × Y') => (y.1, fy y.2)) fun (z : ι × Z') => (z.1, fz z.2)

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.directSumCyclic {F : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [Field F] {r d D : ℕ} {ι : Type u_11} [DecidableEq ι] {T : ι → Tensor F X Y Z} (A : (directSum T).PolynomialApproximation r d D) : (directSum fun (i : ι) => (T i).cyclic).PolynomialApproximation r d D

Cyclically permute every direct-sum summand of a polynomial approximation.

Equations

• A.directSumCyclic = ⋯.mp A.cyclic

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.matrixCoefficientsSymmetrized {F : Type u_1} [Field F] {r d D : ℕ} {A : Type u_11} {B : Type u_12} {C : Type u_13} [DecidableEq A] [DecidableEq B] [DecidableEq C] (P : (matrixCoefficients A B C).PolynomialApproximation r d D) : (matrixCoefficients (A × B × C) (A × B × C) (A × B × C)).PolynomialApproximation (r ^ 3) (3 * d) (3 * D)

Combine the three cyclic rectangular matrix tensors into a square matrix tensor approximation.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.matrixCoefficientsDirectSumSymmetrized {F : Type u_1} [Field F] {r d D : ℕ} {A : Type u_11} {B : Type u_12} {C : Type u_13} [DecidableEq A] [DecidableEq B] [DecidableEq C] {ι : Type u_14} [DecidableEq ι] (P : (directSum fun (x : ι) => matrixCoefficients A B C).PolynomialApproximation r d D) : (directSum fun (x : (ι × ι) × ι) => matrixCoefficients (A × B × C) (A × B × C) (A × B × C)).PolynomialApproximation (r ^ 3) (3 * d) (3 * D)

Symmetrize a direct sum of rectangular matrix tensors, cubing its rank and summand count.

Equations

• One or more equations did not get rendered due to their size.