PhysLean Documentation

PhysLean.Mathematics.KroneckerDelta

Kronecker delta #

This module defines the Kronecker delta.

source
def KroneckerDelta.kroneckerDelta {α : Type u_1} [DecidableEq α] (i j : α) :
ℕ

The Kronecker delta function, ite (i = j) 1 0.

Equations
Instances For
    source
    def KroneckerDelta.«termδ[_,_]» :
    Lean.ParserDescr

    The Kronecker delta function, ite (i = j) 1 0.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem KroneckerDelta.eq_one_of_same {α : Type u_1} [DecidableEq α] (i : α) :
      δ[i,i] = 1
      source
      theorem KroneckerDelta.eq_zero_of_ne {α : Type u_1} [DecidableEq α] {i j : α} (h : i ≠ j) :
      δ[i,j] = 0
      source
      @[simp]
      theorem KroneckerDelta.eq_of_coe {α : Type u_1} [DecidableEq α] {p : α → Prop} (i j : Subtype p) :
      δ[↑i,↑j] = δ[i,j]
      source
      theorem KroneckerDelta.eq_zero_of_not {α : Type u_1} [DecidableEq α] {p : α → Prop} {i j : α} (hi : ¬p i) (hj : p j) :
      δ[i,j] = 0

      Conditions for smul to vanish #

      source
      theorem KroneckerDelta.smul_of_eq_zero {α : Type u_1} {M : Type u_2} [DecidableEq α] [AddMonoid M] (i j : α) {f : α → α → M} (hf : f i i = 0) :
      δ[i,j] • f i j = 0
      source
      theorem KroneckerDelta.smul_eq_zero_iff {α : Type u_1} {M : Type u_2} [DecidableEq α] [AddMonoid M] (i j : α) (f : α → α → M) :
      δ[i,j] • f i j = 0 ↔ i ≠ j ∨ f i i = 0
      source
      theorem KroneckerDelta.smul_eq_zero_iff' {α : Type u_1} {M : Type u_2} [DecidableEq α] [AddMonoid M] (i : α) (f : α → α → M) :
      (∀ (j : α), δ[i,j] • f i j = 0) ↔ f i i = 0
      source
      theorem KroneckerDelta.smul_eq_zero_iff'' {α : Type u_1} {M : Type u_2} [DecidableEq α] [AddMonoid M] (f : α → α → M) :
      (∀ (i j : α), δ[i,j] • f i j = 0) ↔ ∀ (i : α), f i i = 0

      Symmetrization #

      source
      theorem KroneckerDelta.symm {α : Type u_1} [DecidableEq α] (i j : α) :
      δ[i,j] = δ[j,i]
      source
      theorem KroneckerDelta.smul_symm {α : Type u_1} {M : Type u_2} [DecidableEq α] [AddMonoid M] (i j : α) (f : α → α → M) :
      δ[i,j] • f j i = δ[i,j] • f i j
      source
      theorem KroneckerDelta.symmetrize {α : Type u_1} {M : Type u_2} [DecidableEq α] [AddMonoid M] (i j : α) (f : α → α → M) :
      δ[i,j] • (f i j + f j i) = (2 * δ[i,j]) • f i j
      source
      theorem KroneckerDelta.symmetrize' {α : Type u_1} {M : Type u_2} [DecidableEq α] [AddCommMonoid M] {K : Type u_3} [Semifield K] [CharZero K] [Module K M] (i j : α) (f : α → α → M) :
      δ[i,j] • 2⁻¹ • (f i j + f j i) = δ[i,j] • f i j
      source
      @[simp]
      theorem KroneckerDelta.smul_sub_eq_zero {α : Type u_1} {M : Type u_2} [DecidableEq α] [AddGroup M] (i j : α) (f : α → α → M) :
      δ[i,j] • (f i j - f j i) = 0

      Sums #

      source
      @[simp]
      theorem KroneckerDelta.sum_mul {α : Type u_1} [DecidableEq α] [Fintype α] (i j : α) :
      ∑ k : α, δ[i,k] * δ[k,j] = δ[i,j]
      source
      @[simp]
      theorem KroneckerDelta.sum_smul {α : Type u_1} {M : Type u_2} [DecidableEq α] [AddCommMonoid M] [Fintype α] (i : α) (f : α → M) :
      ∑ j : α, δ[i,j] • f j = f i
      source
      theorem KroneckerDelta.sum_sum_smul_eq_zero {α : Type u_1} {M : Type u_2} [DecidableEq α] [AddCommMonoid M] [Fintype α] {f : α → α → M} (hf : ∀ (i : α), f i i = 0) :
      ∑ i : α, ∑ j : α, δ[i,j] • f i j = 0
      source
      theorem KroneckerDelta.finset_sum_smul {α : Type u_1} {M : Type u_2} [DecidableEq α] [AddCommMonoid M] (s : Finset α) (i : α) (f : α → M) :
      ∑ j ∈ s, δ[i,j] • f j = if i ∈ s then f i else 0
      source
      theorem KroneckerDelta.finset_sum_sum_smul_eq_zero {α : Type u_1} {M : Type u_2} [DecidableEq α] [AddCommMonoid M] {s s' : Finset α} {f : α → α → M} (hf : ∀ i ∈ s ∩ s', f i i = 0) :
      ∑ i ∈ s, ∑ j ∈ s', δ[i,j] • f i j = 0