From 59192cd19619b618401e92119586d44f54c64354 Mon Sep 17 00:00:00 2001 From: gloges Date: Thu, 5 Mar 2026 17:10:38 +0900 Subject: [PATCH 1/6] delta sum lemmas --- PhysLean/Mathematics/KroneckerDelta.lean | 50 ++++++++++++++++++++---- 1 file changed, 42 insertions(+), 8 deletions(-) diff --git a/PhysLean/Mathematics/KroneckerDelta.lean b/PhysLean/Mathematics/KroneckerDelta.lean index 448a6e026..e8685e678 100644 --- a/PhysLean/Mathematics/KroneckerDelta.lean +++ b/PhysLean/Mathematics/KroneckerDelta.lean @@ -3,7 +3,10 @@ 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 /-! @@ -16,18 +19,49 @@ TODO "YVABB" "Build functionality for working with sums involving Kronecker delt 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 @[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 From bfbae490f6e93064adb3be66ccfa25608d68c569 Mon Sep 17 00:00:00 2001 From: gloges Date: Thu, 5 Mar 2026 17:10:49 +0900 Subject: [PATCH 2/6] todo ideas --- PhysLean/Mathematics/KroneckerDelta.lean | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/PhysLean/Mathematics/KroneckerDelta.lean b/PhysLean/Mathematics/KroneckerDelta.lean index e8685e678..f431387c6 100644 --- a/PhysLean/Mathematics/KroneckerDelta.lean +++ b/PhysLean/Mathematics/KroneckerDelta.lean @@ -14,8 +14,14 @@ import PhysLean.Meta.TODO.Basic 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 From 1149033eaaf87481224d3dae8db9e0061e5abf1d Mon Sep 17 00:00:00 2001 From: gloges Date: Thu, 5 Mar 2026 17:22:28 +0900 Subject: [PATCH 3/6] commutator fixes (sorryful) --- .../DDimensions/Operators/Commutation.lean | 76 ++++++------------- 1 file changed, 24 insertions(+), 52 deletions(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean index f0055c8f7..301edc995 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean @@ -119,7 +119,7 @@ lemma momentumSqr_comp_momentum_commute {d : ℕ} (i : Fin d) : 𝐩² ∘L 𝐩 /-- The canonical commutation relations: `[xᵢ, pⱼ] = iℏ δᵢⱼ𝟙`. -/ lemma position_commutation_momentum {d : ℕ} (i j : Fin d) : ⁅𝐱[i], 𝐩[j]⁆ = (Complex.I * ℏ * δ[i,j]) • ContinuousLinearMap.id ℂ 𝓢(Space d, ℂ) := by - dsimp only [Bracket.bracket, kroneckerDelta] + dsimp only [Bracket.bracket] ext ψ x simp only [ContinuousLinearMap.smul_apply, SchwartzMap.smul_apply, coe_id', id_eq, smul_eq_mul, coe_sub', coe_mul, Pi.sub_apply, Function.comp_apply, SchwartzMap.sub_apply] @@ -132,9 +132,8 @@ lemma position_commutation_momentum {d : ℕ} (i j : Fin d) : ⁅𝐱[i], 𝐩[j simp only [Space.coord_apply, Complex.real_smul, Pi.smul_apply'] rw [h] rw [Space.deriv_smul (by fun_prop) (SchwartzMap.differentiableAt ψ)] - rw [Space.deriv_component, ite_cond_symm j i] - simp only [mul_add, Complex.real_smul, ite_smul, one_smul, zero_smul, mul_ite, mul_one, mul_zero, - ite_mul, zero_mul] + rw [Space.deriv_component, ← kroneckerDelta_eq, kroneckerDelta_symm] + simp only [Complex.real_smul] ring lemma momentum_comp_position_eq (i j : Fin d) : 𝐩[j] ∘L 𝐱[i] = @@ -163,13 +162,8 @@ lemma position_commutation_momentumSqr {d : ℕ} (i : Fin d) : ⁅𝐱[i], 𝐩 unfold momentumOperatorSqr rw [lie_sum] simp only [position_commutation_momentum_momentum] - dsimp only [kroneckerDelta] - simp only [mul_ite_zero, ite_zero_smul, Finset.sum_add_distrib, Finset.sum_ite_eq, - Finset.mem_univ, ↓reduceIte] - ext ψ x - simp only [ContinuousLinearMap.add_apply, coe_smul', Pi.smul_apply, SchwartzMap.add_apply, - SchwartzMap.smul_apply, smul_eq_mul] - ring + simp only [Finset.sum_add_distrib, sum_kroneckerDelta] + simp only [← two_smul ℂ, smul_smul, mul_assoc] lemma radiusRegPow_commutation_momentum (hε : 0 < ε) (i : Fin d) : ⁅radiusRegPowOperator (d := d) ε s, 𝐩[i]⁆ = (s * Complex.I * ℏ) • 𝐫[ε,s-2] ∘L 𝐱[i] := by @@ -229,20 +223,19 @@ lemma radiusRegPow_commutation_momentumSqr (hε : 0 < ε) : rw [lie_leibniz, radiusRegPow_commutation_momentum hε] rw [comp_smul, ← comp_assoc, momentum_comp_radiusRegPow_eq hε] rw [sub_comp, comp_assoc, momentum_comp_position_eq] - simp only [kroneckerDelta, ↓reduceIte, mul_one] - simp only [smul_comp, comp_sub, comp_smul, comp_id, smul_sub, comp_assoc, - Finset.sum_add_distrib, Finset.sum_sub_distrib, ← Finset.smul_sum, Finset.sum_const, - Finset.card_univ, Fintype.card_fin, ← ContinuousLinearMap.comp_finset_sum] - rw [positionOperatorSqr_eq hε, comp_sub, radiusRegPowOperator_comp_eq hε, comp_smul, comp_id] - rw [← Nat.cast_smul_eq_nsmul ℂ] - ext ψ x - simp only [Complex.ofReal_sub, Complex.ofReal_ofNat, sub_add_cancel, coe_sub', Pi.sub_apply, - ContinuousLinearMap.add_apply, coe_smul', coe_comp', coe_sum', Pi.smul_apply, - Function.comp_apply, Finset.sum_apply, map_sum, SchwartzMap.sub_apply, SchwartzMap.add_apply, - SchwartzMap.smul_apply, SchwartzMap.sum_apply, smul_eq_mul, Complex.real_smul, - Complex.ofReal_pow, Complex.ofReal_add, Complex.ofReal_natCast, Complex.ofReal_mul] + simp only [smul_sub, comp_sub, Finset.sum_sub_distrib, Finset.sum_add_distrib, ← Finset.smul_sum, + ← comp_finset_sum, sum_kroneckerDelta_self, smul_comp, comp_assoc, smul_smul] + simp only [comp_smul, comp_id, smul_smul, positionOperatorSqr_eq hε, comp_sub, + radiusRegPowOperator_comp_eq hε] + ext + simp only [Complex.ofReal_sub, Complex.ofReal_ofNat, sub_add_cancel, + ContinuousLinearMap.add_apply, coe_sub', coe_smul', coe_comp', coe_sum', Pi.sub_apply, + Pi.smul_apply, Function.comp_apply, Finset.sum_apply, map_sum, SchwartzMap.add_apply, + SchwartzMap.sub_apply, SchwartzMap.smul_apply, SchwartzMap.sum_apply, smul_eq_mul, + Complex.real_smul, Complex.ofReal_pow, Complex.ofReal_mul, Complex.ofReal_add, + Complex.ofReal_natCast] ring_nf - rw [Complex.I_sq] + simp only [Complex.I_sq] ring /- @@ -308,9 +301,7 @@ lemma angularMomentum_commutation_momentumSqr {d : ℕ} (i j : Fin d) : rw [lie_leibniz, angularMomentum_commutation_momentum] simp only [comp_sub, comp_smulₛₗ, RingHom.id_apply, sub_comp, smul_comp] rw [momentum_comp_commute _ i, momentum_comp_commute j _] - dsimp only [kroneckerDelta] - simp only [Finset.sum_add_distrib, Finset.sum_sub_distrib, mul_ite, mul_zero, ite_smul, - zero_smul, Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte, sub_self, add_zero] + simp [Finset.sum_add_distrib, Finset.sum_sub_distrib, sum_kroneckerDelta] lemma momentumSqr_comp_angularMomentum_commute {d : ℕ} (i j : Fin d) : 𝐩² ∘L 𝐋[i,j] = 𝐋[i,j] ∘L 𝐩² := by @@ -340,35 +331,16 @@ lemma angularMomentum_commutation_angularMomentum {d : ℕ} (i j k l : Fin d) : simp only [ContinuousLinearMap.comp_sub, ContinuousLinearMap.sub_comp, ContinuousLinearMap.comp_smul, ContinuousLinearMap.smul_comp] ext ψ x - simp only [mul_ite, mul_one, mul_zero, ite_smul, zero_smul, coe_sub', Pi.sub_apply, - ContinuousLinearMap.add_apply, SchwartzMap.sub_apply, SchwartzMap.add_apply, smul_sub] + simp only [coe_sub', Pi.sub_apply, ContinuousLinearMap.add_apply, coe_smul', coe_comp', + Pi.smul_apply, Function.comp_apply, SchwartzMap.sub_apply, SchwartzMap.add_apply, + SchwartzMap.smul_apply, positionOperator_apply, momentumOperator_apply, neg_mul, mul_neg, + smul_eq_mul, sub_neg_eq_add] ring +@[sorryful] lemma angularMomentumSqr_commutation_angularMomentum {d : ℕ} (i j : Fin d) : ⁅angularMomentumOperatorSqr (d := d), 𝐋[i,j]⁆ = 0 := by - unfold angularMomentumOperatorSqr - conv_lhs => - simp only [smul_lie, sum_lie, leibniz_lie, angularMomentum_commutation_angularMomentum] - dsimp only [kroneckerDelta] - simp only [comp_add, comp_sub, add_comp, sub_comp, comp_smul, smul_comp, mul_ite, mul_zero, - mul_one] - simp only [ite_smul, zero_smul] - - -- Split into individual terms to do one of the sums, then recombine - simp only [Finset.sum_add_distrib, Finset.sum_sub_distrib, Finset.sum_ite_irrel, - Finset.sum_const_zero, Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte] - simp only [← Finset.sum_add_distrib, ← Finset.sum_sub_distrib] - - ext ψ x - simp only [angularMomentumOperator_antisymm _ i, angularMomentumOperator_antisymm j _, - neg_comp, comp_neg, neg_neg, smul_neg, sub_neg_eq_add] - simp only [ContinuousLinearMap.sum_apply, ContinuousLinearMap.add_apply, - ContinuousLinearMap.sub_apply, ContinuousLinearMap.smul_apply, ContinuousLinearMap.comp_apply, - ContinuousLinearMap.neg_apply, ContinuousLinearMap.zero_apply, SchwartzMap.add_apply, - SchwartzMap.sum_apply, SchwartzMap.sub_apply, SchwartzMap.smul_apply, SchwartzMap.neg_apply, - SchwartzMap.zero_apply] - ring_nf - rw [Finset.sum_const_zero, smul_zero] + sorry end end QuantumMechanics From 310710a26d7fa477001a836c7f59d37e9524f6a8 Mon Sep 17 00:00:00 2001 From: gloges Date: Thu, 5 Mar 2026 17:28:41 +0900 Subject: [PATCH 4/6] LRL fixes (sorryful) --- .../Hydrogen/LaplaceRungeLenzVector.lean | 144 ++++-------------- 1 file changed, 32 insertions(+), 112 deletions(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean b/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean index 474cc0a24..be31263ca 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean +++ b/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 @@ -521,61 +488,14 @@ private lemma rr_comm_pL_Lp (hε : 0 < ε) (i : Fin H.d) : smul_add] ring_nf +@[sorryful] 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]) From 398631cfe715b13e8bc590f1d54a3b8929bdccdf Mon Sep 17 00:00:00 2001 From: gloges Date: Fri, 6 Mar 2026 07:58:49 +0900 Subject: [PATCH 5/6] lint fix --- .../DDimensions/Hydrogen/LaplaceRungeLenzVector.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean b/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean index be31263ca..89a45d1f6 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean @@ -488,7 +488,6 @@ private lemma rr_comm_pL_Lp (hε : 0 < ε) (i : Fin H.d) : smul_add] ring_nf -@[sorryful] 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 From ccc9afa05bd56a22f10876dc8da2693469d92438 Mon Sep 17 00:00:00 2001 From: gloges Date: Fri, 6 Mar 2026 17:08:45 +0900 Subject: [PATCH 6/6] general ring + coercion --- PhysLean/Mathematics/KroneckerDelta.lean | 63 ++++++++++++------- .../DDimensions/Operators/Commutation.lean | 2 +- 2 files changed, 40 insertions(+), 25 deletions(-) diff --git a/PhysLean/Mathematics/KroneckerDelta.lean b/PhysLean/Mathematics/KroneckerDelta.lean index f431387c6..d3f7e4083 100644 --- a/PhysLean/Mathematics/KroneckerDelta.lean +++ b/PhysLean/Mathematics/KroneckerDelta.lean @@ -5,8 +5,8 @@ Authors: Gregory J. Loges -/ import Mathlib.Algebra.BigOperators.Group.Finset.Piecewise import Mathlib.Algebra.Module.Basic +import Mathlib.Algebra.Ring.Subring.Basic import Mathlib.Data.Complex.Basic -import Mathlib.Data.Fintype.Card import PhysLean.Meta.TODO.Basic /-! @@ -15,17 +15,17 @@ import PhysLean.Meta.TODO.Basic 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 +- Symmetrization (i.e. `δᵢⱼfᵢⱼ = ½ δᵢⱼ(fᵢⱼ + fⱼᵢ)`) and `∑ᵢ∑ⱼ δᵢⱼfᵢⱼ = 0` if f is antisymmetric -/ TODO "YVABB" "Build full API for working with sums involving Kronecker deltas." namespace KroneckerDelta -variable {d : ℕ} +variable + {R : Type*} [Ring R] + {d : ℕ} (i j : Fin d) /-! @@ -34,40 +34,55 @@ variable {d : ℕ} -/ /-- The Kronecker delta function, `ite (i = j) 1 0`. -/ -def kroneckerDelta (i j : Fin d) : ℝ := if (i = j) then 1 else 0 +def kroneckerDelta : R := if (i = j) then 1 else 0 @[inherit_doc kroneckerDelta] notation "δ[" i "," j "]" => kroneckerDelta i j -lemma kroneckerDelta_eq (i j : Fin d) : δ[i,j] = ite (i = j) 1 0 := rfl +@[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 -lemma kroneckerDelta_symm (i j : Fin d) : δ[i,j] = δ[j,i] := - ite_cond_congr (Eq.propIntro Eq.symm Eq.symm) +/-! + +## B. Coercion -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 +@[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] /-! -## B. Sums +## C. 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] +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 sum_kroneckerDelta' [AddCommGroup M] [Module ℂ M] - (c : ℂ) (i : Fin d) (f : Fin d → M) : ∑ j, (c * δ[j,i]) • f j = c • f i := by +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 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] +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 diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean index a3fba75b6..8a7d3bc48 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean @@ -184,7 +184,7 @@ lemma position_commutation_momentum {d : ℕ} (i j : Fin d) : ⁅𝐱[i], 𝐩[j rw [h] rw [Space.deriv_smul (by fun_prop) (SchwartzMap.differentiableAt ψ)] rw [Space.deriv_component, ← kroneckerDelta_eq, kroneckerDelta_symm] - simp only [Complex.real_smul] + simp only [Complex.real_smul, kroneckerDelta_ofReal] ring lemma momentum_comp_position_eq (i j : Fin d) : 𝐩[j] ∘L 𝐱[i] =