def GeneralizedPerspectiveFunction.JointlyConvexOn {E : Type u_1} {F : Type u_2} {G : Type u_3} [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] [Preorder G] [AddCommMonoid G] [Module ℝ G] (s : Set E) (t : Set F) (Φ : E → F → G) : Prop

Joint convexity of a two-variable map on prescribed domains in each argument.

Equations

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

def GeneralizedPerspectiveFunction.JointlyConvex {E : Type u_1} {F : Type u_2} {G : Type u_3} [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] [Preorder G] [AddCommMonoid G] [Module ℝ G] (Φ : E → F → G) : Prop

Joint convexity of a two-variable map without domain restrictions.

Equations

• GeneralizedPerspectiveFunction.JointlyConvex Φ = GeneralizedPerspectiveFunction.JointlyConvexOn Set.univ Set.univ Φ

def GeneralizedPerspectiveFunction.JointlyConcaveOn {E : Type u_1} {F : Type u_2} {G : Type u_3} [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] [Preorder G] [AddCommMonoid G] [Module ℝ G] (s : Set E) (t : Set F) (Φ : E → F → G) : Prop

Joint concavity of a two-variable map on prescribed domains in each argument.

Equations

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

def GeneralizedPerspectiveFunction.JointlyConcave {E : Type u_1} {F : Type u_2} {G : Type u_3} [AddCommMonoid E] [Module ℝ E] [AddCommMonoid F] [Module ℝ F] [Preorder G] [AddCommMonoid G] [Module ℝ G] (Φ : E → F → G) : Prop

Joint concavity of a two-variable map without domain restrictions.

Equations

• GeneralizedPerspectiveFunction.JointlyConcave Φ = GeneralizedPerspectiveFunction.JointlyConcaveOn Set.univ Set.univ Φ

noncomputable def GeneralizedPerspectiveFunction.hSqrt {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] (h : ℝ → ℝ) (B : LownerHeinzTheorem.L ℋ) : LownerHeinzTheorem.L ℋ

The operator h(B)^(1/2) defined by real continuous functional calculus.

Equations

• GeneralizedPerspectiveFunction.hSqrt h B = LownerHeinzTheorem.cfcR (fun (x : ℝ) => h x ^ (1 / 2)) B

noncomputable def GeneralizedPerspectiveFunction.hInvSqrt {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] (h : ℝ → ℝ) (B : LownerHeinzTheorem.L ℋ) : LownerHeinzTheorem.L ℋ

The operator h(B)^(-1/2) defined by real continuous functional calculus.

Equations

• GeneralizedPerspectiveFunction.hInvSqrt h B = LownerHeinzTheorem.cfcR (fun (x : ℝ) => h x ^ (-1 / 2)) B

noncomputable def GeneralizedPerspectiveFunction.GeneralizedPerspective {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] (f h : ℝ → ℝ) (A B : LownerHeinzTheorem.L ℋ) : LownerHeinzTheorem.L ℋ

The generalized perspective function (fΔh)(A, B) = h(B)^(1/2) f(h(B)^(-1/2) A h(B)^(-1/2)) h(B)^(1/2).

This definition is intended to be used when A is Hermitian and h(B) is positive/invertible.

Equations

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

def GeneralizedPerspectiveFunction.term_Δ_ : Lean.TrailingParserDescr

Infix notation for generalized perspective: (f Δ h) A B = GeneralizedPerspective f h A B.

Equations

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

def GeneralizedPerspectiveFunction.psdSet {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] : Set (LownerHeinzTheorem.L ℋ)

Positive semidefinite operators.

Equations

• GeneralizedPerspectiveFunction.psdSet = {A : LownerHeinzTheorem.L ℋ | IsSelfAdjoint A ∧ spectrum ℝ A ⊆ Set.Ici 0}

def GeneralizedPerspectiveFunction.pdSet {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] : Set (LownerHeinzTheorem.L ℋ)

Strictly positive operators.

Equations

• GeneralizedPerspectiveFunction.pdSet = {A : LownerHeinzTheorem.L ℋ | IsSelfAdjoint A ∧ spectrum ℝ A ⊆ Set.Ioi 0}

theorem GeneralizedPerspectiveFunction.theorem_2_5_forward_jointlyConvexOn_psd_pd {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [Nontrivial ℋ] {f h : ℝ → ℝ} (hf : JensenOperatorInequality.CondIAll f) (hconc : LownerHeinzTheorem.OperatorConcaveOn (Set.Ioi 0) h) (hcont : ContinuousOn h (Set.Ioi 0)) (hpos : ∀ x ∈ Set.Ioi 0, 0 < h x) : JointlyConvexOn psdSet pdSet fun (A B : LownerHeinzTheorem.L ℋ) => GeneralizedPerspective f h A B

theorem GeneralizedPerspectiveFunction.theorem_2_5_forward_jointlyConvexOn_psd_pd_Ici {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [Nontrivial ℋ] {f h : ℝ → ℝ} (hf : JensenOperatorInequality.CondIciAll f) (hconc : LownerHeinzTheorem.OperatorConcaveOn (Set.Ioi 0) h) (hcont : ContinuousOn h (Set.Ioi 0)) (hpos : ∀ x ∈ Set.Ioi 0, 0 < h x) : JointlyConvexOn psdSet pdSet fun (A B : LownerHeinzTheorem.L ℋ) => GeneralizedPerspective f h A B

theorem GeneralizedPerspectiveFunction.theorem_2_6_forward_jointlyConcaveOn_psd_pd {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [Nontrivial ℋ] {f h : ℝ → ℝ} (hfconc : LownerHeinzTheorem.OperatorConcaveAll f) (hf0 : 0 ≤ f 0) (hconc : LownerHeinzTheorem.OperatorConcaveOn (Set.Ioi 0) h) (hcont : ContinuousOn h (Set.Ioi 0)) (hpos : ∀ x ∈ Set.Ioi 0, 0 < h x) : JointlyConcaveOn psdSet pdSet fun (A B : LownerHeinzTheorem.L ℋ) => GeneralizedPerspective f h A B

Restricted forward form of Corollary 2.6 on the positive cone.

theorem GeneralizedPerspectiveFunction.theorem_2_6_forward_jointlyConcaveOn_psd_pd_Ici {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [Nontrivial ℋ] {f h : ℝ → ℝ} (hfconc : LownerHeinzTheorem.OperatorConcaveOnAll (Set.Ici 0) f) (hfcont : ContinuousOn f (Set.Ici 0)) (hf0 : 0 ≤ f 0) (hconc : LownerHeinzTheorem.OperatorConcaveOn (Set.Ioi 0) h) (hcont : ContinuousOn h (Set.Ioi 0)) (hpos : ∀ x ∈ Set.Ioi 0, 0 < h x) : JointlyConcaveOn psdSet pdSet fun (A B : LownerHeinzTheorem.L ℋ) => GeneralizedPerspective f h A B

Restricted localized forward form of Corollary 2.6 on the positive cone.