@[reducible, inline]

abbrev JensenOperatorInequality.HSum (ℋ : Type u) [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] : Type u

A two-fold Hilbert sum used for the block-operator proof of Jensen's inequality.

Equations

• JensenOperatorInequality.HSum ℋ = PiLp 2 fun (x : Fin 2) => ℋ

noncomputable def JensenOperatorInequality.hsumEquiv (ℋ : Type u) [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] : HSum ℋ ≃L[ℂ] Fin 2 → ℋ

Equations

• JensenOperatorInequality.hsumEquiv ℋ = PiLp.continuousLinearEquiv 2 ℂ fun (x : Fin 2) => ℋ

noncomputable def JensenOperatorInequality.hsumProj (ℋ : Type u) [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] (i : Fin 2) : HSum ℋ →L[ℂ] ℋ

Equations

• JensenOperatorInequality.hsumProj ℋ i = (ContinuousLinearMap.proj i).comp ↑(JensenOperatorInequality.hsumEquiv ℋ)

noncomputable def JensenOperatorInequality.hsumIncl (ℋ : Type u) [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] (i : Fin 2) : ℋ →L[ℂ] HSum ℋ

Equations

• JensenOperatorInequality.hsumIncl ℋ i = (↑(JensenOperatorInequality.hsumEquiv ℋ).symm).comp (ContinuousLinearMap.single ℂ (fun (x : Fin 2) => ℋ) i)

@[simp]

theorem JensenOperatorInequality.hsumProj_hsumIncl_apply {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] (i j : Fin 2) (x : ℋ) : (hsumProj ℋ i) ((hsumIncl ℋ j) x) = if i = j then x else 0

@[simp]

theorem JensenOperatorInequality.inner_hsumIncl_hsumIncl {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] (i j : Fin 2) (x y : ℋ) : inner ℂ ((hsumIncl ℋ i) x) ((hsumIncl ℋ j) y) = if i = j then inner ℂ x y else 0

@[simp]

theorem JensenOperatorInequality.hsumIncl_adjoint {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] (i : Fin 2) : ContinuousLinearMap.adjoint (hsumIncl ℋ i) = hsumProj ℋ i

@[simp]

theorem JensenOperatorInequality.hsumProj_adjoint {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] (i : Fin 2) : ContinuousLinearMap.adjoint (hsumProj ℋ i) = hsumIncl ℋ i

@[simp]

theorem JensenOperatorInequality.hsumIncl_proj_sum {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] (z : HSum ℋ) : (hsumIncl ℋ 0) ((hsumProj ℋ 0) z) + (hsumIncl ℋ 1) ((hsumProj ℋ 1) z) = z

noncomputable def JensenOperatorInequality.blockDiagonal {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] (A B : LownerHeinzTheorem.L ℋ) : LownerHeinzTheorem.L (HSum ℋ)

The block diagonal operator diag(A, B) on the two-fold Hilbert sum.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def JensenOperatorInequality.blockOp {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] (A00 A01 A10 A11 : LownerHeinzTheorem.L ℋ) : LownerHeinzTheorem.L (HSum ℋ)

A general 2 × 2 block operator on HSum ℋ.

Equations

• One or more equations did not get rendered due to their size.

theorem JensenOperatorInequality.blockOp_ext {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] {T S : LownerHeinzTheorem.L (HSum ℋ)} (h0 : ∀ (z : HSum ℋ), (hsumProj ℋ 0) (T z) = (hsumProj ℋ 0) (S z)) (h1 : ∀ (z : HSum ℋ), (hsumProj ℋ 1) (T z) = (hsumProj ℋ 1) (S z)) : T = S

@[simp]

theorem JensenOperatorInequality.blockDiagonal_star {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] (A B : LownerHeinzTheorem.L ℋ) : star (blockDiagonal A B) = blockDiagonal (star A) (star B)

noncomputable def JensenOperatorInequality.blockDiagonalHom {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] : LownerHeinzTheorem.L ℋ × LownerHeinzTheorem.L ℋ →⋆ₐ[ℝ] LownerHeinzTheorem.L (HSum ℋ)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem JensenOperatorInequality.blockDiagonalHom_apply {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] (p : LownerHeinzTheorem.L ℋ × LownerHeinzTheorem.L ℋ) : blockDiagonalHom p = blockDiagonal p.1 p.2

@[simp]

theorem JensenOperatorInequality.hsumProj_blockDiagonal_zero {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] (A B : LownerHeinzTheorem.L ℋ) (z : HSum ℋ) : (hsumProj ℋ 0) ((blockDiagonal A B) z) = A ((hsumProj ℋ 0) z)

@[simp]

theorem JensenOperatorInequality.hsumProj_blockDiagonal_one {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] (A B : LownerHeinzTheorem.L ℋ) (z : HSum ℋ) : (hsumProj ℋ 1) ((blockDiagonal A B) z) = B ((hsumProj ℋ 1) z)

@[simp]

theorem JensenOperatorInequality.blockDiagonal_one {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] : blockDiagonal 1 1 = 1

theorem JensenOperatorInequality.blockDiagonal_nonneg {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] {A B : LownerHeinzTheorem.L ℋ} (hA : 0 ≤ A) (hB : 0 ≤ B) : 0 ≤ blockDiagonal A B

@[simp]

theorem JensenOperatorInequality.hsumProj_blockOp_zero {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] (A00 A01 A10 A11 : LownerHeinzTheorem.L ℋ) (z : HSum ℋ) : (hsumProj ℋ 0) ((blockOp A00 A01 A10 A11) z) = A00 ((hsumProj ℋ 0) z) + A01 ((hsumProj ℋ 1) z)

@[simp]

theorem JensenOperatorInequality.hsumProj_blockOp_one {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] (A00 A01 A10 A11 : LownerHeinzTheorem.L ℋ) (z : HSum ℋ) : (hsumProj ℋ 1) ((blockOp A00 A01 A10 A11) z) = A10 ((hsumProj ℋ 0) z) + A11 ((hsumProj ℋ 1) z)

@[simp]

theorem JensenOperatorInequality.blockOp_star {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] (A00 A01 A10 A11 : LownerHeinzTheorem.L ℋ) : star (blockOp A00 A01 A10 A11) = blockOp (star A00) (star A10) (star A01) (star A11)