feat: Kronecker delta sums

PhysLean/Mathematics/KroneckerDelta.lean

@@ -3,31 +3,86 @@ 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.Algebra.Ring.Subring.Basic
+import Mathlib.Data.Complex.Basic
 import PhysLean.Meta.TODO.Basic
 /-!
 
 # Kronecker delta
 
 This file defines the Kronecker delta, `δ[i,j] ≔ if (i = j) then 1 else 0`.
 
+TODO ideas:
+- Double sums
+- Symmetrization (i.e. `δᵢⱼfᵢⱼ = ½ δᵢⱼ(fᵢⱼ + fⱼᵢ)`) and `∑ᵢ∑ⱼ δᵢⱼfᵢⱼ = 0` if 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
+  {R : Type*} [Ring R]
+  {d : ℕ} (i j : Fin 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 : R := if (i = j) then 1 else 0
 
 @[inherit_doc kroneckerDelta]
-macro "δ[" i:term "," j:term "]" : term => `(kroneckerDelta $i $j)
+notation "δ[" i "," j "]" => kroneckerDelta i j
+
+@[inherit_doc kroneckerDelta]
+notation "δ[" R' "," i "," j "]" => kroneckerDelta (R := R') i j
+
+lemma kroneckerDelta_eq : δ[R,i,j] = ite (i = j) 1 0 := rfl
+
+lemma kroneckerDelta_symm : δ[R,i,j] = δ[R,j,i] := ite_cond_congr (Eq.propIntro Eq.symm Eq.symm)
+
+lemma kroneckerDelta_self : δ[R,i,i] = 1 := if_pos rfl
+
+lemma kroneckerDelta_diff {i j : Fin d} (h : i ≠ j) : δ[R,i,j] = 0 := if_neg h
+
+/-!
+
+## B. Coercion
+
+-/
+
+@[simp]
+lemma kroneckerDelta_coe {R' : Subring R} : δ[R',i,j] = δ[R,i,j] := by
+  rcases eq_or_ne i j with (rfl | hne)
+  · simp [kroneckerDelta_self]
+  · simp [kroneckerDelta_diff hne]
+
+@[simp]
+lemma kroneckerDelta_ofReal : δ[ℝ,i,j] = δ[ℂ,i,j] := by
+  rcases eq_or_ne i j with (rfl | hne)
+  · simp [kroneckerDelta_self]
+  · simp [kroneckerDelta_diff hne]
+
+/-!
+
+## C. Sums
+
+-/
+
+variable {M : Type*} [AddCommMonoid M] [Module R M]
+
+lemma sum_kroneckerDelta (c : R) (f : Fin d → M) : ∑ j, (c * δ[i,j]) • f j = c • f i := by
+  simp [kroneckerDelta_eq]
 
-lemma kroneckerDelta_symm [Ring R] (i j : Fin d) :
-    kroneckerDelta (R := R) i j = kroneckerDelta j i :=
-  ite_cond_congr (Eq.propIntro Eq.symm Eq.symm)
+lemma sum_kroneckerDelta' (c : R) (f : Fin d → M) : ∑ j, (c * δ[j,i]) • f j = c • f i := by
+  simp [kroneckerDelta_symm, sum_kroneckerDelta]
 
-lemma kroneckerDelta_self [Ring R] : ∀ i : Fin d, kroneckerDelta (R := R) i i = 1 := by
-  intro i
-  exact if_pos rfl
+lemma sum_kroneckerDelta_self (c : R) (f : M) : ∑ (i : Fin d), (c * δ[i,i]) • f = (d * c) • f := by
+  simp [kroneckerDelta_self, ← Nat.cast_smul_eq_nsmul R, smul_smul]
 
 end KroneckerDelta

PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean

@@ -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·𝐫(ε)⁻¹𝐱ᵢ` -/
@@ -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·𝐫(ε)⁻¹𝐱ᵢ` -/
@@ -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. -/
@@ -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
@@ -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
@@ -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])