The diagonal operator on an ℓ² direct sum

Given a family of Hilbert spaces E i and a uniformly bounded family of operators T i : E i →L[𝕜] E i, the diagonal operator lpDiag T acts on the ℓ²-direct sum lp E 2 coordinatewise: (lpDiag T x) i = T i (x i). It is built from Memℓp.mono' (well-definedness) and LinearMap.mkContinuous (the operator-norm bound ‖lpDiag T‖ ≤ K).

This file records the *-algebra-hom laws of the diagonal operator, as a function of the family:

• lpDiag_apply_coe — the coordinate action;
• lpDiag_congr — the operator is independent of the chosen bound;
• lpDiag_one, lpDiag_mul, lpDiag_add, lpDiag_smul — the unital, multiplicative, additive, and 𝕜-linear laws;
• lpDiag_star — the adjoint of a diagonal is the diagonal of adjoints.

These are the pieces from which a direct-sum *-representation ⊕ᵢ πᵢ is assembled (the diagonal operator of fun i ↦ πᵢ a, uniformly bounded by ‖a‖). The file is spacetime/AQFT-agnostic.

noncomputable def Physicslib4.lpDiag {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace 𝕜 (E i)] (T : (i : ι) → E i →L[𝕜] E i) {K : ℝ} (hK : 0 ≤ K) (hTK : ∀ (i : ι), ‖T i‖ ≤ K) : ↥(lp E 2) →L[𝕜] ↥(lp E 2)

The diagonal operator on the ℓ²-direct sum lp E 2 induced by a uniformly bounded family T i : E i →L[𝕜] E i, acting coordinatewise.

Equations

• Physicslib4.lpDiag T hK hTK = { toFun := fun (x : ↥(lp E 2)) => ⟨fun (i : ι) => (T i) (↑x i), ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous K ⋯

@[simp]

theorem Physicslib4.lpDiag_apply_coe {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace 𝕜 (E i)] (T : (i : ι) → E i →L[𝕜] E i) {K : ℝ} (hK : 0 ≤ K) (hTK : ∀ (i : ι), ‖T i‖ ≤ K) (x : ↥(lp E 2)) (i : ι) : ↑((lpDiag T hK hTK) x) i = (T i) (↑x i)

theorem Physicslib4.lpDiag_congr {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace 𝕜 (E i)] (T : (i : ι) → E i →L[𝕜] E i) {K K' : ℝ} (hK : 0 ≤ K) (hK' : 0 ≤ K') (hTK : ∀ (i : ι), ‖T i‖ ≤ K) (hTK' : ∀ (i : ι), ‖T i‖ ≤ K') : lpDiag T hK hTK = lpDiag T hK' hTK'

The diagonal operator depends only on the family, not on the chosen bound.

theorem Physicslib4.lpDiag_ext {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace 𝕜 (E i)] {F G : ↥(lp E 2) →L[𝕜] ↥(lp E 2)} (h : ∀ (x : ↥(lp E 2)) (i : ι), ↑(F x) i = ↑(G x) i) : F = G

Coordinatewise extensionality for operators on lp E 2.

theorem Physicslib4.lpDiag_one {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace 𝕜 (E i)] : lpDiag (fun (i : ι) => 1) ⋯ ⋯ = 1

Diagonal of the identities is the identity.

theorem Physicslib4.lpDiag_mul {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace 𝕜 (E i)] (S T : (i : ι) → E i →L[𝕜] E i) {KS KT KST : ℝ} (hKS : 0 ≤ KS) (hKT : 0 ≤ KT) (hKST : 0 ≤ KST) (hSK : ∀ (i : ι), ‖S i‖ ≤ KS) (hTK : ∀ (i : ι), ‖T i‖ ≤ KT) (hSTK : ∀ (i : ι), ‖S i ∘SL T i‖ ≤ KST) : lpDiag (fun (i : ι) => S i ∘SL T i) hKST hSTK = lpDiag S hKS hSK ∘SL lpDiag T hKT hTK

The diagonal operator is multiplicative: the diagonal of the composites is the composite of the diagonals.

theorem Physicslib4.lpDiag_add {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace 𝕜 (E i)] (S T : (i : ι) → E i →L[𝕜] E i) {KS KT KST : ℝ} (hKS : 0 ≤ KS) (hKT : 0 ≤ KT) (hKST : 0 ≤ KST) (hSK : ∀ (i : ι), ‖S i‖ ≤ KS) (hTK : ∀ (i : ι), ‖T i‖ ≤ KT) (hSTK : ∀ (i : ι), ‖S i + T i‖ ≤ KST) : lpDiag (fun (i : ι) => S i + T i) hKST hSTK = lpDiag S hKS hSK + lpDiag T hKT hTK

The diagonal operator is additive.

theorem Physicslib4.lpDiag_smul {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace 𝕜 (E i)] (c : 𝕜) (T : (i : ι) → E i →L[𝕜] E i) {K KcT : ℝ} (hK : 0 ≤ K) (hKcT : 0 ≤ KcT) (hTK : ∀ (i : ι), ‖T i‖ ≤ K) (hcTK : ∀ (i : ι), ‖c • T i‖ ≤ KcT) : lpDiag (fun (i : ι) => c • T i) hKcT hcTK = c • lpDiag T hK hTK

The diagonal operator is 𝕜-linear in the family.

theorem Physicslib4.lpDiag_star {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace 𝕜 (E i)] [∀ (i : ι), CompleteSpace (E i)] (T : (i : ι) → E i →L[𝕜] E i) {K : ℝ} (hK : 0 ≤ K) (hTK : ∀ (i : ι), ‖T i‖ ≤ K) : star (lpDiag T hK hTK) = lpDiag (fun (i : ι) => star (T i)) hK ⋯

The adjoint of a diagonal operator is the diagonal of the adjoints.