Documentation

LeanPool.MatrixMultiplicationAllFields.LinearAlgebra.MatrixMultiplication.AuxiliarySeparation.Sector.Character

The character inequality from the three-sector degeneration #

The retained tensor has three branches sharing its actual first-input space. Their two remaining coordinate intervals determine matching branch labels. The uniform three-branch tag inequality and polynomial degeneration then yield the character inequality of Section 5.2 before symmetrization.

source
noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.branchFamily (K : Type) [Field K] (a h : ℕ) (b : Fin 3) :
Foundation.Tensor K (Fin a) (YIndex a h) (ZIndex a h)

The actual three retained tensors in their original ambient spaces.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.branchFamily_zero {K : Type} [Field K] (a h : ℕ) :
    branchFamily K a h 0 = leftTensor K a h
    source
    @[simp]
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.branchFamily_one {K : Type} [Field K] (a h : ℕ) :
    branchFamily K a h 1 = middleTensor K a h
    source
    @[simp]
    theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.branchFamily_two {K : Type} [Field K] (a h : ℕ) :
    branchFamily K a h 2 = rightTensor K a h
    source
    def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.yLabel (a h : ℕ) (j : YIndex a h) :
    Fin 3

    Label a second-leg coordinate by its interval.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.zLabel (a h : ℕ) (k : ZIndex a h) :
      Fin 3

      Label a third-leg coordinate by its corresponding interval.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.branchFamily_labels {K : Type} [Field K] (a h : ℕ) (b : Fin 3) (i : Fin a) (j : YIndex a h) (k : ZIndex a h) (hn : branchFamily K a h b i j k ≠ 0) :
        yLabel a h j = b ∧ zLabel a h k = b

        Every nonzero branch coefficient lies in the two matching labelled sectors.

        source
        theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.sum_branchFamily {K : Type} [Field K] (a h : ℕ) :
        ∑ b : Fin 3, branchFamily K a h b = retained K a h

        The branch family sums to exactly the retained tensor.

        source
        theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.value_retained_le_source {K : Type} [Field K] [IsAlgClosed K] (χ : Character K) (a h : ℕ) :
        χ.value (retained K a h) ≤ χ.value (source K a h)

        The character comparison uses the actual polynomial degeneration.

        source
        theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.value_sharedFirst_branchFamily {K : Type} [Field K] (χ : Character K) (a h : ℕ) :
        χ.value (sharedFirstTensor (branchFamily K a h)) = χ.value (retained K a h)

        Both interval labels can be recovered without changing the common first input, so the tagged branch tensor has precisely the retained tensor's value.

        source
        theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.branchFamily_nonzero {K : Type} [Field K] {a h : ℕ} (ha : 0 < a) (hh : 0 < h) (b : Fin 3) :
        branchFamily K a h b ≠ 0
        source
        theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.uniform_branchFamily_product {K : Type} [Field K] (χ : Character K) (a h : ℕ) (ha : 0 < a) (hh : 0 < h) :
        ∏ b : Fin 3, χ.value (branchFamily K a h b) ^ (Foundation.FiniteLaw.uniform (Fin 3)).mass b = χ.value (convolution K a h) ^ (2 / 3) * χ.value (exchangedConvolution K a h) ^ (1 / 3)

        The uniform branch product combines the two outer convolution values.

        source
        theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Sector.convolution_tripling_tag {K : Type} [Field K] [IsAlgClosed K] (χ : Character K) (a h : ℕ) (ha : 0 < a) (hh : 0 < h) :
        3 ^ χ.pX * χ.value (convolution K a h) ^ (2 / 3) * (χ.value fun (i : Fin a) (s : Fin (a + h - 1)) (r : Fin h) => convolution K a h i r s) ^ (1 / 3) ≤ χ.value (convolution K a (3 * h + a - 1))

        The per-character three-sector inequality, before multiplication over the six tensor-leg permutations. All tensor values are actual convolution values, with only the middle branch exchanging its last two legs.