Character.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

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.

def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.branch line 27

Source documentation

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

def branch (d e : ℕ) (n : Fin 2) :
    Tensor ℂ (Fin (d + 1)) (Index e) (Index (d + e))
  | i, .inl j, .inl k => if n = 0 then if i.val + j.val = k.val then 1 else 0 else 0
  | i, .inr j, .inr k => if n = 1 then if i.val + j.val = k.val then 1 else 0 else 0
  | _, _, _ => 0

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.Index

def OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.branchLabel line 33
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.branch_support line 37
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.sum_branch line 43
theorem OAI.MatrixMultiplication.AuxiliarySeparation.DeterminantFiltration.branch_ne_zero line 48
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_determinant_branch_zero line 66
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_determinant_branch_one line 89
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_bool_dot line 112
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_determinant_source_le line 127
Source documentation
The auxiliary dot product is charged once, on the actual source tensor.
```
theorem value_determinant_source_le (d e : ℕ) :
    χ.value (sourceTensor d e) ≤
      (2 : ℝ) ^ χ.pX * χ.value (convolution (d + 1) (e + 1)) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.convolution
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_determinant_graded_le line 136
Source documentation
Actual basis-change and degeneration certificates give this comparison.
```
theorem value_determinant_graded_le (d e : ℕ) :
    χ.value (gradedTensor d e) ≤
      (2 : ℝ) ^ χ.pX * χ.value (convolution (d + 1) (e + 1)) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.convolution

theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.convolution_concavity_tag_dims line 149

Source documentation

The binary tag bound before normalizing over all six characters.

theorem convolution_concavity_tag_dims (d e : ℕ) (he : 0 < e)
    (q : ℝ) (hq₀ : 0 ≤ q) (hq₁ : q ≤ 1) :
    Real.exp (χ.pX * Real.binEntropy q) *
        χ.value (convolution (d + 1) (e + 2)) ^ q *
        χ.value (convolution (d + 1) e) ^ (1 - q) ≤
      (2 : ℝ) ^ χ.pX * χ.value (convolution (d + 1) (e + 1)) := by
…

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.convolution

theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.convolution_concavity_tag line 166

Source documentation

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

theorem convolution_concavity_tag (a b : ℕ) (ha : 0 < a) (hb : 2 ≤ b)
    (q : ℝ) (hq₀ : 0 ≤ q) (hq₁ : q ≤ 1) :
    Real.exp (χ.pX * Real.binEntropy q) *
        χ.value (convolution a (b + 1)) ^ q *
        χ.value (convolution a (b - 1)) ^ (1 - q) ≤
      (2 : ℝ) ^ χ.pX * χ.value (convolution a b) := by
…

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.convolution