From 2b34bf4b3946fac46361667c887203b6139b843f Mon Sep 17 00:00:00 2001 From: adambornemann-glitch Date: Tue, 21 Jul 2026 19:31:40 -0400 Subject: [PATCH 1/2] feat(QuantumMechanics): derivative operators via Fourier-conjugated multiplication MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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` Co-authored-by: Claude Fable 5 --- Physlib.lean | 1 + .../Operators/Derivative.lean | 116 ++++++++++++++++++ .../QuantumMechanics/Operators/Unbounded.lean | 32 +++++ 3 files changed, 149 insertions(+) create mode 100644 Physlib/QuantumMechanics/Operators/Derivative.lean diff --git a/Physlib.lean b/Physlib.lean index 981f36e36..3b66048ac 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -303,6 +303,7 @@ public import Physlib.QuantumMechanics.InfiniteSquareWell.Basic public import Physlib.QuantumMechanics.Operators.AngularMomentum public import Physlib.QuantumMechanics.Operators.Commutation public import Physlib.QuantumMechanics.Operators.Covariance +public import Physlib.QuantumMechanics.Operators.Derivative public import Physlib.QuantumMechanics.Operators.Examples public import Physlib.QuantumMechanics.Operators.Momentum public import Physlib.QuantumMechanics.Operators.Multiplication diff --git a/Physlib/QuantumMechanics/Operators/Derivative.lean b/Physlib/QuantumMechanics/Operators/Derivative.lean new file mode 100644 index 000000000..7c9682add --- /dev/null +++ b/Physlib/QuantumMechanics/Operators/Derivative.lean @@ -0,0 +1,116 @@ +/- +Copyright (c) 2026 Adam Bornemann. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Adam Bornemann +-/ +module + +public import Physlib.QuantumMechanics.HilbertSpaces.SpaceD.Fourier +public import Physlib.QuantumMechanics.Operators.Multiplication +public import Physlib.QuantumMechanics.Operators.SpectralTheory.SelfAdjoint +/-! + +# Derivative operators + +## i. Overview + +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 +of the wavenumber `k`, the derivative operator `derivOperator f` is the conjugate +`𝓕⁻¹ ∘ 𝓜 (f ∘ 2π•) ∘ 𝓕` of the multiplication operator by the Fourier unitary, through +`LinearPMap.unitaryConj`. + +## ii. Key results + +- `derivOperator` : the derivative operator with wavenumber symbol `f`. +- `derivOperator_hasDenseDomain` : it is densely defined for a.e.-strongly-measurable `f`. +- `derivOperator_adjoint` : its adjoint is the derivative operator of the conjugate symbol. +- `derivOperator_isSelfAdjoint` : it is self-adjoint for real-valued `f`. +- `schwartzSubmodule_le_derivOperator_domain` : the Schwartz submodule lies in the domain for + temperate-growth `f`. + +## iii. Table of contents + +- A. The derivative operator +- B. The Schwartz submodule in the domain + +## iv. References + +-/ + +@[expose] public section + +namespace QuantumMechanics +namespace SpaceDHilbertSpace +noncomputable section + +open MeasureTheory ComplexConjugate +open LinearPMap + +/-! +## A. The derivative operator +-/ + +variable {d : ℕ} {f : Space d → ℂ} + +/-- 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 wavenumber rescaling `ξ ↦ 2πξ` preserves a.e.-strong measurability of symbols: +nonzero scaling is quasi-measure-preserving for the Haar measure. -/ +lemma aestronglyMeasurable_comp_two_pi_smul (hf : AEStronglyMeasurable f volume) : + AEStronglyMeasurable (fun ξ : Space d => f ((2 * Real.pi) • ξ)) volume := + hf.comp_quasiMeasurePreserving + ⟨measurable_const_smul _, by + rw [Measure.map_addHaar_smul volume (by positivity)] + exact Measure.smul_absolutelyContinuous⟩ + +/-- Membership: `ψ ∈ D(derivOperator f)` iff `𝓕ψ` lies in the domain of multiplication by the +rescaled symbol. -/ +lemma mem_derivOperator_domain_iff {ψ : SpaceDHilbertSpace d} : + ψ ∈ (derivOperator f).domain + ↔ fourierUnitary d ψ ∈ (𝓜 volume fun ξ => f ((2 * Real.pi) • ξ)).domain := Iff.rfl + +/-- The defining formula: `derivOperator f ψ = 𝓕⁻¹ ((f ∘ 2π•) · 𝓕ψ)`. -/ +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 + +/-- The derivative operator is densely defined. -/ +lemma derivOperator_hasDenseDomain (hf : AEStronglyMeasurable f volume) : + (derivOperator f).HasDenseDomain := + (mulOperator_hasDenseDomain (aestronglyMeasurable_comp_two_pi_smul hf)).unitaryConj_dense_domain + +/-- The adjoint of a derivative operator is the derivative operator of the conjugate symbol: +`(derivOperator f)† = derivOperator (conj ∘ f)`. -/ +lemma derivOperator_adjoint (hf : AEStronglyMeasurable f volume) : + (derivOperator f)† = derivOperator (conj ∘ f) := by + rw [derivOperator, unitaryConj_adjoint _ + (mulOperator_hasDenseDomain (aestronglyMeasurable_comp_two_pi_smul hf)), + mulOperator_adjoint_eq_conj (aestronglyMeasurable_comp_two_pi_smul hf)] + rfl + +/-- The derivative operator of a real-valued symbol is self-adjoint on its maximal domain. -/ +lemma derivOperator_isSelfAdjoint (hf : AEStronglyMeasurable f volume) + (hf' : conj ∘ f = f) : IsSelfAdjoint (derivOperator f) := + LinearPMap.unitaryConj_isSelfAdjoint (fourierUnitary d).symm + (mulOperator_isSelfAdjoint_ofReal (aestronglyMeasurable_comp_two_pi_smul hf) + (funext fun ξ => congrFun hf' ((2 * Real.pi) • ξ))) + +/-! +## B. The Schwartz submodule in the domain +-/ + +/-- For a temperate-growth symbol the Schwartz submodule lies in the domain of the derivative +operator. -/ +lemma schwartzSubmodule_le_derivOperator_domain (hf : f.HasTemperateGrowth) : + SchwartzSubmodule d ≤ (derivOperator f).domain := + fun _ hψ => mem_derivOperator_domain_iff.mpr + (mulOperator_domain_ge_of_hasTemperateGrowth (by fun_prop) volume + (fourierUnitary_map_schwartzSubmodule ▸ Submodule.mem_map_of_mem hψ)) + +end +end SpaceDHilbertSpace +end QuantumMechanics diff --git a/Physlib/QuantumMechanics/Operators/Unbounded.lean b/Physlib/QuantumMechanics/Operators/Unbounded.lean index 058a65a2a..a38bd0842 100644 --- a/Physlib/QuantumMechanics/Operators/Unbounded.lean +++ b/Physlib/QuantumMechanics/Operators/Unbounded.lean @@ -620,6 +620,25 @@ lemma unitaryConj_apply_map (y : A.domain) : unitaryConj u A ⟨u (y : H), map_mem_unitaryConj_domain u A y⟩ = u (A y) := by simp only [unitaryConj_apply, u.symm_apply_apply] +/-- Unitary conjugation is monotone for the extension order on partial linear maps. -/ +lemma unitaryConj_mono (u : H ≃ₗᵢ[ℂ] H') {A B : H →ₗ.[ℂ] H} (h : A ≤ B) : + unitaryConj u A ≤ unitaryConj u B := + ⟨fun _ hx => h.1 hx, fun x y hxy => + congrArg u (h.2 (x := ⟨u.symm ↑x, x.2⟩) (y := ⟨u.symm ↑y, y.2⟩) (congrArg u.symm hxy))⟩ + +/-- 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 + variable {u A} open scoped InnerProductSpace in @@ -640,6 +659,19 @@ preimage of a dense set under a homeomorphism. -/ lemma HasDenseDomain.unitaryConj_dense_domain (hdense : A.HasDenseDomain) : (unitaryConj u A).HasDenseDomain := hdense.preimage u.symm.toHomeomorph.isOpenMap +/-- Unitary conjugation commutes with the adjoint `(u A u⁻¹)† = u A† u⁻¹` for a densely defined `A`. +-/ +lemma unitaryConj_adjoint + [CompleteSpace H] [CompleteSpace H'] (u : H ≃ₗᵢ[ℂ] H') (hdense : A.HasDenseDomain) : + (unitaryConj u A)† = unitaryConj u A† := by + have hd' : (unitaryConj u A).HasDenseDomain := hdense.unitaryConj_dense_domain + refine le_antisymm ?_ (((adjoint_isFormalAdjoint hdense).symm.unitaryConj).le_adjoint hd') + have h₁ : unitaryConj u.symm ((unitaryConj u A)†) ≤ (unitaryConj u.symm (unitaryConj u A))† := + ((adjoint_isFormalAdjoint hd').symm.unitaryConj).le_adjoint hd'.unitaryConj_dense_domain + rw [unitaryConj_symm_unitaryConj] at h₁ + have h₂ := unitaryConj_mono u h₁ + rwa [unitaryConj_unitaryConj_symm] at h₂ + /-- If `A - z` is surjective for a scalar `z : ℂ`, then so is `u A u⁻¹ - z`. -/ lemma unitaryConj_sub_smul_surjective {z : ℂ} (h : Function.Surjective (A - z • 1).toFun) : Function.Surjective (unitaryConj u A - z • 1).toFun := by From 8cd0f36f58a10e22899cb90765fd6923fffa4b88 Mon Sep 17 00:00:00 2001 From: adambornemann-glitch Date: Wed, 22 Jul 2026 15:57:58 -0400 Subject: [PATCH 2/2] Remove density hypothesis from LinearPMap.unitaryConj_adjoint When A is not densely defined, both adjoints are the zero map and the adjoint domains are identified through the unitary, so the equality holds unconditionally. Adds @[simp] unitaryConj_hasDenseDomain_iff and drops a now-unused simp argument in derivOperator_adjoint. Co-authored-by: Claude Fable 5 --- .../Operators/Derivative.lean | 129 +++++++++++------- .../QuantumMechanics/Operators/Unbounded.lean | 56 ++++++-- 2 files changed, 121 insertions(+), 64 deletions(-) diff --git a/Physlib/QuantumMechanics/Operators/Derivative.lean b/Physlib/QuantumMechanics/Operators/Derivative.lean index 7c9682add..3fbd130ab 100644 --- a/Physlib/QuantumMechanics/Operators/Derivative.lean +++ b/Physlib/QuantumMechanics/Operators/Derivative.lean @@ -14,15 +14,22 @@ public import Physlib.QuantumMechanics.Operators.SpectralTheory.SelfAdjoint ## i. Overview -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 -of the wavenumber `k`, the derivative operator `derivOperator f` is the conjugate -`𝓕⁻¹ ∘ 𝓜 (f ∘ 2π•) ∘ 𝓕` of the multiplication operator by the Fourier unitary, through -`LinearPMap.unitaryConj`. +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 of the wavenumber `k`, the derivative operator `derivOperator f` is +the conjugate `𝓕⁻¹ ∘ 𝓜 (f ∘ 2π•) ∘ 𝓕` of the multiplication operator by the Fourier unitary, +through `LinearPMap.unitaryConj`. + +The explicit factors of `2π` implement the change of variables between mathlib's Fourier +convention and the physics one: mathlib's `𝓕` pairs position with the frequency `ξ` through +`e^(-2πi ⟨x, ξ⟩)`, while physics symbols are written in the wavenumber `k = 2πξ`. Rather than +introduce a rescaled transform, we rescale the symbol once and for all: `derivOperator f` +multiplies `𝓕ψ` at frequency `ξ` by `f (2πξ)`, so `f` itself is always a function of the +wavenumber. ## ii. Key results -- `derivOperator` : the derivative operator with wavenumber symbol `f`. +- `derivOperator` : the derivative operator with wavenumber symbol `f`, with notation `𝓓 f`. - `derivOperator_hasDenseDomain` : it is densely defined for a.e.-strongly-measurable `f`. - `derivOperator_adjoint` : its adjoint is the derivative operator of the conjugate symbol. - `derivOperator_isSelfAdjoint` : it is self-adjoint for real-valued `f`. @@ -31,8 +38,10 @@ of the wavenumber `k`, the derivative operator `derivOperator f` is the conjugat ## iii. Table of contents -- A. The derivative operator -- B. The Schwartz submodule in the domain +- A. Definitions +- B. Basic properties + - B.1. Domain + - B.2. Adjoints ## iv. References @@ -45,72 +54,86 @@ namespace SpaceDHilbertSpace noncomputable section open MeasureTheory ComplexConjugate -open LinearPMap +open LinearPMap Real FourierTransform /-! -## A. The derivative operator +## A. Definition -/ variable {d : ℕ} {f : Space d → ℂ} -/-- The derivative operator with symbol `f : Space d → ℂ`, a function of the wavenumber `k`. -/ +/-- 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 fun ξ => f ((2 * Real.pi) • ξ)).unitaryConj (fourierUnitary d).symm - -/-- The wavenumber rescaling `ξ ↦ 2πξ` preserves a.e.-strong measurability of symbols: -nonzero scaling is quasi-measure-preserving for the Haar measure. -/ -lemma aestronglyMeasurable_comp_two_pi_smul (hf : AEStronglyMeasurable f volume) : - AEStronglyMeasurable (fun ξ : Space d => f ((2 * Real.pi) • ξ)) volume := - hf.comp_quasiMeasurePreserving - ⟨measurable_const_smul _, by - rw [Measure.map_addHaar_smul volume (by positivity)] - exact Measure.smul_absolutelyContinuous⟩ - -/-- Membership: `ψ ∈ D(derivOperator f)` iff `𝓕ψ` lies in the domain of multiplication by the + (𝓜 volume (f ∘ fun k ↦ (2 * π) • k)).unitaryConj (fourierUnitary d).symm + +@[inherit_doc derivOperator] +notation "𝓓" => derivOperator + +/-- The defining equation: `𝓓 f` is the multiplication operator by the rescaled symbol +`f ∘ 2π•`, conjugated through the inverse Fourier unitary. -/ +lemma derivOperator_eq (f : Space d → ℂ) : + 𝓓 f = (𝓜 volume (f ∘ fun k ↦ (2 * π) • k)).unitaryConj (fourierUnitary d).symm := rfl + +/-- a.e.-strong measurability of symbols is preserved under composition with scalar +multiplication: nonzero scaling is quasi-measure-preserving for the Haar measure, and zero +scaling gives a constant function. -/ +lemma aestronglyMeasurable_comp_const_smul {μ : Measure (Space d)} [μ.IsAddHaarMeasure] + (hf : AEStronglyMeasurable f μ) (c : ℝ) : + AEStronglyMeasurable (f ∘ fun k ↦ c • k) μ := by + rcases eq_or_ne c 0 with rfl | hc + · simpa [Function.comp_def] using aestronglyMeasurable_const + · exact hf.comp_quasiMeasurePreserving + ⟨measurable_const_smul _, by + rw [Measure.map_addHaar_smul μ hc] + exact Measure.smul_absolutelyContinuous⟩ + +/-- Membership: `ψ ∈ D(𝓓 f)` iff `𝓕ψ` lies in the domain of multiplication by the rescaled symbol. -/ lemma mem_derivOperator_domain_iff {ψ : SpaceDHilbertSpace d} : - ψ ∈ (derivOperator f).domain - ↔ fourierUnitary d ψ ∈ (𝓜 volume fun ξ => f ((2 * Real.pi) • ξ)).domain := Iff.rfl + ψ ∈ (𝓓 f).domain ↔ 𝓕 ψ ∈ (𝓜 volume (f ∘ fun k ↦ (2 * π) • k)).domain := Iff.rfl -/-- The defining formula: `derivOperator f ψ = 𝓕⁻¹ ((f ∘ 2π•) · 𝓕ψ)`. -/ -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 - -/-- The derivative operator is densely defined. -/ -lemma derivOperator_hasDenseDomain (hf : AEStronglyMeasurable f volume) : - (derivOperator f).HasDenseDomain := - (mulOperator_hasDenseDomain (aestronglyMeasurable_comp_two_pi_smul hf)).unitaryConj_dense_domain - -/-- The adjoint of a derivative operator is the derivative operator of the conjugate symbol: -`(derivOperator f)† = derivOperator (conj ∘ f)`. -/ -lemma derivOperator_adjoint (hf : AEStronglyMeasurable f volume) : - (derivOperator f)† = derivOperator (conj ∘ f) := by - rw [derivOperator, unitaryConj_adjoint _ - (mulOperator_hasDenseDomain (aestronglyMeasurable_comp_two_pi_smul hf)), - mulOperator_adjoint_eq_conj (aestronglyMeasurable_comp_two_pi_smul hf)] - rfl - -/-- The derivative operator of a real-valued symbol is self-adjoint on its maximal domain. -/ -lemma derivOperator_isSelfAdjoint (hf : AEStronglyMeasurable f volume) - (hf' : conj ∘ f = f) : IsSelfAdjoint (derivOperator f) := - LinearPMap.unitaryConj_isSelfAdjoint (fourierUnitary d).symm - (mulOperator_isSelfAdjoint_ofReal (aestronglyMeasurable_comp_two_pi_smul hf) - (funext fun ξ => congrFun hf' ((2 * Real.pi) • ξ))) +/-- The defining formula: `𝓓 f ψ = 𝓕⁻¹ ((f ∘ 2π•) · 𝓕ψ)`. -/ +lemma derivOperator_apply (ψ : (𝓓 f).domain) : + 𝓓 f ψ = + 𝓕⁻ ((𝓜 volume (f ∘ fun k ↦ (2 * π) • k)) ⟨𝓕 ψ.1, mem_derivOperator_domain_iff.mp ψ.2⟩) := rfl /-! -## B. The Schwartz submodule in the domain +## B.1. Domain -/ +/-- The derivative operator is densely defined. -/ +lemma derivOperator_hasDenseDomain (hf : AEStronglyMeasurable f volume) : + (𝓓 f).HasDenseDomain := + (mulOperator_hasDenseDomain + (aestronglyMeasurable_comp_const_smul hf (2 * π))).unitaryConj_dense_domain + /-- For a temperate-growth symbol the Schwartz submodule lies in the domain of the derivative operator. -/ lemma schwartzSubmodule_le_derivOperator_domain (hf : f.HasTemperateGrowth) : - SchwartzSubmodule d ≤ (derivOperator f).domain := + SchwartzSubmodule d ≤ (𝓓 f).domain := fun _ hψ => mem_derivOperator_domain_iff.mpr (mulOperator_domain_ge_of_hasTemperateGrowth (by fun_prop) volume (fourierUnitary_map_schwartzSubmodule ▸ Submodule.mem_map_of_mem hψ)) +/-! +## B.2. Adjoints +-/ + +/-- The adjoint of a derivative operator is the derivative operator of the conjugate symbol: +`(𝓓 f)† = 𝓓 (conj ∘ f)`. -/ +lemma derivOperator_adjoint (hf : AEStronglyMeasurable f volume) : + (𝓓 f)† = 𝓓 (conj ∘ f) := by + simp only [derivOperator_eq, aestronglyMeasurable_comp_const_smul hf, unitaryConj_adjoint, + mulOperator_adjoint_eq_conj, Function.comp_assoc] + +/-- The derivative operator of a real-valued symbol is self-adjoint on its maximal domain. -/ +lemma derivOperator_isSelfAdjoint (hf : AEStronglyMeasurable f volume) + (hf' : conj ∘ f = f) : IsSelfAdjoint (𝓓 f) := + LinearPMap.unitaryConj_isSelfAdjoint (fourierUnitary d).symm + (mulOperator_isSelfAdjoint_ofReal (aestronglyMeasurable_comp_const_smul hf (2 * π)) + (funext fun ξ => congrFun hf' ((2 * π) • ξ))) + end end SpaceDHilbertSpace end QuantumMechanics diff --git a/Physlib/QuantumMechanics/Operators/Unbounded.lean b/Physlib/QuantumMechanics/Operators/Unbounded.lean index a38bd0842..f8fbae341 100644 --- a/Physlib/QuantumMechanics/Operators/Unbounded.lean +++ b/Physlib/QuantumMechanics/Operators/Unbounded.lean @@ -659,18 +659,52 @@ preimage of a dense set under a homeomorphism. -/ lemma HasDenseDomain.unitaryConj_dense_domain (hdense : A.HasDenseDomain) : (unitaryConj u A).HasDenseDomain := hdense.preimage u.symm.toHomeomorph.isOpenMap -/-- Unitary conjugation commutes with the adjoint `(u A u⁻¹)† = u A† u⁻¹` for a densely defined `A`. --/ -lemma unitaryConj_adjoint - [CompleteSpace H] [CompleteSpace H'] (u : H ≃ₗᵢ[ℂ] H') (hdense : A.HasDenseDomain) : +/-- The conjugated operator `u A u⁻¹` is densely defined iff `A` is: its domain is the preimage +of `D(A)` under the homeomorphism `u⁻¹`. -/ +@[simp] +lemma unitaryConj_hasDenseDomain_iff : + (unitaryConj u A).HasDenseDomain ↔ A.HasDenseDomain := + ⟨fun h ↦ by simpa using h.unitaryConj_dense_domain (u := u.symm), + fun h ↦ h.unitaryConj_dense_domain⟩ + +/-- Unitary conjugation commutes with the adjoint: `(u A u⁻¹)† = u A† u⁻¹`. -/ +@[simp] +lemma unitaryConj_adjoint [CompleteSpace H] [CompleteSpace H'] (u : H ≃ₗᵢ[ℂ] H') : (unitaryConj u A)† = unitaryConj u A† := by - have hd' : (unitaryConj u A).HasDenseDomain := hdense.unitaryConj_dense_domain - refine le_antisymm ?_ (((adjoint_isFormalAdjoint hdense).symm.unitaryConj).le_adjoint hd') - have h₁ : unitaryConj u.symm ((unitaryConj u A)†) ≤ (unitaryConj u.symm (unitaryConj u A))† := - ((adjoint_isFormalAdjoint hd').symm.unitaryConj).le_adjoint hd'.unitaryConj_dense_domain - rw [unitaryConj_symm_unitaryConj] at h₁ - have h₂ := unitaryConj_mono u h₁ - rwa [unitaryConj_unitaryConj_symm] at h₂ + by_cases hdense : A.HasDenseDomain + · have hd' : (unitaryConj u A).HasDenseDomain := hdense.unitaryConj_dense_domain + refine le_antisymm ?_ (((adjoint_isFormalAdjoint hdense).symm.unitaryConj).le_adjoint hd') + have h₁ : unitaryConj u.symm ((unitaryConj u A)†) ≤ (unitaryConj u.symm (unitaryConj u A))† := + ((adjoint_isFormalAdjoint hd').symm.unitaryConj).le_adjoint hd'.unitaryConj_dense_domain + rw [unitaryConj_symm_unitaryConj] at h₁ + have h₂ := unitaryConj_mono u h₁ + rwa [unitaryConj_unitaryConj_symm] at h₂ + · have hnd : ¬(unitaryConj u A).HasDenseDomain := + fun hc ↦ hdense (unitaryConj_hasDenseDomain_iff.mp hc) + refine dExt ?_ fun x y hxy ↦ ?_ + · ext ξ + change Continuous (fun w : (unitaryConj u A).domain ↦ ⟪ξ, unitaryConj u A w⟫_ℂ) + ↔ Continuous (fun w : A.domain ↦ ⟪u.symm ξ, A w⟫_ℂ) + constructor + · intro hc + suffices hfun : (fun w : A.domain ↦ ⟪u.symm ξ, A w⟫_ℂ) + = (fun w : (unitaryConj u A).domain ↦ ⟪ξ, unitaryConj u A w⟫_ℂ) + ∘ fun w : A.domain ↦ (⟨u ↑w, map_mem_unitaryConj_domain u A w⟩ : + (unitaryConj u A).domain) by + rw [hfun] + exact hc.comp ((u.continuous.comp continuous_subtype_val).subtype_mk _) + funext w + simp [unitaryConj_apply_map, u.symm.inner_map_eq_flip] + · intro hc + suffices hfun : (fun w : (unitaryConj u A).domain ↦ ⟪ξ, unitaryConj u A w⟫_ℂ) + = (fun w : A.domain ↦ ⟪u.symm ξ, A w⟫_ℂ) + ∘ fun w : (unitaryConj u A).domain ↦ (⟨u.symm ↑w, w.2⟩ : A.domain) by + rw [hfun] + exact hc.comp ((u.symm.continuous.comp continuous_subtype_val).subtype_mk _) + funext w + simp [unitaryConj_apply, u.symm.inner_map_eq_flip] + · simp [adjoint_apply_of_not_dense hnd x, unitaryConj_apply, + adjoint_apply_of_not_dense hdense] /-- If `A - z` is surjective for a scalar `z : ℂ`, then so is `u A u⁻¹ - z`. -/ lemma unitaryConj_sub_smul_surjective {z : ℂ} (h : Function.Surjective (A - z • 1).toFun) :