feat: Kronecker delta sums

[gloges]

• Adds new lemmas for sums involving Kronecker deltas (of the form I've encountered - definitely room to generalize and expand the API).
• Adds some ideas for future Kronecker delta lemmas

In making these changes a few commutator proofs broke in Commutation.lean and LaplaceRungeLenzVector.lean; I have fixed those which had a quick solution and replaced those which are more computation-heavy with sorries. I will simplify / golf these two files soon.

[morrison-daniel]

I'm not sure this is a good idea, if anything we'd want to generalize this definition further and not narrow the uses. Can you explain why you want to revise the definition in this way?

[gloges]

No good reason - I've reverted to a general ring. Are the newly added simp lemmas the best way to handle coercion? (I have ℝ → ℂ separate because for some reason ℝ is not a subring of ℂ...!)

[morrison-daniel]

Okay so this probably going to be a long comment but I think this is a great lesson worth learning about formalization and designing definitions.

Generally the goal with definitions is to define them so they are usable in as many scenarios as possible. The Kronecker delta function is useful any time you take a sum, and there are lots of types that aren't compatible with ℝ and are not rings where we may want to take a sum. Probably the easiest example is ℕ: you can't multiply ℕ by ℝ and it is not a ring, but rather a semiring since it doesn't have a negation.

So you may say, okay let's change the definition to Semiring R. But this is also a trap! You see, 1 means a lot of things in Lean and not just numbers, any type with an instance of the One class will let you use 1. In a semiring or ring, 1 is the multiplicative identity. So 1 doesn't always mean the number one (natural, integer, real, or otherwise) but is something of the given type. An easy example is Matrix, where 1 refers to the identity matrix.

With what you have now, the Kronecker delta function on a Matrix type will map to either the zero matrix or the identity matrix, and Lean would allow you to then multiply the Kronecker delta function and a vector, which isn't really what we want. We genuinely want the numbers 0 and 1.

Then how do we define and use this function? Your inclination to map into the ring R makes sense since that would allow you to multiply the Kronecker delta with an element of the ring. However, this is not the multiplication - we also have access to scalar multiplication. If a type α has an instance of SMul ℕ α this lets us write n • a where n is of type ℕ and a is of type α, and the result is type α as well. So what we want is to define this as a map into ℕ and then use it with scalar multiplication on other types.

The other thing we can generalize in the definition is the type of i and j being in Fin d. Again it makes sense that you did that as this is a common use but really we can do this in any type where we can compare i and j. This is encoded in an instance of the type [DecidableEq α], which essentially means that Lean knows how to tell if i and j are equal.

Putting it all together, we can define

def kroneckerDelta {α : Type*} [DecidableEq α] (i j : α) : ℕ := if i = j then 1 else 0

When you want to prove lemmas about sums, you are using notation for Finset.sum which is done on a type M with an instance [AddCommMonoid M], so you will need

variable {M : Type*} [AddCommMonoid M]

for those lemmas. Remember we should also need an instance [SMul ℕ M] to apply the Kronecker delta function, but Lean is able to figure out this on its own from AddCommMonoid M. Basically the scalar multiplication is defined by repeated addition, as you would expect.

Hopefully this makes sense, writing the right definition is a skill you have to learn with formalization because Lean will be picky about things you take for granted. If you like, I'm also happy to help set up the API.

[morrison-daniel]

PS: Would you mind if I used snippets of your code here to write up a general explanation on how to make effective definitions? It's a common confusion for new contributors and I think this is a great example.

[morrison-daniel]

On the comment about subrings, there is a good reason that we don't have a statement that ℝ is a subring of ℂ - it is not true (from a Lean perspective). If you look at the definition of Subring, you see that the type Subring R consists of an element Set R plus some properties. Set R is a set of elements of type R. So something of type Subring ℂ is a set of elements of type ℂ - but ℝ is it's own independent type. The precise statement that is true in Lean is that the embedding of ℝ in ℂ induces subring of ℂ. RingHom.range is the more general statement of this idea. Again, this is an instance of Lean being picky about things you would normally totally ignore - to Lean real numbers and complex numbers are completely different objects and you need a map to move between them. As you found, this makes it really easy to get into trouble when you aren't careful about writing exactly what you mean!

[morrison-daniel]

I know this is a lot to take in, but please don't be discouraged! It is a rite of passage for all Lean contributors to fall victim to this trap - usually many times - before getting the hang of things.

[gloges]

Thanks for taking the time to write up this clear explanation and exemplifying the mindset that goes into proper formalization. The 'traps' would not have (and did not!) occur to me but are obvious with hindsight. I think this also sheds some light why in some calculation-heavy proofs I kept running into something like 2 : 𝓢(Space d, ℂ) →L[ℂ] 𝓢(Space d, ℂ).
Please feel free to use this as an example - it has been a good learning experience for me and now hopefully for others!
I think I will close this PR and attack it again from scratch.