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.

[adambornemann-glitch]

done!
-awaiting-author

[gloges]

One more opportunity for generalization that we both missed.
Can you also go through and clean up the implicit/explicit arguments and add appropriate simp tags for the unitaryConj lemmas? The rule of thumb is that args should be explicit unless they can be inferred from other arguments. I think that unitaryConj_apply and mem_unitaryConj_domain_iff are deserving of simp tags, but let me know what you think.

[gloges]

Suggested change

	/-- Conjugating by `u` and then by `u⁻¹` recovers the original operator. -/
	@[simp]
	lemma unitaryConj_symm_unitaryConj (u : H ≃ₗᵢ[ℂ] H') (A : H →ₗ.[ℂ] H) :
	unitaryConj u.symm (unitaryConj u A) = A := by
	ext x hx hx'
	· simp [mem_unitaryConj_domain_iff]
	· simp [unitaryConj_apply]
	/-- Conjugating by `u⁻¹` and then by `u` recovers the original operator. -/
	@[simp]
	lemma unitaryConj_unitaryConj_symm (u : H ≃ₗᵢ[ℂ] H') (B : H' →ₗ.[ℂ] H') :
	unitaryConj u (unitaryConj u.symm B) = B := unitaryConj_symm_unitaryConj u.symm B
	@[simp]
	lemma unitaryConj_refl : unitaryConj (LinearIsometryEquiv.refl ℂ H) A = A := rfl
	@[simp]
	lemma unitaryConj_unitaryConj (u' : H' ≃ₗᵢ[ℂ] H'') :
	unitaryConj u' (unitaryConj u A) = unitaryConj (u.trans u') A := by
	ext <;> simp

These can be generalized.