Degeneration.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Characters decrease under polynomial degeneration

Finite interpolation expresses a polynomial's leading coefficient as a sum of evaluations. Applying it after tensor powering gives only a linear overhead, which disappears in the exponential growth rate. No continuity assumption on the character is used.

theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_scale_le line 28
Source documentation
Scalar multiplication is a restriction, including when the scalar is zero.
```
theorem value_scale_le (c : ℂ) (T : Tensor ℂ X Y Z) :
    χ.value (fun x y z => c * T x y z) ≤ χ.value T := by
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_scale line 44
Source documentation
Nonzero scalar multiplication preserves a character.
```
theorem value_scale (c : ℂ) (hc : c ≠ 0) (T : Tensor ℂ X Y Z) :
    χ.value (fun x y z => c * T x y z) = χ.value T := by
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_sum_le line 51
Source documentation
Adding tensors is a restriction of their independent direct sum.
```
theorem value_sum_le {ι : Type} [Fintype ι] (T : ι → Tensor ℂ X Y Z) :
    χ.value (fun x y z => ∑ i, T i x y z) ≤ ∑ i, χ.value (T i) := by
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_coefficient_le line 67
Source documentation
Exact interpolation bounds any polynomial coefficient by the sum of the character values of finitely many evaluation tensors.
```
theorem value_coefficient_le (P : Tensor (Polynomial ℂ) X Y Z) (d D : ℕ)
    (hdegree : ∀ x y z, (P x y z).degree ≤ D) :
    χ.value (fun x y z => (P x y z).coeff d) ≤
      ∑ i : Fin (D + 1), χ.value (fun x y z => (P x y z).eval (interpolationNode D i)) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.interpolationNode

theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_le_of_polynomialApproximation line 89

Source documentation

A uniform bound on nonzero evaluations bounds the leading tensor. The proof uses tensor powers and removes their linear interpolation overhead.

theorem value_le_of_polynomialApproximation
    {U : Tensor ℂ X Y Z} {r d D : ℕ}
    (A : Tensor.PolynomialApproximation U r d D) {b : ℝ} (hb : 0 ≤ b)
    (hbound : ∀ t : ℂ, t ≠ 0 →
      χ.value (fun x y z => (A.polynomial x y z).eval t) ≤ b) :
    χ.value U ≤ b := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.exists_rankAtMost line 128

theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_polynomialRestrictionDegeneration_le line 141

Source documentation

The character axioms imply monotonicity under polynomial degeneration. Continuity of the character is neither assumed nor used.

theorem value_polynomialRestrictionDegeneration_le
    {X' Y' Z' : Type} [Fintype X'] [Fintype Y'] [Fintype Z']
    {T : Tensor ℂ X Y Z} {U : Tensor ℂ X' Y' Z'} {k Lx Ly Lz : ℕ}
    (L : Tensor.PolynomialRestrictionDegeneration T U k Lx Ly Lz) :
    χ.value U ≤ χ.value T := by
…