1. Physlib
  2. Mathematics
  3. InnerProductSpace
  4. Adjoint
Imports
/- Copyright (c) 2025 Tomas Skrivan. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Tomas Skrivan -/ module public import Physlib.Mathematics.InnerProductSpace.Basic public import Mathlib.Analysis.InnerProductSpace.Adjoint

Adjoint of a linear map

This module defines the adjoint of a linear map f : E → F where E and F carry the instances of InnerProductSpace' over a field 𝕜.

This is a generalization of the usual adjoint defined on InnerProductSpace for continuous linear maps.

@[expose] public sectionlocal notation "⟪" x ", " y "⟫" => inner 𝕜 x yAll goals completed! 🐙lemma HasAdjoint.adjoint_apply_zero {f : E → F} {f' : F → E} (hf : HasAdjoint 𝕜 f f') : f' 0 = 0 := 𝕜:Type u_1E:Type u_2F:Type u_3inst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 Einst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Ff:E → Ff':F → Ehf:HasAdjoint 𝕜 f f'⊢ f' 0 = 0 All goals completed! 🐙lemma HasAdjoint.adjoint {f : E → F} {f' : F → E} (hf : HasAdjoint 𝕜 f f') : adjoint 𝕜 f = f' := 𝕜:Type u_1E:Type u_2F:Type u_3inst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 Einst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Ff:E → Ff':F → Ehf:HasAdjoint 𝕜 f f'⊢ _root_.adjoint 𝕜 f = f' 𝕜:Type u_1E:Type u_2F:Type u_3inst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 Einst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Ff:E → Ff':F → Ehf:HasAdjoint 𝕜 f f'y:F⊢ _root_.adjoint 𝕜 f y = f' y 𝕜:Type u_1E:Type u_2F:Type u_3inst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 Einst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Ff:E → Ff':F → Ehf:HasAdjoint 𝕜 f f'y:F⊢ ∀ (v : E), ⟪_root_.adjoint 𝕜 f y, v⟫ = ⟪f' y, v⟫ 𝕜:Type u_1E:Type u_2F:Type u_3inst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 Einst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Ff:E → Ff':F → Ehf:HasAdjoint 𝕜 f f'y:F⊢ ∀ (v : E), ⟪(if h : ∃ f', HasAdjoint 𝕜 f f' then Classical.choose h else 0) y, v⟫ = ⟪f' y, v⟫ 𝕜:Type u_1E:Type u_2F:Type u_3inst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 Einst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Ff:E → Ff':F → Ehf:HasAdjoint 𝕜 f f'y:Fh:∃ f', HasAdjoint 𝕜 f f'⊢ ∀ (v : E), ⟪(if h : ∃ f', HasAdjoint 𝕜 f f' then Classical.choose h else 0) y, v⟫ = ⟪f' y, v⟫ 𝕜:Type u_1E:Type u_2F:Type u_3inst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 Einst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Ff:E → Ff':F → Ehf:HasAdjoint 𝕜 f f'y:Fh:∃ f', HasAdjoint 𝕜 f f'this:∀ (x : E) (y : F), ⟪h.choose y, x⟫ = ⟪y, f x⟫⊢ ∀ (v : E), ⟪(if h : ∃ f', HasAdjoint 𝕜 f f' then Classical.choose h else 0) y, v⟫ = ⟪f' y, v⟫ 𝕜:Type u_1E:Type u_2F:Type u_3inst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 Einst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Ff:E → Ff':F → Ehf:HasAdjoint 𝕜 f f'y:Fh:∃ f', HasAdjoint 𝕜 f f'this:∀ (x : E) (y : F), ⟪h.choose y, x⟫ = ⟪y, f x⟫⊢ ∀ (v : E), ⟪y, f v⟫ = ⟪f' y, v⟫ All goals completed! 🐙lemma HasAdjoint.congr_adj (f : E → F) (f' g') (adjoint : HasAdjoint 𝕜 f g') (eq : g' = f') : HasAdjoint 𝕜 f f' := 𝕜:Type u_1E:Type u_2F:Type u_3inst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 Einst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Ff:E → Ff':F → Eg':F → Eadjoint:HasAdjoint 𝕜 f g'eq:g' = f'⊢ HasAdjoint 𝕜 f f' All goals completed! 🐙lemma hasAdjoint_id : HasAdjoint 𝕜 (fun x : E => x) (fun x => x) := 𝕜:Type u_1E:Type u_2inst✝³:RCLike 𝕜inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Einst✝:InnerProductSpace' 𝕜 E⊢ HasAdjoint 𝕜 (fun x => x) fun x => x 𝕜:Type u_1E:Type u_2inst✝³:RCLike 𝕜inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Einst✝:InnerProductSpace' 𝕜 E⊢ ∀ (x y : E), ⟪y, x⟫ = ⟪y, x⟫; 𝕜:Type u_1E:Type u_2inst✝³:RCLike 𝕜inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace 𝕜 Einst✝:InnerProductSpace' 𝕜 Ex✝:Ey✝:E⊢ ⟪y✝, x✝⟫ = ⟪y✝, x✝⟫; All goals completed! 🐙lemma hasAdjoint_zero : HasAdjoint 𝕜 (fun _ : E => (0 : F)) (fun _ => 0) := 𝕜:Type u_1E:Type u_2F:Type u_3inst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 Einst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 F⊢ HasAdjoint 𝕜 (fun x => 0) fun x => 0 𝕜:Type u_1E:Type u_2F:Type u_3inst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 Einst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 F⊢ ∀ (x : E) (y : F), ⟪0, x⟫ = ⟪y, 0⟫; 𝕜:Type u_1E:Type u_2F:Type u_3inst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 Einst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Fx✝:Ey✝:F⊢ ⟪0, x✝⟫ = ⟪y✝, 0⟫; All goals completed! 🐙lemma HasAdjoint.comp {f : F → G} {g : E → F} {f' g'} (hf : HasAdjoint 𝕜 f f') (hg : HasAdjoint 𝕜 g g') : HasAdjoint 𝕜 (fun x : E => f (g x)) (fun x => g' (f' x)) := 𝕜:Type u_1E:Type u_2F:Type u_3G:Type u_4inst✝⁹:RCLike 𝕜inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 Einst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 Finst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:F → Gg:E → Ff':G → Fg':F → Ehf:HasAdjoint 𝕜 f f'hg:HasAdjoint 𝕜 g g'⊢ HasAdjoint 𝕜 (fun x => f (g x)) fun x => g' (f' x) 𝕜:Type u_1E:Type u_2F:Type u_3G:Type u_4inst✝⁹:RCLike 𝕜inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 Einst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 Finst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:F → Gg:E → Ff':G → Fg':F → Ehf:HasAdjoint 𝕜 f f'hg:HasAdjoint 𝕜 g g'⊢ ∀ (x : E) (y : G), ⟪g' (f' y), x⟫ = ⟪y, f (g x)⟫; 𝕜:Type u_1E:Type u_2F:Type u_3G:Type u_4inst✝⁹:RCLike 𝕜inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 Einst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 Finst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:F → Gg:E → Ff':G → Fg':F → Ehf:HasAdjoint 𝕜 f f'hg:HasAdjoint 𝕜 g g'x✝:Ey✝:G⊢ ⟪g' (f' y✝), x✝⟫ = ⟪y✝, f (g x✝)⟫; All goals completed! 🐙set_option backward.isDefEq.respectTransparency false in lemma HasAdjoint.prodMk {f : E → F} {g : E → G} {f' g'} (hf : HasAdjoint 𝕜 f f') (hg : HasAdjoint 𝕜 g g') : HasAdjoint 𝕜 (fun x : E => (f x, g x)) (fun yz => f' yz.1 + g' yz.2) := 𝕜:Type u_1E:Type u_2F:Type u_3G:Type u_4inst✝⁹:RCLike 𝕜inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 Einst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 Finst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → Fg:E → Gf':F → Eg':G → Ehf:HasAdjoint 𝕜 f f'hg:HasAdjoint 𝕜 g g'⊢ HasAdjoint 𝕜 (fun x => (f x, g x)) fun yz => f' yz.1 + g' yz.2 𝕜:Type u_1E:Type u_2F:Type u_3G:Type u_4inst✝⁹:RCLike 𝕜inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 Einst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 Finst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → Fg:E → Gf':F → Eg':G → Ehf:HasAdjoint 𝕜 f f'hg:HasAdjoint 𝕜 g g'⊢ ∀ (x : E) (y : F × G), ⟪f' y.1 + g' y.2, x⟫ = ⟪y, (f x, g x)⟫; 𝕜:Type u_1E:Type u_2F:Type u_3G:Type u_4inst✝⁹:RCLike 𝕜inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 Einst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 Finst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → Fg:E → Gf':F → Eg':G → Ehf:HasAdjoint 𝕜 f f'hg:HasAdjoint 𝕜 g g'x✝:Ey✝:F × G⊢ ⟪f' y✝.1 + g' y✝.2, x✝⟫ = ⟪y✝, (f x✝, g x✝)⟫ All goals completed! 🐙set_option backward.isDefEq.respectTransparency false in lemma HasAdjoint.fst {f : E → F×G} {f'} (hf : HasAdjoint 𝕜 f f') : HasAdjoint 𝕜 (fun x : E => (f x).1) (fun y => f' (y, 0)) := 𝕜:Type u_1E:Type u_2F:Type u_3G:Type u_4inst✝⁹:RCLike 𝕜inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 Einst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 Finst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → F × Gf':F × G → Ehf:HasAdjoint 𝕜 f f'⊢ HasAdjoint 𝕜 (fun x => (f x).1) fun y => f' (y, 0) 𝕜:Type u_1E:Type u_2F:Type u_3G:Type u_4inst✝⁹:RCLike 𝕜inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 Einst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 Finst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → F × Gf':F × G → Ehf:HasAdjoint 𝕜 f f'⊢ ∀ (x : E) (y : F), ⟪f' (y, 0), x⟫ = ⟪y, (f x).1⟫; 𝕜:Type u_1E:Type u_2F:Type u_3G:Type u_4inst✝⁹:RCLike 𝕜inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 Einst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 Finst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → F × Gf':F × G → Ehf:HasAdjoint 𝕜 f f'x✝:Ey✝:F⊢ ⟪f' (y✝, 0), x✝⟫ = ⟪y✝, (f x✝).1⟫ All goals completed! 🐙set_option backward.isDefEq.respectTransparency false in lemma HasAdjoint.snd {f : E → F×G} {f'} (hf : HasAdjoint 𝕜 f f') : HasAdjoint 𝕜 (fun x : E => (f x).2) (fun z => f' (0, z)) := 𝕜:Type u_1E:Type u_2F:Type u_3G:Type u_4inst✝⁹:RCLike 𝕜inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 Einst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 Finst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → F × Gf':F × G → Ehf:HasAdjoint 𝕜 f f'⊢ HasAdjoint 𝕜 (fun x => (f x).2) fun z => f' (0, z) 𝕜:Type u_1E:Type u_2F:Type u_3G:Type u_4inst✝⁹:RCLike 𝕜inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 Einst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 Finst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → F × Gf':F × G → Ehf:HasAdjoint 𝕜 f f'⊢ ∀ (x : E) (y : G), ⟪f' (0, y), x⟫ = ⟪y, (f x).2⟫; 𝕜:Type u_1E:Type u_2F:Type u_3G:Type u_4inst✝⁹:RCLike 𝕜inst✝⁸:NormedAddCommGroup Einst✝⁷:NormedSpace 𝕜 Einst✝⁶:InnerProductSpace' 𝕜 Einst✝⁵:NormedAddCommGroup Finst✝⁴:NormedSpace 𝕜 Finst✝³:InnerProductSpace' 𝕜 Finst✝²:NormedAddCommGroup Ginst✝¹:NormedSpace 𝕜 Ginst✝:InnerProductSpace' 𝕜 Gf:E → F × Gf':F × G → Ehf:HasAdjoint 𝕜 f f'x✝:Ey✝:G⊢ ⟪f' (0, y✝), x✝⟫ = ⟪y✝, (f x✝).2⟫ All goals completed! 🐙lemma HasAdjoint.neg {f : E → F} {f'} (hf : HasAdjoint 𝕜 f f') : HasAdjoint 𝕜 (fun x : E => -f x) (fun y => -f' y) := 𝕜:Type u_1E:Type u_2F:Type u_3inst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 Einst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Ff:E → Ff':F → Ehf:HasAdjoint 𝕜 f f'⊢ HasAdjoint 𝕜 (fun x => -f x) fun y => -f' y 𝕜:Type u_1E:Type u_2F:Type u_3inst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 Einst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Ff:E → Ff':F → Ehf:HasAdjoint 𝕜 f f'⊢ ∀ (x : E) (y : F), ⟪-f' y, x⟫ = ⟪y, -f x⟫; 𝕜:Type u_1E:Type u_2F:Type u_3inst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 Einst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Ff:E → Ff':F → Ehf:HasAdjoint 𝕜 f f'x✝:Ey✝:F⊢ ⟪-f' y✝, x✝⟫ = ⟪y✝, -f x✝⟫ All goals completed! 🐙lemma HasAdjoint.add {f g : E → F} {f' g'} (hf : HasAdjoint 𝕜 f f') (hg : HasAdjoint 𝕜 g g') : HasAdjoint 𝕜 (fun x : E => f x + g x) (fun y => f' y + g' y) := 𝕜:Type u_1E:Type u_2F:Type u_3inst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 Einst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Ff:E → Fg:E → Ff':F → Eg':F → Ehf:HasAdjoint 𝕜 f f'hg:HasAdjoint 𝕜 g g'⊢ HasAdjoint 𝕜 (fun x => f x + g x) fun y => f' y + g' y 𝕜:Type u_1E:Type u_2F:Type u_3inst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 Einst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Ff:E → Fg:E → Ff':F → Eg':F → Ehf:HasAdjoint 𝕜 f f'hg:HasAdjoint 𝕜 g g'⊢ ∀ (x : E) (y : F), ⟪f' y + g' y, x⟫ = ⟪y, f x + g x⟫; 𝕜:Type u_1E:Type u_2F:Type u_3inst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 Einst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Ff:E → Fg:E → Ff':F → Eg':F → Ehf:HasAdjoint 𝕜 f f'hg:HasAdjoint 𝕜 g g'x✝:Ey✝:F⊢ ⟪f' y✝ + g' y✝, x✝⟫ = ⟪y✝, f x✝ + g x✝⟫ All goals completed! 🐙lemma HasAdjoint.sub {f g : E → F} {f' g'} (hf : HasAdjoint 𝕜 f f') (hg : HasAdjoint 𝕜 g g') : HasAdjoint 𝕜 (fun x : E => f x - g x) (fun y => f' y - g' y) := 𝕜:Type u_1E:Type u_2F:Type u_3inst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 Einst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Ff:E → Fg:E → Ff':F → Eg':F → Ehf:HasAdjoint 𝕜 f f'hg:HasAdjoint 𝕜 g g'⊢ HasAdjoint 𝕜 (fun x => f x - g x) fun y => f' y - g' y 𝕜:Type u_1E:Type u_2F:Type u_3inst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 Einst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Ff:E → Fg:E → Ff':F → Eg':F → Ehf:HasAdjoint 𝕜 f f'hg:HasAdjoint 𝕜 g g'⊢ ∀ (x : E) (y : F), ⟪f' y - g' y, x⟫ = ⟪y, f x - g x⟫; 𝕜:Type u_1E:Type u_2F:Type u_3inst✝⁶:RCLike 𝕜inst✝⁵:NormedAddCommGroup Einst✝⁴:NormedSpace 𝕜 Einst✝³:InnerProductSpace' 𝕜 Einst✝²:NormedAddCommGroup Finst✝¹:NormedSpace 𝕜 Finst✝:InnerProductSpace' 𝕜 Ff:E → Fg:E → Ff':F → Eg':F → Ehf:HasAdjoint 𝕜 f f'hg:HasAdjoint 𝕜 g g'x✝:Ey✝:F⊢ ⟪f' y✝ - g' y✝, x✝⟫ = ⟪y✝, f x✝ - g x✝⟫ All goals completed! 🐙