Scalar.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Natural numbers and rank in the tensor semiring

The natural number r is the class of the diagonal scalar tensor with r terms. Consequently, comparison with r in the restriction order is exactly the existence of a rank decomposition with r terms.

theorem OAI.MatrixMultiplication.AuxiliarySeparation.scalarTensor_add_reindex line 22
Source documentation
Splitting the diagonal index set splits its scalar tensor into two blocks.
```
theorem scalarTensor_add_reindex (m n : ℕ) :
    Tensor.pullback (finSumFinEquiv : Fin m ⊕ Fin n ≃ Fin (m + n))
      finSumFinEquiv finSumFinEquiv (scalarTensor (m + n)) =
      sumTensor (scalarTensor m) (scalarTensor n) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.scalarTensor, OAI.MatrixMultiplication.AuxiliarySeparation.sumTensor
theorem OAI.MatrixMultiplication.AuxiliarySeparation.scalarTensor_rankAtMost line 32
Source documentation
A diagonal scalar tensor has its evident decomposition into simple terms.
```
theorem scalarTensor_rankAtMost (r : ℕ) : Tensor.RankAtMost (scalarTensor r) r := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.scalarTensor
theorem OAI.MatrixMultiplication.AuxiliarySeparation.exactRank_scalarTensor line 41
Source documentation
The diagonal flattening also gives the matching lower bound.
```
@[simp] theorem exactRank_scalarTensor (r : ℕ) : exactRank (scalarTensor r) = r := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.exactRank, OAI.MatrixMultiplication.AuxiliarySeparation.scalarTensor
theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf_scalarTensor_add line 50
Source documentation
Addition of the diagonal index sets is semiring addition.
```
theorem classOf_scalarTensor_add (m n : ℕ) :
    classOf (scalarTensor (m + n)) =
      classOf (scalarTensor m) + classOf (scalarTensor n) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf, OAI.MatrixMultiplication.AuxiliarySeparation.scalarTensor
theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf_scalarTensor_zero line 56
theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf_scalarTensor_one line 63
theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf_scalarTensor line 72
Source documentation
Natural numbers in the quotient semiring have their intended tensor meaning.
```
@[simp] theorem classOf_scalarTensor (r : ℕ) :
    classOf (scalarTensor r) = (r : TensorClass) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf, OAI.MatrixMultiplication.AuxiliarySeparation.scalarTensor, OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.TensorClass
theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.rankAtMost_iff_isRestriction_scalarTensor line 82
Source documentation
Exact rank decompositions are precisely restrictions of diagonal tensors.
```
theorem rankAtMost_iff_isRestriction_scalarTensor
    {X Y Z : Type*} [Fintype X] [Fintype Y] [Fintype Z]
    (T : Tensor ℂ X Y Z) (r : ℕ) :
    Tensor.RankAtMost T r ↔ IsRestriction T (scalarTensor r) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.IsRestriction, OAI.MatrixMultiplication.AuxiliarySeparation.scalarTensor
theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf_le_nat_iff_rankAtMost line 96
Source documentation
The restriction order below a natural number is exactly the usual rank bound.
```
theorem classOf_le_nat_iff_rankAtMost
    {X Y Z : Type*} [Fintype X] [Fintype Y] [Fintype Z]
    (T : Tensor ℂ X Y Z) (r : ℕ) :
    classOf T ≤ (r : TensorClass) ↔ Tensor.RankAtMost T r := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf, OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.TensorClass
theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.rank_natCast line 104
Source documentation
Rank takes its usual value on natural numbers in the tensor semiring.
```
@[simp] theorem rank_natCast (r : ℕ) : rank (r : TensorClass) = r := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.rank, OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.TensorClass
theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.le_rank line 108
Source documentation
The rank is a natural-number upper bound in the restriction order.
```
theorem le_rank (T : TensorClass) : T ≤ (rank T : TensorClass) := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.TensorClass, OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.rank
theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.natCast_le_natCast_iff line 117
Source documentation
The tensor restriction order induces the usual order on natural numbers.
```
@[simp] theorem natCast_le_natCast_iff (m n : ℕ) :
    (m : TensorClass) ≤ (n : TensorClass) ↔ m ≤ n := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.TensorClass
theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.le_nat_mul_of_ne_zero line 129
Source documentation
A natural multiple of any nonzero tensor contains any prescribed tensor by restriction.
```
theorem le_nat_mul_of_ne_zero (T S : TensorClass) (hS : S ≠ 0) :
    T ≤ (rank T : TensorClass) * S := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.TensorClass, OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.rank