Function TENSOR-TO-MATRIX


Slots on this function:

Documentation:
Function that maps a tensor to matrix for a particular basis. Tensor-to-Matrix is defined for first and second order tensors (vector-quantities & dyads). Tensor-to-Matrix maps a vector-quantity into a
row matrix of column-dimension equal to the spatial.dimension of the vector-quantity. Dyads are mapped into square matrices of row- and column-dimension equal to the spatial dimension of the dyad. The scalar components of the resulting matrices corresspond to dot (inner) products of the tensor with appropriate basis vectors.
Instance-Of: Function
Arity: 3

Equivalence Axioms:

(<=> (Tensor-To-Matrix ?T ?Basis)
     (And (Tensor-Quantity ?T)
          (Orthonormal-Basis ?Basis)
          (=> (Member ?Q (Tensor-Order ?T)) (Member ?Q (Setof 1 2)))
          (Matrix-Quantity ?M)
          (=> (= (Tensor-Order ?T) 1)
              (= (Row-Dimension ?M) 1)
              (= (Column-Dimension ?M) (Spatial.Dimension ?T))
              (Forall (?I)
                      (= (Value ?M 1 ?I)
                         (Vector-Component ?T ?I ?Basis))))
          (=> (= (Tensor-Order ?T) 2)
              (Square-Matrix ?M)
              (= (Size ?M) (Spatial.Dimension ?T))
              (Forall (?I ?J)
                      (= (Value ?M ?I ?J)
                         (Dyad-Component ?T ?I ?J ?Basis))))))


Axioms:

(Nth-Domain Tensor-To-Matrix 3 Matrix-Quantity)

(Nth-Domain Tensor-To-Matrix 2 Orthonormal-Basis)

(Nth-Domain Tensor-To-Matrix 1 Tensor-Quantity)


Other Related Axioms:

(=> (= (Tensor-To-Matrix ?T ?Basis) ?M)
    (=> (= (Tensor-Order ?T) 2)
        (Square-Matrix ?M)
        (= (Size ?M) (Spatial.Dimension ?T))
        (Forall (?I ?J)
                (= (Value ?M ?I ?J) (Dyad-Component ?T ?I ?J ?Basis)))))

(=> (= (Tensor-To-Matrix ?T ?Basis) ?M)
    (=> (= (Tensor-Order ?T) 1)
        (= (Row-Dimension ?M) 1)
        (= (Column-Dimension ?M) (Spatial.Dimension ?T))
        (Forall (?I)
                (= (Value ?M 1 ?I) (Vector-Component ?T ?I ?Basis)))))

(=> (= (Tensor-To-Matrix ?T ?Basis) ?M) (Matrix-Quantity ?M))

(=> (= (Tensor-To-Matrix ?T ?Basis) ?M)
    (=> (Member ?Q (Tensor-Order ?T)) (Member ?Q (Setof 1 2))))

(=> (= (Tensor-To-Matrix ?T ?Basis) ?M) (Orthonormal-Basis ?Basis))

(=> (= (Tensor-To-Matrix ?T ?Basis) ?M) (Tensor-Quantity ?T))

(=> (And (Vector-Quantity ?V1) (Dyad ?T1))
    (<=> (Dot ?V1 ?T1 ?V)
         (And (Vector-Quantity ?V)
              (Forall (?B)
                      (= ?T
                         (The-Vector-Quantity (* (Tensor-To-Matrix ?V1
                                                                   ?B)
                                                 (Tensor-To-Matrix ?T1
                                                                   ?B))
                                              ?B)))
              (Forall 
                  (?B ?I ?J)
                  (=> (= (Basis.Dimension ?B)
                         (Spatial.Dimension ?V1))
                      (= ?T
                         (Summation 
                             (Lambda 
                                 (?I)
                                 (* (Basis.Vec ?B ?I)
                                    (Summation 
                                        (Lambda (?J)
                                                (* (Vector-Component 
                                                       ?V1
                                                       ?J
                                                       ?B)
                                                   (Dyad-Component ?T1
                                                                   ?J
                                                                   ?I
                                                                   ?B)))
                                        1
                                        (Spatial.Dimension ?V1))))
                             1
                             (Spatial.Dimension ?V1))))))))

(=> (And (Dyad ?T1) (Vector-Quantity ?V1))
    (<=> (Dot ?T1 ?V1 ?V)
         (And (Vector-Quantity ?V)
              (Forall 
                  (?B)
                  (= ?T
                     (The-Vector-Quantity 
                         (Transpose (* (Tensor-To-Matrix ?T1 ?B)
                                       (Transpose (Tensor-To-Matrix 
                                                      ?V1
                                                      ?B))))
                         ?B)))
              (Forall 
                  (?B ?I ?J)
                  (=> (= (Basis.Dimension ?B)
                         (Spatial.Dimension ?V1))
                      (= ?T
                         (Summation 
                             (Lambda 
                                 (?I)
                                 (* (Basis.Vec ?B ?I)
                                    (Summation 
                                        (Lambda (?J)
                                                (* (Dyad-Component ?T1
                                                                   ?I
                                                                   ?J
                                                                   ?B)
                                                   (Vector-Component 
                                                       ?V1
                                                       ?J
                                                       ?B)))
                                        1
                                        (Spatial.Dimension ?V1))))
                             1
                             (Spatial.Dimension ?V1))))))))

(=> (And (Dyad ?T1) (Dyad ?T2))
    (<=> (Dot ?T1 ?T2 ?T)
         (And (Dyad ?T)
              (Forall (?B)
                      (= ?T
                         (The-Dyad (* (Tensor-To-Matrix ?T1 ?B)
                                      (Tensor-To-Matrix ?T2 ?B))
                                   ?B)))
              (Forall 
                  (?B ?I ?J)
                  (=> (= (Basis.Dimension ?B)
                         (Spatial.Dimension ?T1))
                      (= ?T
                         (Summation 
                             (Lambda 
                                 (?I)
                                 (Summation 
                                     (Lambda (?J)
                                             (* (* (Basis.Vec ?B ?I)
                                                   (Basis.Vec ?B ?J))
                                                (* (Dyad-Component ?T1
                                                                   ?I
                                                                   ?J
                                                                   ?B)
                                                   (Dyad-Component ?T2
                                                                   ?J
                                                                   ?I
                                                                   ?B))))
                                     1
                                     (Spatial.Dimension ?T1)))
                             1
                             (Spatial.Dimension ?T1))))))))

(=> (And (Vector-Quantity ?V1) (Vector-Quantity ?V2))
    (<=> (Dot ?V1 ?V2 ?S)
         (And (Scalar-Quantity ?S)
              (Forall (?B)
                      (= ?S
                         (Value (* (Tensor-To-Matrix ?V1 ?B)
                                   (Transpose (Tensor-To-Matrix ?V2
                                                                ?B)))
                                11)))
              (Forall (?B ?J)
                      (=> (= (Basis.Dimension ?B)
                             (Spatial.Dimension ?V1))
                          (= ?S
                             (Summation (Lambda (?J)
                                                (* (Vector-Component 
                                                       ?V1
                                                       ?J
                                                       ?B)
                                                   (Vector-Component 
                                                       ?V2
                                                       ?J
                                                       ?B)))
                                        1
                                        (Spatial.Dimension ?V1))))))))