noncomputable def OperatorGeometricMean.operatorPowerMean {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] (α β : ℝ) (A B : LownerHeinzTheorem.L ℋ) : LownerHeinzTheorem.L ℋ

The operator (α, β)-power mean, realized as a generalized perspective.

Equations

• OperatorGeometricMean.operatorPowerMean α β A B = GeneralizedPerspectiveFunction.GeneralizedPerspective (fun (x : ℝ) => x ^ α) (fun (x : ℝ) => x ^ β) A B

theorem OperatorGeometricMean.operatorPowerMean_jointlyConcaveOn_pdSet {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [Nontrivial ℋ] {α β : ℝ} (hα : α ∈ Set.Icc 0 1) (hβ : β ∈ Set.Icc 0 1) : GeneralizedPerspectiveFunction.JointlyConcaveOn GeneralizedPerspectiveFunction.pdSet GeneralizedPerspectiveFunction.pdSet (operatorPowerMean α β)

Theorem 1.1, concave range: the operator (α, β)-power mean is jointly concave on strictly positive operators for 0 ≤ α, β ≤ 1.

theorem OperatorGeometricMean.operatorPowerMean_jointlyConvexOn_pdSet {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [Nontrivial ℋ] {α β : ℝ} (hα : α ∈ Set.Icc 1 2) (hβ : β ∈ Set.Icc 0 1) : GeneralizedPerspectiveFunction.JointlyConvexOn GeneralizedPerspectiveFunction.pdSet GeneralizedPerspectiveFunction.pdSet (operatorPowerMean α β)

Theorem 1.1, convex range: the operator (α, β)-power mean is jointly convex on strictly positive operators for 1 ≤ α ≤ 2 and 0 ≤ β ≤ 1.