Probability laws for the polynomial tensor inequalities

The determinant filtration uses an arbitrary binary law, while the three-sector filtration uses the uniform law on three branches.

def MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.binaryLaw (q : ℝ) (hq₀ : 0 ≤ q) (hq₁ : q ≤ 1) : Foundation.FiniteLaw (Fin 2)

The common binary probability law used for every permuted character.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.binaryLaw q hq₀ hq₁ = { mass := fun (i : Fin 2) => if i = 0 then q else 1 - q, nonneg := ⋯, total := ⋯ }

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.binaryLaw_zero (q : ℝ) (hq₀ : 0 ≤ q) (hq₁ : q ≤ 1) : (binaryLaw q hq₀ hq₁).mass 0 = q

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.binaryLaw_one (q : ℝ) (hq₀ : 0 ≤ q) (hq₁ : q ≤ 1) : (binaryLaw q hq₀ hq₁).mass 1 = 1 - q

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.binaryLaw_entropy (q : ℝ) (hq₀ : 0 ≤ q) (hq₁ : q ≤ 1) : Foundation.finiteEntropy (binaryLaw q hq₀ hq₁).mass = Real.binEntropy q

The finite-law entropy agrees exactly with the binary entropy convention.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.binaryLaw_product (q : ℝ) (hq₀ : 0 ≤ q) (hq₁ : q ≤ 1) (f : Fin 2 → ℝ) : ∏ i : Fin 2, f i ^ (binaryLaw q hq₀ hq₁).mass i = f 0 ^ q * f 1 ^ (1 - q)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.uniformThree_entropy_factor (p : ℝ) : Real.exp (p * Foundation.finiteEntropy (Foundation.FiniteLaw.uniform (Fin 3)).mass) = 3 ^ p

The three-sector entropy factor is 3 ^ p.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.uniformThree_product (f : Fin 3 → ℝ) : ∏ i : Fin 3, f i ^ (Foundation.FiniteLaw.uniform (Fin 3)).mass i = f 0 ^ (1 / 3) * f 1 ^ (1 / 3) * f 2 ^ (1 / 3)