FiniteSeparation.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The character bound from finite separation

The explicit Fourier and square-weight construction gives a polynomial tensor whose nonzero evaluations restrict from exactly 5M complete source copies. Character monotonicity follows by interpolation and tensor powering; it does not require continuity of the character.

theorem OAI.MatrixMultiplication.AuxiliarySeparation.polynomial_rank_bound line 28
def OAI.MatrixMultiplication.AuxiliarySeparation.separationPolynomialApproximation line 43
Source documentation
The explicit separation polynomial, viewed as a polynomial approximation to its constant tensor. Its rank bound is supplied by a coordinate expansion.
```
def separationPolynomialApproximation {ζ : ℂ} (hM : 0 < M)
    (hζ : IsPrimitiveRoot ζ (5 * M)) (B : Fin M → Tensor ℂ X Y Z) :
    Tensor.PolynomialApproximation (separationTarget B)
      (Fintype.card ((X × Fin M) × ((Fin M × Y) × Fin M))) 0 ((M - 1) ^ 2) where
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.separationTarget
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_separationTarget_le line 63
Source documentation
The separated constant tensor costs at most the character of the 5M source copies. This uses the explicit polynomial, not topological continuity.
```
theorem value_separationTarget_le (hM : 0 < M) (B : Fin M → Tensor ℂ X Y Z) :
    χ.value (separationTarget B) ≤
      5 * (M : ℝ) * χ.value (sharedFirstTensor B) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.separationTarget, OAI.MatrixMultiplication.AuxiliarySeparation.sharedFirstTensor
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_separationTarget line 81
Source documentation
Character accounting for the genuine direct sum in the separated tensor.
```
theorem value_separationTarget (hM : 0 < M) (B : Fin M → Tensor ℂ X Y Z) :
    χ.value (separationTarget B) =
      (∑ h, χ.value (B h)) * (M : ℝ) ^ χ.pX := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.separationTarget
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.finiteSeparation_bound line 90
Source documentation
Exact finite character separation: the common first coordinate can be separated at a cost of 5M, retaining an M-dimensional first-leg dot factor.
```
theorem finiteSeparation_bound (hM : 0 < M) (B : Fin M → Tensor ℂ X Y Z) :
    (∑ h, χ.value (B h)) * (M : ℝ) ^ χ.pX ≤
      5 * (M : ℝ) * χ.value (sharedFirstTensor B) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.sharedFirstTensor