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.

structure HasAdjoint (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] (f : E → F) (f' : F → E) : Prop

Adjoint of a linear map f such that ∀ x y, ⟪adjoint 𝕜 f y, x⟫ = ⟪y, f x⟫.

This computes adjoint of a linear map the same way as ContinuousLinearMap.adjoint but it is defined over InnerProductSpace', which is a generalization of InnerProductSpace that provides instances for products and function types. These instances make it easier to perform computations compared to using the standard InnerProductSpace class.

• adjoint_inner_left (x : E) (y : F) : inner 𝕜 (f' y) x = inner 𝕜 y (f x)

noncomputable def adjoint (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] (f : E → F) : F → E

Adjoint of a linear map f such that ∀ x y, ⟪adjoint 𝕜 f y, x⟫ = ⟪y, f x⟫.

This computes adjoint of a linear map the same way as ContinuousLinearMap.adjoint but it is defined over InnerProductSpace', which is a generalization of InnerProductSpace that provides instances for products and function types. These instances make it easier to perform computations compared to using the standard InnerProductSpace class.

Equations

• adjoint 𝕜 f = if h : ∃ (f' : F → E), HasAdjoint 𝕜 f f' then Classical.choose h else 0

theorem HasAdjoint.adjoint_inner_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] {f' : F → E} {x : E} {y : F} {f : E → F} (hf : HasAdjoint 𝕜 f f') : inner 𝕜 x (f' y) = inner 𝕜 (f x) y

theorem ContinuousLinearMap.hasAdjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] [CompleteSpace E] [CompleteSpace F] (f : E →L[𝕜] F) : HasAdjoint 𝕜 ⇑f fun (y : F) => (InnerProductSpace'.fromL2 𝕜) ((adjoint ((InnerProductSpace'.toL2 𝕜).comp (f.comp (InnerProductSpace'.fromL2 𝕜)))) ((InnerProductSpace'.toL2 𝕜) y))

theorem adjoint_eq_clm_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] [CompleteSpace E] [CompleteSpace F] (f : E →L[𝕜] F) : adjoint 𝕜 ⇑f = ⇑((InnerProductSpace'.fromL2 𝕜).comp ((ContinuousLinearMap.adjoint ((InnerProductSpace'.toL2 𝕜).comp (f.comp (InnerProductSpace'.fromL2 𝕜)))).comp (InnerProductSpace'.toL2 𝕜)))

theorem HasAdjoint.adjoint_apply_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] {f : E → F} {f' : F → E} (hf : HasAdjoint 𝕜 f f') : f' 0 = 0

theorem HasAdjoint.adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] {f : E → F} {f' : F → E} (hf : HasAdjoint 𝕜 f f') : _root_.adjoint 𝕜 f = f'

theorem HasAdjoint.congr_adj {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] (f : E → F) (f' g' : F → E) (adjoint : HasAdjoint 𝕜 f g') (eq : g' = f') : HasAdjoint 𝕜 f f'

theorem hasAdjoint_id {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] : HasAdjoint 𝕜 (fun (x : E) => x) fun (x : E) => x

theorem hasAdjoint_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] : HasAdjoint 𝕜 (fun (x : E) => 0) fun (x : F) => 0

theorem HasAdjoint.comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [InnerProductSpace' 𝕜 G] {f : F → G} {g : E → F} {f' : G → F} {g' : F → E} (hf : HasAdjoint 𝕜 f f') (hg : HasAdjoint 𝕜 g g') : HasAdjoint 𝕜 (fun (x : E) => f (g x)) fun (x : G) => g' (f' x)

theorem HasAdjoint.prodMk {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [InnerProductSpace' 𝕜 G] {f : E → F} {g : E → G} {f' : F → E} {g' : G → E} (hf : HasAdjoint 𝕜 f f') (hg : HasAdjoint 𝕜 g g') : HasAdjoint 𝕜 (fun (x : E) => (f x, g x)) fun (yz : F × G) => f' yz.1 + g' yz.2

theorem HasAdjoint.fst {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [InnerProductSpace' 𝕜 G] {f : E → F × G} {f' : F × G → E} (hf : HasAdjoint 𝕜 f f') : HasAdjoint 𝕜 (fun (x : E) => (f x).1) fun (y : F) => f' (y, 0)

theorem HasAdjoint.snd {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [InnerProductSpace' 𝕜 G] {f : E → F × G} {f' : F × G → E} (hf : HasAdjoint 𝕜 f f') : HasAdjoint 𝕜 (fun (x : E) => (f x).2) fun (z : G) => f' (0, z)

theorem HasAdjoint.neg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] {f : E → F} {f' : F → E} (hf : HasAdjoint 𝕜 f f') : HasAdjoint 𝕜 (fun (x : E) => -f x) fun (y : F) => -f' y

theorem HasAdjoint.add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] {f g : E → F} {f' g' : F → E} (hf : HasAdjoint 𝕜 f f') (hg : HasAdjoint 𝕜 g g') : HasAdjoint 𝕜 (fun (x : E) => f x + g x) fun (y : F) => f' y + g' y

theorem HasAdjoint.sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] {f g : E → F} {f' g' : F → E} (hf : HasAdjoint 𝕜 f f') (hg : HasAdjoint 𝕜 g g') : HasAdjoint 𝕜 (fun (x : E) => f x - g x) fun (y : F) => f' y - g' y

theorem HasAdjoint.smul_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] {f : E → F} {f' : F → E} (c : 𝕜) (hf : HasAdjoint 𝕜 f f') : HasAdjoint 𝕜 (fun (x : E) => c • f x) fun (y : F) => (starRingEnd 𝕜) c • f' y

theorem HasAdjoint.smul_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [InnerProductSpace' 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [InnerProductSpace' 𝕜 F] {f : E → 𝕜} {f' : 𝕜 → E} (v : F) (hf : HasAdjoint 𝕜 f f') : HasAdjoint 𝕜 (fun (x : E) => f x • v) fun (y : F) => f' ((starRingEnd 𝕜) (inner 𝕜 y v))