OAI/LinearAlgebra/MatrixMultiplication/AuxiliarySeparation/Tensor/Semiring.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

Finite tensors modulo mutual restriction

Representatives have three natural-number dimensions and complex coefficients. The order is actual linear restriction, and equality in the quotient is mutual restriction. In particular, changing coordinates does not change the class.

  1. def OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.IsRestriction line 32

    Source documentation

    T is obtained from S by three linear maps on its coordinate spaces.

    def IsRestriction (T : Tensor ℂ X Y Z) (S : Tensor ℂ U V W) : Prop :=
…
  2. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.IsRestriction.refl line 36
  3. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.IsRestriction.trans line 41
  4. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.IsRestriction.pullback line 50
  5. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.IsRestriction.of_reindex line 57
  6. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.IsRestriction.reindex_iff line 66
  7. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.IsRestriction.product line 84
  8. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.IsRestriction.sum line 94
  9. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.IsRestriction.zero line 104
  10. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.IsRestriction.rank_le line 110
  11. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.IsRestriction.eq_zero_of_zero line 116
  12. structure OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.FiniteTensor line 126

    Source documentation

    A set-sized presentation of any finite complex coefficient tensor.

    structure FiniteTensor where
…
  13. def OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.FiniteTensor.ofTensor line 135

    Source documentation

    Replace arbitrary finite coordinate sets by standard finite sets.

    def ofTensor {X Y Z : Type*} [Fintype X] [Fintype Y] [Fintype Z]
    (T : Tensor ℂ X Y Z) : FiniteTensor where
…

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.FiniteTensor

  14. instance OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.FiniteTensor.(instance at line 143) line 143
  15. instance OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.FiniteTensor.(instance at line 145) line 145
  16. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.FiniteTensor.ofTensor_le_iff line 149
  17. def OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.FiniteTensor.product line 156
  18. def OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.FiniteTensor.sum line 159
  19. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.FiniteTensor.product_mono line 162
  20. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.FiniteTensor.sum_mono line 166
  21. abbrev OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.TensorClass line 174

    Source documentation

    Finite complex tensors, with two presentations identified exactly when each is a linear restriction of the other.

    abbrev TensorClass := Antisymmetrization FiniteTensor (· ≤ ·)

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.FiniteTensor

  22. def OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.tensorClass line 177

    Source documentation

    The class of a finite tensor presentation.

    def tensorClass (T : FiniteTensor) : TensorClass := toAntisymmetrization (· ≤ ·) T

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.FiniteTensor, OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.TensorClass

  23. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.tensorClass_eq_iff line 179
  24. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.tensorClass_le_iff line 183
  25. def OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf line 187

    Source documentation

    The quotient class of a tensor on any three finite coordinate sets.

    def classOf {X Y Z : Type*} [Fintype X] [Fintype Y] [Fintype Z]
    (T : Tensor ℂ X Y Z) : TensorClass := tensorClass (FiniteTensor.ofTensor T)

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.TensorClass, OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.tensorClass, OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.FiniteTensor.ofTensor

  26. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf_le_iff line 190
  27. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf_eq_iff line 196
  28. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf_reindex line 203
  29. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf_eq_of_reindex line 211
  30. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf_coeff line 219
  31. instance OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.(instance at line 223) line 223
  32. instance OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.(instance at line 229) line 229
  33. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.tensorClass_product line 234
  34. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.tensorClass_sum line 237
  35. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf_product line 240
  36. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf_sum line 251
  37. instance OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.(instance at line 274) line 274
  38. instance OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.(instance at line 275) line 275
  39. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf_zero line 277
  40. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.class_add_assoc line 281
  41. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.class_add_comm line 291
  42. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.class_add_zero line 299
  43. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.class_zero_add line 308
  44. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.class_mul_assoc line 311
  45. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.class_mul_comm line 321
  46. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.class_mul_one line 329
  47. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.class_one_mul line 337
  48. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.class_mul_zero line 340
  49. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.class_zero_mul line 351
  50. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.class_left_distrib line 354
  51. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.class_right_distrib line 364
  52. instance OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.(instance at line 367) line 367
  53. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.mul_mono line 382
  54. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.add_mono line 390
  55. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.zero_le line 399

    Source documentation

    Every tensor class is nonnegative in the restriction order.

    theorem zero_le (T : TensorClass) : 0 ≤ T := by
…

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.TensorClass

  56. instance OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.(instance at line 405) line 405
  57. instance OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.(instance at line 409) line 409
  58. instance OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.(instance at line 412) line 412
  59. instance OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.(instance at line 415) line 415
  60. def OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.rank line 425

    Source documentation

    Exact rank descends to mutual-restriction classes.

    def rank : TensorClass → ℕ := Quotient.lift (fun T : FiniteTensor => exactRank T.coeff)
…

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.TensorClass, OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.FiniteTensor, OAI.MatrixMultiplication.AuxiliarySeparation.exactRank

  61. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.rank_tensorClass line 430
  62. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.rank_classOf line 433
  63. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.rank_mono line 437
  64. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.rank_mul_le line 442
  65. def OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.matrixClass line 451

    Source documentation

    Square matrix multiplication as an element of the tensor semiring.

    def matrixClass (n : ℕ) : TensorClass := classOf (Tensor.matrixMultiplication n n n)

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.TensorClass, OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf

  66. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.rank_matrixClass line 453
  67. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf_matrixCoefficients_equiv line 456
  68. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.matrixClass_mul line 465
  69. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.matrixClass_one line 479
  70. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.matrixClass_pow line 488
  71. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf_eq_zero_iff line 493
  72. instance OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.(instance at line 503) line 503
  73. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.one_le_classOf_of_ne_zero line 512

    Source documentation

    A nonzero tensor has a nonzero coefficient, which restricts to scalar multiplication.

    theorem one_le_classOf_of_ne_zero {X Y Z : Type*}
    [Fintype X] [Fintype Y] [Fintype Z] {T : Tensor ℂ X Y Z} (hT : T ≠ 0) :
    1 ≤ classOf T := by
…

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf

  74. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.one_le_of_ne_zero line 530

    Source documentation

    Every nonzero class dominates the multiplicative unit.

    theorem one_le_of_ne_zero {T : TensorClass} (hT : T ≠ 0) : 1 ≤ T := by
…

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.TensorClass