diff --git a/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean b/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean index c7ea6d838..f13223592 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean @@ -29,7 +29,7 @@ The main results are namespace QuantumMechanics namespace HydrogenAtom noncomputable section -open Constants +open Complex Constants open KroneckerDelta open ContinuousLinearMap SchwartzMap @@ -47,72 +47,50 @@ def lrlOperatorSqr (Ξ΅ : ℝˣ) : 𝓒(Space H.d, β„‚) β†’L[β„‚] 𝓒(Space H.d, /-- `𝐀(Ξ΅)α΅’ = 𝐱ᡒ𝐩² - (𝐱ⱼ𝐩ⱼ)𝐩ᡒ + Β½iℏ(d-1)𝐩ᡒ - mk·𝐫(Ξ΅)⁻¹𝐱ᡒ` -/ lemma lrlOperator_eq (Ξ΅ : ℝˣ) (i : Fin H.d) : H.lrlOperator Ξ΅ i = 𝐱[i] ∘L 𝐩² - (βˆ‘ j, 𝐱[j] ∘L 𝐩[j]) ∘L 𝐩[i] - + (2⁻¹ * Complex.I * ℏ * (H.d - 1)) β€’ 𝐩[i] - (H.m * H.k) β€’ 𝐫[Ξ΅,-1] ∘L 𝐱[i] := by - unfold lrlOperator angularMomentumOperator - congr - conv_lhs => - enter [2, 2, j] - rw [comp_sub, sub_comp] - repeat rw [← comp_assoc, momentum_comp_position_eq, sub_comp, smul_comp, id_comp] - repeat rw [comp_assoc] - rw [momentum_comp_commute i j] - - simp only [Finset.sum_add_distrib, Finset.sum_sub_distrib] - rw [← ContinuousLinearMap.comp_finset_sum] - simp only [← comp_assoc, ← ContinuousLinearMap.finset_sum_comp] - rw [← momentumOperatorSqr] - unfold kroneckerDelta - simp only [↓reduceIte, Finset.sum_const, Finset.card_univ, Fintype.card_fin, ← smul_assoc] - ext ψ x - 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 + + (2⁻¹ * I * ℏ * (H.d - 1)) β€’ 𝐩[i] - (H.m * H.k) β€’ 𝐫[Ξ΅,-1] ∘L 𝐱[i] := by + dsimp [lrlOperator] + rw [sub_left_inj] -- mkΒ·r⁻¹x terms match exactly + calc + _ = (2 : β„‚)⁻¹ β€’ βˆ‘ j, ((𝐩[j] ∘L 𝐱[i]) ∘L 𝐩[j] + 𝐱[i] ∘L 𝐩[j] ∘L 𝐩[j] + - ((𝐩[j] ∘L 𝐱[j]) ∘L 𝐩[i] + 𝐱[j] ∘L 𝐩[j] ∘L 𝐩[i])) := by + simp [angularMomentumOperator, add_sub, comp_assoc, sub_add_eq_add_sub, sub_sub, + momentum_comp_commute, ← Complex.coe_smul] + _ = (2 : β„‚)⁻¹ β€’ βˆ‘ j, ((2 : β„‚) β€’ 𝐱[i] ∘L 𝐩[j] ∘L 𝐩[j] - (I * ℏ) β€’ Ξ΄[i,j] β€’ 𝐩[j] + - ((2 : β„‚) β€’ (𝐱[j] ∘L 𝐩[j]) ∘L 𝐩[i] - (I * ℏ) β€’ 𝐩[i])) := by + simp only [momentum_comp_position_eq, sub_comp, smul_comp, id_comp, sub_add_eq_add_sub, + comp_assoc, two_smul, eq_one_of_same, one_smul] + _ = (2 : β„‚)⁻¹ β€’ βˆ‘ j, ((2 : β„‚) β€’ 𝐱[i] ∘L 𝐩[j] ∘L 𝐩[j] - (2 : β„‚) β€’ (𝐱[j] ∘L 𝐩[j]) ∘L 𝐩[i] + + (I * ℏ) β€’ 𝐩[i] - (I * ℏ) β€’ Ξ΄[i,j] β€’ 𝐩[j]) := by + conv_lhs => + enter [2, 2, j] + rw [sub_sub_sub_comm, sub_sub_eq_add_sub] + simp only [Finset.sum_add_distrib, Finset.sum_sub_distrib, ← Finset.smul_sum, ← comp_finset_sum, + ← finset_sum_comp, sum_smul, Finset.sum_const, Finset.card_univ, Fintype.card_fin, smul_sub, + smul_add, ← add_sub] + simp only [momentumOperatorSqr, ← Nat.cast_smul_eq_nsmul β„‚, smul_smul, ← sub_smul] + grind [one_smul] /-- `𝐀(Ξ΅)α΅’ = 𝐋ᡒⱼ𝐩ⱼ + Β½iℏ(d-1)𝐩ᡒ - mk·𝐫(Ξ΅)⁻¹𝐱ᡒ` -/ lemma lrlOperator_eq' (Ξ΅ : ℝˣ) (i : Fin H.d) : H.lrlOperator Ξ΅ i = βˆ‘ j, 𝐋[i,j] ∘L 𝐩[j] - + (2⁻¹ * Complex.I * ℏ * (H.d - 1)) β€’ 𝐩[i] - (H.m * H.k) β€’ 𝐫[Ξ΅,-1] ∘L 𝐱[i] := by - unfold lrlOperator - congr - conv_lhs => - 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 - 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 [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 + + (2⁻¹ * I * ℏ * (H.d - 1)) β€’ 𝐩[i] - (H.m * H.k) β€’ 𝐫[Ξ΅,-1] ∘L 𝐱[i] := by + rw [lrlOperator_eq, sub_left_inj, add_left_inj] + symm + trans βˆ‘ j, 𝐱[i] ∘L 𝐩[j] ∘L 𝐩[j] - βˆ‘ j, (𝐱[j] ∘L 𝐩[j]) ∘L 𝐩[i] + Β· simp [angularMomentumOperator, comp_assoc, momentum_comp_commute] + simp [← comp_finset_sum, ← finset_sum_comp, momentumOperatorSqr] /-- `𝐀(Ξ΅)α΅’ = 𝐩ⱼ𝐋ᡒⱼ - Β½iℏ(d-1)𝐩ᡒ - mk·𝐫(Ξ΅)⁻¹𝐱ᡒ` -/ lemma lrlOperator_eq'' (Ξ΅ : ℝˣ) (i : Fin H.d) : H.lrlOperator Ξ΅ i = βˆ‘ j, 𝐩[j] ∘L 𝐋[i,j] - - (2⁻¹ * Complex.I * ℏ * (H.d - 1)) β€’ 𝐩[i] - (H.m * H.k) β€’ 𝐫[Ξ΅,-1] ∘L 𝐱[i] := by - unfold lrlOperator - congr - conv_lhs => - 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] - 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 [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] + - (2⁻¹ * I * ℏ * (H.d - 1)) β€’ 𝐩[i] - (H.m * H.k) β€’ 𝐫[Ξ΅,-1] ∘L 𝐱[i] := by + trans (2 : ℝ) β€’ H.lrlOperator Ξ΅ i - H.lrlOperator Ξ΅ i + Β· simp [two_smul] + nth_rw 2 [lrlOperator_eq'] + simp only [lrlOperator, Finset.sum_add_distrib, smul_add, smul_sub, smul_smul] + ring_nf + ext + simp only [one_smul, coe_sub', coe_smul', Pi.sub_apply, ContinuousLinearMap.add_apply, + Pi.smul_apply, SchwartzMap.sub_apply, SchwartzMap.add_apply, SchwartzMap.smul_apply, real_smul, + ofReal_mul, ofReal_ofNat] ring /-- The operator `𝐱ᡒ𝐩ᡒ` on Schwartz maps. -/ @@ -274,7 +252,7 @@ private lemma positionCompMomentumSqr_comm_constMomentum_add {d} (i j : Fin d) : unfold positionCompMomentumSqr constMomentum 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] + position_commutation_momentum, smul_comp, smul_comp, id_comp] rw [symm j i, add_neg_eq_zero] private lemma positionDotMomentumCompMomentum_comm_constMomentum_add {d} (i j : Fin d) : @@ -350,7 +328,7 @@ private lemma positionDotMomentumCompMomentum_comm_constRadiusRegInvCompPosition 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, + simp only [comp_neg, comp_smulβ‚›β‚—, RingHom.id_apply, Complex.ofReal_neg, Complex.ofReal_one, neg_mul, one_mul, neg_smul, neg_neg, comp_add, sub_comp, smul_comp, add_comp, neg_comp, smul_add, smul_neg, neg_add_rev, ContinuousLinearMap.add_apply, ContinuousLinearMap.neg_apply, coe_smul', coe_comp', Pi.smul_apply, Function.comp_apply, @@ -370,7 +348,7 @@ private lemma constMomentum_comm_constRadiusRegInvCompPosition_add (Ξ΅ : ℝˣ) simp only [neg_comp, smul_comp, comp_assoc] 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, + simp only [comp_neg, comp_smulβ‚›β‚—, RingHom.id_apply, Complex.ofReal_neg, Complex.ofReal_one, neg_mul, one_mul, neg_smul, neg_neg, smul_add, smul_neg, neg_add_rev, ContinuousLinearMap.add_apply, ContinuousLinearMap.neg_apply, coe_smul', Pi.smul_apply, coe_comp', Function.comp_apply, SchwartzMap.add_apply, SchwartzMap.neg_apply, @@ -467,8 +445,8 @@ private lemma pSqr_comm_rx (Ξ΅ : ℝˣ) (i : Fin H.d) : rw [← lie_skew, radiusRegPow_commutation_momentumSqr] ext ψ x simp only [comp_neg, comp_smulβ‚›β‚—, RingHom.id_apply, Complex.ofReal_neg, Complex.ofReal_one, - mul_neg, mul_one, neg_mul, neg_smul, one_mul, neg_add_rev, neg_neg, add_comp, smul_comp, - sub_comp, ContinuousLinearMap.add_apply, ContinuousLinearMap.neg_apply, coe_smul', coe_comp', + mul_neg, mul_one, neg_mul, neg_smul, one_mul, + ContinuousLinearMap.add_apply, ContinuousLinearMap.neg_apply, coe_smul', coe_comp', Pi.smul_apply, Function.comp_apply, coe_sub', Pi.sub_apply, coe_sum', Finset.sum_apply, map_sum, SchwartzMap.add_apply, SchwartzMap.neg_apply, SchwartzMap.smul_apply, smul_eq_mul, SchwartzMap.sub_apply, Complex.real_smul, Complex.ofReal_sub, Complex.ofReal_add, @@ -518,46 +496,40 @@ private lemma xL_Lx_eq {d : β„•} (Ξ΅ : ℝˣ) (i : Fin d) : βˆ‘ j, (𝐱[j] ∘L 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 + + (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 [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, Complex.real_smul, Complex.ofReal_ofNat] + ext + simp only [nsmul_eq_mul, comp_add, comp_smulβ‚›β‚—, RingHom.id_apply, comp_sub, coe_sub', + coe_comp', coe_smul', coe_mul, coe_id', CompTriple.comp_eq, Pi.sub_apply, + ContinuousLinearMap.add_apply, Function.comp_apply, Pi.smul_apply, natCast_apply, + map_smul_of_tower, SchwartzMap.sub_apply, SchwartzMap.add_apply, positionOperator_apply, + momentumOperator_apply, neg_mul, mul_neg, SchwartzMap.smul_apply, smul_eq_mul, + sub_neg_eq_add, one_smul, comp_id, smul_neg, real_smul, 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 + + (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 + + (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] + ext + simp only [nsmul_eq_mul, comp_add, comp_smulβ‚›β‚—, RingHom.id_apply, coe_sub', coe_smul', + Pi.sub_apply, ContinuousLinearMap.add_apply, coe_comp', Function.comp_apply, coe_mul, + coe_id', CompTriple.comp_eq, Pi.smul_apply, natCast_apply, map_smul_of_tower, + SchwartzMap.sub_apply, SchwartzMap.add_apply, positionOperator_apply, + momentumOperator_apply, neg_mul, mul_neg, SchwartzMap.smul_apply, smul_eq_mul, smul_neg, + real_smul, ofReal_ofNat, sub_neg_eq_add, sub_left_inj] ring simp only [Finset.sum_sub_distrib, Finset.sum_add_distrib, ← Finset.smul_sum, ← finset_sum_comp] - rw [positionOperatorSqr_eq d Ξ΅, sub_comp, smul_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, - positionOperator_apply, momentumOperator_apply, neg_mul, mul_neg, Finset.sum_neg_distrib, - smul_neg, Complex.real_smul, Complex.ofReal_ofNat, radiusRegPowOperator_apply, ne_eq, - OfNat.ofNat_ne_zero, not_false_eq_true, div_self, Real.rpow_one, Complex.ofReal_add, - Complex.ofReal_pow, one_apply, 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] + rw [positionOperatorSqr_eq Ξ΅, sub_comp, smul_comp, sum_smul, id_comp] + simp only [smul_sub, ← sub_add, smul_smul, Finset.sum_const, Finset.card_univ, Fintype.card_fin, + ← Nat.cast_smul_eq_nsmul β„‚] + simp only [sub_eq_add_neg, add_assoc, ← neg_smul, ← add_smul] + congr ring /-- `⁅𝐇(Ξ΅), 𝐀(Ξ΅)ᡒ⁆ = iℏkΡ²(¾𝐫(Ξ΅)⁻⁡(𝐱ⱼ𝐋ᡒⱼ + 𝐋ᡒⱼ𝐱ⱼ) + 3iℏ/2 𝐫(Ξ΅)⁻⁡𝐱ᡒ + 𝐫(Ξ΅)⁻³𝐩ᡒ)` -/ @@ -703,7 +675,7 @@ private lemma sum_Lprx (Ξ΅ : ℝˣ) : rw [symm j i, sub_sub_sub_cancel_right] rw [← angularMomentumOperator] rw [← angularMomentumOperatorSqr, ← sub_eq_zero] - exact angularMomentumSqr_commutation_radiusRegPow Ξ΅ + exact angularMomentumSqr_commutation_radiusRegPow Ξ΅ _ private lemma sum_rxpL (Ξ΅ : ℝˣ) : βˆ‘ i : Fin H.d, βˆ‘ j, 𝐫[Ξ΅,-1] ∘L 𝐱[i] ∘L 𝐩[j] ∘L 𝐋[i,j] = 𝐫[Ξ΅,-1] ∘L 𝐋² := by @@ -724,7 +696,7 @@ private lemma sum_prx (d : β„•) (Ξ΅ : ℝˣ) : βˆ‘ i : Fin d, 𝐩[i] ∘L 𝐫[ rw [sub_comp, smul_comp, comp_assoc, comp_assoc] rw [comp_eq_comp_sub_commute 𝐩[_] 𝐱[_], position_commutation_momentum] rw [eq_one_of_same] - rw [comp_sub, comp_smul, comp_id] + rw [comp_sub, comp_smul, one_smul, comp_id] repeat rw [Finset.sum_sub_distrib, ← Finset.smul_sum, ← comp_finset_sum] rw [positionOperatorSqr_eq, comp_sub, radiusRegPowOperator_comp_eq, comp_smul] diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean index cb8089ca4..79b1fd729 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean @@ -50,26 +50,25 @@ Commutator lemmas come in three flavors: namespace QuantumMechanics noncomputable section -open Constants +open Complex Constants open KroneckerDelta +open Bracket open SchwartzMap ContinuousLinearMap +variable {d : β„•} (i j k l : Fin d) (Ξ΅ : ℝˣ) (s t : ℝ) + /-! ## A. General -/ -private lemma ite_cond_symm (i j : Fin d) : - (if i = j then A else B) = (if j = i then A else B) := - ite_cond_congr (Eq.propIntro Eq.symm Eq.symm) - -lemma leibniz_lie {d : β„•} (A B C : 𝓒(Space d, β„‚) β†’L[β„‚] 𝓒(Space d, β„‚)) : +lemma leibniz_lie (A B C : 𝓒(Space d, β„‚) β†’L[β„‚] 𝓒(Space d, β„‚)) : ⁅A ∘L B, C⁆ = A ∘L ⁅B, C⁆ + ⁅A, C⁆ ∘L B := by dsimp only [Bracket.bracket] simp only [ContinuousLinearMap.mul_def, comp_assoc, comp_sub, sub_comp, sub_add_sub_cancel] -lemma lie_leibniz {d : β„•} (A B C : 𝓒(Space d, β„‚) β†’L[β„‚] 𝓒(Space d, β„‚)) : +lemma lie_leibniz (A B C : 𝓒(Space d, β„‚) β†’L[β„‚] 𝓒(Space d, β„‚)) : ⁅A, B ∘L C⁆ = B ∘L ⁅A, C⁆ + ⁅A, B⁆ ∘L C := by dsimp only [Bracket.bracket] simp only [ContinuousLinearMap.mul_def, comp_assoc, comp_sub, sub_comp, sub_add_sub_cancel'] @@ -97,35 +96,25 @@ lemma comp_eq_comp_sub_commute (A B : 𝓒(Space d, β„‚) β†’L[β„‚] 𝓒(Space d, -/ /-- Position operators commute: `[xα΅’, xβ±Ό] = 0`. -/ -lemma position_commutation_position {d : β„•} (i j : Fin d) : ⁅𝐱[i], 𝐱[j]⁆ = 0 := by - dsimp only [Bracket.bracket] - ext ψ x - simp only [coe_sub', coe_mul, Pi.sub_apply, Function.comp_apply, SchwartzMap.sub_apply, - ContinuousLinearMap.zero_apply, SchwartzMap.zero_apply, positionOperator_apply] - ring +@[simp] +lemma position_commutation_position : ⁅𝐱[i], 𝐱[j]⁆ = 0 := by + ext + simp [bracket, ← mul_assoc, mul_comm] -lemma position_comp_commute {d : β„•} (i j : Fin d) : 𝐱[i] ∘L 𝐱[j] = 𝐱[j] ∘L 𝐱[i] := by - rw [← sub_eq_zero] - exact position_commutation_position i j +lemma position_comp_commute : 𝐱[i] ∘L 𝐱[j] = 𝐱[j] ∘L 𝐱[i] := by + rw [comp_eq_comp_add_commute, position_commutation_position, add_zero] -lemma position_commutation_radiusRegPow {d : β„•} (i : Fin d) (Ξ΅ : ℝˣ) (s : ℝ) : - ⁅𝐱[i], 𝐫[d,Ξ΅,s]⁆ = 0 := by - dsimp only [Bracket.bracket] - ext ψ x - simp only [coe_sub', coe_mul, Pi.sub_apply, Function.comp_apply, SchwartzMap.sub_apply] - simp only [positionOperator_apply, radiusRegPowOperator_apply] - simp only [Complex.real_smul, ContinuousLinearMap.zero_apply, SchwartzMap.zero_apply] - ring +@[simp] +lemma position_commutation_radiusRegPow : ⁅𝐱[i], 𝐫[d,Ξ΅,s]⁆ = 0 := by + ext + simp [bracket, ← mul_assoc, mul_comm] -lemma position_comp_radiusRegPow_commute {d : β„•} (i : Fin d) (Ξ΅ : ℝˣ) (s : ℝ) : - 𝐱[i] ∘L 𝐫[Ξ΅,s] = 𝐫[Ξ΅,s] ∘L 𝐱[i] := by - rw [← sub_eq_zero] - exact position_commutation_radiusRegPow _ _ _ +lemma position_comp_radiusRegPow_commute : 𝐱[i] ∘L 𝐫[Ξ΅,s] = 𝐫[Ξ΅,s] ∘L 𝐱[i] := by + rw [comp_eq_comp_add_commute, position_commutation_radiusRegPow, add_zero] -lemma radiusRegPow_commutation_radiusRegPow {d : β„•} (Ξ΅ : ℝˣ) (s t : ℝ) : - ⁅𝐫[d,Ξ΅,s], 𝐫[d,Ξ΅,t]⁆ = 0 := by - dsimp only [Bracket.bracket] - simp only [ContinuousLinearMap.mul_def, radiusRegPowOperator_comp_eq, add_comm, sub_self] +@[simp] +lemma radiusRegPow_commutation_radiusRegPow : ⁅𝐫[d,Ξ΅,s], 𝐫[d,Ξ΅,t]⁆ = 0 := by + simp [bracket, mul_def, radiusRegPowOperator_comp_eq, add_comm] /-! @@ -134,36 +123,23 @@ lemma radiusRegPow_commutation_radiusRegPow {d : β„•} (Ξ΅ : ℝˣ) (s t : ℝ) : -/ /-- Momentum operators commute: `[pα΅’, pβ±Ό] = 0`. -/ -lemma momentum_commutation_momentum {d : β„•} (i j : Fin d) : ⁅𝐩[i], 𝐩[j]⁆ = 0 := by - dsimp only [Bracket.bracket] +@[simp] +lemma momentum_commutation_momentum : ⁅𝐩[i], 𝐩[j]⁆ = 0 := by ext ψ x - simp only [coe_sub', coe_mul, Pi.sub_apply, Function.comp_apply, SchwartzMap.sub_apply, - ContinuousLinearMap.zero_apply, SchwartzMap.zero_apply, momentumOperator_apply_fun] - rw [Space.deriv_const_smul _ ?_, Space.deriv_const_smul _ ?_] - Β· rw [Space.deriv_commute _ (ψ.smooth _), sub_self] - Β· exact Space.deriv_differentiable (ψ.smooth _) i - Β· exact Space.deriv_differentiable (ψ.smooth _) j - -lemma momentum_comp_commute {d : β„•} (i j : Fin d) : 𝐩[i] ∘L 𝐩[j] = 𝐩[j] ∘L 𝐩[i] := by - rw [← sub_eq_zero] - exact momentum_commutation_momentum i j - -lemma momentumSqr_commutation_momentum {d : β„•} (i : Fin d) : - ⁅momentumOperatorSqr (d := d), 𝐩[i]⁆ = 0 := by - dsimp only [Bracket.bracket, momentumOperatorSqr] - rw [Finset.mul_sum, Finset.sum_mul, ← Finset.sum_sub_distrib] - conv_lhs => - enter [2, j] - simp only [ContinuousLinearMap.mul_def] - rw [comp_assoc] - rw [momentum_comp_commute j i, ← comp_assoc] - rw [momentum_comp_commute j i, comp_assoc] - rw [sub_self] - rw [Finset.sum_const_zero] - -lemma momentumSqr_comp_momentum_commute {d : β„•} (i : Fin d) : 𝐩² ∘L 𝐩[i] = 𝐩[i] ∘L 𝐩² := by - rw [← sub_eq_zero] - exact momentumSqr_commutation_momentum i + have hdiff (k : Fin d) : Differentiable ℝ (βˆ‚[k] ψ) := Space.deriv_differentiable (ψ.smooth 2) k + show 𝐩[i] (𝐩[j] ψ) x - 𝐩[j] (𝐩[i] ψ) x = 0 + simp only [momentumOperator_apply_fun, Space.deriv_const_smul _ (hdiff _), + Space.deriv_commute _ (ψ.smooth 2), sub_self] + +lemma momentum_comp_commute : 𝐩[i] ∘L 𝐩[j] = 𝐩[j] ∘L 𝐩[i] := by + rw [comp_eq_comp_add_commute, momentum_commutation_momentum, add_zero] + +@[simp] +lemma momentumSqr_commutation_momentum : ⁅momentumOperatorSqr (d := d), 𝐩[i]⁆ = 0 := by + simp [momentumOperatorSqr, sum_lie, leibniz_lie] + +lemma momentumSqr_comp_momentum_commute : 𝐩² ∘L 𝐩[i] = 𝐩[i] ∘L 𝐩² := by + rw [comp_eq_comp_add_commute, momentumSqr_commutation_momentum, add_zero] /-! @@ -172,133 +148,97 @@ 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] +lemma position_commutation_momentum : ⁅𝐱[i], 𝐩[j]⁆ = + (I * ℏ) β€’ Ξ΄[i,j] β€’ ContinuousLinearMap.id β„‚ 𝓒(Space d, β„‚) := by 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] - rw [positionOperator_apply, momentumOperator_apply_fun] - rw [momentumOperator_apply, positionOperator_apply_fun] - simp only [neg_mul, Pi.smul_apply, smul_eq_mul, mul_neg, sub_neg_eq_add] - have h : ⇑(smulLeftCLM β„‚ ⇑(Space.coordCLM i) β€’ ψ) = (fun (x : Space d) ↦ x i) β€’ ψ := by - ext x - rw [ContinuousLinearMap.smul_def, smulLeftCLM_apply_apply (by fun_prop), Space.coordCLM_apply] - 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_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 - rw [← position_commutation_momentum] - dsimp only [Bracket.bracket] - simp only [ContinuousLinearMap.mul_def, sub_sub_cancel] - -lemma position_position_commutation_momentum {d : β„•} (i j k : Fin d) : ⁅𝐱[i] ∘L 𝐱[j], 𝐩[k]⁆ = - (Complex.I * ℏ * Ξ΄[i,k]) β€’ 𝐱[j] + (Complex.I * ℏ * Ξ΄[j,k]) β€’ 𝐱[i] := by - rw [leibniz_lie] - rw [position_commutation_momentum, position_commutation_momentum] - rw [ContinuousLinearMap.comp_smul, ContinuousLinearMap.smul_comp] - rw [id_comp, comp_id] - rw [add_comm] - -lemma position_commutation_momentum_momentum {d : β„•} (i j k : Fin d) : ⁅𝐱[i], 𝐩[j] ∘L 𝐩[k]⁆ = - (Complex.I * ℏ * Ξ΄[i,k]) β€’ 𝐩[j] + (Complex.I * ℏ * Ξ΄[i,j]) β€’ 𝐩[k] := by - rw [lie_leibniz] - rw [position_commutation_momentum, position_commutation_momentum] - rw [ContinuousLinearMap.comp_smul, ContinuousLinearMap.smul_comp] - rw [id_comp, comp_id] - -lemma position_commutation_momentumSqr {d : β„•} (i : Fin d) : ⁅𝐱[i], 𝐩²⁆ = - (2 * Complex.I * ℏ) β€’ 𝐩[i] := by - unfold momentumOperatorSqr - rw [lie_sum] - simp only [position_commutation_momentum_momentum] - dsimp only [kroneckerDelta] - 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_nf - simp - -lemma radiusRegPow_commutation_momentum {d : β„•} (Ξ΅ : ℝˣ) (s : ℝ) (i : Fin d) : - ⁅𝐫[d,Ξ΅,s], 𝐩[i]⁆ = (s * Complex.I * ℏ) β€’ 𝐫[Ξ΅,s-2] ∘L 𝐱[i] := by - dsimp only [Bracket.bracket] + show 𝐱[i] (𝐩[j] ψ) x - 𝐩[j] (𝐱[i] ψ) x = _ + trans (I * ℏ) * (-x i * βˆ‚[j] ψ x + βˆ‚[j] ((fun x : Space d ↦ x i) β€’ β‡‘Οˆ) x) + Β· simp only [positionOperator_apply, momentumOperator_apply, positionOperator_apply_fun] + ring + rw [Space.deriv_smul (by fun_prop) (by fun_prop)] + rw [Space.deriv_component] + rcases eq_or_ne i j with (rfl | hne) + Β· simp + Β· simp [eq_zero_of_ne hne, hne.symm] + +lemma momentum_comp_position_eq : 𝐩[j] ∘L 𝐱[i] = + 𝐱[i] ∘L 𝐩[j] - (I * ℏ) β€’ Ξ΄[i,j] β€’ ContinuousLinearMap.id β„‚ 𝓒(Space d, β„‚) := by + rw [comp_eq_comp_sub_commute, position_commutation_momentum] + +lemma position_position_commutation_momentum : ⁅𝐱[i] ∘L 𝐱[j], 𝐩[k]⁆ = + (I * ℏ) β€’ (Ξ΄[i,k] β€’ 𝐱[j] + Ξ΄[j,k] β€’ 𝐱[i]) := by + simp only [leibniz_lie, position_commutation_momentum, comp_smul, smul_comp, comp_id, id_comp, + smul_add, add_comm] + +lemma position_commutation_momentum_momentum : ⁅𝐱[i], 𝐩[j] ∘L 𝐩[k]⁆ = + (I * ℏ) β€’ (Ξ΄[i,k] β€’ 𝐩[j] + Ξ΄[i,j] β€’ 𝐩[k]) := by + simp only [lie_leibniz, position_commutation_momentum, comp_smul, smul_comp, comp_id, id_comp, + smul_add] + +lemma position_commutation_momentumSqr : ⁅𝐱[i], 𝐩²⁆ = (2 * I * ℏ) β€’ 𝐩[i] := by + simp only [momentumOperatorSqr, lie_sum, lie_leibniz, position_commutation_momentum, comp_smul, + smul_comp, comp_id, id_comp, ← two_smul β„‚, smul_smul, mul_assoc, ← Finset.smul_sum, sum_smul] + +lemma radiusRegPow_commutation_momentum : + ⁅𝐫[d,Ξ΅,s], 𝐩[i]⁆ = (s * I * ℏ) β€’ 𝐫[Ξ΅,s-2] ∘L 𝐱[i] := by ext ψ x - simp only [coe_sub', coe_mul, Pi.sub_apply, Function.comp_apply, SchwartzMap.sub_apply, coe_smul', - coe_comp', Pi.smul_apply, SchwartzMap.smul_apply, smul_eq_mul] + have hne := Ne.symm (ne_of_lt <| norm_sq_add_unit_sq_pos Ξ΅ x) + have hdiff1 : DifferentiableAt ℝ (fun x => (β€–xβ€– ^ 2 + ↑Ρ ^ 2) ^ (s / 2)) x := by + refine DifferentiableAt.rpow_const ?_ (Or.intro_left _ hne) + exact Differentiable.differentiableAt (by fun_prop) + have hdiff2 := Real.differentiableAt_rpow_const_of_ne (s / 2) hne + have hdiff3 : DifferentiableAt ℝ (fun x ↦ β€–xβ€– ^ 2 + Ξ΅ ^ 2) x := + Differentiable.differentiableAt (by fun_prop) + show 𝐫[Ξ΅,s] (𝐩[i] ψ) x - 𝐩[i] (𝐫[Ξ΅,s] ψ) x = (s * I * ℏ) * 𝐫[Ξ΅,s-2] (𝐱[i] ψ) x simp only [momentumOperator_apply, positionOperator_apply, radiusRegPowOperator_apply_fun] - - have hne : βˆ€ x : Space d, β€–xβ€– ^ 2 + Ξ΅ ^ 2 β‰  0 := by - intro x - apply ne_of_gt - exact add_pos_of_nonneg_of_pos (sq_nonneg _) (sq_pos_iff.mpr <| Units.ne_zero Ξ΅) - - have h : (fun x ↦ (β€–xβ€– ^ 2 + Ξ΅ ^ 2) ^ (s / 2) β€’ ψ x) = - (fun (x : Space d) ↦ (β€–xβ€– ^ 2 + Ξ΅ ^ 2) ^ (s / 2)) β€’ ψ := rfl - have h' : βˆ‚[i] (fun x ↦ (β€–xβ€– ^ 2 + Ξ΅ ^ 2) ^ (s / 2)) = - fun x ↦ s * (β€–xβ€– ^ 2 + Ξ΅ ^ 2) ^ (s / 2 - 1) * x i := by - trans βˆ‚[i] ((fun x ↦ x ^ (s / 2)) ∘ (fun x ↦ β€–xβ€– ^ 2 + Ξ΅ ^ 2)) - Β· congr - ext x - rw [Space.deriv_eq, fderiv_comp] - Β· simp only [fderiv_add_const, fderiv_norm_sq_apply, comp_smul, coe_smul', coe_comp', - coe_innerSL_apply, Pi.smul_apply, Function.comp_apply, Space.inner_basis, - fderiv_eq_smul_deriv, smul_eq_mul, nsmul_eq_mul, Nat.cast_ofNat] - rw [deriv_rpow_const] - Β· simp only [deriv_id'', one_mul] - ring - Β· fun_prop - Β· left - exact hne _ - Β· exact Real.differentiableAt_rpow_const_of_ne (s / 2) (hne x) - Β· exact Differentiable.differentiableAt (by fun_prop) - - rw [h, Space.deriv_smul] - Β· rw [h'] - simp only [neg_mul, smul_neg, Complex.real_smul, Complex.ofReal_mul, sub_neg_eq_add] + rw [← Pi.smul_def', Space.deriv_smul hdiff1 (by fun_prop)] + suffices βˆ‚[i] (fun x ↦ (β€–xβ€– ^ 2 + Ξ΅ ^ 2) ^ (s / 2)) x = + s * (β€–xβ€– ^ 2 + Ξ΅ ^ 2) ^ (s / 2 - 1) * x i by + simp only [this, real_smul, ofReal_mul] ring_nf - Β· refine DifferentiableAt.rpow ?_ (by fun_prop) (hne _) - exact Differentiable.differentiableAt (by fun_prop) - Β· fun_prop - -lemma momentum_comp_radiusRegPow_eq {d : β„•} (i : Fin d) (Ξ΅ : ℝˣ) (s : ℝ) : - 𝐩[i] ∘L 𝐫[Ξ΅,s] = 𝐫[Ξ΅,s] ∘L 𝐩[i] - (s * Complex.I * ℏ) β€’ 𝐫[Ξ΅,s-2] ∘L 𝐱[i] := by - rw [← radiusRegPow_commutation_momentum] - dsimp only [Bracket.bracket] - simp only [ContinuousLinearMap.mul_def, sub_sub_cancel] - -lemma radiusRegPow_commutation_momentumSqr (Ξ΅ : ℝˣ) (s : ℝ) : - ⁅𝐫[d,Ξ΅,s], momentumOperatorSqr (d := d)⁆ = - (2 * s * Complex.I * ℏ) β€’ 𝐫[Ξ΅,s-2] ∘L βˆ‘ i, 𝐱[i] ∘L 𝐩[i] - + (s * ℏ ^ 2) β€’ ((d + s - 2) β€’ 𝐫[Ξ΅,s-2] - (Ξ΅ ^ 2 * (s - 2)) β€’ 𝐫[Ξ΅,s-4]) := by - unfold momentumOperatorSqr - rw [lie_sum] - conv_lhs => - enter [2, i] - rw [lie_leibniz, radiusRegPow_commutation_momentum] - rw [comp_smul, ← comp_assoc, momentum_comp_radiusRegPow_eq] - 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, comp_sub, radiusRegPowOperator_comp_eq, comp_smul] - 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, one_apply] - ring_nf - rw [Complex.I_sq] - ring + change βˆ‚[i] ((fun r ↦ r ^ (s / 2)) ∘ (fun x ↦ β€–xβ€– ^ 2 + Ξ΅ ^ 2)) x = _ + rw [Space.deriv_eq, fderiv_comp x hdiff2 hdiff3, fderiv_add_const, fderiv_norm_sq_apply] + simp [Real.deriv_rpow_const, mul_comm, ← mul_assoc, mul_div_cancelβ‚€ s (NeZero.ne' 2).symm] + +lemma momentum_comp_radiusRegPow_eq : + 𝐩[i] ∘L 𝐫[Ξ΅,s] = 𝐫[Ξ΅,s] ∘L 𝐩[i] - (s * I * ℏ) β€’ 𝐫[Ξ΅,s-2] ∘L 𝐱[i] := by + rw [comp_eq_comp_sub_commute, radiusRegPow_commutation_momentum] + +lemma radiusRegPow_commutation_momentumSqr : + ⁅𝐫[d,Ξ΅,s], momentumOperatorSqr (d := d)⁆ = (2 * s * I * ℏ) β€’ 𝐫[Ξ΅,s-2] ∘L βˆ‘ i, 𝐱[i] ∘L 𝐩[i] + + (s * (d + s - 2) * ℏ ^ 2) β€’ 𝐫[Ξ΅,s-2] - (Ξ΅ ^ 2 * s * (s - 2) * ℏ ^ 2) β€’ 𝐫[Ξ΅,s-4] := by + calc + _ = (s * I * ℏ) β€’ βˆ‘ i, ((𝐩[i] ∘L 𝐫[Ξ΅,s-2]) ∘L 𝐱[i] + 𝐫[Ξ΅,s-2] ∘L 𝐱[i] ∘L 𝐩[i]) := by + simp [momentumOperatorSqr, lie_sum, lie_leibniz, radiusRegPow_commutation_momentum, + ← smul_add, ← Finset.smul_sum, comp_assoc] + _ = (s * I * ℏ) β€’ βˆ‘ i, (𝐫[Ξ΅,s-2] ∘L 𝐩[i] ∘L 𝐱[i] + 𝐫[Ξ΅,s-2] ∘L 𝐱[i] ∘L 𝐩[i] + - (↑(s - 2) * I * ℏ) β€’ 𝐫[Ξ΅,s-4] ∘L 𝐱[i] ∘L 𝐱[i]) := by + simp only [momentum_comp_radiusRegPow_eq, sub_comp, smul_comp, sub_add_eq_add_sub, comp_assoc] + ring_nf + _ = (s * I * ℏ) β€’ βˆ‘ i, ((2 : β„‚) β€’ 𝐫[Ξ΅,s-2] ∘L 𝐱[i] ∘L 𝐩[i] - (I * ℏ) β€’ 𝐫[Ξ΅,s-2] + - (↑(s - 2) * I * ℏ) β€’ 𝐫[Ξ΅,s-4] ∘L 𝐱[i] ∘L 𝐱[i]) := by + simp [momentum_comp_position_eq, sub_add_eq_add_sub, ← two_smul β„‚] + simp only [Finset.sum_sub_distrib, ← Finset.smul_sum, smul_sub, smul_smul, ← comp_finset_sum] + have hsumr : βˆ‘ i : Fin d, 𝐫[d,Ξ΅,s-2] = (d : β„‚) β€’ 𝐫[Ξ΅,s-2] := by + simp only [Finset.sum_const, Finset.card_univ, Fintype.card_fin, Nat.cast_smul_eq_nsmul] + have hrxx : 𝐫[d,Ξ΅,s-4] ∘L βˆ‘ i, 𝐱[i] ∘L 𝐱[i] = 𝐫[Ξ΅,s-2] - (Ξ΅ ^ 2 : β„‚) β€’ 𝐫[Ξ΅,s-4] := by + rw [positionOperatorSqr_eq Ξ΅, comp_sub, comp_smul, comp_id, radiusRegPowOperator_comp_eq, + ← Complex.coe_smul (Ξ΅.1 ^ 2), ofReal_pow] + ring_nf + rw [hsumr, hrxx, smul_smul, smul_sub, ← sub_add, sub_sub, ← add_smul, smul_smul] + simp only [sub_eq_add_neg, ← neg_smul] + congr 3 -- match coefficients of `r[s-4]βˆ‘xα΅’pα΅’`, `r[s-2]` and `r[s-4]` + Β· ring + Β· ring_nf + simp only [I_sq, ofReal_add, ofReal_neg, RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe, + MonoidHom.toOneHom_coe, MonoidHom.coe_coe, coe_algebraMap, ZeroHom.coe_mk, ofReal_sub, + ofReal_mul, ofReal_natCast, ofReal_pow] + ring + Β· ring_nf + simp only [I_sq, ofReal_add, ofReal_neg, RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe, + MonoidHom.toOneHom_coe, MonoidHom.coe_coe, coe_algebraMap, ZeroHom.coe_mk, ofReal_sub, + ofReal_mul, ofReal_pow] + ring /-! @@ -306,35 +246,24 @@ lemma radiusRegPow_commutation_momentumSqr (Ξ΅ : ℝˣ) (s : ℝ) : -/ -lemma angularMomentum_commutation_position {d : β„•} (i j k : Fin d) : ⁅𝐋[i,j], 𝐱[k]⁆ = - (Complex.I * ℏ * Ξ΄[i,k]) β€’ 𝐱[j] - (Complex.I * ℏ * Ξ΄[j,k]) β€’ 𝐱[i] := by - unfold angularMomentumOperator - rw [sub_lie] - rw [leibniz_lie, leibniz_lie] - rw [position_commutation_position, position_commutation_position] - rw [← lie_skew, position_commutation_momentum] - rw [← lie_skew, position_commutation_momentum] - 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] - -lemma angularMomentum_commutation_radiusRegPow (i j : Fin d) (Ξ΅ : ℝˣ) (s : ℝ) : - ⁅𝐋[i,j], 𝐫[d,Ξ΅,s]⁆ = 0 := by - dsimp only [Bracket.bracket] - unfold angularMomentumOperator - simp only [sub_mul, ContinuousLinearMap.mul_def, ContinuousLinearMap.comp_assoc] - repeat rw [momentum_comp_radiusRegPow_eq] - simp only [comp_sub, comp_smulβ‚›β‚—, RingHom.id_apply, ← ContinuousLinearMap.comp_assoc] - repeat rw [position_comp_radiusRegPow_commute] - simp only [ContinuousLinearMap.comp_assoc] - rw [position_comp_commute] - simp only [sub_sub_sub_cancel_right, sub_self] - -lemma angularMomentumSqr_commutation_radiusRegPow (Ξ΅ : ℝˣ) : +lemma angularMomentum_commutation_position : + ⁅𝐋[i,j], 𝐱[k]⁆ = (I * ℏ) β€’ (Ξ΄[i,k] β€’ 𝐱[j] - Ξ΄[j,k] β€’ 𝐱[i]) := by + trans 𝐱[i] ∘L ⁅𝐩[j], 𝐱[k]⁆ - 𝐱[j] ∘L ⁅𝐩[i], 𝐱[k]⁆ + Β· simp [angularMomentumOperator, leibniz_lie] + simp only [← lie_skew 𝐩[_] 𝐱[_], comp_neg, sub_neg_eq_add, add_comm, ← sub_eq_add_neg, + position_commutation_momentum, comp_smul, comp_id, smul_sub, symm k _] + +@[simp] +lemma angularMomentum_commutation_radiusRegPow : ⁅𝐋[i,j], 𝐫[d,Ξ΅,s]⁆ = 0 := by + trans 𝐱[i] ∘L ⁅𝐩[j], 𝐫[Ξ΅,s]⁆ - 𝐱[j] ∘L ⁅𝐩[i], 𝐫[Ξ΅,s]⁆ + Β· simp [angularMomentumOperator, leibniz_lie] + simp [← lie_skew 𝐩[_] 𝐫[_,_], radiusRegPow_commutation_momentum, comp_neg, + ← position_comp_radiusRegPow_commute, ← comp_assoc, position_comp_commute] + +@[simp] +lemma angularMomentumSqr_commutation_radiusRegPow : ⁅angularMomentumOperatorSqr (d := d), 𝐫[d,Ξ΅,s]⁆ = 0 := by - unfold angularMomentumOperatorSqr - simp only [sum_lie, smul_lie, leibniz_lie, angularMomentum_commutation_radiusRegPow, - comp_zero, zero_comp, add_zero, smul_zero, Finset.sum_const_zero] + simp [angularMomentumOperatorSqr, sum_lie, leibniz_lie] /-! @@ -342,47 +271,29 @@ lemma angularMomentumSqr_commutation_radiusRegPow (Ξ΅ : ℝˣ) : -/ -lemma angularMomentum_commutation_momentum {d : β„•} (i j k : Fin d) : ⁅𝐋[i,j], 𝐩[k]⁆ = - (Complex.I * ℏ * Ξ΄[i,k]) β€’ 𝐩[j] - (Complex.I * ℏ * Ξ΄[j,k]) β€’ 𝐩[i] := by - unfold angularMomentumOperator - rw [sub_lie] - rw [leibniz_lie, leibniz_lie] - rw [momentum_commutation_momentum, momentum_commutation_momentum] - rw [position_commutation_momentum, position_commutation_momentum] - simp only [ContinuousLinearMap.smul_comp, id_comp, comp_zero, zero_add] - -lemma momentum_comp_angularMomentum_eq {d : β„•} (i j k : Fin d) : 𝐩[k] ∘L 𝐋[i,j] = - 𝐋[i,j] ∘L 𝐩[k] - (Complex.I * ℏ * Ξ΄[i,k]) β€’ 𝐩[j] + (Complex.I * ℏ * Ξ΄[j,k]) β€’ 𝐩[i] := by - rw [← sub_eq_zero, sub_add] - rw [← angularMomentum_commutation_momentum] - dsimp only [Bracket.bracket] - simp only [ContinuousLinearMap.mul_def, sub_sub_cancel, sub_eq_zero] - -lemma angularMomentum_commutation_momentumSqr {d : β„•} (i j : Fin d) : - ⁅𝐋[i,j], momentumOperatorSqr (d := d)⁆ = 0 := by - unfold momentumOperatorSqr - conv_lhs => - rw [lie_sum] - enter [2, k] - 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 [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 angularMomentum_commutation_momentum : ⁅𝐋[i,j], 𝐩[k]⁆ = + (I * ℏ) β€’ (Ξ΄[i,k] β€’ 𝐩[j] - Ξ΄[j,k] β€’ 𝐩[i]) := by + trans ⁅𝐱[i], 𝐩[k]⁆ ∘L 𝐩[j] - ⁅𝐱[j], 𝐩[k]⁆ ∘L 𝐩[i] + Β· simp [angularMomentumOperator, leibniz_lie] + simp only [position_commutation_momentum, smul_comp, id_comp, smul_sub] -lemma momentumSqr_comp_angularMomentum_commute {d : β„•} (i j : Fin d) : - 𝐩² ∘L 𝐋[i,j] = 𝐋[i,j] ∘L 𝐩² := by - apply Eq.symm - rw [← sub_eq_zero] - exact angularMomentum_commutation_momentumSqr i j +lemma momentum_comp_angularMomentum_eq : 𝐩[k] ∘L 𝐋[i,j] = + 𝐋[i,j] ∘L 𝐩[k] - (I * ℏ) β€’ (Ξ΄[i,k] β€’ 𝐩[j] - Ξ΄[j,k] β€’ 𝐩[i]) := by + rw [comp_eq_comp_sub_commute, angularMomentum_commutation_momentum] -lemma angularMomentumSqr_commutation_momentumSqr {d : β„•} : +@[simp] +lemma angularMomentum_commutation_momentumSqr : ⁅𝐋[i,j], momentumOperatorSqr (d := d)⁆ = 0 := by + simp only [momentumOperatorSqr, lie_sum, lie_leibniz, angularMomentum_commutation_momentum, + comp_smul, comp_sub, smul_comp, sub_comp, ← smul_add, ← Finset.smul_sum, Finset.sum_add_distrib, + Finset.sum_sub_distrib, sum_smul, sub_add_sub_cancel, sub_self, smul_zero] + +lemma momentumSqr_comp_angularMomentum_commute : 𝐩² ∘L 𝐋[i,j] = 𝐋[i,j] ∘L 𝐩² := by + rw [comp_eq_comp_sub_commute, angularMomentum_commutation_momentumSqr, sub_zero] + +@[simp] +lemma angularMomentumSqr_commutation_momentumSqr : ⁅angularMomentumOperatorSqr (d := d), momentumOperatorSqr (d := d)⁆ = 0 := by - unfold angularMomentumOperatorSqr - simp only [smul_lie, sum_lie, leibniz_lie] - simp [angularMomentum_commutation_momentumSqr] + simp [angularMomentumOperatorSqr, sum_lie, leibniz_lie] /-! @@ -390,20 +301,16 @@ lemma angularMomentumSqr_commutation_momentumSqr {d : β„•} : -/ -lemma angularMomentum_commutation_angularMomentum {d : β„•} (i j k l : Fin d) : ⁅𝐋[i,j], 𝐋[k,l]⁆ = - (Complex.I * ℏ * Ξ΄[i,k]) β€’ 𝐋[j,l] - (Complex.I * ℏ * Ξ΄[i,l]) β€’ 𝐋[j,k] - - (Complex.I * ℏ * Ξ΄[j,k]) β€’ 𝐋[i,l] + (Complex.I * ℏ * Ξ΄[j,l]) β€’ 𝐋[i,k] := by +lemma angularMomentum_commutation_angularMomentum : ⁅𝐋[i,j], 𝐋[k,l]⁆ = + (I * ℏ) β€’ (Ξ΄[i,k] β€’ 𝐋[j,l] - Ξ΄[i,l] β€’ 𝐋[j,k] - Ξ΄[j,k] β€’ 𝐋[i,l] + Ξ΄[j,l] β€’ 𝐋[i,k]) := by nth_rw 2 [angularMomentumOperator] - rw [lie_sub] - rw [lie_leibniz, lie_leibniz] - rw [angularMomentum_commutation_momentum, angularMomentum_commutation_position] - rw [angularMomentum_commutation_momentum, angularMomentum_commutation_position] - dsimp only [angularMomentumOperator, kroneckerDelta] - simp only [ContinuousLinearMap.comp_sub, ContinuousLinearMap.sub_comp, - ContinuousLinearMap.comp_smul, ContinuousLinearMap.smul_comp] - ext ψ x - simp only [coe_sub', Pi.sub_apply, ContinuousLinearMap.add_apply, SchwartzMap.sub_apply, - SchwartzMap.add_apply, smul_sub] + simp only [angularMomentum_commutation_position, angularMomentum_commutation_momentum, + lie_sub, lie_leibniz, comp_smul, smul_comp, comp_sub, sub_comp, ← smul_add, ← smul_sub] + dsimp [angularMomentumOperator] + ext + simp only [nsmul_eq_mul, coe_smul', coe_sub', Pi.smul_apply, Pi.sub_apply, + ContinuousLinearMap.add_apply, coe_mul, SchwartzMap.smul_apply, SchwartzMap.sub_apply, + SchwartzMap.add_apply, smul_eq_mul, map_comp_sub] ring private lemma angularMomentum_comp_antisymm_sum {d : β„•} (a b : Fin d) : @@ -421,8 +328,7 @@ lemma angularMomentumSqr_commutation_angularMomentum {d : β„•} (i j : Fin d) : smul_add, smul_sub, Finset.sum_add_distrib, Finset.sum_sub_distrib, ← Finset.smul_sum] dsimp only [kroneckerDelta] - simp only [Nat.cast_ite, Nat.cast_one, CharP.cast_eq_zero, mul_ite, mul_one, mul_zero, - ite_smul, zero_smul] + simp only [ite_smul, zero_smul] simp_rw [Finset.sum_ite_eq' Finset.univ, Finset.mem_univ, if_true] rw [angularMomentum_comp_antisymm_sum i j, angularMomentum_comp_antisymm_sum j i] abel diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Position.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Position.lean index 845124a7c..293c92873 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Operators/Position.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Position.lean @@ -68,17 +68,14 @@ def positionOperator : 𝓒(Space d, β„‚) β†’L[β„‚] 𝓒(Space d, β„‚) := @[inherit_doc positionOperator] notation "𝐱[" i "]" => positionOperator i -lemma positionOperator_apply_fun (ψ : 𝓒(Space d, β„‚)) : - 𝐱[i] ψ = smulLeftCLM β„‚ (coordCLM i) β€’ ψ := by - unfold positionOperator - ext x - simp [smulLeftCLM_apply_apply (g := Complex.ofRealCLM ∘ (coordCLM i)) (by fun_prop) _ _, - smulLeftCLM_apply (g := coordCLM i) (by fun_prop) _] +lemma positionOperator_apply_fun (ψ : 𝓒(Space d, β„‚)) : 𝐱[i] ψ = (fun x : Space d ↦ x i) β€’ β‡‘Οˆ := by + ext + simp [positionOperator, coordCLM_apply, coord_apply, + smulLeftCLM_apply_apply (g := Complex.ofRealCLM ∘ (coordCLM i)) (by fun_prop)] @[simp] lemma positionOperator_apply (ψ : 𝓒(Space d, β„‚)) (x : Space d) : 𝐱[i] ψ x = x i * ψ x := by - simp [positionOperator_apply_fun, smulLeftCLM_apply (g := coordCLM i) (by fun_prop) _, - coordCLM_apply, coord_apply] + simp [positionOperator_apply_fun] /-! @@ -143,11 +140,13 @@ lemma radiusRegPowOperator_comp_eq {d : β„•} (Ξ΅ : ℝˣ) (s t : ℝ) : simp [add_div, Real.rpow_add (norm_sq_add_unit_sq_pos Ξ΅ x), mul_assoc] @[simp] -lemma radiusRegPowOperator_zero {d : β„•} (Ξ΅ : ℝˣ) : 𝐫[d,Ξ΅,0] = 1 := by +lemma radiusRegPowOperator_zero {d : β„•} (Ξ΅ : ℝˣ) : + 𝐫[d,Ξ΅,0] = ContinuousLinearMap.id β„‚ 𝓒(Space d, β„‚) := by ext simp -lemma positionOperatorSqr_eq (d : β„•) (Ξ΅ : ℝˣ) : βˆ‘ i, 𝐱[i] ∘L 𝐱[i] = 𝐫[d,Ξ΅,2] - Ξ΅.1 ^ 2 β€’ 1 := by +lemma positionOperatorSqr_eq {d : β„•} (Ξ΅ : ℝˣ) : + βˆ‘ i, 𝐱[i] ∘L 𝐱[i] = 𝐫[d,Ξ΅,2] - Ξ΅.1 ^ 2 β€’ ContinuousLinearMap.id β„‚ 𝓒(Space d, β„‚) := by ext simp [Space.norm_sq_eq, add_mul, ← mul_assoc, ← pow_two, Finset.sum_mul]