diff --git a/PhysLean/Mathematics/SpecialFunctions/PhyscisistsHermite.lean b/PhysLean/Mathematics/SpecialFunctions/PhyscisistsHermite.lean index 6d5f2f36..f286aaed 100644 --- a/PhysLean/Mathematics/SpecialFunctions/PhyscisistsHermite.lean +++ b/PhysLean/Mathematics/SpecialFunctions/PhyscisistsHermite.lean @@ -146,7 +146,7 @@ noncomputable def physHermiteFun (n : ℕ) : ℝ → ℝ := fun x => aeval x (ph lemma physHermiteFun_zero_apply (x : ℝ) : physHermiteFun 0 x = 1 := by simp [physHermiteFun, aeval] -lemma physHermiteFun_pow (n m : ℕ) (x : ℝ) : +lemma physHermiteFun_pow (n m : ℕ) (x : ℝ) : physHermiteFun n x ^ m = aeval x (physHermite n ^ m) := by simp [physHermiteFun] @@ -455,7 +455,7 @@ lemma physHermiteFun_norm_cons (n : ℕ) (c : ℝ) : (fun x => physHermiteFun n x * physHermiteFun n x * Real.exp (-x ^ 2)) c] rw [physHermiteFun_norm] -lemma polynomial_mem_physHermiteFun_span_induction (P : Polynomial ℤ) : (n : ℕ) → +lemma polynomial_mem_physHermiteFun_span_induction (P : Polynomial ℤ) : (n : ℕ) → (hn : P.natDegree = n) → (fun x => P.aeval x) ∈ Submodule.span ℝ (Set.range physHermiteFun) | 0, h => by @@ -481,8 +481,10 @@ lemma polynomial_mem_physHermiteFun_span_induction (P : Polynomial ℤ) : (n : exact Submodule.zero_mem (Submodule.span ℝ (Set.range physHermiteFun)) · exact polynomial_mem_physHermiteFun_span_induction P' P'.natDegree (by rfl) simp only [P'] at hP'mem - have hl : (fun x => (aeval x) ((physHermite (n + 1)).coeff (n + 1) • P - P.coeff (n + 1) • physHermite (n + 1))) - = (2 ^ (n + 1) : ℝ) • (fun (x : ℝ) => (aeval x) P) - ↑(P.coeff (n + 1) : ℝ) • (fun (x : ℝ)=> (aeval x) (physHermite (n + 1)) ):= by + have hl : (fun x => (aeval x) ((physHermite (n + 1)).coeff (n + 1) • P - + P.coeff (n + 1) • physHermite (n + 1))) + = (2 ^ (n + 1) : ℝ) • (fun (x : ℝ) => (aeval x) P) - ↑(P.coeff (n + 1) : ℝ) • + (fun (x : ℝ)=> (aeval x) (physHermite (n + 1))) := by funext x simp simp [aeval] @@ -500,7 +502,7 @@ decreasing_by rw [Polynomial.natDegree_lt_iff_degree_lt] apply (Polynomial.degree_lt_iff_coeff_zero _ _).mpr intro m hm' - simp only [coeff_physHermite_self_succ, Int.cast_pow, Int.cast_ofNat, coeff_sub, + simp only [coeff_physHermite_self_succ, Int.cast_pow, Int.cast_ofNat, coeff_sub, Int.cast_id] change n + 1 ≤ m at hm' rw [coeff_smul, coeff_smul] @@ -526,7 +528,7 @@ lemma polynomial_mem_physHermiteFun_span (P : Polynomial ℤ) : lemma cos_mem_physHermiteFun_span_topologicalClosure (c : ℝ) : (fun (x : ℝ) => Real.cos (c * x)) ∈ (Submodule.span ℝ (Set.range physHermiteFun)).topologicalClosure := by - change (fun (x : ℝ) => Real.cos (c * x)) ∈ + change (fun (x : ℝ) => Real.cos (c * x)) ∈ closure (Submodule.span ℝ (Set.range physHermiteFun)) have h1 := Real.hasSum_cos simp [HasSum] at h1 @@ -536,8 +538,8 @@ lemma cos_mem_physHermiteFun_span_topologicalClosure (c : ℝ) : exact tendsto_pi_nhds.mpr fun x => h1 (c * x) have h2 (z : Finset ℕ) : (fun y => ∑ x ∈ z, (-1) ^ x * (c * y) ^ (2 * x) / ↑(2 * x)!) ∈ ↑(Submodule.span ℝ (Set.range physHermiteFun)) := by - have h0 : (fun y => ∑ x ∈ z, (-1) ^ x * (c * y) ^ (2 * x) / ↑(2 * x)!) = - ∑ x ∈ z, (((-1) ^ x * c ^ (2 * x) / ↑(2 * x)!) • fun (y : ℝ) => (y) ^ (2 * x) ) := by + have h0 : (fun y => ∑ x ∈ z, (-1) ^ x * (c * y) ^ (2 * x) / ↑(2 * x)!) = + ∑ x ∈ z, (((-1) ^ x * c ^ (2 * x) / ↑(2 * x)!) • fun (y : ℝ) => (y) ^ (2 * x)) := by funext y simp congr @@ -556,6 +558,4 @@ lemma cos_mem_physHermiteFun_span_topologicalClosure (c : ℝ) : refine mem_closure_of_tendsto h1 ?_ simp [h2] - - end PhysLean diff --git a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean index d6b9fb7b..e08e677e 100644 --- a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean +++ b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean @@ -54,9 +54,14 @@ namespace QuantumMechanics namespace OneDimension +/-- A quantum harmonic oscillator specified by a mass, a value of Plancck's and + an angular frequency. -/ structure HarmonicOscillator where + /-- The mass of the particle. -/ m : ℝ + /-- Reduced Planck's constant. -/ ℏ : ℝ + /-- The angular frequency of the harmonic oscillator. -/ ω : ℝ hℏ : 0 < ℏ hω : 0 < ω @@ -76,7 +81,7 @@ lemma m_mul_ω_div_two_ℏ_pos : 0 < Q.m * Q.ω / (2 * Q.ℏ) := by exact mul_pos (by norm_num) Q.hℏ @[simp] -lemma m_mul_ω_div_ℏ_pos : 0 < Q.m * Q.ω / Q.ℏ := by +lemma m_mul_ω_div_ℏ_pos : 0 < Q.m * Q.ω / Q.ℏ := by apply div_pos exact mul_pos Q.hm Q.hω exact Q.hℏ @@ -93,7 +98,7 @@ lemma ℏ_ne_zero : Q.ℏ ≠ 0 := by The prime `'` in the name is to signify that this is not defined on equivalence classes of square integrable functions. -/ -noncomputable def schrodingerOperator (ψ : ℝ → ℂ) : ℝ → ℂ := +noncomputable def schrodingerOperator (ψ : ℝ → ℂ) : ℝ → ℂ := fun y => - Q.ℏ ^ 2 / (2 * Q.m) * (deriv (deriv ψ) y) + 1/2 * Q.m * Q.ω^2 * y^2 * ψ y end HarmonicOscillator diff --git a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean index 65e65a2c..d6bf5ec3 100644 --- a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean +++ b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean @@ -55,9 +55,9 @@ lemma mul_eigenfunction_integrable (f : ℝ → ℂ) (hf : MemHS f) : lemma mul_physHermiteFun_integrable (f : ℝ → ℂ) (hf : MemHS f) (n : ℕ) : MeasureTheory.Integrable (fun x => (physHermiteFun n (√(Q.m * Q.ω / Q.ℏ) * x)) * (f x * ↑(Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ))))) := by - have h2 : (1 / ↑√(2 ^ n * ↑n !) * ↑√√(Q.m * Q.ω / (Real.pi * Q.ℏ)) : ℂ) • (fun (x : ℝ ) => + have h2 : (1 / ↑√(2 ^ n * ↑n !) * ↑√√(Q.m * Q.ω / (Real.pi * Q.ℏ)) : ℂ) • (fun (x : ℝ) => (physHermiteFun n (√(Q.m * Q.ω / Q.ℏ) * x) * - (f x * Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ))))) = fun x => + (f x * Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ))))) = fun x => Q.eigenfunction n x * f x := by funext x simp [eigenfunction_eq] @@ -75,13 +75,15 @@ lemma mul_physHermiteFun_integrable (f : ℝ → ℂ) (hf : MemHS f) (n : ℕ) : · apply mul_pos Real.pi_pos Q.hℏ lemma mul_polynomial_integrable (f : ℝ → ℂ) (hf : MemHS f) (P : Polynomial ℤ) : - MeasureTheory.Integrable (fun x => ((fun x => P.aeval x) (√(Q.m * Q.ω / Q.ℏ) * x)) * + MeasureTheory.Integrable (fun x => ((fun x => P.aeval x) (√(Q.m * Q.ω / Q.ℏ) * x)) * (f x * Real.exp (- Q.m * Q.ω * x^2 / (2 * Q.ℏ)))) volume := by have h1 := polynomial_mem_physHermiteFun_span P rw [Finsupp.mem_span_range_iff_exists_finsupp] at h1 obtain ⟨a, ha⟩ := h1 - have h2 : (fun x => ↑((fun x => P.aeval x) (√(Q.m * Q.ω / Q.ℏ) * x)) * (f x * ↑(Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ))))) - = (fun x => ∑ r ∈ a.support, a r * (physHermiteFun r (√(Q.m * Q.ω / Q.ℏ) * x)) * (f x * Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ)))) := by + have h2 : (fun x => ↑((fun x => P.aeval x) (√(Q.m * Q.ω / Q.ℏ) * x)) * + (f x * ↑(Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ))))) + = (fun x => ∑ r ∈ a.support, a r * (physHermiteFun r (√(Q.m * Q.ω / Q.ℏ) * x)) * + (f x * Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ)))) := by funext x rw [← ha] rw [← Finset.sum_mul] @@ -93,7 +95,8 @@ lemma mul_polynomial_integrable (f : ℝ → ℂ) (hf : MemHS f) (P : Polynomial intro i hi simp only [mul_assoc] have hf' : (fun a_1 => - ↑(a i) * (↑(physHermiteFun i (√(Q.m * Q.ω / Q.ℏ) * a_1)) * (f a_1 * ↑(Real.exp (- Q.m * (Q.ω * a_1 ^ 2) / (2 * Q.ℏ)))))) + ↑(a i) * (↑(physHermiteFun i (√(Q.m * Q.ω / Q.ℏ) * a_1)) * + (f a_1 * ↑(Real.exp (- Q.m * (Q.ω * a_1 ^ 2) / (2 * Q.ℏ)))))) = fun x => (a i) • ((physHermiteFun i (√(Q.m * Q.ω / Q.ℏ) * x)) * (f x * ↑(Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ))))) := by funext x @@ -104,14 +107,16 @@ lemma mul_polynomial_integrable (f : ℝ → ℂ) (hf : MemHS f) (P : Polynomial apply MeasureTheory.Integrable.smul exact Q.mul_physHermiteFun_integrable f hf i -lemma mul_power_integrable (f : ℝ → ℂ) (hf : MemHS f) (r : ℕ) : +lemma mul_power_integrable (f : ℝ → ℂ) (hf : MemHS f) (r : ℕ) : MeasureTheory.Integrable (fun x => x ^ r * (f x * Real.exp (- Q.m * Q.ω * x^2 / (2 * Q.ℏ)))) volume := by by_cases hr : r ≠ 0 - · have h1 := Q.mul_polynomial_integrable f hf (Polynomial.X ^ r) + · have h1 := Q.mul_polynomial_integrable f hf (Polynomial.X ^ r) simp at h1 - have h2 : (fun x => (↑√(Q.m * Q.ω / Q.ℏ) * ↑x) ^ r * (f x * Complex.exp (-(↑Q.m * ↑Q.ω * ↑x ^ 2) / (2 * ↑Q.ℏ)))) - = (↑√(Q.m * Q.ω / Q.ℏ) : ℂ) ^ r • (fun x => (↑x ^r * (f x * Real.exp (-(↑Q.m * ↑Q.ω * ↑x ^ 2) / (2 * ↑Q.ℏ))))) := by + have h2 : (fun x => (↑√(Q.m * Q.ω / Q.ℏ) * ↑x) ^ r * + (f x * Complex.exp (-(↑Q.m * ↑Q.ω * ↑x ^ 2) / (2 * ↑Q.ℏ)))) + = (↑√(Q.m * Q.ω / Q.ℏ) : ℂ) ^ r • (fun x => (↑x ^r * + (f x * Real.exp (-(↑Q.m * ↑Q.ω * ↑x ^ 2) / (2 * ↑Q.ℏ))))) := by funext x simp ring @@ -119,7 +124,7 @@ lemma mul_power_integrable (f : ℝ → ℂ) (hf : MemHS f) (r : ℕ) : rw [IsUnit.integrable_smul_iff] at h1 simpa using h1 simp - have h1 : √(Q.m * Q.ω / Q.ℏ) ≠ 0 := by + have h1 : √(Q.m * Q.ω / Q.ℏ) ≠ 0 := by refine Real.sqrt_ne_zero'.mpr ?_ refine div_pos ?_ ?_ · exact mul_pos Q.hm Q.hω @@ -127,7 +132,7 @@ lemma mul_power_integrable (f : ℝ → ℂ) (hf : MemHS f) (r : ℕ) : simp [h1] · simp at hr subst hr - simpa using Q.mul_physHermiteFun_integrable f hf 0 + simpa using Q.mul_physHermiteFun_integrable f hf 0 /-! @@ -136,7 +141,7 @@ lemma mul_power_integrable (f : ℝ → ℂ) (hf : MemHS f) (r : ℕ) : -/ lemma orthogonal_eigenfunction_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f) - (hOrth : ∀ n : ℕ, ⟪HilbertSpace.mk (Q.eigenfunction_memHS n) , HilbertSpace.mk hf⟫_ℂ = 0) + (hOrth : ∀ n : ℕ, ⟪HilbertSpace.mk (Q.eigenfunction_memHS n), HilbertSpace.mk hf⟫_ℂ = 0) (n : ℕ) : ∫ (x : ℝ), Q.eigenfunction n x * f x = 0 := by rw [← hOrth n] rw [inner_mk_mk] @@ -150,14 +155,16 @@ local notation "hℏ" => Q.hℏ local notation "hω" => Q.hω lemma orthogonal_physHermiteFun_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f) - (hOrth : ∀ n : ℕ, ⟪HilbertSpace.mk (Q.eigenfunction_memHS n) , HilbertSpace.mk hf⟫_ℂ = 0) + (hOrth : ∀ n : ℕ, ⟪HilbertSpace.mk (Q.eigenfunction_memHS n), HilbertSpace.mk hf⟫_ℂ = 0) (n : ℕ) : - ∫ (x : ℝ), (physHermiteFun n (√(Q.m * Q.ω / Q.ℏ) * x)) * (f x * ↑(Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ)))) + ∫ (x : ℝ), (physHermiteFun n (√(Q.m * Q.ω / Q.ℏ) * x)) * + (f x * ↑(Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ)))) = 0 := by have h1 := Q.orthogonal_eigenfunction_of_mem_orthogonal f hf hOrth n - have h2 : (fun (x : ℝ ) => + have h2 : (fun (x : ℝ) => (1 / ↑√(2 ^ n * ↑n !) * ↑√√(Q.m * Q.ω / (Real.pi * Q.ℏ)) : ℂ) * - (physHermiteFun n (√(Q.m * Q.ω / Q.ℏ) * x) * f x * Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ)))) + (physHermiteFun n (√(Q.m * Q.ω / Q.ℏ) * x) * f x * + Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ)))) = fun x => Q.eigenfunction n x * f x := by funext x simp [eigenfunction_eq] @@ -180,16 +187,18 @@ lemma orthogonal_physHermiteFun_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS simp ring -lemma orthogonal_polynomial_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f) - (hOrth : ∀ n : ℕ, ⟪HilbertSpace.mk (Q.eigenfunction_memHS n) , HilbertSpace.mk hf⟫_ℂ = 0) +lemma orthogonal_polynomial_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f) + (hOrth : ∀ n : ℕ, ⟪HilbertSpace.mk (Q.eigenfunction_memHS n), HilbertSpace.mk hf⟫_ℂ = 0) (P : Polynomial ℤ) : - ∫ x : ℝ, ((fun x => P.aeval x) (√(m * ω / ℏ) * x)) * + ∫ x : ℝ, ((fun x => P.aeval x) (√(m * ω / ℏ) * x)) * (f x * Real.exp (- m * ω * x^2 / (2 * ℏ))) = 0 := by have h1 := polynomial_mem_physHermiteFun_span P rw [Finsupp.mem_span_range_iff_exists_finsupp] at h1 obtain ⟨a, ha⟩ := h1 - have h2 : (fun x => ↑((fun x => P.aeval x) (√(m * ω / ℏ) * x)) * (f x * ↑(Real.exp (-m * ω * x ^ 2 / (2 * ℏ))))) - = (fun x => ∑ r ∈ a.support, a r * (physHermiteFun r (√(m * ω / ℏ) * x)) * (f x * Real.exp (-m * ω * x ^ 2 / (2 * ℏ)))) := by + have h2 : (fun x => ↑((fun x => P.aeval x) (√(m * ω / ℏ) * x)) * + (f x * ↑(Real.exp (-m * ω * x ^ 2 / (2 * ℏ))))) + = (fun x => ∑ r ∈ a.support, a r * (physHermiteFun r (√(m * ω / ℏ) * x)) * + (f x * Real.exp (-m * ω * x ^ 2 / (2 * ℏ)))) := by funext x rw [← ha] rw [← Finset.sum_mul] @@ -214,25 +223,28 @@ lemma orthogonal_polynomial_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f) ring · /- Integrablility -/ intro i hi - have hf' : - (fun x => ↑(a i) * ↑(physHermiteFun i (√(m * ω / ℏ) * x)) * (f x * ↑(Real.exp (-m * ω * x ^ 2 / (2 * ℏ))))) - = a i • (fun x => (physHermiteFun i (√(m * ω / ℏ) * x)) * (f x * ↑(Real.exp (-m * ω * x ^ 2 / (2 * ℏ))))) := by - funext x - simp - ring + have hf' : (fun x => ↑(a i) * ↑(physHermiteFun i (√(m * ω / ℏ) * x)) * + (f x * ↑(Real.exp (-m * ω * x ^ 2 / (2 * ℏ))))) + = a i • (fun x => (physHermiteFun i (√(m * ω / ℏ) * x)) * + (f x * ↑(Real.exp (-m * ω * x ^ 2 / (2 * ℏ))))) := by + funext x + simp + ring rw [hf'] apply Integrable.smul exact Q.mul_physHermiteFun_integrable f hf i lemma orthogonal_power_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f) - (hOrth : ∀ n : ℕ, ⟪HilbertSpace.mk (Q.eigenfunction_memHS n) , HilbertSpace.mk hf⟫_ℂ = 0) + (hOrth : ∀ n : ℕ, ⟪HilbertSpace.mk (Q.eigenfunction_memHS n), HilbertSpace.mk hf⟫_ℂ = 0) (r : ℕ) : ∫ x : ℝ, (x ^ r * (f x * Real.exp (- m * ω * x^2 / (2 * ℏ)))) = 0 := by by_cases hr : r ≠ 0 · have h1 := Q.orthogonal_polynomial_of_mem_orthogonal f hf hOrth (Polynomial.X ^ r) simp at h1 - have h2 : (fun x => (↑√(m * ω / ℏ) * ↑x) ^ r * (f x * Complex.exp (-(↑m * ↑ω * ↑x ^ 2) / (2 * ↑ℏ)))) - = (fun x => (↑√(m * ω / ℏ) : ℂ) ^ r * (↑x ^r * (f x * Complex.exp (-(↑m * ↑ω * ↑x ^ 2) / (2 * ↑ℏ))))) := by + have h2 : (fun x => (↑√(m * ω / ℏ) * ↑x) ^ r * + (f x * Complex.exp (-(↑m * ↑ω * ↑x ^ 2) / (2 * ↑ℏ)))) + = (fun x => (↑√(m * ω / ℏ) : ℂ) ^ r * (↑x ^r * + (f x * Complex.exp (-(↑m * ↑ω * ↑x ^ 2) / (2 * ↑ℏ))))) := by funext x ring rw [h2] at h1 @@ -262,14 +274,15 @@ lemma orthogonal_power_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f) open Finset lemma orthogonal_exp_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f) - (hOrth : ∀ n : ℕ, ⟪HilbertSpace.mk (Q.eigenfunction_memHS n) , HilbertSpace.mk hf⟫_ℂ = 0) - (c : ℝ) : - ∫ x : ℝ, Complex.exp (Complex.I * c * x) * (f x * Real.exp (- m * ω * x^2 / (2 * ℏ))) = 0 := by + (hOrth : ∀ n : ℕ, ⟪HilbertSpace.mk (Q.eigenfunction_memHS n), HilbertSpace.mk hf⟫_ℂ = 0) + (c : ℝ) : ∫ x : ℝ, Complex.exp (Complex.I * c * x) * + (f x * Real.exp (- m * ω * x^2 / (2 * ℏ))) = 0 := by /- Rewriting the intergrand as a limit. -/ - have h1 (y : ℝ) : Filter.Tendsto (fun n => ∑ r ∈ range n, + have h1 (y : ℝ) : Filter.Tendsto (fun n => ∑ r ∈ range n, (Complex.I * ↑c * ↑y) ^ r / r ! * (f y * Real.exp (- m * ω * y^2 / (2 * ℏ)))) - Filter.atTop (nhds (Complex.exp (Complex.I * c * y) * (f y * Real.exp (- m * ω * y^2 / (2 * ℏ))))) := by - have h11 : (fun n => ∑ r ∈ range n, + Filter.atTop (nhds (Complex.exp (Complex.I * c * y) * + (f y * Real.exp (- m * ω * y^2 / (2 * ℏ))))) := by + have h11 : (fun n => ∑ r ∈ range n, (Complex.I * ↑c * ↑y) ^ r / r ! * (f y * Real.exp (- m * ω * y^2 / (2 * ℏ)))) = fun n => (∑ r ∈ range n, @@ -278,8 +291,8 @@ lemma orthogonal_exp_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f) funext s simp [Finset.sum_mul] rw [h11] - have h12 : (Complex.exp (Complex.I * c * y) * (f y * Real.exp (- m * ω * y^2 / (2 * ℏ)))) - = ( Complex.exp (Complex.I * c * y)) * (f y * Real.exp (- m * ω * y^2 / (2 * ℏ))):= by + have h12 : (Complex.exp (Complex.I * c * y) * (f y * Real.exp (- m * ω * y^2 / (2 * ℏ)))) + = (Complex.exp (Complex.I * c * y)) * (f y * Real.exp (- m * ω * y^2 / (2 * ℏ))) := by simp rw [h12] apply Filter.Tendsto.mul_const @@ -291,15 +304,18 @@ lemma orthogonal_exp_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f) /- Rewritting the integral as a limit using dominated_convergence -/ have h1' : Filter.Tendsto (fun n => ∫ y : ℝ, ∑ r ∈ range n, (Complex.I * ↑c * ↑y) ^ r / r ! * (f y * Real.exp (- m * ω * y^2 / (2 * ℏ)))) - Filter.atTop (nhds (∫ y : ℝ, Complex.exp (Complex.I * c * y) * (f y * Real.exp (- m * ω * y^2 / (2 * ℏ))))) := by + Filter.atTop (nhds (∫ y : ℝ, Complex.exp (Complex.I * c * y) * + (f y * Real.exp (- m * ω * y^2 / (2 * ℏ))))) := by let bound : ℝ → ℝ := fun x => Real.exp (|c * x|) * Complex.abs (f x) * (Real.exp (-m * ω * x ^ 2 / (2 * ℏ))) apply MeasureTheory.tendsto_integral_of_dominated_convergence bound · intro n apply Finset.aestronglyMeasurable_sum intro r hr - have h1 : (fun a => (Complex.I * ↑c * ↑a) ^ r / ↑r ! * (f a * ↑(Real.exp (-m * ω * a ^ 2 / (2 * ℏ))))) - = fun a => (Complex.I * ↑c) ^ r / ↑r ! * (f a * Complex.ofReal (a ^ r * (Real.exp (-m * ω * a ^ 2 / (2 * ℏ))))) := by + have h1 : (fun a => (Complex.I * ↑c * ↑a) ^ r / ↑r ! * + (f a * ↑(Real.exp (-m * ω * a ^ 2 / (2 * ℏ))))) + = fun a => (Complex.I * ↑c) ^ r / ↑r ! * + (f a * Complex.ofReal (a ^ r * (Real.exp (-m * ω * a ^ 2 / (2 * ℏ))))) := by funext a simp ring @@ -309,25 +325,24 @@ lemma orthogonal_exp_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f) · exact aeStronglyMeasurable_of_memHS hf · apply MeasureTheory.Integrable.aestronglyMeasurable apply MeasureTheory.Integrable.ofReal - change Integrable (fun x => (x ^ r) * (Real.exp (-m * ω * x ^ 2 / (2 * ℏ)))) + change Integrable (fun x => (x ^ r) * (Real.exp (-m * ω * x ^ 2 / (2 * ℏ)))) have h1 : (fun x => (x ^ r)*(Real.exp (-m * ω * x ^ 2 / (2 * ℏ)))) = - (fun x => (Polynomial.X ^ r : Polynomial ℤ).aeval x * + (fun x => (Polynomial.X ^ r : Polynomial ℤ).aeval x * (Real.exp (- (m * ω / (2* ℏ)) * x ^ 2))) := by funext x - simp [neg_mul, mul_eq_mul_left_iff, Real.exp_eq_exp] + simp [neg_mul, mul_eq_mul_left_iff, Real.exp_eq_exp] left field_simp rw [h1] apply guassian_integrable_polynomial simp · /- Prove the bound is integrable. -/ - have hbound : bound = - (fun x => Real.exp |c * x| * Complex.abs (f x) * Real.exp (-(m * ω / (2 * ℏ)) * x ^ 2)) - := by - simp [bound] - funext x - congr - field_simp + have hbound : bound = (fun x => Real.exp |c * x| * Complex.abs (f x) * + Real.exp (-(m * ω / (2 * ℏ)) * x ^ 2)) := by + simp [bound] + funext x + congr + field_simp rw [hbound] apply HilbertSpace.exp_abs_mul_abs_mul_gaussian_integrable · exact hf @@ -359,7 +374,7 @@ lemma orthogonal_exp_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f) rw [_root_.mul_le_mul_right] · have h1 := Real.sum_le_exp_of_nonneg (x := |c * y|) (abs_nonneg (c * y)) n refine le_trans ?_ h1 - have h2 : Complex.abs (∑ i ∈ range n, (Complex.I * (↑c * ↑y)) ^ i / ↑i !) ≤ + have h2 : Complex.abs (∑ i ∈ range n, (Complex.I * (↑c * ↑y)) ^ i / ↑i !) ≤ ∑ i ∈ range n, Complex.abs ((Complex.I * (↑c * ↑y)) ^ i / ↑i !) := by exact AbsoluteValue.sum_le _ _ _ refine le_trans h2 ?_ @@ -370,20 +385,23 @@ lemma orthogonal_exp_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f) congr rw [abs_mul] · refine mul_pos ?_ ?_ - have h1 : 0 ≤ Complex.abs (f y) := by exact AbsoluteValue.nonneg Complex.abs (f y) + have h1 : 0 ≤ Complex.abs (f y) := by exact AbsoluteValue.nonneg Complex.abs (f y) apply lt_of_le_of_ne h1 (fun a => hf (id (Eq.symm a))) exact Real.exp_pos (-(m * ω * y ^ 2) / (2 * ℏ)) · apply Filter.Eventually.of_forall intro y exact h1 y - have h3b : (fun n => ∫ y : ℝ, ∑ r ∈ range n, - (Complex.I * ↑c * ↑y) ^ r / r ! * (f y * Real.exp (- m * ω * y^2 / (2 * ℏ)))) = fun (n : ℕ) => 0 := by + have h3b : (fun n => ∫ y : ℝ, ∑ r ∈ range n, + (Complex.I * ↑c * ↑y) ^ r / r ! * + (f y * Real.exp (- m * ω * y^2 / (2 * ℏ)))) = fun (n : ℕ) => 0 := by funext n rw [MeasureTheory.integral_finset_sum] · apply Finset.sum_eq_zero intro r hr - have hf' : (fun a => (Complex.I * ↑c * ↑a) ^ r / ↑r ! * (f a * ↑(Real.exp (-m * ω * a ^ 2 / (2 * ℏ))))) - = fun a => ((Complex.I * ↑c) ^ r / ↑r !) * (a^ r * (f a * ↑(Real.exp (-m * ω * a ^ 2 / (2 * ℏ))))) := by + have hf' : (fun a => (Complex.I * ↑c * ↑a) ^ r / ↑r ! * + (f a * ↑(Real.exp (-m * ω * a ^ 2 / (2 * ℏ))))) + = fun a => ((Complex.I * ↑c) ^ r / ↑r !) * + (a^ r * (f a * ↑(Real.exp (-m * ω * a ^ 2 / (2 * ℏ))))) := by funext a simp ring @@ -392,24 +410,25 @@ lemma orthogonal_exp_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f) rw [Q.orthogonal_power_of_mem_orthogonal f hf hOrth r] simp · intro r hr - have hf' : (fun a => (Complex.I * ↑c * ↑a) ^ r / ↑r ! * (f a * ↑(Real.exp (-m * ω * a ^ 2 / (2 * ℏ))))) - = ((Complex.I * ↑c) ^ r / ↑r !) • fun a => (a^ r * (f a * ↑(Real.exp (-m * ω * a ^ 2 / (2 * ℏ))))) := by + have hf' : (fun a => (Complex.I * ↑c * ↑a) ^ r / ↑r ! * + (f a * ↑(Real.exp (-m * ω * a ^ 2 / (2 * ℏ))))) + = ((Complex.I * ↑c) ^ r / ↑r !) • + fun a => (a^ r * (f a * ↑(Real.exp (-m * ω * a ^ 2 / (2 * ℏ))))) := by funext a simp ring rw [hf'] apply MeasureTheory.Integrable.smul - exact Q.mul_power_integrable f hf r + exact Q.mul_power_integrable f hf r rw [h3b] at h1' apply tendsto_nhds_unique h1' rw [tendsto_const_nhds_iff] +open FourierTransform MeasureTheory Real Lp Memℒp Filter Complex Topology + ComplexInnerProductSpace ComplexConjugate -open FourierTransform MeasureTheory Real Lp Memℒp Filter Complex Topology ComplexInnerProductSpace ComplexConjugate - - -lemma fourierIntegral_zero_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f) - (hOrth : ∀ n : ℕ, ⟪HilbertSpace.mk (Q.eigenfunction_memHS n) , HilbertSpace.mk hf⟫_ℂ = 0) : +lemma fourierIntegral_zero_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f) + (hOrth : ∀ n : ℕ, ⟪HilbertSpace.mk (Q.eigenfunction_memHS n), HilbertSpace.mk hf⟫_ℂ = 0) : 𝓕 (fun x => f x * Real.exp (- m * ω * x^2 / (2 * ℏ))) = 0 := by funext c rw [Real.fourierIntegral_eq] @@ -423,13 +442,13 @@ lemma fourierIntegral_zero_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f) congr 2 ring -lemma zero_of_orthogonal_mk (f : ℝ → ℂ) (hf : MemHS f) - (hOrth : ∀ n : ℕ, ⟪HilbertSpace.mk (Q.eigenfunction_memHS n) , HilbertSpace.mk hf⟫_ℂ = 0) +lemma zero_of_orthogonal_mk (f : ℝ → ℂ) (hf : MemHS f) + (hOrth : ∀ n : ℕ, ⟪HilbertSpace.mk (Q.eigenfunction_memHS n), HilbertSpace.mk hf⟫_ℂ = 0) (plancherel_theorem: ∀ {f : ℝ → ℂ} (hf : Integrable f volume) (_ : Memℒp f 2), - eLpNorm (𝓕 f) 2 volume = eLpNorm f 2 volume): + eLpNorm (𝓕 f) 2 volume = eLpNorm f 2 volume) : HilbertSpace.mk hf = 0 := by have hf' : (fun x => f x * ↑(rexp (-m * ω * x ^ 2 / (2 * ℏ)))) - = (fun x => f x * ↑(rexp (- (m * ω / (2 * ℏ)) * (x - 0) ^ 2 ))) := by + = (fun x => f x * ↑(rexp (- (m * ω / (2 * ℏ)) * (x - 0) ^ 2))) := by funext x simp left @@ -439,7 +458,7 @@ lemma zero_of_orthogonal_mk (f : ℝ → ℂ) (hf : MemHS f) rw [← plancherel_theorem] rw [Q.fourierIntegral_zero_of_mem_orthogonal f hf hOrth] simp - · /- f x * Real.exp (- m * ω * x^2 / (2 * ℏ)) is integrable -/ + · /- f x * Real.exp (- m * ω * x^2 / (2 * ℏ)) is integrable -/ rw [hf'] rw [← memℒp_one_iff_integrable] apply HilbertSpace.mul_gaussian_mem_Lp_one f hf (m * ω / (2 * ℏ)) 0 @@ -447,7 +466,7 @@ lemma zero_of_orthogonal_mk (f : ℝ → ℂ) (hf : MemHS f) · exact mul_pos hm hω · have h1 := Q.hℏ linarith - · /- f x * Real.exp (- m * ω * x^2 / (2 * ℏ)) is square-integrable -/ + · /- f x * Real.exp (- m * ω * x^2 / (2 * ℏ)) is square-integrable -/ rw [hf'] refine HilbertSpace.mul_gaussian_mem_Lp_two f hf (m * ω / (2 * ℏ)) 0 ?_ refine div_pos ?_ ?_ @@ -457,19 +476,17 @@ lemma zero_of_orthogonal_mk (f : ℝ → ℂ) (hf : MemHS f) refine (norm_eq_zero_iff (by simp)).mp ?_ simp [Norm.norm] have h2 : eLpNorm f 2 volume = 0 := by - rw [MeasureTheory.eLpNorm_eq_zero_iff] at h1 ⊢ + rw [MeasureTheory.eLpNorm_eq_zero_iff] at h1 ⊢ rw [Filter.eventuallyEq_iff_all_subsets] at h1 ⊢ - have h3 (x : ℝ) : f x * ↑(rexp (-m * ω * x ^ 2 / (2 * ℏ))) = 0 ↔ - f x = 0 := by simp - simp [h3] at h1 + simp at h1 exact h1 exact aeStronglyMeasurable_of_memHS hf simp - · /- f x * Real.exp (- m * ω * x^2 / (2 * ℏ)) is strongly measurable -/ + · /- f x * Real.exp (- m * ω * x^2 / (2 * ℏ)) is strongly measurable -/ rw [hf'] apply Integrable.aestronglyMeasurable rw [← memℒp_one_iff_integrable] - apply HilbertSpace.mul_gaussian_mem_Lp_one f hf (m * ω / (2 * ℏ)) 0 + apply HilbertSpace.mul_gaussian_mem_Lp_one f hf (m * ω / (2 * ℏ)) 0 refine div_pos ?_ ?_ · exact mul_pos hm hω · have h1 := Q.hℏ @@ -481,16 +498,18 @@ lemma zero_of_orthogonal_mk (f : ℝ → ℂ) (hf : MemHS f) lemma zero_of_orthogonal_eigenVector (f : HilbertSpace) (hOrth : ∀ n : ℕ, ⟪HilbertSpace.mk (Q.eigenfunction_memHS n), f⟫_ℂ = 0) (plancherel_theorem: ∀ {f : ℝ → ℂ} (hf : Integrable f volume) (_ : Memℒp f 2), - eLpNorm (𝓕 f) 2 volume = eLpNorm f 2 volume) : f = 0 := by + eLpNorm (𝓕 f) 2 volume = eLpNorm f 2 volume) : f = 0 := by obtain ⟨f, hf, rfl⟩ := HilbertSpace.mk_surjective f exact zero_of_orthogonal_mk Q f hf hOrth plancherel_theorem lemma completness_eigenvector (plancherel_theorem : ∀ {f : ℝ → ℂ} (hf : Integrable f volume) (_ : Memℒp f 2), - eLpNorm (𝓕 f) 2 volume = eLpNorm f 2 volume) : - (Submodule.span ℂ (Set.range (fun n => HilbertSpace.mk (Q.eigenfunction_memHS n)))).topologicalClosure = ⊤ := by + eLpNorm (𝓕 f) 2 volume = eLpNorm f 2 volume) : + (Submodule.span ℂ + (Set.range (fun n => HilbertSpace.mk (Q.eigenfunction_memHS n)))).topologicalClosure = ⊤ := by rw [Submodule.topologicalClosure_eq_top_iff] - refine (Submodule.eq_bot_iff (Submodule.span ℂ (Set.range (fun n => HilbertSpace.mk (Q.eigenfunction_memHS n))))ᗮ).mpr ?_ + refine (Submodule.eq_bot_iff (Submodule.span ℂ + (Set.range (fun n => HilbertSpace.mk (Q.eigenfunction_memHS n))))ᗮ).mpr ?_ intro f hf apply Q.zero_of_orthogonal_eigenVector f ?_ plancherel_theorem intro n diff --git a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean index be765d41..0bd8ec10 100644 --- a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean +++ b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Eigenfunction.lean @@ -10,7 +10,6 @@ import PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Basic -/ - namespace QuantumMechanics namespace OneDimension @@ -117,9 +116,10 @@ lemma eigenfunction_point_norm (n : ℕ) (x : ℝ) : simp [abs_of_nonneg] lemma eigenfunction_point_norm_sq (n : ℕ) (x : ℝ) : - ‖Q.eigenfunction n x‖ ^ 2 = (1/Real.sqrt (2 ^ n * n !) * + ‖Q.eigenfunction n x‖ ^ 2 = (1/Real.sqrt (2 ^ n * n !) * Real.sqrt (Real.sqrt (Q.m * Q.ω / (Real.pi * Q.ℏ)))) ^ 2 * - ((physHermiteFun n (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x)) ^ 2 * Real.exp (- Q.m * Q.ω * x^2 / Q.ℏ)) := by + ((physHermiteFun n + (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x)) ^ 2 * Real.exp (- Q.m * Q.ω * x^2 / Q.ℏ)) := by trans (1/Real.sqrt (2 ^ n * n !) * Real.sqrt (Real.sqrt (Q.m * Q.ω / (Real.pi * Q.ℏ)))) ^ 2 * ((|physHermiteFun n (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x)|) ^ 2 * @@ -137,7 +137,8 @@ lemma eigenfunction_point_norm_sq (n : ℕ) (x : ℝ) : @[fun_prop] lemma eigenfunction_square_integrable (n : ℕ) : MeasureTheory.Integrable (fun x => ‖Q.eigenfunction n x‖ ^ 2) := by - have h0 (x : ℝ) : Real.exp (- Q.m * Q.ω * x ^ 2 / Q.ℏ) = Real.exp (- (Q.m * Q.ω /Q.ℏ) * x ^ 2) := by + have h0 (x : ℝ) : Real.exp (- Q.m * Q.ω * x ^ 2 / Q.ℏ) = + Real.exp (- (Q.m * Q.ω /Q.ℏ) * x ^ 2) := by simp only [neg_mul, Real.exp_eq_exp] ring conv => @@ -186,7 +187,8 @@ lemma eigenfunction_mul (n p : ℕ) : _ = (1/Real.sqrt (2 ^ n * n !) * 1/Real.sqrt (2 ^ p * p !)) * (Real.sqrt (Real.sqrt (Q.m * Q.ω / (Real.pi * Q.ℏ))) * Real.sqrt (Real.sqrt (Q.m * Q.ω / (Real.pi * Q.ℏ)))) * - (physHermiteFun n (Real.sqrt (Q.m * Q.ω /Q.ℏ) * x) * physHermiteFun p (Real.sqrt (Q.m * Q.ω /Q.ℏ) * x)) * + (physHermiteFun n (Real.sqrt (Q.m * Q.ω /Q.ℏ) * x) * + physHermiteFun p (Real.sqrt (Q.m * Q.ω /Q.ℏ) * x)) * (Real.exp (- Q.m * Q.ω * x^2 / (2 * Q.ℏ)) * Real.exp (- Q.m * Q.ω * x^2 / (2 * Q.ℏ))) := by simp only [eigenfunction, ofNat_nonneg, pow_nonneg, Real.sqrt_mul, Complex.ofReal_mul, one_div, mul_inv_rev, neg_mul, Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg, @@ -194,7 +196,8 @@ lemma eigenfunction_mul (n p : ℕ) : ring _ = (1/Real.sqrt (2 ^ n * n !) * 1/Real.sqrt (2 ^ p * p !)) * ((Real.sqrt (Q.m * Q.ω / (Real.pi * Q.ℏ)))) * - (physHermiteFun n (Real.sqrt (Q.m * Q.ω /Q.ℏ) * x) * physHermiteFun p (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x)) * + (physHermiteFun n (Real.sqrt (Q.m * Q.ω /Q.ℏ) * x) * + physHermiteFun p (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x)) * (Real.exp (- Q.m * Q.ω * x^2 / Q.ℏ)) := by congr 1 · congr 1 @@ -231,7 +234,8 @@ lemma eigenfunction_mul_self (n : ℕ) : ring _ = (1/ (2 ^ n * n !)) * ((Real.sqrt (Q.m * Q.ω / (Real.pi * Q.ℏ)))) * - (physHermiteFun n (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x))^2 * (Real.exp (- Q.m * Q.ω * x^2 /Q.ℏ)) := by + (physHermiteFun n (Real.sqrt (Q.m * Q.ω / Q.ℏ) * x))^2 * + (Real.exp (- Q.m * Q.ω * x^2 /Q.ℏ)) := by congr 1 · congr 1 · congr 1 @@ -263,8 +267,9 @@ lemma eigenfunction_mul_self (n : ℕ) : open InnerProductSpace /-- The eigenfunction are normalized. -/ -lemma eigenfunction_normalized (n : ℕ) : - ⟪HilbertSpace.mk (Q.eigenfunction_memHS n), HilbertSpace.mk (Q.eigenfunction_memHS n)⟫_ℂ = 1 := by +lemma eigenfunction_normalized (n : ℕ) : + ⟪HilbertSpace.mk (Q.eigenfunction_memHS n), + HilbertSpace.mk (Q.eigenfunction_memHS n)⟫_ℂ = 1 := by rw [inner_mk_mk] conv_lhs => enter [2, x] @@ -279,7 +284,8 @@ lemma eigenfunction_normalized (n : ℕ) : refine div_nonneg ?_ ?_ exact (mul_nonneg_iff_of_pos_left Q.hm).mpr (le_of_lt Q.hω) exact le_of_lt Q.hℏ - have hc : (∫ (x : ℝ), physHermiteFun n (√(Q.m * Q.ω / Q.ℏ) * x) ^ 2 * Real.exp (- Q.m * Q.ω * x ^ 2 / Q.ℏ)) + have hc : (∫ (x : ℝ), physHermiteFun n (√(Q.m * Q.ω / Q.ℏ) * x) ^ 2 * + Real.exp (- Q.m * Q.ω * x ^ 2 / Q.ℏ)) = ∫ (x : ℝ), (physHermiteFun n (c * x) * physHermiteFun n (c * x)) * Real.exp (- c^2 * x ^ 2) := by congr @@ -340,11 +346,12 @@ lemma eigenfunction_normalized (n : ℕ) : /-- The eigen-functions of the quantum harmonic oscillator are orthogonal. -/ lemma eigenfunction_orthogonal {n p : ℕ} (hnp : n ≠ p) : - ⟪HilbertSpace.mk (Q.eigenfunction_memHS n), HilbertSpace.mk (Q.eigenfunction_memHS p)⟫_ℂ = 0 := by + ⟪HilbertSpace.mk (Q.eigenfunction_memHS n), + HilbertSpace.mk (Q.eigenfunction_memHS p)⟫_ℂ = 0 := by rw [inner_mk_mk] conv_lhs => enter [2, x] - rw [eigenfunction_conj, Q.eigenfunction_mul n p ] + rw [eigenfunction_conj, Q.eigenfunction_mul n p] rw [MeasureTheory.integral_mul_left] rw [integral_complex_ofReal] let c := √(Q.m * Q.ω / Q.ℏ) @@ -371,7 +378,6 @@ lemma eigenfunction_orthogonal {n p : ℕ} (hnp : n ≠ p) : mul_one, Complex.ofReal_zero, mul_zero, c] exact hnp - /-- The eigenvectors are orthonormal within the Hilbert space. s-/ lemma eigenfunction_orthonormal : Orthonormal ℂ (fun n => HilbertSpace.mk (Q.eigenfunction_memHS n)) := by @@ -383,7 +389,6 @@ lemma eigenfunction_orthonormal : · simp only [hnp, reduceIte] exact Q.eigenfunction_orthogonal hnp - end HarmonicOscillator end OneDimension end QuantumMechanics diff --git a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/TISE.lean b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/TISE.lean index 81b29454..5cf2a28b 100644 --- a/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/TISE.lean +++ b/PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/TISE.lean @@ -10,7 +10,6 @@ import PhysLean.QuantumMechanics.OneDimension.HarmonicOscillator.Eigenfunction -/ - namespace QuantumMechanics namespace OneDimension @@ -22,11 +21,10 @@ open Nat open PhysLean open HilbertSpace - /-- The eigenvalues for the Harmonic oscillator. -/ noncomputable def eigenValue (n : ℕ) : ℝ := (n + 1/2) * Q.ℏ * Q.ω -lemma deriv_eigenfunction_zero : deriv (Q.eigenfunction 0) = +lemma deriv_eigenfunction_zero : deriv (Q.eigenfunction 0) = Complex.ofReal (- Q.m * Q.ω / Q.ℏ) • Complex.ofReal * Q.eigenfunction 0 := by rw [eigenfunction_zero] simp only [neg_mul, deriv_const_mul_field', Complex.ofReal_div, Complex.ofReal_neg, @@ -64,13 +62,11 @@ lemma deriv_eigenfunction_zero : deriv (Q.eigenfunction 0) = rw [h1] ring - - lemma deriv_deriv_eigenfunction_zero (x : ℝ) : deriv (deriv (Q.eigenfunction 0)) x = - (Q.m * Q.ω) / Q.ℏ * (Q.eigenfunction 0 x + x * (-(Q.m * Q.ω) / Q.ℏ * x * Q.eigenfunction 0 x)) := by simp [deriv_eigenfunction_zero] - trans deriv (fun x => (-(↑Q.m * ↑Q.ω) / ↑Q.ℏ) • (Complex.ofReal x * Q.eigenfunction 0 x)) x + trans deriv (fun x => (-(↑Q.m * ↑Q.ω) / ↑Q.ℏ) • (Complex.ofReal x * Q.eigenfunction 0 x)) x · congr funext x simp @@ -169,13 +165,13 @@ lemma deriv_deriv_eigenfunction_one (x : ℝ) : deriv (fun x => deriv (Q.eigenfunction 1) x) x = Complex.ofReal (1/Real.sqrt (2 ^ 1 * 1 !)) * ((((-(Q.m * Q.ω) / Q.ℏ) * ↑√(Q.m * Q.ω / Q.ℏ) * (4 * x) + - (-(Q.m * Q.ω) / Q.ℏ) * (1 + (-(Q.m * Q.ω) / Q.ℏ) * x ^ 2) * (2* (√(Q.m * Q.ω / Q.ℏ) * x)))) * - Q.eigenfunction 0 x) := by + (-(Q.m * Q.ω) / Q.ℏ) * (1 + (-(Q.m * Q.ω) / Q.ℏ) * x ^ 2) * + (2 * (√(Q.m * Q.ω / Q.ℏ) * x)))) * Q.eigenfunction 0 x) := by rw [deriv_deriv_eigenfunction_succ] congr 2 simp [physHermiteFun_eq_aeval_physHermite, physHermite_one, Polynomial.aeval] -lemma schrodingerOperator_eigenfunction_one (x : ℝ) : +lemma schrodingerOperator_eigenfunction_one (x : ℝ) : Q.schrodingerOperator (Q.eigenfunction 1) x= Q.eigenValue 1 * Q.eigenfunction 1 x := by simp [schrodingerOperator, eigenValue] @@ -191,8 +187,6 @@ lemma schrodingerOperator_eigenfunction_one (x : ℝ) : field_simp [hl, hℏ] ring - - lemma deriv_deriv_eigenfunction_succ_succ (n : ℕ) (x : ℝ) : deriv (fun x => deriv (Q.eigenfunction (n + 2)) x) x = (- Q.m * Q.ω / Q.ℏ) * (2 * (n + 2) + (1 + (-(Q.m * Q.ω) / Q.ℏ) * x ^ 2)) * Q.eigenfunction (n + 2) x := by @@ -206,14 +200,16 @@ lemma deriv_deriv_eigenfunction_succ_succ (n : ℕ) (x : ℝ) : 2 * (n + 1) * (physHermiteFun n (√(Q.m * Q.ω / Q.ℏ) * x))) + (-(Q.m * Q.ω) / Q.ℏ) * √(Q.m * Q.ω / Q.ℏ) * (4 * (n + 1 + 1) * x) * (physHermiteFun (n + 1) (√(Q.m * Q.ω / Q.ℏ) * x)) + - (-(Q.m * Q.ω) / Q.ℏ) * (1 + (-(Q.m * Q.ω) / Q.ℏ) * x ^ 2) * (physHermiteFun (n + 2) (√(Q.m * Q.ω / Q.ℏ) * x))) + (-(Q.m * Q.ω) / Q.ℏ) * (1 + (-(Q.m * Q.ω) / Q.ℏ) * x ^ 2) * + (physHermiteFun (n + 2) (√(Q.m * Q.ω / Q.ℏ) * x))) · rw [deriv_physHermiteFun_succ] simp - trans ((Q.m * Q.ω / Q.ℏ) * 2 * (n + 1 + 1) * (2 * (n + 1) * (physHermiteFun n (√(Q.m * Q.ω / Q.ℏ) * x))) + - (- (Q.m * Q.ω) / Q.ℏ) * √(Q.m * Q.ω / Q.ℏ) * (4 * (n + 1 + 1) * x) * - (physHermiteFun (n + 1) (√(Q.m * Q.ω / Q.ℏ) * x)) + - (-(Q.m * Q.ω) / Q.ℏ) * (1 + (-(Q.m * Q.ω) / Q.ℏ) * x ^ 2) * - (physHermiteFun (n + 2) (√(Q.m * Q.ω / Q.ℏ) * x))) + trans ((Q.m * Q.ω / Q.ℏ) * 2 * (n + 1 + 1) * (2 * (n + 1) * + (physHermiteFun n (√(Q.m * Q.ω / Q.ℏ) * x))) + + (- (Q.m * Q.ω) / Q.ℏ) * √(Q.m * Q.ω / Q.ℏ) * (4 * (n + 1 + 1) * x) * + (physHermiteFun (n + 1) (√(Q.m * Q.ω / Q.ℏ) * x)) + + (-(Q.m * Q.ω) / Q.ℏ) * (1 + (-(Q.m * Q.ω) / Q.ℏ) * x ^ 2) * + (physHermiteFun (n + 2) (√(Q.m * Q.ω / Q.ℏ) * x))) · congr 2 trans (↑√(Q.m * Q.ω / Q.ℏ) * ↑√(Q.m * Q.ω / Q.ℏ)) * 2 * (↑n + 1 + 1) * (2 * (↑n + 1) * ↑(physHermiteFun n (√(Q.m * Q.ω / Q.ℏ) * x))) @@ -263,7 +259,6 @@ open Filter Finset open InnerProductSpace - end HarmonicOscillator end OneDimension end QuantumMechanics diff --git a/PhysLean/QuantumMechanics/OneDimension/HilbertSpace/Basic.lean b/PhysLean/QuantumMechanics/OneDimension/HilbertSpace/Basic.lean index 2b54f2b1..9b992b7f 100644 --- a/PhysLean/QuantumMechanics/OneDimension/HilbertSpace/Basic.lean +++ b/PhysLean/QuantumMechanics/OneDimension/HilbertSpace/Basic.lean @@ -29,6 +29,7 @@ noncomputable abbrev HilbertSpace := MeasureTheory.Lp (α := ℝ) ℂ 2 namespace HilbertSpace open MeasureTheory +/-- The proposition which is true if a function `f` can be lifted to the Hilbert space. -/ def MemHS (f : ℝ → ℂ) : Prop := Memℒp f 2 MeasureTheory.volume lemma aeStronglyMeasurable_of_memHS {f : ℝ → ℂ} (h : MemHS f) : @@ -54,7 +55,7 @@ lemma memHS_iff {f : ℝ → ℂ} : MemHS f ↔ exact ENNReal.ofNat_ne_top lemma aeEqFun_mk_mem_iff (f : ℝ → ℂ) (hf : AEStronglyMeasurable f volume) : - AEEqFun.mk f hf ∈ HilbertSpace ↔ MemHS f := by + AEEqFun.mk f hf ∈ HilbertSpace ↔ MemHS f := by rw [MemHS, HilbertSpace] rw [MeasureTheory.Lp.mem_Lp_iff_memℒp] apply MeasureTheory.memℒp_congr_ae @@ -124,14 +125,14 @@ lemma mem_iff' {f : ℝ → ℂ} (hf : MeasureTheory.AEStronglyMeasurable f Meas -/ open MeasureTheory -lemma gaussian_integrable {b : ℝ} (c : ℝ) (hb : 0 < b) : +lemma gaussian_integrable {b : ℝ} (c : ℝ) (hb : 0 < b) : MeasureTheory.Integrable (fun x => (Real.exp (- b * (x - c)^ 2) : ℂ)) := by apply MeasureTheory.Integrable.ofReal have hf : (fun x => (Real.exp (-b * (x - c) ^ 2))) = fun y => (fun x => (Real.exp (-b * x ^ 2))) (y - c) := by exact rfl erw [hf] - apply Integrable.comp_sub_right (f := (fun x => Real.exp (- b * x ^ 2))) + apply Integrable.comp_sub_right (f := (fun x => Real.exp (- b * x ^ 2))) exact integrable_exp_neg_mul_sq hb lemma gaussian_aestronglyMeasurable {b : ℝ} (c : ℝ) (hb : 0 < b) : @@ -140,7 +141,7 @@ lemma gaussian_aestronglyMeasurable {b : ℝ} (c : ℝ) (hb : 0 < b) : exact gaussian_integrable c hb lemma gaussian_memHS {b : ℝ} (c : ℝ) (hb : 0 < b) : - MemHS (fun x => (Real.exp (- b * (x - c) ^2) : ℂ)) := by + MemHS (fun x => (Real.exp (- b * (x - c) ^2) : ℂ)) := by rw [memHS_iff] apply And.intro · exact gaussian_aestronglyMeasurable c hb @@ -160,9 +161,9 @@ lemma gaussian_memHS {b : ℝ} (c : ℝ) (hb : 0 < b) : apply integrable_exp_neg_mul_sq linarith -lemma exp_mul_gaussian_integrable (b c : ℝ) (hb : 0 < b) : - MeasureTheory.Integrable (fun x => Real.exp (c * x) * Real.exp (- b * x ^ 2)) := by - have h1 : (fun x => Real.exp (c * x) * Real.exp (- b * x ^ 2)) +lemma exp_mul_gaussian_integrable (b c : ℝ) (hb : 0 < b) : + MeasureTheory.Integrable (fun x => Real.exp (c * x) * Real.exp (- b * x ^ 2)) := by + have h1 : (fun x => Real.exp (c * x) * Real.exp (- b * x ^ 2)) = (fun x => Real.exp (c^2 /(4 * b)) * Real.exp (- b * (x - c/(2 * b)) ^ 2)) := by funext x rw [← Real.exp_add, ← Real.exp_add] @@ -172,24 +173,24 @@ lemma exp_mul_gaussian_integrable (b c : ℝ) (hb : 0 < b) : rw [h1] apply MeasureTheory.Integrable.const_mul have h1 :(fun x => Real.exp (- b * (x - c/(2 * b)) ^ 2)) - = fun y => (fun x => Real.exp (- b * x ^ 2)) (y - c/(2 * b)) := by + = fun y => (fun x => Real.exp (- b * x ^ 2)) (y - c/(2 * b)) := by funext x rw [sub_sq] ring_nf rw [h1] - apply Integrable.comp_sub_right (f := (fun x => Real.exp (- b * x ^ 2))) + apply Integrable.comp_sub_right (f := (fun x => Real.exp (- b * x ^ 2))) exact integrable_exp_neg_mul_sq hb -lemma exp_abs_mul_gaussian_integrable (b c : ℝ) (hb : 0 < b) : - MeasureTheory.Integrable (fun x => Real.exp (|c * x|) * Real.exp (- b * x ^ 2)) := by +lemma exp_abs_mul_gaussian_integrable (b c : ℝ) (hb : 0 < b) : + MeasureTheory.Integrable (fun x => Real.exp (|c * x|) * Real.exp (- b * x ^ 2)) := by rw [← MeasureTheory.integrableOn_univ] - have h1 : Set.univ (α := ℝ) = (Set.Iic 0) ∪ Set.Ici 0 := by + have h1 : Set.univ (α := ℝ) = (Set.Iic 0) ∪ Set.Ici 0 := by exact Eq.symm Set.Iic_union_Ici rw [h1] apply MeasureTheory.IntegrableOn.union · let g := fun x => Real.exp ((- |c|) * x) * Real.exp (- b * x ^ 2) rw [integrableOn_congr_fun (g := g) _ measurableSet_Iic] - · apply MeasureTheory.IntegrableOn.left_of_union (t := Set.Ici 0 ) + · apply MeasureTheory.IntegrableOn.left_of_union (t := Set.Ici 0) rw [← h1, MeasureTheory.integrableOn_univ] exact exp_mul_gaussian_integrable b (- |c|) hb · intro x hx @@ -200,7 +201,7 @@ lemma exp_abs_mul_gaussian_integrable (b c : ℝ) (hb : 0 < b) : ring · let g := fun x => Real.exp (|c| * x) * Real.exp (- b * x ^ 2) rw [integrableOn_congr_fun (g := g) _ measurableSet_Ici] - · apply MeasureTheory.IntegrableOn.right_of_union (s := Set.Iic 0 ) + · apply MeasureTheory.IntegrableOn.right_of_union (s := Set.Iic 0) rw [← h1, MeasureTheory.integrableOn_univ] exact exp_mul_gaussian_integrable b (|c|) hb · intro x hx @@ -212,9 +213,9 @@ lemma exp_abs_mul_gaussian_integrable (b c : ℝ) (hb : 0 < b) : lemma mul_gaussian_mem_Lp_one (f : ℝ → ℂ) (hf : MemHS f) (b c : ℝ) (hb : 0 < b) : MeasureTheory.Memℒp (fun x => f x * Real.exp (- b * (x - c) ^ 2)) 1 volume := by refine memℒp_one_iff_integrable.mpr ?_ - let g : HilbertSpace := mk (gaussian_memHS c hb) + let g : HilbertSpace := mk (gaussian_memHS c hb) have h1 := MeasureTheory.L2.integrable_inner (𝕜 := ℂ) g (mk hf) - refine (integrable_congr ?_).mp h1 + refine (integrable_congr ?_).mp h1 simp conv_lhs => enter [x] @@ -230,7 +231,7 @@ lemma mul_gaussian_mem_Lp_one (f : ℝ → ℂ) (hf : MemHS f) (b c : ℝ) (hb : rw [Complex.conj_ofReal] simp -lemma mul_gaussian_mem_Lp_two (f : ℝ → ℂ) (hf : MemHS f) (b c : ℝ) (hb : 0 < b) : +lemma mul_gaussian_mem_Lp_two (f : ℝ → ℂ) (hf : MemHS f) (b c : ℝ) (hb : 0 < b) : MeasureTheory.Memℒp (fun x => f x * Real.exp (- b * (x - c) ^ 2)) 2 volume := by apply MeasureTheory.Memℒp.mul_of_top_left (p := 2) · apply MeasureTheory.memℒp_top_of_bound (C := Real.exp (0)) @@ -248,7 +249,7 @@ lemma mul_gaussian_mem_Lp_two (f : ℝ → ℂ) (hf : MemHS f) (b c : ℝ) (hb · exact hf lemma abs_mul_gaussian_integrable (f : ℝ → ℂ) (hf : MemHS f) (b c : ℝ) (hb : 0 < b) : - MeasureTheory.Integrable (fun x => Complex.abs (f x) * Real.exp (- b * (x - c)^2)) := by + MeasureTheory.Integrable (fun x => Complex.abs (f x) * Real.exp (- b * (x - c)^2)) := by have h1 : (fun x => Complex.abs (f x) * Real.exp (- b * (x - c)^2)) = (fun x => Complex.abs (f x * Real.exp (- b *(x - c)^2))) := by funext x @@ -262,11 +263,13 @@ lemma abs_mul_gaussian_integrable (f : ℝ → ℂ) (hf : MemHS f) (b c : ℝ) ( exact mul_gaussian_mem_Lp_one f hf b c hb simpa using MeasureTheory.Memℒp.integrable_norm_rpow h2 (by simp) (by simp) -lemma exp_mul_abs_mul_gaussian_integrable (f : ℝ → ℂ) (hf : MemHS f) - (b c : ℝ) (hb : 0 < b) : - MeasureTheory.Integrable (fun x => Real.exp (c * x) * Complex.abs (f x) * Real.exp (- b * x ^ 2)) := by - have h1 : (fun x => Real.exp (c * x) * Complex.abs (f x) * Real.exp (- b * x ^ 2)) - = (fun x => Real.exp (c^2 /(4 * b)) * (Complex.abs (f x) * Real.exp (- b * (x - c/(2 * b)) ^ 2))) := by +lemma exp_mul_abs_mul_gaussian_integrable (f : ℝ → ℂ) (hf : MemHS f) + (b c : ℝ) (hb : 0 < b) : MeasureTheory.Integrable + (fun x => Real.exp (c * x) * Complex.abs (f x) * Real.exp (- b * x ^ 2)) := by + have h1 : (fun x => Real.exp (c * x) * + Complex.abs (f x) * Real.exp (- b * x ^ 2)) + = (fun x => Real.exp (c^2 /(4 * b)) * + (Complex.abs (f x) * Real.exp (- b * (x - c/(2 * b)) ^ 2))) := by funext x rw [mul_comm,← mul_assoc] trans (Real.exp (c ^ 2 / (4 * b)) * Real.exp (-b * (x - c / (2 * b)) ^ 2)) * Complex.abs (f x) @@ -280,16 +283,17 @@ lemma exp_mul_abs_mul_gaussian_integrable (f : ℝ → ℂ) (hf : MemHS f) apply MeasureTheory.Integrable.const_mul exact abs_mul_gaussian_integrable f hf b (c / (2 * b)) hb -lemma exp_abs_mul_abs_mul_gaussian_integrable (f : ℝ → ℂ) (hf : MemHS f) (b c : ℝ) (hb : 0 < b) : - MeasureTheory.Integrable (fun x => Real.exp (|c * x|) * Complex.abs (f x) * Real.exp (- b * x ^ 2)) := by +lemma exp_abs_mul_abs_mul_gaussian_integrable (f : ℝ → ℂ) (hf : MemHS f) (b c : ℝ) (hb : 0 < b) : + MeasureTheory.Integrable + (fun x => Real.exp (|c * x|) * Complex.abs (f x) * Real.exp (- b * x ^ 2)) := by rw [← MeasureTheory.integrableOn_univ] - have h1 : Set.univ (α := ℝ) = (Set.Iic 0) ∪ Set.Ici 0 := by + have h1 : Set.univ (α := ℝ) = (Set.Iic 0) ∪ Set.Ici 0 := by exact Eq.symm Set.Iic_union_Ici rw [h1] apply MeasureTheory.IntegrableOn.union · let g := fun x => Real.exp ((- |c|) * x) * Complex.abs (f x) * Real.exp (- b * x ^ 2) rw [integrableOn_congr_fun (g := g) _ measurableSet_Iic] - · apply MeasureTheory.IntegrableOn.left_of_union (t := Set.Ici 0 ) + · apply MeasureTheory.IntegrableOn.left_of_union (t := Set.Ici 0) rw [← h1, MeasureTheory.integrableOn_univ] exact exp_mul_abs_mul_gaussian_integrable f hf b (-|c|) hb · intro x hx @@ -299,9 +303,9 @@ lemma exp_abs_mul_abs_mul_gaussian_integrable (f : ℝ → ℂ) (hf : MemHS f) rw [abs_mul] rw [abs_of_nonpos hx] ring - · let g := fun x => Real.exp (|c| * x) * Complex.abs (f x) * Real.exp (- b * x ^ 2) + · let g := fun x => Real.exp (|c| * x) * Complex.abs (f x) * Real.exp (- b * x ^ 2) rw [integrableOn_congr_fun (g := g) _ measurableSet_Ici] - · apply MeasureTheory.IntegrableOn.right_of_union (s := Set.Iic 0 ) + · apply MeasureTheory.IntegrableOn.right_of_union (s := Set.Iic 0) rw [← h1, MeasureTheory.integrableOn_univ] exact exp_mul_abs_mul_gaussian_integrable f hf b |c| hb · intro x hx @@ -311,5 +315,4 @@ lemma exp_abs_mul_abs_mul_gaussian_integrable (f : ℝ → ℂ) (hf : MemHS f) rw [abs_mul] rw [abs_of_nonneg hx] - end HilbertSpace