feat(QuantumMechanics): derivative operators via Fourier-conjugated m…

[adambornemann-glitch]

…ultiplication

Define derivOperator f, the Fourier conjugate 𝓕⁻¹ ∘ 𝓜 (f ∘ 2π•) ∘ 𝓕 of the multiplication operator, for a symbol f of the wavenumber k.

• derivOperator with domain/apply characterizations and aestronglyMeasurable_comp_two_pi_smul (rescaling is quasi-measure- preserving for the Haar measure)
• derivOperator_hasDenseDomain for a.e.-strongly-measurable symbols
• derivOperator_adjoint : (derivOperator f)† = derivOperator (conj ∘ f)
• derivOperator_isSelfAdjoint for real-valued symbols
• schwartzSubmodule_le_derivOperator_domain for temperate-growth symbols
• supporting unitary-conjugation transfers in Unbounded.lean §B.5: unitaryConj_mono, the involution pair (simp), and unitaryConj_adjoint

[github-actions]

Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally.

If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks.

If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip.

Important: If a reviewer adds an awaiting-author label to your PR, once you have addressed the review comments, please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

[gloges]

Thanks, these look good! I've left a few minor suggestions to improve the documentation, organization and Fourier/simp lemmas. There are also two lemmas which can be generalized while (I think!) leaving the proofs essentially unchanged.

[gloges]

Suggested change

	open LinearPMap
	open LinearPMap Real

Might be convenient to have the π notation since 2 * Real.pi is common - up to you!

[gloges]

Suggested change

	Every constant-coefficient differential operator is, up to the Fourier transform, a multiplication
	operator. In this module we take that as a definition: for a symbol `f : Space d → ℂ`, a function
	Every constant-coefficient differential operator is unitarily equivalent, via the Fourier transform, to a multiplication
	operator. In this module we take that as a definition: for a symbol `f : Space d → ℂ`, a function

Something like this might be clearer.

[gloges]

We should explain the design decision to have explicit factors of 2π here.

[gloges]

Suggested change

	/-- The derivative operator with symbol `f : Space d → ℂ`, a function of the wavenumber `k`. -/
	def derivOperator (f : Space d → ℂ) : SpaceDHilbertSpace d →ₗ.[ℂ] SpaceDHilbertSpace d :=
	(𝓜 volume fun ξ => f ((2 * Real.pi) • ξ)).unitaryConj (fourierUnitary d).symm
	/-- The derivative operator with symbol `f : Space d → ℂ`, interpreted as a function of the wavenumber `k`. -/
	def derivOperator (f : Space d → ℂ) : SpaceDHilbertSpace d →ₗ.[ℂ] SpaceDHilbertSpace d :=
	(𝓜 volume (f ∘ fun k ↦ (2 * π) • k)).unitaryConj (fourierUnitary d).symm

[gloges]

1. Let's add a derivOperator_eq lemma expressing the definition of derivOperator f.
2. It might be nice to have a \MCD notation for derivOperator analogous to that for mulOperator.

[gloges]

Suggested change

	lemma mem_derivOperator_domain_iff {ψ : SpaceDHilbertSpace d} :
	ψ ∈ (derivOperator f).domain
	↔ fourierUnitary d ψ ∈ (𝓜 volume fun ξ => f ((2 * Real.pi) • ξ)).domain := Iff.rfl
	lemma mem_derivOperator_domain_iff {ψ : SpaceDHilbertSpace d} :
	ψ ∈ (derivOperator f).domain ↔ 𝓕 ψ ∈ (𝓜 volume (f ∘ fun k ↦ (2 * π) • k)).domain := Iff.rfl

Remember from #1426 that 𝓕 ψ is the simp normal form of fourierUnitary d ψ.

[gloges]

Suggested change

	lemma derivOperator_apply (ψ : (derivOperator f).domain) :
	derivOperator f ψ = (fourierUnitary d).symm
	((𝓜 volume fun ξ => f ((2 * Real.pi) • ξ))
	⟨fourierUnitary d ↑ψ, mem_derivOperator_domain_iff.mp ψ.2⟩) := rfl
	lemma derivOperator_apply (ψ : (derivOperator f).domain) :
	derivOperator f ψ =
	𝓕⁻ ((𝓜 volume (f ∘ fun k ↦ (2 * π) • k)) ⟨𝓕 ψ.1, mem_derivOperator_domain_iff.mp ψ.2⟩) :=
	rfl

Same here.

[gloges]

Suggested change

	rw [derivOperator, unitaryConj_adjoint _
	(mulOperator_hasDenseDomain (aestronglyMeasurable_comp_two_pi_smul hf)),
	mulOperator_adjoint_eq_conj (aestronglyMeasurable_comp_two_pi_smul hf)]
	rfl
	simp only [derivOperator_eq, aestronglyMeasurable_comp_const_smul hf, mulOperator_hasDenseDomain,
	unitaryConj_adjoint, mulOperator_adjoint_eq_conj, Function.comp_assoc]

derivOperator_eq to unpack the definition of the derivative operators and can use simp to avoid repetition of the aestronglyMeasurable_comp lemma.

[gloges]

I think this should be a simp lemma.
Also, I'm pretty sure the hdense hypothesis can be removed: if A is not densely defined then both sides are zero operators (c.f. adjoint_apply_of_not_dense) so just need to check domains match.

[gloges]

Let's organize by (def + defining properties), (domain), (adjoints). We'll definitely have more domain-type lemmas in the future so best to keep them together from the beginning.