Inequalities.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The inequalities for the polynomial profile

The six character values are combined before the common probability law is optimized. Each first-leg exponent occurs twice, so the total entropy exponent is exactly six times the mean exponent used to normalize the profile.

theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.permutedCharacter_meanExponent line 29
Source documentation
All six permuted characters have the same mean singleton-leg exponent.
```
theorem permutedCharacter_meanExponent (i : Fin 6) :
    (χ.permutedCharacter i).meanExponent = χ.meanExponent := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Character.meanExponent
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.sum_permutedCharacter_pX_mean line 34
Source documentation
The exponents of the six permuted characters have the normalization total.
```
theorem sum_permutedCharacter_pX_mean :
    (∑ i : Fin 6, (χ.permutedCharacter i).pX) = 6 * χ.meanExponent := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Character.pX
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.permutedCharacter_convolution_pos line 41
Source documentation
All six factors associated to a positive-size polynomial tensor are positive.
```
theorem permutedCharacter_convolution_pos {a b : ℕ} (ha : 0 < a) (hb : 0 < b)
    (i : Fin 6) : 0 < (χ.permutedCharacter i).value (convolution a b) :=
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.convolution
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.prod_permutedCharacter_swapped_convolution line 46
Source documentation
Exchanging the two output-side positions reorders the six convolution factors.
```
theorem prod_permutedCharacter_swapped_convolution (a b : ℕ) :
    (∏ i : Fin 6, (χ.permutedCharacter i).value
      (fun x z y => convolution a b x y z)) =
    ∏ i : Fin 6, (χ.permutedCharacter i).value (convolution a b) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.convolution

theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.convolutionProfile_concave line 54

Source documentation

The actual polynomial profile is concave in its second positive index.

theorem convolutionProfile_concave {a b : ℕ} (ht : 0 < χ.meanExponent)
    (ha : 0 < a) (hb : 2 ≤ b) :
    χ.convolutionProfile a (b - 1) + χ.convolutionProfile a (b + 1) ≤
      2 * χ.convolutionProfile a b := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.convolutionProfile_tripling line 75

Source documentation

The actual three-sector degeneration triples the normalized profile.

theorem convolutionProfile_tripling {a h : ℕ} (ht : 0 < χ.meanExponent)
    (ha : 0 < a) (hh : 0 < h) :
    3 * χ.convolutionProfile a h ≤ χ.convolutionProfile a (3 * h + a - 1) := by
…

def OAI.MatrixMultiplication.AuxiliarySeparation.Character.toScalarProfile line 97
Source documentation
The polynomial profile satisfies every hypothesis of the scalar growth theorem.
```
def toScalarProfile (ht : 0 < χ.meanExponent) : ScalarProfile χ.meanExponent where
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.ScalarProfile
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.meanExponent_le_three_quarters line 110
Source documentation
Every actual tensor character has mean singleton-leg exponent at most 3/4.
```
theorem meanExponent_le_three_quarters : χ.meanExponent ≤ 3 / 4 := by
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.exponent_sum_le_nine_quarters line 117
Source documentation
The three dot-product exponents of an actual character sum to at most 9/4.
```
theorem exponent_sum_le_nine_quarters : χ.pX + χ.pY + χ.pZ ≤ 9 / 4 := by
…
```