CharacterBounds.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Character values on powers and varying-dimension direct sums

These are consequences of the normalized restriction-monotone character interface. Coordinate changes preserve values; permuting the three tensor legs need not preserve an individual character.

theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_extendByZero line 31

Source documentation

Extending finite coordinates by zero does not change a character value.

theorem value_extendByZero (T : Tensor ℂ X Y Z)
    (fx : X → X') (fy : Y → Y') (fz : Z → Z')
    (hx : Function.Injective fx) (hy : Function.Injective fy)
    (hz : Function.Injective fz) :
    χ.value (Tensor.restrict
      (fun x' x => if fx x = x' then 1 else 0)
      (fun y' y => if fy y = y' then 1 else 0)
      (fun z' z => if fz z = z' then 1 else 0) T) = χ.value T := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_power line 61
Source documentation
Tensor powers turn a character value into an ordinary natural power.
```
@[simp] theorem value_power (T : Tensor ℂ X Y Z) (n : ℕ) :
    χ.value (Tensor.power T n) = χ.value T ^ n := by
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_copies line 84
Source documentation
Full independent copies contribute their exact multiplicity.
```
theorem value_copies (T : Tensor ℂ X Y Z) (r : ℕ) :
    χ.value (Tensor.directSum (fun _ : Fin r => T)) = r * χ.value T := by
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_power_copies line 90
Source documentation
The character cost of an exact number of full copies of a tensor power.
```
theorem value_power_copies (T : Tensor ℂ X Y Z) (r n : ℕ) :
    χ.value (Tensor.directSum (fun _ : Fin r => Tensor.power T n)) =
      r * χ.value T ^ n := by
…
```
def OAI.MatrixMultiplication.AuxiliarySeparation.Character.paddedBranch line 104
Source documentation
A branch extended to the common ambient sigma coordinate spaces.
```
def paddedBranch (T : ∀ i, Tensor ℂ (X i) (Y i) (Z i)) (i : ι) :
    Tensor ℂ (Σ i, X i) (Σ i, Y i) (Σ i, Z i) :=
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_paddedBranch line 111
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.paddedBranch_matching line 121
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.paddedBranch_zero_left line 128
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.paddedBranch_zero_middle line 137
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.paddedBranch_zero_right line 146

theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.directSum_paddedBranch line 155

Source documentation

Redundant outer labels give a zero extension of the varying-dimension sum.

theorem directSum_paddedBranch
    (T : ∀ i, Tensor ℂ (X i) (Y i) (Z i)) :
    Tensor.directSum (paddedBranch T) = Tensor.restrict
      (fun (x' : ι × (Σ i, X i)) x => if (x.1, x) = x' then 1 else 0)
      (fun (y' : ι × (Σ i, Y i)) y => if (y.1, y) = y' then 1 else 0)
      (fun (z' : ι × (Σ i, Z i)) z => if (z.1, z) = z' then 1 else 0)
      (Tensor.dependentDirectSum T) := by
…

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Character.paddedBranch

theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_dependentDirectSum line 203
Source documentation
Additivity holds even when each summand has different coordinate types.
```
theorem value_dependentDirectSum
    (T : ∀ i, Tensor ℂ (X i) (Y i) (Z i)) :
    χ.value (Tensor.dependentDirectSum T) = ∑ i, χ.value (T i) := by
…
```