PhyslibSearch

Physlib.Mathematics.KroneckerDelta

16 declarations

definition

Kronecker delta δij\delta_{ij}

#kroneckerDelta

For any type α\alpha and elements i,jαi, j \in \alpha, the Kronecker delta δij\delta_{ij} is defined as 11 if i=ji = j and 00 if iji \neq j.

definition

Kronecker delta notation δ[i,j]\delta[i, j]

#termδ[_,_]

The notation δ[i,j]\delta[i, j] represents the Kronecker delta function applied to the indices ii and jj.

theorem

f(i,i)=0f(i, i) = 0 implies δijf(i,j)=0\delta_{ij} \cdot f(i, j) = 0

#smul_of_eq_zero

Let MM be an additive monoid and α\alpha be a type. For any elements i,jαi, j \in \alpha and any function f:ααMf : \alpha \to \alpha \to M, if f(i,i)=0f(i, i) = 0, then δijf(i,j)=0\delta_{ij} \cdot f(i, j) = 0, where δij\delta_{ij} is the Kronecker delta, defined as 11 if i=ji = j and 00 if iji \neq j.

theorem

δijf(i,j)=0    ijf(i,i)=0\delta_{ij} \cdot f(i, j) = 0 \iff i \neq j \lor f(i, i) = 0

#smul_eq_zero_iff

Let MM be an additive monoid and α\alpha be a set. For any elements i,jαi, j \in \alpha and any function f:ααMf : \alpha \to \alpha \to M, the scalar multiplication of the Kronecker delta δij\delta_{ij} and f(i,j)f(i, j) is zero, i.e., δijf(i,j)=0\delta_{ij} \cdot f(i, j) = 0, if and only if iji \neq j or f(i,i)=0f(i, i) = 0. Here, δij\delta_{ij} is defined to be 11 if i=ji = j and 00 if iji \neq j.

theorem

(j,δijf(i,j)=0)    f(i,i)=0(\forall j, \delta_{ij} \cdot f(i, j) = 0) \iff f(i, i) = 0

#smul_eq_zero_iff'

Let MM be an additive monoid and α\alpha be a type. For any element iαi \in \alpha and any function f:ααMf : \alpha \to \alpha \to M, the condition δijf(i,j)=0\delta_{ij} \cdot f(i, j) = 0 holds for all jαj \in \alpha if and only if f(i,i)=0f(i, i) = 0. Here, δij\delta_{ij} denotes the Kronecker delta, defined as 11 if i=ji = j and 00 if iji \neq j.

theorem

(i,j,δijf(i,j)=0)    i,f(i,i)=0(\forall i, j, \delta_{ij} \cdot f(i, j) = 0) \iff \forall i, f(i, i) = 0

#smul_eq_zero_iff''

Let MM be an additive monoid and α\alpha be a type. For any function f:ααMf : \alpha \to \alpha \to M, the condition δijf(i,j)=0\delta_{ij} \cdot f(i, j) = 0 holds for all i,jαi, j \in \alpha if and only if f(i,i)=0f(i, i) = 0 for all iαi \in \alpha. Here, δij\delta_{ij} denotes the Kronecker delta, defined as 11 if i=ji = j and 00 if iji \neq j, and \cdot denotes scalar multiplication of a natural number on an element of the additive monoid.

theorem

δij=δji\delta_{ij} = \delta_{ji}

#symm

For any elements ii and jj of a type α\alpha, the Kronecker delta δij\delta_{ij} is symmetric in its indices, satisfying the identity δij=δji\delta_{ij} = \delta_{ji}. Here, δij\delta_{ij} is defined to be 11 if i=ji = j and 00 if iji \neq j.

theorem

δijf(j,i)=δijf(i,j)\delta_{ij} \cdot f(j, i) = \delta_{ij} \cdot f(i, j)

#smul_symm

For any type α\alpha and any additive monoid MM, let f:α×αMf: \alpha \times \alpha \to M be a function. For any elements i,jαi, j \in \alpha, the following equality holds: δijf(j,i)=δijf(i,j)\delta_{ij} \cdot f(j, i) = \delta_{ij} \cdot f(i, j) where δij\delta_{ij} is the Kronecker delta, defined as 11 if i=ji = j and 00 if iji \neq j, and \cdot denotes the scalar multiplication of a natural number on an element of the additive monoid.

theorem

δij(f(i,j)+f(j,i))=(2δij)f(i,j)\delta_{ij} \cdot (f(i, j) + f(j, i)) = (2\delta_{ij}) \cdot f(i, j)

#symmetrize

For any additive monoid MM, any function f:ααMf : \alpha \to \alpha \to M, and any elements i,jαi, j \in \alpha, the following identity holds: δij(f(i,j)+f(j,i))=(2δij)f(i,j)\delta_{ij} \cdot (f(i, j) + f(j, i)) = (2\delta_{ij}) \cdot f(i, j) where δij\delta_{ij} is the Kronecker delta, which equals 11 if i=ji = j and 00 otherwise, and the multiplication denotes the scalar action of natural numbers on the monoid.

theorem

δij12(f(i,j)+f(j,i))=δijf(i,j)\delta_{ij} \cdot \frac{1}{2}(f(i, j) + f(j, i)) = \delta_{ij} f(i, j)

#symmetrize'

Let MM be an additive commutative monoid and KK be a semifield of characteristic zero such that MM is a KK-module. For any i,jαi, j \in \alpha and any function f:ααMf : \alpha \to \alpha \to M, the following identity holds: δij12(f(i,j)+f(j,i))=δijf(i,j)\delta_{ij} \cdot \frac{1}{2}(f(i, j) + f(j, i)) = \delta_{ij} f(i, j) where δij\delta_{ij} is the Kronecker delta, which is 11 if i=ji = j and 00 otherwise.

theorem

δij(f(i,j)f(j,i))=0\delta_{ij} \cdot (f(i, j) - f(j, i)) = 0

#smul_sub_eq_zero

For any additive group MM, type α\alpha, elements i,jαi, j \in \alpha, and function f:ααMf : \alpha \to \alpha \to M, the product of the Kronecker delta δij\delta_{ij} and the difference f(i,j)f(j,i)f(i, j) - f(j, i) is zero, i.e., δij(f(i,j)f(j,i))=0\delta_{ij} \cdot (f(i, j) - f(j, i)) = 0.

theorem

kδikδkj=δij\sum_k \delta_{ik} \delta_{kj} = \delta_{ij}

#sum_mul

For any finite type α\alpha and elements i,jαi, j \in \alpha, the sum over all kαk \in \alpha of the product of Kronecker deltas δik\delta_{ik} and δkj\delta_{kj} is equal to δij\delta_{ij}, expressed as: kαδikδkj=δij\sum_{k \in \alpha} \delta_{ik} \delta_{kj} = \delta_{ij} where δab\delta_{ab} is the Kronecker delta, which is 11 if a=ba = b and 00 otherwise.

theorem

jδijf(j)=f(i)\sum_j \delta_{ij} f(j) = f(i)

#sum_smul

Let α\alpha be a finite set. For any element iαi \in \alpha and any function f:αMf : \alpha \to M mapping into a module MM, the sum over all jαj \in \alpha of the Kronecker delta δij\delta_{ij} acting on f(j)f(j) is equal to f(i)f(i). That is, jαδijf(j)=f(i)\sum_{j \in \alpha} \delta_{ij} \cdot f(j) = f(i) where δij=1\delta_{ij} = 1 if i=ji = j and δij=0\delta_{ij} = 0 if iji \neq j.

theorem

i,jαδijf(i,j)=0\sum_{i,j \in \alpha} \delta_{ij} f(i, j) = 0 if f(i,i)=0f(i, i) = 0

#sum_sum_smul_eq_zero

Let α\alpha be a finite set and f:ααMf: \alpha \to \alpha \to M be a function into a module MM. If f(i,i)=0f(i, i) = 0 for all iαi \in \alpha, then the double sum over α\alpha of the scalar multiplication of the Kronecker delta δij\delta_{ij} and f(i,j)f(i, j) is zero: iαjαδijf(i,j)=0\sum_{i \in \alpha} \sum_{j \in \alpha} \delta_{ij} \cdot f(i, j) = 0 where δij\delta_{ij} is the Kronecker delta, defined as 11 if i=ji = j and 00 if iji \neq j.

theorem

Sifting property of the Kronecker delta over a finite set: jsδijf(j)=f(i)\sum_{j \in s} \delta_{ij} f(j) = f(i) if isi \in s else 00

#finset_sum_smul

Let ss be a finite set of elements of type α\alpha, ii be an element of α\alpha, and f:αMf: \alpha \to M be a function into an additive group MM. The sum of the scalar multiplication of the Kronecker delta δij\delta_{ij} and f(j)f(j) over all jsj \in s is given by: jsδijf(j)={f(i)if is0if is\sum_{j \in s} \delta_{ij} f(j) = \begin{cases} f(i) & \text{if } i \in s \\ 0 & \text{if } i \notin s \end{cases} where δij=1\delta_{ij} = 1 if i=ji = j and δij=0\delta_{ij} = 0 if iji \neq j.

theorem

isjsδijf(i,j)=0\sum_{i \in s} \sum_{j \in s'} \delta_{ij} f(i, j) = 0 if f(i,i)=0f(i, i) = 0 on sss \cap s'

#finset_sum_sum_smul_eq_zero

Let ss and ss' be finite sets of elements of type α\alpha, and let f:ααMf: \alpha \to \alpha \to M be a function into an additive group MM. If f(i,i)=0f(i, i) = 0 for all issi \in s \cap s', then the double sum of the scalar multiplication of the Kronecker delta δij\delta_{ij} and f(i,j)f(i, j) over isi \in s and jsj \in s' is zero: isjsδijf(i,j)=0\sum_{i \in s} \sum_{j \in s'} \delta_{ij} f(i, j) = 0 where δij\delta_{ij} is the Kronecker delta, which is 11 if i=ji = j and 00 if iji \neq j.