feat(Analysis/InnerProductSpace/LinearPMap): the adjoint is closed (#…

…6537)

Define the graph of the adjoint and prove that the adjoint operator is always closed.

Mathlib/Analysis/InnerProductSpace/LinearPMap.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Moritz Doll
 -/
 import Mathlib.Analysis.InnerProductSpace.Adjoint
+import Mathlib.Analysis.InnerProductSpace.ProdL2
 import Mathlib.Topology.Algebra.Module.LinearPMap
 import Mathlib.Topology.Algebra.Module.Basic
 
@@ -27,6 +28,8 @@ We will develop the basics of the theory of unbounded operators on Hilbert space
 * `LinearPMap.IsFormalAdjoint.le_adjoint`: Every formal adjoint is contained in the adjoint
 * `ContinuousLinearMap.toPMap_adjoint_eq_adjoint_toPMap_of_dense`: The adjoint on
   `ContinuousLinearMap` and `LinearPMap` coincide.
+* `LinearPMap.adjoint_isClosed`: The adjoint is a closed operator.
+* `IsSelfAdjoint.isClosed`: Every self-adjoint operator is closed.
 
 ## Notation
 
@@ -51,7 +54,7 @@ Unbounded operators, closed operators
 
 noncomputable section
 
-open IsROrC
+open IsROrC LinearPMap
 
 open scoped ComplexConjugate Classical
 
@@ -268,3 +271,93 @@ theorem _root_.IsSelfAdjoint.dense_domain (hA : IsSelfAdjoint A) : Dense (A.doma
 end LinearPMap
 
 end Star
+
+/-! ### The graph of the adjoint -/
+
+namespace Submodule
+
+/-- The adjoint of a submodule
+
+Note that the adjoint is taken with respect to the L^2 inner product on `E × F`, which is defined
+as `WithLp 2 (E × F)`. -/
+protected noncomputable
+def adjoint (g : Submodule 𝕜 (E × F)) : Submodule 𝕜 (F × E) :=
+    (g.map <| (LinearEquiv.skewSwap 𝕜 F E).symm.trans
+      (WithLp.linearEquiv 2 𝕜 (F × E)).symm).orthogonal.map (WithLp.linearEquiv 2 𝕜 (F × E))
+
+@[simp]
+theorem mem_adjoint_iff (g : Submodule 𝕜 (E × F)) (x : F × E) :
+    x ∈ g.adjoint ↔
+    ∀ a b, (a, b) ∈ g → inner (𝕜 := 𝕜) b x.fst - inner a x.snd = 0 := by
+  simp only [Submodule.adjoint, Submodule.mem_map, Submodule.mem_orthogonal, LinearMap.coe_comp,
+    LinearEquiv.coe_coe, WithLp.linearEquiv_symm_apply, Function.comp_apply,
+    LinearEquiv.skewSwap_symm_apply, Prod.exists, WithLp.prod_inner_apply, forall_exists_index,
+    and_imp, WithLp.linearEquiv_apply]
+  constructor
+  · rintro ⟨y, h1, h2⟩ a b hab
+    rw [← h2, WithLp.equiv_fst, WithLp.equiv_snd]
+    specialize h1 (b, -a) a b hab rfl
+    simp only [inner_neg_left, ← sub_eq_add_neg] at h1
+    exact h1
+  · intro h
+    refine ⟨x, ?_, rfl⟩
+    intro u a b hab hu
+    simp [← hu, ← sub_eq_add_neg, h a b hab]
+
+variable {T : E →ₗ.[𝕜] F} [CompleteSpace E]
+
+theorem _root_.LinearPMap.adjoint_graph_eq_graph_adjoint (hT : Dense (T.domain : Set E)) :
+    T†.graph = T.graph.adjoint := by
+  ext x
+  simp only [mem_graph_iff, Subtype.exists, exists_and_left, exists_eq_left, mem_adjoint_iff,
+    forall_exists_index, forall_apply_eq_imp_iff']
+  constructor
+  · rintro ⟨hx, h⟩ a ha
+    rw [← h, (adjoint_isFormalAdjoint hT).symm ⟨a, ha⟩ ⟨x.fst, hx⟩, sub_self]
+  · intro h
+    simp_rw [sub_eq_zero] at h
+    have hx : x.fst ∈ T†.domain
+    · apply mem_adjoint_domain_of_exists
+      use x.snd
+      rintro ⟨a, ha⟩
+      rw [← inner_conj_symm, ← h a ha, inner_conj_symm]
+    use hx
+    apply hT.eq_of_inner_right
+    rintro ⟨a, ha⟩
+    rw [← h a ha, (adjoint_isFormalAdjoint hT).symm ⟨a, ha⟩ ⟨x.fst, hx⟩]
+
+@[simp]
+theorem _root_.LinearPMap.graph_adjoint_toLinearPMap_eq_adjoint (hT : Dense (T.domain : Set E)) :
+    T.graph.adjoint.toLinearPMap = T† := by
+  apply eq_of_eq_graph
+  rw [adjoint_graph_eq_graph_adjoint hT]
+  apply Submodule.toLinearPMap_graph_eq
+  intro x hx hx'
+  simp only [mem_adjoint_iff, mem_graph_iff, Subtype.exists, exists_and_left, exists_eq_left,
+    forall_exists_index, forall_apply_eq_imp_iff', hx', inner_zero_right, zero_sub,
+    neg_eq_zero] at hx
+  apply hT.eq_zero_of_inner_right
+  rintro ⟨a, ha⟩
+  exact hx a ha
+
+end Submodule
+
+/-! ### Closedness -/
+
+namespace LinearPMap
+
+variable {T : E →ₗ.[𝕜] F} [CompleteSpace E]
+
+theorem adjoint_isClosed (hT : Dense (T.domain : Set E)) :
+    T†.IsClosed := by
+  rw [IsClosed, adjoint_graph_eq_graph_adjoint hT, Submodule.adjoint]
+  simp only [Submodule.map_coe, WithLp.linearEquiv_apply]
+  rw [Equiv.image_eq_preimage]
+  exact (Submodule.isClosed_orthogonal _).preimage (WithLp.prod_continuous_equiv_symm _ _ _)
+
+/-- Every self-adjoint `LinearPMap` is closed. -/
+theorem _root_.IsSelfAdjoint.isClosed {A : E →ₗ.[𝕜] E} (hA : IsSelfAdjoint A) : A.IsClosed := by
+  rw [← isSelfAdjoint_def.mp hA]
+  exact adjoint_isClosed hA.dense_domain
+
+end LinearPMap

Mathlib/LinearAlgebra/Prod.lean

@@ -759,6 +759,36 @@ theorem snd_comp_prodComm :
 
 end prodComm
 
+section SkewSwap
+
+variable (R M N)
+variable [Semiring R]
+variable [AddCommGroup M] [AddCommGroup N]
+variable [Module R M] [Module R N]
+
+/-- The map `(x, y) ↦ (-y, x)` as a linear equivalence. -/
+protected def skewSwap : (M × N) ≃ₗ[R] (N × M) where
+  toFun x := (-x.2, x.1)
+  invFun x := (x.2, -x.1)
+  map_add' _ _ := by
+    simp [add_comm]
+  map_smul' _ _ := by
+    simp
+  left_inv _ := by
+    simp
+  right_inv _ := by
+    simp
+
+variable {R M N}
+
+@[simp]
+theorem skewSwap_apply (x : M × N) : LinearEquiv.skewSwap R M N x = (-x.2, x.1) := rfl
+
+@[simp]
+theorem skewSwap_symm_apply (x : N × M) : (LinearEquiv.skewSwap R M N).symm x = (x.2, -x.1) := rfl
+
+end SkewSwap
+
 section
 
 variable (R M M₂ M₃ M₄)