Symmetry.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Character identities for polynomial convolution

The boundary convolution tensors are dot products. In the sixfold character product, each possible singleton leg appears exactly twice. Consequently the normalization by the average dot-product exponent gives the boundary values of the polynomial profile from Section 5.

theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.sixfoldProduct_dotPairing line 27
Source documentation
A symmetric dot product occurs twice in each of its three leg positions.
```
theorem sixfoldProduct_dotPairing (n : ℕ) :
    χ.sixfoldProduct (Tensor.dotPairing (K := ℂ) (Fin n)) =
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.sixfoldProduct_convolution_one_left line 56
Source documentation
The boundary C(1,b) has the sixfold product of a dot product.
```
theorem sixfoldProduct_convolution_one_left (b : ℕ) :
    χ.sixfoldProduct (convolution 1 b) =
      χ.sixfoldProduct (Tensor.dotPairing (K := ℂ) (Fin b)) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.convolution
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.sixfoldProduct_convolution_one_right line 70
Source documentation
The boundary C(a,1) has the same dot-product product.
```
theorem sixfoldProduct_convolution_one_right (a : ℕ) :
    χ.sixfoldProduct (convolution a 1) =
      χ.sixfoldProduct (Tensor.dotPairing (K := ℂ) (Fin a)) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.convolution
def OAI.MatrixMultiplication.AuxiliarySeparation.Character.meanExponent line 76
Source documentation
The mean of the character's three singleton-leg exponents.
```
def meanExponent : ℝ := (χ.pX + χ.pY + χ.pZ) / 3
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.meanExponent_nonneg line 78
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.meanExponent_le_one line 82
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.sixfoldProduct_dotPairing_eq_rpow line 90
Source documentation
The three exponents occur twice in the sixfold boundary product.
```
theorem sixfoldProduct_dotPairing_eq_rpow {n : ℕ} (hn : 0 < n) :
    χ.sixfoldProduct (Tensor.dotPairing (K := ℂ) (Fin n)) =
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.sixfoldProduct_convolution_one_left_eq_rpow line 104
Source documentation
The positive-size boundary product has its exact normalized power.
```
theorem sixfoldProduct_convolution_one_left_eq_rpow {b : ℕ} (hb : 0 < b) :
    χ.sixfoldProduct (convolution 1 b) = (b : ℝ) ^ (6 * χ.meanExponent) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.convolution
def OAI.MatrixMultiplication.AuxiliarySeparation.Character.convolutionProfile line 109
Source documentation
The polynomial profile P(a,b) normalized by the actual mean exponent.
```
def convolutionProfile (a b : ℕ) : ℝ :=
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.convolutionProfile_comm line 113
Source documentation
Swapping the two polynomial inputs preserves the normalized profile.
```
theorem convolutionProfile_comm (a b : ℕ) :
    χ.convolutionProfile a b = χ.convolutionProfile b a := by
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.convolutionProfile_nonneg line 118
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.convolutionProfile_pos line 122
Source documentation
Nonzero polynomial multiplication gives a positive normalized profile.
```
theorem convolutionProfile_pos {a b : ℕ} (ha : 0 < a) (hb : 0 < b) :
    0 < χ.convolutionProfile a b :=
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.convolutionProfile_le line 127
Source documentation
The evaluation/interpolation algorithm bounds the normalized profile.
```
theorem convolutionProfile_le {a b : ℕ} (ht : 0 < χ.meanExponent) :
    χ.convolutionProfile a b ≤ (a + b - 1 : ℕ) ^ (1 / χ.meanExponent) :=
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.convolutionProfile_one_left line 132
Source documentation
The normalization gives the exact initial value P(1,b) = b.
```
theorem convolutionProfile_one_left {b : ℕ} (ht : 0 < χ.meanExponent) (hb : 0 < b) :
    χ.convolutionProfile 1 b = b := by
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.convolutionProfile_one_right line 142
Source documentation
Input symmetry gives the other exact initial value P(a,1) = a.
```
theorem convolutionProfile_one_right {a : ℕ} (ht : 0 < χ.meanExponent) (ha : 0 < a) :
    χ.convolutionProfile a 1 = a := by
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_convolution_le line 147
Source documentation
Interpolation bounds an individual character on polynomial convolution.
```
theorem value_convolution_le (a b : ℕ) :
    χ.value (convolution a b) ≤ (a + b - 1 : ℕ) :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.convolution
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_convolution_pos line 152
Source documentation
Positive input sizes give a positive individual character value.
```
theorem value_convolution_pos {a b : ℕ} (ha : 0 < a) (hb : 0 < b) :
    0 < χ.value (convolution a b) :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.convolution