diff --git a/PhysLean/Mathematics/KroneckerDelta.lean b/PhysLean/Mathematics/KroneckerDelta.lean index 5a935b36c..a5b23d9f8 100644 --- a/PhysLean/Mathematics/KroneckerDelta.lean +++ b/PhysLean/Mathematics/KroneckerDelta.lean @@ -5,33 +5,130 @@ Authors: Gregory J. Loges -/ module -public import Mathlib.Algebra.Ring.Basic -public import PhysLean.Meta.TODO.Basic +public import Mathlib.Algebra.BigOperators.Group.Finset.Piecewise +public import Mathlib.Algebra.CharZero.Defs +public import Mathlib.Algebra.Field.Defs +public import Mathlib.Algebra.Module.Defs /-! # Kronecker delta -This file defines the Kronecker delta, `δ[i,j] ≔ if (i = j) then 1 else 0`. +This module defines the Kronecker delta. -/ @[expose] public section -TODO "YVABB" "Build functionality for working with sums involving Kronecker deltas." namespace KroneckerDelta +variable {α M : Type*} [DecidableEq α] + /-- 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 : α) : ℕ := if i = j then 1 else 0 + +@[inherit_doc] +notation "δ[" i "," j "]" => kroneckerDelta i j + +@[simp] +lemma eq_one_of_same (i : α) : δ[i,i] = 1 := if_pos rfl + +lemma eq_zero_of_ne {i j : α} (h : i ≠ j) : δ[i,j] = 0 := if_neg h + +@[simp] +lemma eq_of_coe {p : α → Prop} (i j : Subtype p) : δ[(i : α),j] = δ[i,j] := by + rcases eq_or_ne i j with (rfl | hne) + · repeat rw [eq_one_of_same] + · rw [eq_zero_of_ne hne, eq_zero_of_ne <| Subtype.coe_ne_coe.mpr hne] + +lemma eq_zero_of_not {p : α → Prop} {i j : α} (hi : ¬p i) (hj : p j) : δ[i,j] = 0 := + eq_zero_of_ne (fun h ↦ hi (h ▸ hj)) + +/-! +### Conditions for smul to vanish +-/ + +lemma smul_of_eq_zero [AddMonoid M] (i j : α) {f : α → α → M} (hf : f i i = 0) : + δ[i,j] • f i j = 0 := by + rcases eq_or_ne i j with (rfl | hne) + · exact smul_eq_zero_of_right _ hf + · exact smul_eq_zero_of_left (eq_zero_of_ne hne) _ + +lemma smul_eq_zero_iff [AddMonoid M] (i j : α) (f : α → α → M) : + δ[i,j] • f i j = 0 ↔ i ≠ j ∨ f i i = 0 := by + rcases eq_or_ne i j with (rfl | hne) + · simp [one_nsmul] + · simp [eq_zero_of_ne, hne] + +lemma smul_eq_zero_iff' [AddMonoid M] (i : α) (f : α → α → M) : + (∀ j : α, δ[i,j] • f i j = 0) ↔ f i i = 0 := by + refine ⟨fun h ↦ ?_, fun hf j ↦ smul_of_eq_zero i j hf⟩ + simpa [one_nsmul] using h i + +lemma smul_eq_zero_iff'' [AddMonoid M] (f : α → α → M) : + (∀ i j : α, δ[i,j] • f i j = 0) ↔ ∀ i : α, f i i = 0 := + forall_congr' fun j ↦ smul_eq_zero_iff' j f + +/-! +### Symmetrization +-/ + +lemma symm (i j : α) : δ[i,j] = δ[j,i] := ite_cond_congr <| Eq.propIntro Eq.symm Eq.symm + +lemma smul_symm [AddMonoid M] (i j : α) (f : α → α → M) : δ[i,j] • f j i = δ[i,j] • f i j := by + rcases eq_or_ne i j with (rfl | hne) + · rfl + · simp only [eq_zero_of_ne hne, zero_smul] + +lemma symmetrize [AddMonoid M] (i j : α) (f : α → α → M) : + δ[i,j] • (f i j + f j i) = (2 * δ[i,j]) • f i j := by + rcases eq_or_ne i j with (rfl | hne) + · simp [one_nsmul, two_nsmul] + · simp [eq_zero_of_ne hne] + +lemma symmetrize' [AddCommMonoid M] {K : Type*} [Semifield K] [CharZero K] [Module K M] + (i j : α) (f : α → α → M) : δ[i,j] • (2 : K)⁻¹ • (f i j + f j i) = δ[i,j] • f i j := by + rcases eq_or_ne i j with (rfl | hne) + · simp only [eq_one_of_same, one_nsmul, ← two_smul K, smul_smul] + rw [inv_mul_cancel₀ (OfNat.zero_ne_ofNat 2).symm, one_smul] + · simp [eq_zero_of_ne hne] + +@[simp] +lemma smul_sub_eq_zero [AddGroup M] (i j : α) (f : α → α → M) : δ[i,j] • (f i j - f j i) = 0 := by + rcases eq_or_ne i j with (rfl | hne) + · exact smul_eq_zero_of_right _ (sub_self <| f i i) + · exact smul_eq_zero_of_left (eq_zero_of_ne hne) _ + +/-! +### Sums +-/ + +section Sums +open Finset + +variable [AddCommMonoid M] + +@[simp] +lemma sum_mul [Fintype α] (i j : α) : ∑ k : α, δ[i,k] * δ[k,j] = δ[i,j] := by + simp [kroneckerDelta] + +@[simp] +lemma sum_smul [Fintype α] (i : α) (f : α → M) : ∑ j : α, δ[i,j] • f j = f i := by + simp [kroneckerDelta, one_nsmul] + +lemma sum_sum_smul_eq_zero [Fintype α] {f : α → α → M} (hf : ∀ i : α, f i i = 0) : + ∑ i : α, ∑ j : α, δ[i,j] • f i j = 0 := by + simp [sum_smul, hf, sum_const_zero] -@[inherit_doc kroneckerDelta] -macro "δ[" i:term "," j:term "]" : term => `(kroneckerDelta $i $j) +lemma finset_sum_smul (s : Finset α) (i : α) (f : α → M) : + ∑ j ∈ s, δ[i,j] • f j = if i ∈ s then f i else 0 := by + simp [kroneckerDelta, one_nsmul] -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 finset_sum_sum_smul_eq_zero {s s' : Finset α} {f : α → α → M} + (hf : ∀ i ∈ s ∩ s', f i i = 0) : ∑ i ∈ s, ∑ j ∈ s', δ[i,j] • f i j = 0 := by + simp only [finset_sum_smul, Finset.sum_ite_mem] + rw [← sum_coe_sort] + simp [hf] -lemma kroneckerDelta_self [Ring R] : ∀ i : Fin d, kroneckerDelta (R := R) i i = 1 := by - intro i - exact if_pos rfl +end Sums end KroneckerDelta diff --git a/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean b/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean index f93f4ae13..375ecc7aa 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean @@ -62,13 +62,15 @@ lemma lrlOperator_eq (i : Fin H.d) : 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] + simp only [↓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 [Nat.cast_ite, Nat.cast_one, CharP.cast_eq_zero, mul_ite, mul_one, mul_zero, ite_smul, + zero_smul, Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte, nsmul_eq_mul, 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·𝐫(ε)⁻¹𝐱ᵢ` -/ @@ -85,9 +87,11 @@ lemma lrlOperator_eq' (i : Fin H.d) : H.lrlOperator ε i = ∑ j, 𝐋[i,j] ∘L 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 [Nat.cast_ite, Nat.cast_one, CharP.cast_eq_zero, mul_ite, mul_one, mul_zero, + momentumOperator_apply, neg_mul, smul_eq_mul, mul_neg, ite_mul, zero_mul, + Finset.sum_neg_distrib, Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte, Finset.sum_const, + Finset.card_univ, Fintype.card_fin, nsmul_eq_mul, sub_neg_eq_add, smul_add, Complex.real_smul, + Complex.ofReal_inv, Complex.ofReal_ofNat] ring /-- `𝐀(ε)ᵢ = 𝐩ⱼ𝐋ᵢⱼ - ½iℏ(d-1)𝐩ᵢ - mk·𝐫(ε)⁻¹𝐱ᵢ` -/ @@ -105,9 +109,10 @@ lemma lrlOperator_eq'' (i : Fin H.d) : H.lrlOperator ε i = ∑ j, 𝐩[j] ∘L 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 [momentumOperator_apply, neg_mul, Finset.sum_neg_distrib, Nat.cast_ite, Nat.cast_one, + CharP.cast_eq_zero, mul_ite, mul_one, mul_zero, smul_eq_mul, mul_neg, ite_mul, zero_mul, + Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte, Finset.sum_const, Finset.card_univ, + Fintype.card_fin, nsmul_eq_mul, sub_neg_eq_add] ring /-- The operator `𝐱ᵢ𝐩ᵢ` on Schwartz maps. -/ @@ -130,44 +135,14 @@ 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 @@ -177,6 +152,7 @@ lemma angularMomentum_commutation_lrlSqr (hε : 0 < ε) (i j : Fin H.d) : simp [Finset.sum_add_distrib, Finset.sum_sub_distrib] /-- `⁅𝐋², 𝐀(ε)²⁆ = 0` -/ +@[sorryful] lemma angularMomentumSqr_commutation_lrlSqr (hε : 0 < ε) : ⁅angularMomentumOperatorSqr (d := H.d), H.lrlOperatorSqr ε⁆ = 0 := by unfold angularMomentumOperatorSqr @@ -270,7 +246,7 @@ private lemma positionCompMomentumSqr_comm_positionDotMomentumCompMomentum_add { repeat rw [positionDotMomentum_commutation_momentumSqr] simp only [neg_comp, smul_comp, add_comp, comp_zero, zero_add, comp_smul, id_comp, comp_assoc] repeat rw [comp_eq_comp_add_commute 𝐩² 𝐩[_], momentumSqr_commutation_momentum] - rw [kroneckerDelta_symm j i] + rw [symm j i] trans (-Complex.I * ℏ) • 𝐋[i,j] ∘L 𝐩² · ext ψ x unfold angularMomentumOperator @@ -297,7 +273,7 @@ private lemma positionCompMomentumSqr_comm_constMomentum_add {d} (i j : Fin d) : nth_rw 2 [← lie_skew] repeat rw [lie_smul, leibniz_lie, momentumSqr_commutation_momentum, comp_zero, zero_add, position_commutation_momentum, smul_comp, id_comp] - rw [kroneckerDelta_symm j i, add_neg_eq_zero] + rw [symm j i, add_neg_eq_zero] private lemma positionDotMomentumCompMomentum_comm_constMomentum_add {d} (i j : Fin d) : ⁅positionDotMomentumCompMomentum (d := d) i, constMomentum j⁆ + @@ -369,7 +345,7 @@ private lemma positionDotMomentumCompMomentum_comm_constRadiusRegInvCompPosition repeat rw [← lie_skew 𝐩[_] _, radiusRegPow_commutation_momentum hε] repeat rw [positionDotMomentum_commutation_radiusRegPow hε] simp only [smul_comp, neg_comp, comp_assoc] - rw [position_comp_commute j i, kroneckerDelta_symm j i] + rw [position_comp_commute j i, symm j i] unfold angularMomentumOperator ext ψ x simp only [comp_neg, comp_smulₛₗ, RingHom.id_apply, comp_id, Complex.ofReal_neg, @@ -390,7 +366,7 @@ private lemma constMomentum_comm_constRadiusRegInvCompPosition_add (hε : 0 < ε repeat rw [← lie_skew 𝐩[_] _] repeat rw [position_commutation_momentum, radiusRegPow_commutation_momentum hε] simp only [neg_comp, smul_comp, comp_assoc] - rw [position_comp_commute j i, kroneckerDelta_symm j i] + rw [position_comp_commute j i, symm j i] ext ψ x simp only [comp_neg, comp_smulₛₗ, RingHom.id_apply, comp_id, Complex.ofReal_neg, Complex.ofReal_one, neg_mul, one_mul, neg_smul, neg_neg, smul_add, smul_neg, neg_add_rev, @@ -545,12 +521,12 @@ private lemma xL_Lx_eq (hε : 0 < ε) (i : Fin H.d) : ∑ j, (𝐱[j] ∘L 𝐋[ 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] + rw [symm j i, eq_one_of_same] 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] + smul_eq_mul, 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 @@ -574,9 +550,11 @@ private lemma xL_Lx_eq (hε : 0 < ε) (i : Fin H.d) : ∑ j, (𝐱[j] ∘L 𝐋[ 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] + positionOperator_apply, momentumOperator_apply, neg_mul, mul_neg, Finset.sum_neg_distrib, + smul_neg, Complex.real_smul, Complex.ofReal_ofNat, Complex.ofReal_pow, sub_neg_eq_add, smul_add, + Nat.cast_ite, Nat.cast_one, CharP.cast_eq_zero, 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 /-- `⁅𝐇(ε), 𝐀(ε)ᵢ⁆ = iℏkε²(¾𝐫(ε)⁻⁵(𝐱ⱼ𝐋ᵢⱼ + 𝐋ᵢⱼ𝐱ⱼ) + 3iℏ/2 𝐫(ε)⁻⁵𝐱ᵢ + 𝐫(ε)⁻³𝐩ᵢ)` -/ @@ -719,7 +697,7 @@ private lemma sum_Lprx (hε : 0 < ε) : rw [angularMomentumOperator_antisymm j i, neg_comp, neg_comp, ← sub_eq_add_neg] rw [comp_assoc, comp_assoc, ← comp_sub] repeat rw [comp_eq_comp_sub_commute 𝐩[_] 𝐱[_], position_commutation_momentum] - rw [kroneckerDelta_symm j i, sub_sub_sub_cancel_right] + rw [symm j i, sub_sub_sub_cancel_right] rw [← angularMomentumOperator] rw [← angularMomentumOperatorSqr, ← sub_eq_zero] exact angularMomentumSqr_commutation_radiusRegPow hε @@ -742,7 +720,7 @@ private lemma sum_prx (hε : 0 < ε) : ∑ i : Fin H.d, 𝐩[i] ∘L 𝐫[ε,-1] rw [← comp_assoc, comp_eq_comp_sub_commute 𝐩[_] 𝐫[ε,-1], radiusRegPow_commutation_momentum hε] rw [sub_comp, smul_comp, comp_assoc, comp_assoc] rw [comp_eq_comp_sub_commute 𝐩[_] 𝐱[_], position_commutation_momentum] - rw [kroneckerDelta_self] + rw [eq_one_of_same] rw [comp_sub, comp_smul, comp_id] repeat rw [Finset.sum_sub_distrib, ← Finset.smul_sum, ← comp_finset_sum] rw [positionOperatorSqr_eq hε, comp_sub, radiusRegPowOperator_comp_eq hε, comp_smul, comp_id] @@ -751,7 +729,7 @@ private lemma sum_prx (hε : 0 < ε) : ∑ i : Fin H.d, 𝐩[i] ∘L 𝐫[ε,-1] simp only [ContinuousLinearMap.sub_apply, SchwartzMap.sub_apply, ContinuousLinearMap.smul_apply, SchwartzMap.smul_apply, ContinuousLinearMap.sum_apply, SchwartzMap.sum_apply] simp only [coe_comp', coe_sum', Function.comp_apply, Finset.sum_apply, map_sum, - SchwartzMap.sum_apply, mul_one, Finset.sum_const, Finset.card_univ, Fintype.card_fin, + SchwartzMap.sum_apply, Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul, smul_eq_mul, Complex.ofReal_neg, Complex.ofReal_one, neg_mul, one_mul, sub_add_cancel, Complex.real_smul, Complex.ofReal_pow, sub_neg_eq_add] ring_nf diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean index 8c4797506..43e1b9d58 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean @@ -188,9 +188,9 @@ 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, 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] - ring + simp only [mul_add, Complex.real_smul, ite_smul, one_smul, zero_smul, mul_ite, mul_zero, + Nat.cast_ite, Nat.cast_one, mul_ite, mul_one, ite_mul] + ring_nf lemma momentum_comp_position_eq (i j : Fin d) : 𝐩[j] ∘L 𝐱[i] = 𝐱[i] ∘L 𝐩[j] - (Complex.I * ℏ * δ[i,j]) • ContinuousLinearMap.id ℂ 𝓢(Space d, ℂ) := by @@ -219,12 +219,12 @@ lemma position_commutation_momentumSqr {d : ℕ} (i : Fin d) : ⁅𝐱[i], 𝐩 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] + rw [Finset.sum_add_distrib] ext ψ x simp only [ContinuousLinearMap.add_apply, coe_smul', Pi.smul_apply, SchwartzMap.add_apply, SchwartzMap.smul_apply, smul_eq_mul] - ring + ring_nf + simp lemma radiusRegPow_commutation_momentum (hε : 0 < ε) (i : Fin d) : ⁅radiusRegPowOperator (d := d) ε s, 𝐩[i]⁆ = (s * Complex.I * ℏ) • 𝐫[ε,s-2] ∘L 𝐱[i] := by @@ -314,7 +314,7 @@ lemma angularMomentum_commutation_position {d : ℕ} (i j k : Fin d) : ⁅𝐋[i rw [position_commutation_position, position_commutation_position] rw [← lie_skew, position_commutation_momentum] rw [← lie_skew, position_commutation_momentum] - rw [kroneckerDelta_symm k i, kroneckerDelta_symm k j] + rw [symm k i, symm k j] simp only [ContinuousLinearMap.comp_neg, ContinuousLinearMap.comp_smul, comp_id, zero_comp, add_zero, add_comm, sub_neg_eq_add, ← sub_eq_add_neg] @@ -368,8 +368,9 @@ lemma angularMomentum_commutation_momentumSqr {d : ℕ} (i j : Fin d) : 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 only [Nat.cast_ite, Nat.cast_one, CharP.cast_eq_zero, mul_ite, mul_one, mul_zero, ite_smul, + zero_smul, Finset.sum_add_distrib, Finset.sum_sub_distrib, Finset.sum_ite_eq, Finset.mem_univ, + ↓reduceIte, sub_self, add_zero] lemma momentumSqr_comp_angularMomentum_commute {d : ℕ} (i j : Fin d) : 𝐩² ∘L 𝐋[i,j] = 𝐋[i,j] ∘L 𝐩² := by @@ -401,35 +402,14 @@ 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, SchwartzMap.sub_apply, + SchwartzMap.add_apply, smul_sub] 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