Positivity and rank bounds for the normalized profile

The normalization exponent is positive when the mean singleton-leg exponent is positive. Under this hypothesis, passing to the profile preserves order, and a rank bound r becomes the bound r ^ (1 / t).

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.symmetrizedProfile_nonneg {K : Type} [Field K] (χ : Character K) {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z] (t : ℝ) (T : Foundation.Tensor K X Y Z) : 0 ≤ χ.symmetrizedProfile t T

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.symmetrizedProfile_pos {K : Type} [Field K] (χ : Character K) {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z] (t : ℝ) {T : Foundation.Tensor K X Y Z} (hT : T ≠ 0) : 0 < χ.symmetrizedProfile t T

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.one_le_symmetrizedProfile {K : Type} [Field K] (χ : Character K) {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z] {t : ℝ} (ht : 0 < t) {T : Foundation.Tensor K X Y Z} (hT : T ≠ 0) : 1 ≤ χ.symmetrizedProfile t T

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.symmetrizedProfile_product {K : Type} [Field K] (χ : Character K) {X Y Z U V W : Type} [Fintype X] [Fintype Y] [Fintype Z] [Fintype U] [Fintype V] [Fintype W] (t : ℝ) (T : Foundation.Tensor K X Y Z) (S : Foundation.Tensor K U V W) : χ.symmetrizedProfile t (T.product S) = χ.symmetrizedProfile t T * χ.symmetrizedProfile t S

Tensor products become products of normalized profile values.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.symmetrizedProfile_le_iff {K : Type} [Field K] (χ : Character K) {X Y Z U V W : Type} [Fintype X] [Fintype Y] [Fintype Z] [Fintype U] [Fintype V] [Fintype W] {t : ℝ} (ht : 0 < t) (T : Foundation.Tensor K X Y Z) (S : Foundation.Tensor K U V W) : χ.symmetrizedProfile t T ≤ χ.symmetrizedProfile t S ↔ χ.sixfoldProduct T ≤ χ.sixfoldProduct S

Positive normalization preserves the order of the underlying sixfold products.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.symmetrizedProfile_le_rank {K : Type} [Field K] (χ : Character K) {X Y Z : Type} [Fintype X] [Fintype Y] [Fintype Z] {t : ℝ} (ht : 0 < t) {T : Foundation.Tensor K X Y Z} {r : ℕ} (h : T.RankAtMost r) : χ.symmetrizedProfile t T ≤ ↑r ^ (1 / t)

The symmetrized profile has the rank bound used in Section 5.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.mul_symmetrizedProfile_le_of_le {K : Type} [Field K] (χ : Character K) {X Y Z U V W : Type} [Fintype X] [Fintype Y] [Fintype Z] [Fintype U] [Fintype V] [Fintype W] {t c : ℝ} (ht : 0 < t) (hc : 0 ≤ c) (T : Foundation.Tensor K X Y Z) (S : Foundation.Tensor K U V W) (h : c ^ (6 * t) * χ.sixfoldProduct T ≤ χ.sixfoldProduct S) : c * χ.symmetrizedProfile t T ≤ χ.symmetrizedProfile t S

A factor c ^ (6*t) in the sixfold product becomes c in the profile.