From 96ee9a5706e20b2fa9f15aaaf7e779a4a580a12e Mon Sep 17 00:00:00 2001 From: gloges Date: Sun, 15 Mar 2026 23:46:38 +0900 Subject: [PATCH 01/15] x golf --- .../DDimensions/Operators/Commutation.lean | 49 ++++++++----------- 1 file changed, 21 insertions(+), 28 deletions(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean index 6a4b1de95..1910cce98 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean @@ -50,10 +50,13 @@ 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 @@ -64,12 +67,12 @@ 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 +100,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] /-! From 84dab74821df47e665c459e8f0d52d1ae5291fa9 Mon Sep 17 00:00:00 2001 From: gloges Date: Sun, 15 Mar 2026 23:53:32 +0900 Subject: [PATCH 02/15] p golf --- .../DDimensions/Operators/Commutation.lean | 43 +++++++------------ 1 file changed, 15 insertions(+), 28 deletions(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean index 1910cce98..b18c78c0c 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean @@ -127,36 +127,23 @@ lemma radiusRegPow_commutation_radiusRegPow : ⁅𝐫[d,ε,s], 𝐫[d,ε,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 + 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 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 +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] /-! From 0920c478bb2175c21aa921874043b277e4f59435 Mon Sep 17 00:00:00 2001 From: gloges Date: Mon, 16 Mar 2026 00:58:26 +0900 Subject: [PATCH 03/15] xp golf --- .../DDimensions/Operators/Commutation.lean | 158 ++++++++---------- .../DDimensions/Operators/Position.lean | 19 +-- 2 files changed, 80 insertions(+), 97 deletions(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean index b18c78c0c..1a7f9f7bd 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean @@ -152,62 +152,39 @@ lemma momentumSqr_comp_momentum_commute : 𝐩² ∘L 𝐩[i] = 𝐩[i] ∘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 + 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 dsimp only [Bracket.bracket] ext ψ x simp only [coe_sub', coe_mul, Pi.sub_apply, Function.comp_apply, SchwartzMap.sub_apply, coe_smul', @@ -247,38 +224,45 @@ lemma radiusRegPow_commutation_momentum {d : ℕ} (ε : ℝˣ) (s : ℝ) (i : Fi 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 +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 /-! 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] From ff9c3b56ff5814f675f7490433bf105d6a5dfb53 Mon Sep 17 00:00:00 2001 From: gloges Date: Mon, 16 Mar 2026 01:12:54 +0900 Subject: [PATCH 04/15] Lx golf --- .../DDimensions/Operators/Commutation.lean | 45 +++++++------------ 1 file changed, 17 insertions(+), 28 deletions(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean index 1a7f9f7bd..5e02de0cd 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean @@ -270,35 +270,24 @@ lemma radiusRegPow_commutation_momentumSqr : -/ -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] /-! From 5b6ed015379312631639b6d7808d8f62490a43d1 Mon Sep 17 00:00:00 2001 From: gloges Date: Mon, 16 Mar 2026 01:25:01 +0900 Subject: [PATCH 05/15] LL temp fixes --- .../QuantumMechanics/DDimensions/Operators/Commutation.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean index 5e02de0cd..0f15627cd 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean @@ -303,6 +303,7 @@ lemma angularMomentum_commutation_momentum {d : ℕ} (i j k : Fin d) : ⁅𝐋[i 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] + sorry 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 @@ -311,6 +312,7 @@ lemma momentum_comp_angularMomentum_eq {d : ℕ} (i j k : Fin d) : 𝐩[k] ∘L dsimp only [Bracket.bracket] simp only [ContinuousLinearMap.mul_def, sub_sub_cancel, sub_eq_zero] +@[simp] lemma angularMomentum_commutation_momentumSqr {d : ℕ} (i j : Fin d) : ⁅𝐋[i,j], momentumOperatorSqr (d := d)⁆ = 0 := by unfold momentumOperatorSqr @@ -331,6 +333,7 @@ lemma momentumSqr_comp_angularMomentum_commute {d : ℕ} (i j : Fin d) : rw [← sub_eq_zero] exact angularMomentum_commutation_momentumSqr i j +@[simp] lemma angularMomentumSqr_commutation_momentumSqr {d : ℕ} : ⁅angularMomentumOperatorSqr (d := d), momentumOperatorSqr (d := d)⁆ = 0 := by unfold angularMomentumOperatorSqr @@ -357,7 +360,8 @@ lemma angularMomentum_commutation_angularMomentum {d : ℕ} (i j k l : Fin d) : ext ψ x simp only [coe_sub', Pi.sub_apply, ContinuousLinearMap.add_apply, SchwartzMap.sub_apply, SchwartzMap.add_apply, smul_sub] - ring + ring_nf + sorry @[sorryful] lemma angularMomentumSqr_commutation_angularMomentum {d : ℕ} (i j : Fin d) : From 5b86b4617852d307c9e562e76b68f82ee424f7cc Mon Sep 17 00:00:00 2001 From: gloges Date: Mon, 16 Mar 2026 01:25:13 +0900 Subject: [PATCH 06/15] LRL fixes --- .../Hydrogen/LaplaceRungeLenzVector.lean | 55 ++++--------------- 1 file changed, 12 insertions(+), 43 deletions(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean b/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean index c7ea6d838..cbe164b5f 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean @@ -48,30 +48,7 @@ def lrlOperatorSqr (ε : ℝˣ) : 𝓢(Space H.d, ℂ) →L[ℂ] 𝓢(Space H.d, 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 + sorry /-- `𝐀(ε)ᵢ = 𝐋ᵢⱼ𝐩ⱼ + ½iℏ(d-1)𝐩ᵢ - mk·𝐫(ε)⁻¹𝐱ᵢ` -/ lemma lrlOperator_eq' (ε : ℝˣ) (i : Fin H.d) : H.lrlOperator ε i = ∑ j, 𝐋[i,j] ∘L 𝐩[j] @@ -274,7 +251,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 +327,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 +347,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 +444,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, @@ -524,11 +501,7 @@ private lemma xL_Lx_eq {d : ℕ} (ε : ℝˣ) (i : Fin d) : ∑ j, (𝐱[j] ∘L 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] - ring + sorry _ = 𝐱[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] @@ -537,13 +510,9 @@ private lemma xL_Lx_eq {d : ℕ} (ε : ℝˣ) (i : Fin d) : ∑ j, (𝐱[j] ∘L + (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 + sorry simp only [Finset.sum_sub_distrib, Finset.sum_add_distrib, ← Finset.smul_sum, ← finset_sum_comp] - rw [positionOperatorSqr_eq d ε, sub_comp, smul_comp] + rw [positionOperatorSqr_eq ε, sub_comp, smul_comp] unfold kroneckerDelta ext ψ x @@ -554,7 +523,7 @@ private lemma xL_Lx_eq {d : ℕ} (ε : ℝˣ) (i : Fin d) : ∑ j, (𝐱[j] ∘L 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, + Complex.ofReal_pow, id_comp, 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] @@ -703,7 +672,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 +693,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] From 097946616d3f6864d447968e66d6fe871a2168f3 Mon Sep 17 00:00:00 2001 From: gloges Date: Mon, 16 Mar 2026 01:41:27 +0900 Subject: [PATCH 07/15] Lp golf --- .../DDimensions/Operators/Commutation.lean | 55 ++++++------------- 1 file changed, 17 insertions(+), 38 deletions(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean index 0f15627cd..7bdc89e5b 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean @@ -295,50 +295,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] - sorry +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 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 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] @[simp] -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 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 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 {d : ℕ} : +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] /-! From 7fe800d3f88eb70b05afd6085d2a5f2b7df6ed85 Mon Sep 17 00:00:00 2001 From: gloges Date: Mon, 16 Mar 2026 01:54:48 +0900 Subject: [PATCH 08/15] lrl temp fix --- .../Hydrogen/LaplaceRungeLenzVector.lean | 36 ++----------------- 1 file changed, 2 insertions(+), 34 deletions(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean b/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean index cbe164b5f..2c5d83efa 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean @@ -53,44 +53,12 @@ lemma lrlOperator_eq (ε : ℝˣ) (i : Fin H.d) : /-- `𝐀(ε)ᵢ = 𝐋ᵢⱼ𝐩ⱼ + ½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 + sorry /-- `𝐀(ε)ᵢ = 𝐩ⱼ𝐋ᵢⱼ - ½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] - ring + sorry /-- The operator `𝐱ᵢ𝐩ᵢ` on Schwartz maps. -/ private def positionDotMomentum {d} := ∑ i : Fin d, 𝐱[i] ∘L 𝐩[i] From 001bb285d99a6c957fba79dd3ec8eb26f9e83b3e Mon Sep 17 00:00:00 2001 From: gloges Date: Mon, 16 Mar 2026 02:30:41 +0900 Subject: [PATCH 09/15] lint fixes --- .../DDimensions/Hydrogen/LaplaceRungeLenzVector.lean | 6 ++++++ .../QuantumMechanics/DDimensions/Operators/Commutation.lean | 1 + 2 files changed, 7 insertions(+) diff --git a/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean b/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean index 2c5d83efa..9e44940d6 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean @@ -45,17 +45,20 @@ def lrlOperatorSqr (ε : ℝˣ) : 𝓢(Space H.d, ℂ) →L[ℂ] 𝓢(Space H.d, ∑ i, (H.lrlOperator ε i) ∘L (H.lrlOperator ε i) /-- `𝐀(ε)ᵢ = 𝐱ᵢ𝐩² - (𝐱ⱼ𝐩ⱼ)𝐩ᵢ + ½iℏ(d-1)𝐩ᵢ - mk·𝐫(ε)⁻¹𝐱ᵢ` -/ +@[sorryful] 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 sorry /-- `𝐀(ε)ᵢ = 𝐋ᵢⱼ𝐩ⱼ + ½iℏ(d-1)𝐩ᵢ - mk·𝐫(ε)⁻¹𝐱ᵢ` -/ +@[sorryful] 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 sorry /-- `𝐀(ε)ᵢ = 𝐩ⱼ𝐋ᵢⱼ - ½iℏ(d-1)𝐩ᵢ - mk·𝐫(ε)⁻¹𝐱ᵢ` -/ +@[sorryful] 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 sorry @@ -335,6 +338,7 @@ private lemma constRadiusRegInvCompPosition_comm_constRadiusRegInvCompPosition simp only [comp_zero, zero_comp, add_zero, neg_zero, smul_zero] /-- `⁅𝐀(ε)ᵢ, 𝐀(ε)ⱼ⁆ = -iℏ 2m 𝐇(ε)𝐋ᵢⱼ` -/ +@[sorryful] lemma lrl_commutation_lrl (ε : ℝˣ) (i j : Fin H.d) : ⁅H.lrlOperator ε i, H.lrlOperator ε j⁆ = (-2 * Complex.I * ℏ * H.m) • (H.hamiltonianReg ε) ∘L 𝐋[i,j] := by repeat rw [lrlOperator_eq] @@ -498,6 +502,7 @@ private lemma xL_Lx_eq {d : ℕ} (ε : ℝˣ) (i : Fin d) : ∑ j, (𝐱[j] ∘L ring /-- `⁅𝐇(ε), 𝐀(ε)ᵢ⁆ = iℏkε²(¾𝐫(ε)⁻⁵(𝐱ⱼ𝐋ᵢⱼ + 𝐋ᵢⱼ𝐱ⱼ) + 3iℏ/2 𝐫(ε)⁻⁵𝐱ᵢ + 𝐫(ε)⁻³𝐩ᵢ)` -/ +@[sorryful] lemma hamiltonianReg_commutation_lrl (ε : ℝˣ) (i : Fin H.d) : ⁅H.hamiltonianReg ε, H.lrlOperator ε i⁆ = (Complex.I * ℏ * H.k * ε.1 ^ 2) • ((3 * 4⁻¹ : ℝ) • 𝐫[ε,-5] ∘L ∑ j, (𝐱[j] ∘L 𝐋[i,j] + 𝐋[i,j] ∘L 𝐱[j]) @@ -698,6 +703,7 @@ private lemma sum_rxrx (d : ℕ) (ε : ℝˣ) : ∑ i, 𝐫[d,ε,-1] ∘L 𝐱[i /-- The square of the (regularized) LRL vector operator is related to the (regularized) Hamiltonian `𝐇(ε)` of the hydrogen atom, square of the angular momentum `𝐋²` and powers of `𝐫(ε)` as `𝐀(ε)² = 2m 𝐇(ε)(𝐋² + ¼ℏ²(d-1)²) + m²k² - m²k²ε²𝐫(ε)⁻² + mkε²𝐫(ε)⁻³(𝐋² + ¼ℏ²(d-1)(d-3))`. -/ +@[sorryful] lemma lrlOperatorSqr_eq (ε : ℝˣ) : H.lrlOperatorSqr ε = (2 * H.m) • (H.hamiltonianReg ε) ∘L (𝐋² + (4⁻¹ * ℏ ^ 2 * (H.d - 1) ^ 2 : ℝ) • ContinuousLinearMap.id ℂ 𝓢(Space H.d, ℂ)) diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean index 7bdc89e5b..86617a716 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean @@ -325,6 +325,7 @@ lemma angularMomentumSqr_commutation_momentumSqr : -/ +@[sorryful] 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 From d18826f20f09e95ee595f4fa022905c89d4f6a32 Mon Sep 17 00:00:00 2001 From: gloges Date: Mon, 16 Mar 2026 16:20:23 +0900 Subject: [PATCH 10/15] lrlOperator_eq fixed --- .../Hydrogen/LaplaceRungeLenzVector.lean | 53 ++++++++++++++----- 1 file changed, 40 insertions(+), 13 deletions(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean b/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean index 9e44940d6..61b9f6704 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 @@ -45,23 +45,53 @@ def lrlOperatorSqr (ε : ℝˣ) : 𝓢(Space H.d, ℂ) →L[ℂ] 𝓢(Space H.d, ∑ i, (H.lrlOperator ε i) ∘L (H.lrlOperator ε i) /-- `𝐀(ε)ᵢ = 𝐱ᵢ𝐩² - (𝐱ⱼ𝐩ⱼ)𝐩ᵢ + ½iℏ(d-1)𝐩ᵢ - mk·𝐫(ε)⁻¹𝐱ᵢ` -/ -@[sorryful] 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 - sorry + + (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·𝐫(ε)⁻¹𝐱ᵢ` -/ -@[sorryful] 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 - sorry + + (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·𝐫(ε)⁻¹𝐱ᵢ` -/ -@[sorryful] 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 - sorry + - (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. -/ private def positionDotMomentum {d} := ∑ i : Fin d, 𝐱[i] ∘L 𝐩[i] @@ -338,7 +368,6 @@ private lemma constRadiusRegInvCompPosition_comm_constRadiusRegInvCompPosition simp only [comp_zero, zero_comp, add_zero, neg_zero, smul_zero] /-- `⁅𝐀(ε)ᵢ, 𝐀(ε)ⱼ⁆ = -iℏ 2m 𝐇(ε)𝐋ᵢⱼ` -/ -@[sorryful] lemma lrl_commutation_lrl (ε : ℝˣ) (i j : Fin H.d) : ⁅H.lrlOperator ε i, H.lrlOperator ε j⁆ = (-2 * Complex.I * ℏ * H.m) • (H.hamiltonianReg ε) ∘L 𝐋[i,j] := by repeat rw [lrlOperator_eq] @@ -502,7 +531,6 @@ private lemma xL_Lx_eq {d : ℕ} (ε : ℝˣ) (i : Fin d) : ∑ j, (𝐱[j] ∘L ring /-- `⁅𝐇(ε), 𝐀(ε)ᵢ⁆ = iℏkε²(¾𝐫(ε)⁻⁵(𝐱ⱼ𝐋ᵢⱼ + 𝐋ᵢⱼ𝐱ⱼ) + 3iℏ/2 𝐫(ε)⁻⁵𝐱ᵢ + 𝐫(ε)⁻³𝐩ᵢ)` -/ -@[sorryful] lemma hamiltonianReg_commutation_lrl (ε : ℝˣ) (i : Fin H.d) : ⁅H.hamiltonianReg ε, H.lrlOperator ε i⁆ = (Complex.I * ℏ * H.k * ε.1 ^ 2) • ((3 * 4⁻¹ : ℝ) • 𝐫[ε,-5] ∘L ∑ j, (𝐱[j] ∘L 𝐋[i,j] + 𝐋[i,j] ∘L 𝐱[j]) @@ -703,7 +731,6 @@ private lemma sum_rxrx (d : ℕ) (ε : ℝˣ) : ∑ i, 𝐫[d,ε,-1] ∘L 𝐱[i /-- The square of the (regularized) LRL vector operator is related to the (regularized) Hamiltonian `𝐇(ε)` of the hydrogen atom, square of the angular momentum `𝐋²` and powers of `𝐫(ε)` as `𝐀(ε)² = 2m 𝐇(ε)(𝐋² + ¼ℏ²(d-1)²) + m²k² - m²k²ε²𝐫(ε)⁻² + mkε²𝐫(ε)⁻³(𝐋² + ¼ℏ²(d-1)(d-3))`. -/ -@[sorryful] lemma lrlOperatorSqr_eq (ε : ℝˣ) : H.lrlOperatorSqr ε = (2 * H.m) • (H.hamiltonianReg ε) ∘L (𝐋² + (4⁻¹ * ℏ ^ 2 * (H.d - 1) ^ 2 : ℝ) • ContinuousLinearMap.id ℂ 𝓢(Space H.d, ℂ)) From 8dfc943258a91f6121bea548f6b68557436a80f0 Mon Sep 17 00:00:00 2001 From: gloges Date: Tue, 17 Mar 2026 13:50:51 +0900 Subject: [PATCH 11/15] lint fix --- .../DDimensions/Hydrogen/LaplaceRungeLenzVector.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean b/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean index 61b9f6704..c474bfb6c 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean @@ -531,6 +531,7 @@ private lemma xL_Lx_eq {d : ℕ} (ε : ℝˣ) (i : Fin d) : ∑ j, (𝐱[j] ∘L ring /-- `⁅𝐇(ε), 𝐀(ε)ᵢ⁆ = iℏkε²(¾𝐫(ε)⁻⁵(𝐱ⱼ𝐋ᵢⱼ + 𝐋ᵢⱼ𝐱ⱼ) + 3iℏ/2 𝐫(ε)⁻⁵𝐱ᵢ + 𝐫(ε)⁻³𝐩ᵢ)` -/ +@[sorryful] lemma hamiltonianReg_commutation_lrl (ε : ℝˣ) (i : Fin H.d) : ⁅H.hamiltonianReg ε, H.lrlOperator ε i⁆ = (Complex.I * ℏ * H.k * ε.1 ^ 2) • ((3 * 4⁻¹ : ℝ) • 𝐫[ε,-5] ∘L ∑ j, (𝐱[j] ∘L 𝐋[i,j] + 𝐋[i,j] ∘L 𝐱[j]) From 81351a07c07dd7118623a80ea524fde6836cb5c0 Mon Sep 17 00:00:00 2001 From: gloges Date: Tue, 17 Mar 2026 16:15:57 +0900 Subject: [PATCH 12/15] remove sorries --- .../Hydrogen/LaplaceRungeLenzVector.lean | 47 ++++++++++--------- 1 file changed, 24 insertions(+), 23 deletions(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean b/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean index c474bfb6c..f13223592 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Hydrogen/LaplaceRungeLenzVector.lean @@ -496,42 +496,43 @@ 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 - sorry + 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 - sorry + 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 ε, 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, id_comp, 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 𝐫(ε)⁻⁵𝐱ᵢ + 𝐫(ε)⁻³𝐩ᵢ)` -/ -@[sorryful] lemma hamiltonianReg_commutation_lrl (ε : ℝˣ) (i : Fin H.d) : ⁅H.hamiltonianReg ε, H.lrlOperator ε i⁆ = (Complex.I * ℏ * H.k * ε.1 ^ 2) • ((3 * 4⁻¹ : ℝ) • 𝐫[ε,-5] ∘L ∑ j, (𝐱[j] ∘L 𝐋[i,j] + 𝐋[i,j] ∘L 𝐱[j]) From 98d2d985cc6266a7b2c00c2ab5c0a96a1d995205 Mon Sep 17 00:00:00 2001 From: gloges Date: Sun, 22 Mar 2026 15:19:55 +0900 Subject: [PATCH 13/15] rp golf --- .../DDimensions/Operators/Commutation.lean | 54 ++++++------------- 1 file changed, 15 insertions(+), 39 deletions(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean index 86617a716..4cd708985 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean @@ -63,10 +63,6 @@ variable {d : ℕ} (i j k l : Fin d) (ε : ℝˣ) (s t : ℝ) -/ -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 (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] @@ -185,44 +181,24 @@ lemma position_commutation_momentumSqr : ⁅𝐱[i], 𝐩²⁆ = (2 * I * ℏ) lemma radiusRegPow_commutation_momentum : ⁅𝐫[d,ε,s], 𝐩[i]⁆ = (s * I * ℏ) • 𝐫[ε,s-2] ∘L 𝐱[i] := by - dsimp only [Bracket.bracket] 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 + 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 From d5280c8c1ca1bcf2d8781dcbe19defce097c6322 Mon Sep 17 00:00:00 2001 From: gloges Date: Sun, 22 Mar 2026 15:49:34 +0900 Subject: [PATCH 14/15] lint fix --- PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean index 4cd708985..27d01a12f 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean @@ -319,7 +319,6 @@ lemma angularMomentum_commutation_angularMomentum {d : ℕ} (i j k l : Fin d) : ring_nf sorry -@[sorryful] lemma angularMomentumSqr_commutation_angularMomentum {d : ℕ} (i j : Fin d) : ⁅angularMomentumOperatorSqr (d := d), 𝐋[i,j]⁆ = 0 := by sorry From 8bd5f91ffa0349efbc951af62977ae711f95f8e7 Mon Sep 17 00:00:00 2001 From: gloges Date: Sun, 22 Mar 2026 16:06:20 +0900 Subject: [PATCH 15/15] LL sorryfree --- .../DDimensions/Operators/Commutation.lean | 29 +++++++------------ 1 file changed, 11 insertions(+), 18 deletions(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean index a97642034..79b1fd729 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Commutation.lean @@ -301,23 +301,17 @@ lemma angularMomentumSqr_commutation_momentumSqr : -/ -@[sorryful] -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] - ring_nf - sorry + 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) : ∑ x : Fin d, 𝐋[x,a] ∘L 𝐋[b,x] = ∑ x : Fin d, 𝐋[a,x] ∘L 𝐋[x,b] := by @@ -334,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