Polynomial tensor restrictions and exact coefficient extraction.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.restrict_scalar_mul {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {X' : Type u_5} {Y' : Type u_6} {Z' : Type u_7} [CommSemiring K] [Fintype X] [Fintype Y] [Fintype Z] (A : X' → X → K) (B : Y' → Y → K) (C : Z' → Z → K) (P : Tensor K X Y Z) (s : K) : (restrict A B C fun (x : X) (y : Y) (z : Z) => s * P x y z) = fun (x' : X') (y' : Y') (z' : Z') => s * restrict A B C P x' y' z'

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.cyclic_restrict {K : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {X' : Type u_5} {Y' : Type u_6} {Z' : Type u_7} [CommSemiring K] [Fintype X] [Fintype Y] [Fintype Z] (A : X' → X → K) (B : Y' → Y → K) (C : Z' → Z → K) (P : Tensor K X Y Z) : (restrict A B C P).cyclic = restrict B C A P.cyclic

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.coeff_mul_expand_eq_constant {F : Type u_1} [Field F] (M p : Polynomial F) (a : F) (hp : p.coeff 0 = a) (k j : ℕ) (hj : j ≤ k) : (M * (Polynomial.expand F (k + 1)) p).coeff j = (M * Polynomial.C a).coeff j

structure MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialRestrictionDegeneration {F : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {X' : Type u_5} {Y' : Type u_6} {Z' : Type u_7} [Field F] [Fintype X] [Fintype Y] [Fintype Z] (T : Tensor F X Y Z) (U : Tensor F X' Y' Z') (k Lx Ly Lz : ℕ) : Type (max (max (max (max (max (max u_1 u_2) u_3) u_4) u_5) u_6) u_7)

Polynomial coordinate maps certifying a restriction degeneration with controlled degrees.

• leftMap : X' → X → Polynomial F

  Polynomial coordinate map on the first tensor leg.

• middleMap : Y' → Y → Polynomial F

  Polynomial coordinate map on the second tensor leg.

• rightMap : Z' → Z → Polynomial F

  Polynomial coordinate map on the third tensor leg.

• left_degree (x' : X') (x : X) : (self.leftMap x' x).degree ≤ ↑Lx
• middle_degree (y' : Y') (y : Y) : (self.middleMap y' y).degree ≤ ↑Ly
• right_degree (z' : Z') (z : Z) : (self.rightMap z' z).degree ≤ ↑Lz
• vanishes (x' : X') (y' : Y') (z' : Z') (j : ℕ) : j < k → (restrict self.leftMap self.middleMap self.rightMap (fun (x : X) (y : Y) (z : Z) => Polynomial.C (T x y z)) x' y' z').coeff j = 0
• leading (x' : X') (y' : Y') (z' : Z') : (restrict self.leftMap self.middleMap self.rightMap (fun (x : X) (y : Y) (z : Z) => Polynomial.C (T x y z)) x' y' z').coeff k = U x' y' z'

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialRestrictionDegeneration.cyclic {F : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {X' : Type u_5} {Y' : Type u_6} {Z' : Type u_7} [Field F] [Fintype X] [Fintype Y] [Fintype Z] {T : Tensor F X Y Z} {U : Tensor F X' Y' Z'} {k Lx Ly Lz : ℕ} (L : T.PolynomialRestrictionDegeneration U k Lx Ly Lz) : T.cyclic.PolynomialRestrictionDegeneration U.cyclic k Ly Lz Lx

Cyclically permute the legs of a certified polynomial restriction degeneration.

Equations

• L.cyclic = { leftMap := L.middleMap, middleMap := L.rightMap, rightMap := L.leftMap, left_degree := ⋯, middle_degree := ⋯, right_degree := ⋯, vanishes := ⋯, leading := ⋯ }

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialRestrictionDegeneration.basePolynomial {F : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {X' : Type u_5} {Y' : Type u_6} {Z' : Type u_7} [Field F] [Fintype X] [Fintype Y] [Fintype Z] {T : Tensor F X Y Z} {U : Tensor F X' Y' Z'} {k Lx Ly Lz : ℕ} (L : T.PolynomialRestrictionDegeneration U k Lx Ly Lz) : Tensor (Polynomial F) X' Y' Z'

Apply the degeneration's polynomial coordinate maps to the original tensor.

Equations

• L.basePolynomial = MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.restrict L.leftMap L.middleMap L.rightMap fun (x : X) (y : Y) (z : Z) => Polynomial.C (T x y z)

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialRestrictionDegeneration.compositionPolynomial {F : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {X' : Type u_5} {Y' : Type u_6} {Z' : Type u_7} [Field F] [Fintype X] [Fintype Y] [Fintype Z] {T : Tensor F X Y Z} {U : Tensor F X' Y' Z'} {k Lx Ly Lz r d D : ℕ} (L : T.PolynomialRestrictionDegeneration U k Lx Ly Lz) (W : T.PolynomialApproximation r d D) : Tensor (Polynomial F) X' Y' Z'

Compose a restriction degeneration with an approximation after expanding its polynomial variable.

Equations

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

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialRestrictionDegeneration.normalizedComposition {F : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {X' : Type u_5} {Y' : Type u_6} {Z' : Type u_7} [Field F] [Fintype X] [Fintype Y] [Fintype Z] {T : Tensor F X Y Z} {U : Tensor F X' Y' Z'} {k Lx Ly Lz r d D : ℕ} (L : T.PolynomialRestrictionDegeneration U k Lx Ly Lz) (W : T.PolynomialApproximation r d D) : Tensor (Polynomial F) X' Y' Z'

Compose the degeneration with the normalized approximation after expanding its variable.

Equations

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialRestrictionDegeneration.compositionPolynomial_eq {F : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {X' : Type u_5} {Y' : Type u_6} {Z' : Type u_7} [Field F] [Fintype X] [Fintype Y] [Fintype Z] {T : Tensor F X Y Z} {U : Tensor F X' Y' Z'} {k Lx Ly Lz r d D : ℕ} (L : T.PolynomialRestrictionDegeneration U k Lx Ly Lz) (W : T.PolynomialApproximation r d D) (x' : X') (y' : Y') (z' : Z') : L.compositionPolynomial W x' y' z' = Polynomial.X ^ (d * (k + 1)) * L.normalizedComposition W x' y' z'

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialRestrictionDegeneration.normalizedComposition_coeff {F : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {X' : Type u_5} {Y' : Type u_6} {Z' : Type u_7} [Field F] [Fintype X] [Fintype Y] [Fintype Z] {T : Tensor F X Y Z} {U : Tensor F X' Y' Z'} {k Lx Ly Lz r d D : ℕ} (L : T.PolynomialRestrictionDegeneration U k Lx Ly Lz) (W : T.PolynomialApproximation r d D) (j : ℕ) (hj : j ≤ k) (x' : X') (y' : Y') (z' : Z') : (L.normalizedComposition W x' y' z').coeff j = (L.basePolynomial x' y' z').coeff j

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialRestrictionDegeneration.compositionPolynomial_rank {F : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {X' : Type u_5} {Y' : Type u_6} {Z' : Type u_7} [Field F] [Fintype X] [Fintype Y] [Fintype Z] {T : Tensor F X Y Z} {U : Tensor F X' Y' Z'} {k Lx Ly Lz r d D : ℕ} (L : T.PolynomialRestrictionDegeneration U k Lx Ly Lz) (W : T.PolynomialApproximation r d D) : (L.compositionPolynomial W).RankAtMost r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialRestrictionDegeneration.compositionPolynomial_degree {F : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {X' : Type u_5} {Y' : Type u_6} {Z' : Type u_7} [Field F] [Fintype X] [Fintype Y] [Fintype Z] {T : Tensor F X Y Z} {U : Tensor F X' Y' Z'} {k Lx Ly Lz r d D : ℕ} (L : T.PolynomialRestrictionDegeneration U k Lx Ly Lz) (W : T.PolynomialApproximation r d D) (x' : X') (y' : Y') (z' : Z') : (L.compositionPolynomial W x' y' z').degree ≤ ↑D * (↑k + 1) + ↑Lx + ↑Ly + ↑Lz

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialRestrictionDegeneration.compose {F : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {X' : Type u_5} {Y' : Type u_6} {Z' : Type u_7} [Field F] [Fintype X] [Fintype Y] [Fintype Z] {T : Tensor F X Y Z} {U : Tensor F X' Y' Z'} {k Lx Ly Lz r d D : ℕ} (L : T.PolynomialRestrictionDegeneration U k Lx Ly Lz) (W : T.PolynomialApproximation r d D) : U.PolynomialApproximation r (d * (k + 1) + k) (D * (k + 1) + Lx + Ly + Lz)

Construct the composed polynomial approximation with explicit rank and degree bounds.

Equations

• L.compose W = { polynomial := L.compositionPolynomial W, rank_bound := ⋯, vanishes := ⋯, leading := ⋯, degree_bound := ⋯ }

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialRestrictionDegeneration.compose_polynomial {F : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {X' : Type u_5} {Y' : Type u_6} {Z' : Type u_7} [Field F] [Fintype X] [Fintype Y] [Fintype Z] {T : Tensor F X Y Z} {U : Tensor F X' Y' Z'} {k Lx Ly Lz r d D : ℕ} (L : T.PolynomialRestrictionDegeneration U k Lx Ly Lz) (W : T.PolynomialApproximation r d D) : (L.compose W).polynomial = restrict L.leftMap L.middleMap L.rightMap fun (x : X) (y : Y) (z : Z) => (Polynomial.expand F (k + 1)) (W.polynomial x y z)