Documentation

LeanPool.MatrixMultiplicationAllFields.LinearAlgebra.MatrixMultiplication.AuxiliarySeparation.Determinant.Character

The determinant inequality for an actual tensor character #

The shared-input tag inequality is applied to the two concrete branches of the checked determinant degeneration. All basis changes and the output-dual change are supplied by DeterminantFiltration.

source
def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.branch (K : Type) [Field K] (d e : ℕ) (n : Fin 2) :
Foundation.Tensor K (Fin (d + 1)) (Index e) (Index (d + e))

The two graded blocks, padded with zeros in common coordinate spaces.

Equations
Instances For
    source
    def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.branchLabel (e : ℕ) :
    Index e → Fin 2

    Label quotient coordinates by zero and kernel coordinates by one.

    Equations
    Instances For
      source
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.branch_support {K : Type} [Field K] (d e : ℕ) (n : Fin 2) (i : Fin (d + 1)) (j : Index e) (k : Index (d + e)) (h : branch K d e n i j k ≠ 0) :
      branchLabel e j = n ∧ branchLabel (d + e) k = n
      source
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.sum_branch {K : Type} [Field K] (d e : ℕ) :
      ∑ n : Fin 2, branch K d e n = gradedTensor K d e
      source
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.branch_ne_zero {K : Type} [Field K] (d e : ℕ) (he : 0 < e) (n : Fin 2) :
      branch K d e n ≠ 0
      source
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_determinant_branch_zero {K : Type} [Field K] (χ : Character K) (d e : ℕ) :
      χ.value (DeterminantFiltration.branch K d e 0) = χ.value (convolution K (d + 1) (e + 2))
      source
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_determinant_branch_one {K : Type} [Field K] (χ : Character K) (d e : ℕ) :
      χ.value (DeterminantFiltration.branch K d e 1) = χ.value (convolution K (d + 1) e)
      source
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_determinant_source_le {K : Type} [Field K] (χ : Character K) (d e : ℕ) :
      χ.value (DeterminantFiltration.sourceTensor K d e) ≤ 2 ^ χ.pX * χ.value (convolution K (d + 1) (e + 1))

      The auxiliary dot product is charged once, on the actual source tensor.

      source
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_determinant_graded_le {K : Type} [Field K] (χ : Character K) [IsAlgClosed K] (d e : ℕ) :
      χ.value (DeterminantFiltration.gradedTensor K d e) ≤ 2 ^ χ.pX * χ.value (convolution K (d + 1) (e + 1))

      Actual basis-change and degeneration certificates give this comparison.

      source
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.convolution_concavity_tag_dims {K : Type} [Field K] (χ : Character K) [IsAlgClosed K] (d e : ℕ) (he : 0 < e) (q : ℝ) (hq₀ : 0 ≤ q) (hq₁ : q ≤ 1) :
      Real.exp (χ.pX * Real.binEntropy q) * χ.value (convolution K (d + 1) (e + 2)) ^ q * χ.value (convolution K (d + 1) e) ^ (1 - q) ≤ 2 ^ χ.pX * χ.value (convolution K (d + 1) (e + 1))

      The binary tag bound before normalizing over all six characters.

      source
      theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.convolution_concavity_tag {K : Type} [Field K] (χ : Character K) [IsAlgClosed K] (a b : ℕ) (ha : 0 < a) (hb : 2 ≤ b) (q : ℝ) (hq₀ : 0 ≤ q) (hq₁ : q ≤ 1) :
      Real.exp (χ.pX * Real.binEntropy q) * χ.value (convolution K a (b + 1)) ^ q * χ.value (convolution K a (b - 1)) ^ (1 - q) ≤ 2 ^ χ.pX * χ.value (convolution K a b)

      The determinant inequality in the paper's positive-dimension notation.