OAI/LinearAlgebra/MatrixMultiplication/AuxiliarySeparation/Growth/NormalizedProfile.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

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).

  1. theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.symmetrizedProfile_nonneg line 24
  2. theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.symmetrizedProfile_pos line 28
  3. theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.one_le_symmetrizedProfile line 32
  4. theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.symmetrizedProfile_product line 37

    Source documentation

    Tensor products become products of normalized profile values.

    theorem symmetrizedProfile_product (t : ℝ) (T : Tensor ℂ X Y Z)
    (S : Tensor ℂ U V W) :
    χ.symmetrizedProfile t (Tensor.product T S) =
      χ.symmetrizedProfile t T * χ.symmetrizedProfile t S := by
…
  5. theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.symmetrizedProfile_le_iff line 45

    Source documentation

    Positive normalization preserves the order of the underlying sixfold products.

    theorem symmetrizedProfile_le_iff {t : ℝ} (ht : 0 < t)
    (T : Tensor ℂ X Y Z) (S : Tensor ℂ U V W) :
    χ.symmetrizedProfile t T ≤ χ.symmetrizedProfile t S ↔
      χ.sixfoldProduct T ≤ χ.sixfoldProduct S := by
…
  6. theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.symmetrizedProfile_le_rank line 53

    Source documentation

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

    theorem symmetrizedProfile_le_rank {t : ℝ} (ht : 0 < t)
    {T : Tensor ℂ X Y Z} {r : ℕ} (h : Tensor.RankAtMost T r) :
    χ.symmetrizedProfile t T ≤ (r : ℝ) ^ (1 / t) := by
…
  7. theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.mul_symmetrizedProfile_le_of_le line 67

    Source documentation

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

    theorem mul_symmetrizedProfile_le_of_le {t c : ℝ} (ht : 0 < t) (hc : 0 ≤ c)
    (T : Tensor ℂ X Y Z) (S : Tensor ℂ U V W)
    (h : c ^ (6 * t) * χ.sixfoldProduct T ≤ χ.sixfoldProduct S) :
    c * χ.symmetrizedProfile t T ≤ χ.symmetrizedProfile t S := by
…