From 1e6070280c7eb36c0c38c28300f806de692052dc Mon Sep 17 00:00:00 2001 From: Evan Reinhardt Date: Thu, 6 Aug 2026 14:45:20 -0400 Subject: [PATCH 1/3] feat(QuantumMechanics) : Prove potentialOperator_isSelfAdjoint --- .../RectangularBarrier/Basic.lean | 22 +++++++++++++------ 1 file changed, 15 insertions(+), 7 deletions(-) diff --git a/Physlib/QuantumMechanics/RectangularBarrier/Basic.lean b/Physlib/QuantumMechanics/RectangularBarrier/Basic.lean index 986855e23..d7555b189 100644 --- a/Physlib/QuantumMechanics/RectangularBarrier/Basic.lean +++ b/Physlib/QuantumMechanics/RectangularBarrier/Basic.lean @@ -87,10 +87,15 @@ lemma potentialFunction_eq : Q.potentialFunction = fun x ↦ (Icc Q.lower Q.upper).indicator (fun _ ↦ Q.V₀) (x 0) := rfl /-- The piecewise-constant potential of the rectangular barrier is a.e. strongly measurable. -/ -informal_lemma potentialFunction_aestronglyMeasurable where - deps := [``RectangularBarrier] - tag := "QM-RB-aesm" - -- This relies on `Space.val` being measure-preserving. +-- This relies on `Space.val` being measure-preserving. +lemma potentialFunction_aestronglyMeasurable: AEStronglyMeasurable Q.potentialFunction volume := by + unfold potentialFunction + apply AEStronglyMeasurable.indicator + · fun_prop + · change (MeasurableSet ((Icc Q.lower Q.upper) ∘ (fun (x: Space 1) => x.val 0))) + have hi : MeasurableSet (Icc Q.lower Q.upper) := by measurability + have hf : Measurable ((fun x => x.val 0) : Space 1 → ℝ) := by measurability + exact MeasurableSet.preimage hi hf /-! ## C. Hilbert space @@ -119,9 +124,12 @@ def kineticOperator : Q.HS →ₗ.[ℂ] Q.HS := (2 * Q.m)⁻¹ • momentumSqOpe def potentialOperator : Q.HS →ₗ.[ℂ] Q.HS := 𝓜 volume (Complex.ofReal ∘ Q.potentialFunction) /-- The potential operator for the rectangular barrier is self-adjoint. -/ -informal_lemma potentialOperator_isSelfAdjoint where - deps := [``RectangularBarrier] - tag := "QM-RB-sa" +lemma potentialOperator_isSelfAdjoint (Q : RectangularBarrier): IsSelfAdjoint Q.potentialOperator := by + unfold IsSelfAdjoint; unfold potentialOperator + rw [mulOperator_isSelfAdjoint_ofReal] + swap; ext x; simp + have hQ := potentialFunction_aestronglyMeasurable + fun_prop /-! ### D.3. Hamiltonian From 84df24b5c4b934d85b5f7a6103ae3edf472076ff Mon Sep 17 00:00:00 2001 From: Evan Reinhardt Date: Thu, 6 Aug 2026 18:25:25 -0400 Subject: [PATCH 2/3] style(QuantumMechanics): Fix style in RectangularBarrier/Basic.lean --- Physlib/QuantumMechanics/RectangularBarrier/Basic.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Physlib/QuantumMechanics/RectangularBarrier/Basic.lean b/Physlib/QuantumMechanics/RectangularBarrier/Basic.lean index d7555b189..26e4b1980 100644 --- a/Physlib/QuantumMechanics/RectangularBarrier/Basic.lean +++ b/Physlib/QuantumMechanics/RectangularBarrier/Basic.lean @@ -124,10 +124,11 @@ def kineticOperator : Q.HS →ₗ.[ℂ] Q.HS := (2 * Q.m)⁻¹ • momentumSqOpe def potentialOperator : Q.HS →ₗ.[ℂ] Q.HS := 𝓜 volume (Complex.ofReal ∘ Q.potentialFunction) /-- The potential operator for the rectangular barrier is self-adjoint. -/ -lemma potentialOperator_isSelfAdjoint (Q : RectangularBarrier): IsSelfAdjoint Q.potentialOperator := by +lemma potentialOperator_isSelfAdjoint (Q : RectangularBarrier) : + IsSelfAdjoint Q.potentialOperator := by unfold IsSelfAdjoint; unfold potentialOperator rw [mulOperator_isSelfAdjoint_ofReal] - swap; ext x; simp + swap; ext x; simp only [Function.comp_apply, Complex.conj_ofReal] have hQ := potentialFunction_aestronglyMeasurable fun_prop From b4d00382d193ac445cad9867e67d0f855a821297 Mon Sep 17 00:00:00 2001 From: Evan Reinhardt Date: Fri, 7 Aug 2026 09:19:26 -0400 Subject: [PATCH 3/3] style(QuantumMechanics): Separate multi-tactic lines --- Physlib/QuantumMechanics/RectangularBarrier/Basic.lean | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/Physlib/QuantumMechanics/RectangularBarrier/Basic.lean b/Physlib/QuantumMechanics/RectangularBarrier/Basic.lean index 26e4b1980..f4a0c75f0 100644 --- a/Physlib/QuantumMechanics/RectangularBarrier/Basic.lean +++ b/Physlib/QuantumMechanics/RectangularBarrier/Basic.lean @@ -126,9 +126,12 @@ def potentialOperator : Q.HS →ₗ.[ℂ] Q.HS := 𝓜 volume (Complex.ofReal /-- The potential operator for the rectangular barrier is self-adjoint. -/ lemma potentialOperator_isSelfAdjoint (Q : RectangularBarrier) : IsSelfAdjoint Q.potentialOperator := by - unfold IsSelfAdjoint; unfold potentialOperator + unfold IsSelfAdjoint + unfold potentialOperator rw [mulOperator_isSelfAdjoint_ofReal] - swap; ext x; simp only [Function.comp_apply, Complex.conj_ofReal] + swap + ext x + simp only [Function.comp_apply, Complex.conj_ofReal] have hQ := potentialFunction_aestronglyMeasurable fun_prop