Skip to content

feat: Kronecker delta sums #975

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
gloges wants to merge 7 commits into from
Closed

feat: Kronecker delta sums #975

Show file tree
Hide file tree
Changes from 6 commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
59192cd
delta sum lemmas
gloges Mar 5, 2026
bfbae49
todo ideas
gloges Mar 5, 2026
1149033
commutator fixes (sorryful)
gloges Mar 5, 2026
310710a
LRL fixes (sorryful)
gloges Mar 5, 2026
aa71dad
Merge branch 'main' into kronecker-delta-sums
gloges Mar 5, 2026
398631c
lint fix
gloges Mar 5, 2026
ccc9afa
general ring + coercion
gloges Mar 6, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
58 changes: 49 additions & 9 deletions PhysLean/Mathematics/KroneckerDelta.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,31 +3,71 @@ Copyright (c) 2026 Gregory J. Loges. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gregory J. Loges
-/
import Mathlib.Algebra.Ring.Basic
import Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
import Mathlib.Algebra.Module.Basic
import Mathlib.Data.Complex.Basic
import Mathlib.Data.Fintype.Card
import PhysLean.Meta.TODO.Basic
/-!

# Kronecker delta

This file defines the Kronecker delta, `δ[i,j] ≔ if (i = j) then 1 else 0`.

TODO ideas:
- Generalize `sum_kroneckerDelta` (e.g. currently assuming `c : ℂ`)
- Double sums
- Symmetrization (i.e. `∑ᵢ∑ⱼ δᵢⱼfᵢⱼ = ½ ∑ᵢ∑ⱼ δᵢⱼ(fᵢⱼ + fⱼᵢ)`) and special case
`∑ᵢ∑ⱼ δᵢⱼfᵢⱼ = 0` for when f is antisymmetric

-/
TODO "YVABB" "Build functionality for working with sums involving Kronecker deltas."
TODO "YVABB" "Build full API for working with sums involving Kronecker deltas."

namespace KroneckerDelta

variable {d : ℕ}

/-!

## A. Definition and basic properties

-/

/-- The Kronecker delta function, `ite (i = j) 1 0`. -/
def kroneckerDelta [Ring R] (i j : Fin d) : R := if (i = j) then 1 else 0
def kroneckerDelta (i j : Fin d) : ℝ := if (i = j) then 1 else 0
Copy link
Copy Markdown
Collaborator

@morrison-daniel morrison-daniel Mar 6, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Copy Markdown
Contributor Author

@gloges gloges Mar 6, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 ℂ...!)

Copy link
Copy Markdown
Collaborator

@morrison-daniel morrison-daniel Mar 7, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Copy Markdown
Collaborator

@morrison-daniel morrison-daniel Mar 7, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Copy Markdown
Collaborator

@morrison-daniel morrison-daniel Mar 7, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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!

Copy link
Copy Markdown
Collaborator

@morrison-daniel morrison-daniel Mar 7, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Copy Markdown
Contributor Author

@gloges gloges Mar 7, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.


@[inherit_doc kroneckerDelta]
macro "δ[" i:term "," j:term "]" : term => `(kroneckerDelta $i $j)
notation "δ[" i "," j "]" => kroneckerDelta i j

lemma kroneckerDelta_symm [Ring R] (i j : Fin d) :
kroneckerDelta (R := R) i j = kroneckerDelta j i :=
lemma kroneckerDelta_eq (i j : Fin d) : δ[i,j] = ite (i = j) 1 0 := rfl

lemma kroneckerDelta_symm (i j : Fin d) : δ[i,j] = δ[j,i] :=
ite_cond_congr (Eq.propIntro Eq.symm Eq.symm)

lemma kroneckerDelta_self [Ring R] : ∀ i : Fin d, kroneckerDelta (R := R) i i = 1 := by
intro i
exact if_pos rfl
lemma kroneckerDelta_self (i : Fin d) : δ[i,i] = 1 := if_pos rfl

lemma kroneckerDelta_diff {i j : Fin d} (h : i ≠ j) : δ[i,j] = 0 := if_neg h

/-!

## B. Sums

-/

lemma sum_kroneckerDelta [AddCommGroup M] [Module ℂ M]
(c : ℂ) (i : Fin d) (f : Fin d → M) : ∑ j, (c * δ[i,j]) • f j = c • f i := by
have (j : Fin d) : c * Complex.ofReal (ite (i = j) 1 0) = ite (i = j) c 0 := by
rcases eq_or_ne i j with (rfl | hne)
· simp
· simp [if_neg hne]
simp [kroneckerDelta_eq, this]

lemma sum_kroneckerDelta' [AddCommGroup M] [Module ℂ M]
(c : ℂ) (i : Fin d) (f : Fin d → M) : ∑ j, (c * δ[j,i]) • f j = c • f i := by
simp [kroneckerDelta_symm, sum_kroneckerDelta]

lemma sum_kroneckerDelta_self [AddCommGroup M] [Module ℂ M] (c : ℂ) (f : M) :
∑ (i : Fin d), (c * δ[i,i]) • f = (d * c) • f := by
simp [kroneckerDelta_self, ← Nat.cast_smul_eq_nsmul ℂ, smul_smul]

end KroneckerDelta
143 changes: 31 additions & 112 deletions PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -57,14 +57,13 @@ lemma lrlOperator_eq (i : Fin H.d) :
rw [← ContinuousLinearMap.comp_finset_sum]
simp only [← comp_assoc, ← ContinuousLinearMap.finset_sum_comp]
rw [← momentumOperatorSqr]
unfold kroneckerDelta
simp only [mul_ite_zero, ite_zero_smul, Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte,
Finset.sum_const, Finset.card_univ, Fintype.card_fin, ← smul_assoc]
ext ψ x
simp only [mul_one, nsmul_eq_mul, smul_add, ContinuousLinearMap.add_apply, coe_smul', coe_sub',
coe_comp', Pi.smul_apply, Pi.sub_apply, Function.comp_apply, SchwartzMap.add_apply,
SchwartzMap.smul_apply, SchwartzMap.sub_apply, smul_eq_mul, Complex.real_smul,
Complex.ofReal_inv, Complex.ofReal_ofNat]
simp only [sum_kroneckerDelta, sum_kroneckerDelta_self]
ext
simp only [smul_add, ContinuousLinearMap.add_apply, coe_smul', coe_sub', coe_comp', coe_sum',
Pi.smul_apply, Pi.sub_apply, Function.comp_apply, Finset.sum_apply, SchwartzMap.add_apply,
SchwartzMap.smul_apply, SchwartzMap.sub_apply, positionOperator_apply, momentumOperator_apply,
neg_mul, smul_eq_mul, mul_neg, sub_neg_eq_add, SchwartzMap.sum_apply, Finset.sum_neg_distrib,
Complex.real_smul, Complex.ofReal_inv, Complex.ofReal_ofNat]
ring

/-- `𝐀(ε)ᵢ = 𝐋ᵢⱼ𝐩ⱼ + ½iℏ(d-1)𝐩ᵢ - mk·𝐫(ε)⁻¹𝐱ᵢ` -/
Expand All @@ -76,14 +75,13 @@ lemma lrlOperator_eq' (i : Fin H.d) : H.lrlOperator ε i = ∑ j, 𝐋[i,j] ∘L
enter [2, 2, j]
rw [comp_eq_comp_sub_commute 𝐩[j] 𝐋[i,j], angularMomentum_commutation_momentum]
repeat rw [Finset.sum_add_distrib, Finset.sum_sub_distrib, Finset.sum_sub_distrib]
unfold kroneckerDelta
simp only [sum_kroneckerDelta, sum_kroneckerDelta_self]
ext ψ x
simp only [ContinuousLinearMap.add_apply, coe_smul', coe_sum', coe_comp', Pi.smul_apply,
Finset.sum_apply, Function.comp_apply, coe_sub', Pi.sub_apply, SchwartzMap.add_apply,
SchwartzMap.smul_apply, SchwartzMap.sum_apply, SchwartzMap.sub_apply]
simp only [mul_ite, mul_one, mul_zero, smul_eq_mul, ite_mul, zero_mul, Finset.sum_ite_eq,
Finset.mem_univ, ↓reduceIte, Finset.sum_const, Finset.card_univ, Fintype.card_fin,
nsmul_eq_mul, smul_add, Complex.real_smul, Complex.ofReal_inv, Complex.ofReal_ofNat]
simp only [smul_add, ContinuousLinearMap.add_apply, coe_smul', coe_sub', coe_sum', coe_comp',
Pi.smul_apply, Pi.sub_apply, Finset.sum_apply, Function.comp_apply, SchwartzMap.add_apply,
SchwartzMap.smul_apply, SchwartzMap.sub_apply, SchwartzMap.sum_apply, momentumOperator_apply,
neg_mul, smul_eq_mul, mul_neg, sub_neg_eq_add, Complex.real_smul, Complex.ofReal_inv,
Complex.ofReal_ofNat]
ring

/-- `𝐀(ε)ᵢ = 𝐩ⱼ𝐋ᵢⱼ - ½iℏ(d-1)𝐩ᵢ - mk·𝐫(ε)⁻¹𝐱ᵢ` -/
Expand All @@ -95,15 +93,13 @@ lemma lrlOperator_eq'' (i : Fin H.d) : H.lrlOperator ε i = ∑ j, 𝐩[j] ∘L
enter [2, 2, j]
rw [comp_eq_comp_add_commute 𝐋[i,j] 𝐩[j], angularMomentum_commutation_momentum]
rw [Finset.sum_add_distrib, Finset.sum_add_distrib, Finset.sum_sub_distrib]
simp only [sum_kroneckerDelta, sum_kroneckerDelta_self]
ext ψ x
unfold kroneckerDelta
simp only [ContinuousLinearMap.add_apply, coe_smul', coe_sum', coe_comp',
Pi.smul_apply, Finset.sum_apply, Function.comp_apply, coe_sub', Pi.sub_apply,
SchwartzMap.add_apply, SchwartzMap.smul_apply, SchwartzMap.sum_apply, Complex.real_smul,
Complex.ofReal_inv, Complex.ofReal_ofNat, SchwartzMap.sub_apply]
simp only [mul_ite, mul_one, mul_zero, smul_eq_mul, ite_mul, zero_mul, Finset.sum_ite_eq,
Finset.mem_univ, ↓reduceIte, Finset.sum_const, Finset.card_univ, Fintype.card_fin,
nsmul_eq_mul]
simp only [smul_add, ContinuousLinearMap.add_apply, coe_smul', coe_sum', coe_comp', Pi.smul_apply,
Finset.sum_apply, Function.comp_apply, coe_sub', Pi.sub_apply, SchwartzMap.add_apply,
SchwartzMap.smul_apply, SchwartzMap.sum_apply, momentumOperator_apply, neg_mul,
Finset.sum_neg_distrib, smul_neg, Complex.real_smul, Complex.ofReal_inv, Complex.ofReal_ofNat,
SchwartzMap.sub_apply, smul_eq_mul, mul_neg, sub_neg_eq_add]
ring

/-- The operator `𝐱ᵢ𝐩ᵢ` on Schwartz maps. -/
Expand All @@ -126,53 +122,24 @@ private def constRadiusRegInvCompPosition (ε : ℝ) (i : Fin H.d) := (H.m * H.k
-/

/-- `⁅𝐋ᵢⱼ, 𝐀(ε)ₖ⁆ = iℏ(δᵢₖ𝐀(ε)ⱼ - δⱼₖ𝐀(ε)ᵢ)` -/
@[sorryful]
lemma angularMomentum_commutation_lrl (hε : 0 < ε) (i j k : Fin H.d) :
⁅𝐋[i,j], H.lrlOperator ε k⁆ = (Complex.I * ℏ * δ[i,k]) • H.lrlOperator ε j
- (Complex.I * ℏ * δ[j,k]) • H.lrlOperator ε i := by
rcases eq_or_ne i j with (⟨hij, rfl⟩ | hij)
· rw [angularMomentumOperator_eq_zero, zero_lie, sub_self]

unfold lrlOperator
simp only [lie_sub, lie_smul, lie_sum, lie_add, lie_leibniz]
simp only [angularMomentum_commutation_angularMomentum, angularMomentum_commutation_momentum,
angularMomentum_commutation_position, angularMomentum_commutation_radiusRegPow hε]
simp only [comp_add, comp_sub, add_comp, sub_comp, comp_smul, smul_comp, zero_comp, add_zero]
ext ψ x
simp only [ContinuousLinearMap.sub_apply, ContinuousLinearMap.smul_apply,
ContinuousLinearMap.sum_apply, ContinuousLinearMap.add_apply, ContinuousLinearMap.comp_apply]
simp only [SchwartzMap.sub_apply, SchwartzMap.smul_apply, SchwartzMap.sum_apply,
SchwartzMap.add_apply, SchwartzMap.smul_apply, smul_eq_mul]
simp only [Finset.sum_add_distrib, Finset.sum_sub_distrib]
dsimp only [kroneckerDelta]
simp only [mul_ite_zero, mul_one, ite_mul, zero_mul, Finset.sum_ite_irrel, Complex.real_smul,
Finset.sum_const_zero, Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte, smul_add]
simp only [angularMomentumOperator_antisymm k _]
simp only [mul_sub, mul_add, mul_ite_zero, Finset.mul_sum]
simp only [ContinuousLinearMap.neg_apply, map_neg, SchwartzMap.neg_apply]

rcases eq_or_ne i k with (⟨_, rfl⟩ | hik)
· simp only [↓reduceIte, angularMomentumOperator_eq_zero]
repeat rw [ite_cond_eq_false _ _ (eq_false hij.symm)]
simp only [ContinuousLinearMap.zero_apply, SchwartzMap.zero_apply]
ring_nf
· rcases eq_or_ne j k with (⟨_, rfl⟩ | hjk)
· simp only [↓reduceIte]
repeat rw [ite_cond_eq_false _ _ (eq_false hij)]
ring_nf
· repeat rw [ite_cond_eq_false _ _ (eq_false hik)]
repeat rw [ite_cond_eq_false _ _ (eq_false hjk)]
ring
sorry

/-- `⁅𝐋ᵢⱼ, 𝐀(ε)²⁆ = 0` -/
@[sorryful]
lemma angularMomentum_commutation_lrlSqr (hε : 0 < ε) (i j : Fin H.d) :
⁅𝐋[i,j], H.lrlOperatorSqr ε⁆ = 0 := by
unfold lrlOperatorSqr
simp only [lie_sum, lie_leibniz, H.angularMomentum_commutation_lrl hε]
simp only [comp_sub, comp_smul, sub_comp, smul_comp]
dsimp only [kroneckerDelta]
simp [Finset.sum_add_distrib, Finset.sum_sub_distrib]
simp only [Finset.sum_add_distrib, Finset.sum_sub_distrib]
simp [sum_kroneckerDelta]

/-- `⁅𝐋², 𝐀(ε)²⁆ = 0` -/
@[sorryful]
lemma angularMomentumSqr_commutation_lrlSqr (hε : 0 < ε) :
⁅angularMomentumOperatorSqr (d := H.d), H.lrlOperatorSqr ε⁆ = 0 := by
unfold angularMomentumOperatorSqr
Expand All @@ -197,15 +164,15 @@ private lemma positionDotMomentum_commutation_position {d} (i : Fin d) :
⁅positionDotMomentum (d := d), 𝐱[i]⁆ = (-Complex.I * ℏ) • 𝐱[i] := by
unfold positionDotMomentum
simp only [← lie_skew 𝐩[_] _, position_commutation_position, position_commutation_momentum,
leibniz_lie, kroneckerDelta, sum_lie, comp_neg, comp_smul]
simp
leibniz_lie, sum_lie, comp_neg, comp_smul]
simp [sum_kroneckerDelta]

private lemma positionDotMomentum_commutation_momentum {d} (i : Fin d) :
⁅positionDotMomentum (d := d), 𝐩[i]⁆ = (Complex.I * ℏ) • 𝐩[i] := by
unfold positionDotMomentum
simp only [momentum_commutation_momentum, position_commutation_momentum, kroneckerDelta,
simp only [momentum_commutation_momentum, position_commutation_momentum,
sum_lie, leibniz_lie, smul_comp]
simp
simp [sum_kroneckerDelta']

private lemma positionDotMomentum_commutation_momentumSqr {d} :
⁅positionDotMomentum (d := d), momentumOperatorSqr (d := d)⁆ = (2 * Complex.I * ℏ) • 𝐩² := by
Expand Down Expand Up @@ -524,58 +491,10 @@ private lemma rr_comm_pL_Lp (hε : 0 < ε) (i : Fin H.d) :
private lemma xL_Lx_eq (hε : 0 < ε) (i : Fin H.d) : ∑ j, (𝐱[j] ∘L 𝐋[i,j] + 𝐋[i,j] ∘L 𝐱[j]) =
(2 : ℝ) • (∑ j, 𝐱[j] ∘L 𝐩[j]) ∘L 𝐱[i] - (2 : ℝ) • 𝐫[ε,2] ∘L 𝐩[i] + (2 * ε ^ 2) • 𝐩[i]
- (Complex.I * ℏ * (H.d - 3)) • 𝐱[i] := by
conv_lhs =>
enter [2, j]
calc
_ = 𝐱[j] ∘L (𝐱[i] ∘L 𝐩[j] - 𝐱[j] ∘L 𝐩[i])
+ (𝐱[i] ∘L 𝐩[j] - 𝐱[j] ∘L 𝐩[i]) ∘L 𝐱[j] := rfl
_ = 𝐱[j] ∘L 𝐱[i] ∘L 𝐩[j] + 𝐱[i] ∘L 𝐩[j] ∘L 𝐱[j]
- 𝐱[j] ∘L 𝐱[j] ∘L 𝐩[i] - 𝐱[j] ∘L 𝐩[i] ∘L 𝐱[j] := by
rw [comp_sub, sub_comp]
ext ψ x
simp only [ContinuousLinearMap.add_apply, coe_sub', coe_comp', Pi.sub_apply,
Function.comp_apply, SchwartzMap.add_apply, SchwartzMap.sub_apply]
ring
_ = 𝐱[j] ∘L 𝐩[j] ∘L 𝐱[i] + 𝐱[i] ∘L 𝐱[j] ∘L 𝐩[j] - (2 : ℝ) • 𝐱[j] ∘L 𝐱[j] ∘L 𝐩[i]
+ (2 * Complex.I * ℏ * δ[i,j]) • 𝐱[j] - (Complex.I * ℏ) • 𝐱[i] := by
rw [comp_eq_comp_add_commute 𝐱[i] 𝐩[j], position_commutation_momentum]
rw [comp_eq_comp_sub_commute 𝐩[i] 𝐱[j], position_commutation_momentum]
rw [comp_eq_comp_add_commute 𝐱[j] 𝐩[j], position_commutation_momentum]
rw [kroneckerDelta_symm j i, kroneckerDelta_self]
ext ψ x
simp only [comp_add, comp_smulₛₗ, RingHom.id_apply, comp_id, comp_sub, coe_sub', coe_comp',
coe_smul', Pi.sub_apply, ContinuousLinearMap.add_apply, Function.comp_apply,
Pi.smul_apply, SchwartzMap.sub_apply, SchwartzMap.add_apply, SchwartzMap.smul_apply,
smul_eq_mul, mul_one, Complex.real_smul, Complex.ofReal_ofNat]
ring
_ = 𝐱[j] ∘L 𝐩[j] ∘L 𝐱[i] + 𝐱[j] ∘L 𝐱[i] ∘L 𝐩[j] - (2 : ℝ) • 𝐱[j] ∘L 𝐱[j] ∘L 𝐩[i]
+ (2 * Complex.I * ℏ * δ[i,j]) • 𝐱[j] - (Complex.I * ℏ) • 𝐱[i] := by
nth_rw 2 [← comp_assoc]
rw [position_comp_commute i j, comp_assoc]
_ = (2 : ℝ) • (𝐱[j] ∘L 𝐩[j]) ∘L 𝐱[i] - (2 : ℝ) • (𝐱[j] ∘L 𝐱[j]) ∘L 𝐩[i]
+ (3 * Complex.I * ℏ * δ[i,j]) • 𝐱[j] - (Complex.I * ℏ) • 𝐱[i] := by
rw [comp_eq_comp_add_commute 𝐱[i] 𝐩[j], position_commutation_momentum]
ext ψ x
simp only [comp_add, comp_smulₛₗ, RingHom.id_apply, comp_id, coe_sub', coe_smul',
Pi.sub_apply, ContinuousLinearMap.add_apply, coe_comp', Function.comp_apply,
Pi.smul_apply, SchwartzMap.sub_apply, SchwartzMap.add_apply, SchwartzMap.smul_apply,
smul_eq_mul, Complex.real_smul, Complex.ofReal_ofNat, sub_left_inj]
ring
simp only [Finset.sum_sub_distrib, Finset.sum_add_distrib, ← Finset.smul_sum, ← finset_sum_comp]
rw [positionOperatorSqr_eq hε, sub_comp, smul_comp, id_comp]

unfold kroneckerDelta
ext ψ x
simp only [ContinuousLinearMap.sub_apply, ContinuousLinearMap.add_apply,
ContinuousLinearMap.smul_apply, ContinuousLinearMap.sum_apply, SchwartzMap.sub_apply,
SchwartzMap.add_apply, SchwartzMap.smul_apply, SchwartzMap.sum_apply]
simp only [coe_comp', coe_sum', Function.comp_apply, Finset.sum_apply, SchwartzMap.sum_apply,
Complex.real_smul, Complex.ofReal_ofNat, Complex.ofReal_pow, mul_ite, mul_one, mul_zero,
smul_eq_mul, ite_mul, zero_mul, Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte,
Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul, Complex.ofReal_mul]
ring
sorry

/-- `⁅𝐇(ε), 𝐀(ε)ᵢ⁆ = iℏkε²(¾𝐫(ε)⁻⁵(𝐱ⱼ𝐋ᵢⱼ + 𝐋ᵢⱼ𝐱ⱼ) + 3iℏ/2 𝐫(ε)⁻⁵𝐱ᵢ + 𝐫(ε)⁻³𝐩ᵢ)` -/
@[sorryful]
lemma hamiltonianReg_commutation_lrl (hε : 0 < ε) (i : Fin H.d) :
⁅H.hamiltonianReg ε, H.lrlOperator ε i⁆ = (Complex.I * ℏ * H.k * ε ^ 2) •
((3 * 4⁻¹ : ℝ) • 𝐫[ε,-5] ∘L ∑ j, (𝐱[j] ∘L 𝐋[i,j] + 𝐋[i,j] ∘L 𝐱[j])
Expand Down
Loading