Basic.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Characters of finite complex tensors

The tensor operations in this file are the coefficient operations from MatrixMultiplication.Foundation.Tensor. A character is an assumption on those operations, not an assertion that a character exists. Restriction monotonicity forces invariance under independent invertible changes of coordinates, so this interface descends to the mutual-restriction classes of Section 3 of the paper.

def OAI.MatrixMultiplication.AuxiliarySeparation.unitTensor line 24
Source documentation
The scalar multiplication tensor, the multiplicative unit.
```
def unitTensor : Tensor ℂ PUnit PUnit PUnit := fun _ _ _ => 1
```
def OAI.MatrixMultiplication.AuxiliarySeparation.scalarTensor line 27
Source documentation
The direct sum of r scalar multiplication tensors, in diagonal coordinates.
```
def scalarTensor (r : ℕ) : Tensor ℂ (Fin r) (Fin r) (Fin r) :=
…
```
structure OAI.MatrixMultiplication.AuxiliarySeparation.Character line 35
Source documentation
A normalized, additive, multiplicative, restriction-monotone tensor valuation.
Index types vary over all finite types in Type. No character-existence result is included among the fields or claimed by this definition.
```
structure Character where
…
```

theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_pullback_le line 65

Source documentation

Coordinate pullbacks are restrictions.

theorem value_pullback_le (T : Tensor ℂ X Y Z)
    (fx : X' → X) (fy : Y' → Y) (fz : Z' → Z) :
    χ.value (Tensor.pullback fx fy fz T) ≤ χ.value T := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_reindex line 73

Source documentation

Independent coordinate bijections preserve a character.

theorem value_reindex (T : Tensor ℂ X Y Z)
    (ex : X' ≃ X) (ey : Y' ≃ Y) (ez : Z' ≃ Z) :
    χ.value (Tensor.pullback ex ey ez T) = χ.value T := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_eq_of_mutual_restriction line 85

Source documentation

The character has the same value on mutually restricting tensors.

theorem value_eq_of_mutual_restriction (T : Tensor ℂ X Y Z) (S : Tensor ℂ X' Y' Z')
    (A : X' → X → ℂ) (B : Y' → Y → ℂ) (C : Z' → Z → ℂ)
    (A' : X → X' → ℂ) (B' : Y → Y' → ℂ) (C' : Z → Z' → ℂ)
    (hS : S = Tensor.restrict A B C T) (hT : T = Tensor.restrict A' B' C' S) :
    χ.value T = χ.value S := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_scalarTensor line 99
Source documentation
An integer scalar tensor has its expected character value.
```
@[simp] theorem value_scalarTensor (r : ℕ) : χ.value (scalarTensor r) = r := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.scalarTensor

theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.restrict_scalarTensor line 110

Source documentation

Restricting a diagonal scalar tensor realizes a rank decomposition.

theorem restrict_scalarTensor (r : ℕ) (a : Fin r → X → ℂ)
    (b : Fin r → Y → ℂ) (c : Fin r → Z → ℂ) :
    Tensor.restrict (fun x i => a i x) (fun y i => b i y) (fun z i => c i z)
      (scalarTensor r) =
      fun x y z => ∑ i, Tensor.rankOne (a i) (b i) (c i) x y z := by
…

Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.scalarTensor

theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_le_rank line 120
Source documentation
Character values are bounded by every exact rank decomposition size.
```
theorem value_le_rank {T : Tensor ℂ X Y Z} {r : ℕ} (h : Tensor.RankAtMost T r) :
    χ.value T ≤ r := by
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.one_le_value line 127
Source documentation
Every nonzero tensor restricts to the scalar multiplication tensor.
```
theorem one_le_value {T : Tensor ℂ X Y Z} (hT : T ≠ 0) : 1 ≤ χ.value T := by
…
```
theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_eq_zero_iff line 142
Source documentation
Normalization and restriction monotonicity make the character faithful.
```
@[simp] theorem value_eq_zero_iff (T : Tensor ℂ X Y Z) : χ.value T = 0 ↔ T = 0 := by
…
```