Polynomial tensor restrictions and exact coefficient extraction.

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.restrictPolynomial {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} [CommSemiring F] [Fintype X] [Fintype Y] [Fintype Z] (A : X' → X → F) (B : Y' → Y → F) (C : Z' → Z → F) (P : Tensor (Polynomial F) X Y Z) : Tensor (Polynomial F) X' Y' Z'

Restrict a polynomial tensor using coordinate maps with constant polynomial coefficients.

Equations

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

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.restrictPolynomial_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} [CommSemiring F] [Fintype X] [Fintype Y] [Fintype Z] (A : X' → X → F) (B : Y' → Y → F) (C : Z' → Z → F) (P : Tensor (Polynomial F) X Y Z) (k : ℕ) (x' : X') (y' : Y') (z' : Z') : (restrictPolynomial A B C P x' y' z').coeff k = restrict A B C (fun (x : X) (y : Y) (z : Z) => (P x y z).coeff k) x' y' z'

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.RankAtMost.restrictPolynomial {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} [CommSemiring F] [Fintype X] [Fintype Y] [Fintype Z] {P : Tensor (Polynomial F) X Y Z} {r : ℕ} (hP : P.RankAtMost r) (A : X' → X → F) (B : Y' → Y → F) (C : Z' → Z → F) : (Tensor.restrictPolynomial A B C P).RankAtMost r

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.restrictPolynomial_degree_le {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} [CommSemiring F] [Fintype X] [Fintype Y] [Fintype Z] (A : X' → X → F) (B : Y' → Y → F) (C : Z' → Z → F) (P : Tensor (Polynomial F) X Y Z) (D : ℕ) (hdegree : ∀ (x : X) (y : Y) (z : Z), (P x y z).degree ≤ ↑D) (x' : X') (y' : Y') (z' : Z') : (restrictPolynomial A B C P x' y' z').degree ≤ ↑D

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.ofRankAtMost {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 : ℕ) (hT : T.RankAtMost r) : T.PolynomialApproximation r 0 0

Regard an exact rank decomposition as a degree-zero polynomial approximation.

Equations

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

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.ofRankAtMost_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 : ℕ) (hT : T.RankAtMost r) : (ofRankAtMost T r hT).polynomial = fun (x : X) (y : Y) (z : Z) => Polynomial.C (T x y z)

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.restrict {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} {r d D : ℕ} (W : T.PolynomialApproximation r d D) (A : X' → X → F) (B : Y' → Y → F) (C : Z' → Z → F) : (Tensor.restrict A B C T).PolynomialApproximation r d D

Apply fixed linear coordinate maps to a polynomial approximation.

Equations

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

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.PolynomialApproximation.restrict_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} {r d D : ℕ} (W : T.PolynomialApproximation r d D) (A : X' → X → F) (B : Y' → Y → F) (C : Z' → Z → F) : (W.restrict A B C).polynomial = restrictPolynomial A B C W.polynomial