feat: Kronecker delta api#979
Conversation
morrison-daniel
left a comment
morrison-daniel
left a comment
There was a problem hiding this comment.
Just a few style points for now, I'll take a deeper look soon.
|
|
||
| lemma kroneckerDelta_self (i : α) : δ[i,i] = 1 := if_pos rfl | ||
|
|
||
| lemma kroneckerDelta_diff {i j : α} (h : i ≠ j) : δ[i,j] = 0 := if_neg h |
There was a problem hiding this comment.
| lemma kroneckerDelta_diff {i j : α} (h : i ≠ j) : δ[i,j] = 0 := if_neg h | |
| lemma eq_zero_of_ne {i j : α} (h : i ≠ j) : δ[i,j] = 0 := if_neg h |
This a more conventional way of writing this
| -/ | ||
| TODO "YVABB" "Build functionality for working with sums involving Kronecker deltas." | ||
|
|
||
| namespace KroneckerDelta |
There was a problem hiding this comment.
Since you're in the KroneckerDelta namespace you don't need to put kroneckerDelta into lemma names, it's already (implicitly) there.
| @[inherit_doc] | ||
| notation "δ[" i "," j "]" => kroneckerDelta i j | ||
|
|
||
| lemma kroneckerDelta_self (i : α) : δ[i,i] = 1 := if_pos rfl |
There was a problem hiding this comment.
| lemma kroneckerDelta_self (i : α) : δ[i,i] = 1 := if_pos rfl | |
| @[simp] | |
| lemma eq_one_of_same (i : α) : δ[i,i] = 1 := if_pos rfl |
| ### Conditions for nsmul to vanish | ||
| -/ | ||
|
|
||
| lemma nsmul_of_eq_zero [AddMonoid M] (i j : α) {f : α → α → M} (hf : f i i = 0) : |
There was a problem hiding this comment.
| lemma nsmul_of_eq_zero [AddMonoid M] (i j : α) {f : α → α → M} (hf : f i i = 0) : | |
| lemma smul_of_eq_zero [AddMonoid M] (i j : α) {f : α → α → M} (hf : f i i = 0) : |
I think using "nsmul" isn't necessary since the delta function is a natural number it's clear the scalar multiplication is over naturals.
| lemma symmetrize [AddMonoid M] (i j : α) (f : α → α → M) : | ||
| (2 * δ[i,j]) • f i j = δ[i,j] • (f i j + f j i) := by |
There was a problem hiding this comment.
| lemma symmetrize [AddMonoid M] (i j : α) (f : α → α → M) : | |
| (2 * δ[i,j]) • f i j = δ[i,j] • (f i j + f j i) := by | |
| lemma symmetrize [AddMonoid M] (i j : α) (f : α → α → M) : | |
| δ[i,j] • (f i j + f j i) = (2 * δ[i,j]) • f i j := by |
I would say to swap the order here since you generally want the simplified version on the right.
| lemma symmetrize' [AddCommMonoid M] {K : Type*} [Semifield K] [CharZero K] [Module K M] | ||
| (i j : α) (f : α → α → M) : δ[i,j] • f i j = δ[i,j] • (2 : K)⁻¹ • (f i j + f j i) := by |
There was a problem hiding this comment.
Perhaps reverse the equality on this too, but I'm not sure which way you'd want to be using this.
| @[simp] | ||
| lemma sum_self : ∑ i : α, δ[i,i] = card α := by | ||
| simp [kroneckerDelta_self] | ||
|
|
||
| @[simp] | ||
| lemma sum_self_nsmul (f : M) : ∑ i : α, δ[i,i] • f = card α • f := by | ||
| simp [kroneckerDelta_self, one_nsmul] |
There was a problem hiding this comment.
I would remove these, they're really just using the fact that δ[i,i] = 1 and then applying a lemma about sums.
| section Sums | ||
| open Finset Fintype | ||
|
|
||
| variable [Fintype α] [AddCommMonoid M] |
There was a problem hiding this comment.
Having versions for summing over a Fintype is good, but I would also include versions for summing over finite sums in (possibly) infinite types.
2 participants
Introduces a basic api for the Kronecker delta function.
=(unless one side is zero). Hence noδ[i,j] • f i j = δ[i,j] • f i ilemma.