Skip to content

feat(QuantumMechanics) : Prove potentialOperator_isSelfAdjoint #1490

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
jstoobysmith merged 3 commits into from
Aug 7, 2026
+19 −7
Merged

feat(QuantumMechanics) : Prove potentialOperator_isSelfAdjoint #1490

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
1e60702
feat(QuantumMechanics) : Prove potentialOperator_isSelfAdjoint
ereinhardt8 Aug 6, 2026
84df24b
style(QuantumMechanics): Fix style in RectangularBarrier/Basic.lean
ereinhardt8 Aug 6, 2026
b4d0038
style(QuantumMechanics): Separate multi-tactic lines
ereinhardt8 Aug 7, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 19 additions & 7 deletions Physlib/QuantumMechanics/RectangularBarrier/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -119,9 +124,16 @@ 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 only [Function.comp_apply, Complex.conj_ofReal]
have hQ := potentialFunction_aestronglyMeasurable
fun_prop

@jstoobysmith jstoobysmith Aug 7, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hey @ereinhardt8 Many thanks for this first PR! Just one comment from me before this can be merged. It would be convention to not to have more then one tactic on a line e.g. swap; ext x; simp [...] should be three separate lines. Other then that, this PR looks great!


/-!
### D.3. Hamiltonian
Expand Down
Loading