noncomputable def ERealFunction.closedPerspectiveEReal {H : Type u} [AddCommGroup H] [Module ℝ H] (φ : H → ↑(Set.Ioi ⊥)) (hdom : (effectiveDomain φ).Nonempty) : ℝ × H → EReal

The closed perspective of φ as an extended-real-valued function: it agrees with the perspective away from the zero-height slice and takes the recession-function value at height 0. This construction only needs the effective domain of φ to be nonempty.

@[simp]

theorem ERealFunction.closedPerspectiveEReal_apply_zero {H : Type u} [AddCommGroup H] [Module ℝ H] (φ : H → ↑(Set.Ioi ⊥)) (hdom : (effectiveDomain φ).Nonempty) (x : H) : closedPerspectiveEReal φ hdom (0, x) = ↑(recessionFunction φ hdom x)

On the zero-height slice, the closed perspective equals the recession function.

theorem ERealFunction.closedPerspectiveEReal_apply_of_ne_zero {H : Type u} [AddCommGroup H] [Module ℝ H] (φ : H → ↑(Set.Ioi ⊥)) (hdom : (effectiveDomain φ).Nonempty) {ξ : ℝ} {x : H} (hξ : ξ ≠ 0) : closedPerspectiveEReal φ hdom (ξ, x) = perspective (fun (y : H) => ↑(φ y)) (ξ, x)

Away from the zero-height slice, the closed perspective agrees with the ordinary perspective.

theorem ERealFunction.closedPerspectiveEReal_ne_bot {H : Type u} [AddCommGroup H] [Module ℝ H] (φ : H → ↑(Set.Ioi ⊥)) (hdom : (effectiveDomain φ).Nonempty) (p : ℝ × H) : ⊥ < closedPerspectiveEReal φ hdom p

The closed perspective never takes the value -∞.

noncomputable def ERealFunction.closedPerspective {H : Type u} [AddCommGroup H] [Module ℝ H] (φ : H → ↑(Set.Ioi ⊥)) (hdom : (effectiveDomain φ).Nonempty) : ℝ × H → ↑(Set.Ioi ⊥)

The subtype-valued closed perspective associated with closedPerspectiveEReal.

@[simp]

theorem ERealFunction.closedPerspective_coe {H : Type u} [AddCommGroup H] [Module ℝ H] (φ : H → ↑(Set.Ioi ⊥)) (hdom : (effectiveDomain φ).Nonempty) (p : ℝ × H) : ↑(closedPerspective φ hdom p) = closedPerspectiveEReal φ hdom p

Coercing the closed perspective to EReal recovers the explicit closed-perspective formula.

@[implicit_reducible]

noncomputable def ERealFunction.scalar_prod_pseudoMetricSpace_l2 {H : Type u} [NormedAddCommGroup H] : PseudoMetricSpace (ℝ × H)

Helper for Proposition 9.42: view ℝ × H with the ℓ² product metric so the perspective slice lives in the intended Hilbert product space.

@[implicit_reducible]

noncomputable def ERealFunction.scalar_prod_normedAddCommGroup_l2 {H : Type u} [NormedAddCommGroup H] : NormedAddCommGroup (ℝ × H)

Helper for Proposition 9.42: equip ℝ × H with the ℓ² product norm.

@[implicit_reducible]

noncomputable def ERealFunction.scalar_prod_normedSpace_l2 {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] : NormedSpace ℝ (ℝ × H)

Helper for Proposition 9.42: the ℓ² product norm on ℝ × H is compatible with scalar multiplication.

theorem ERealFunction.scalar_prod_completeSpace_l2 {H : Type u} [NormedAddCommGroup H] [CompleteSpace H] : CompleteSpace (ℝ × H)

Helper for Proposition 9.42: completeness of ℝ × H for the ℓ² product metric follows from the uniform equivalence with WithLp 2 (ℝ × H).

@[implicit_reducible]

noncomputable def ERealFunction.scalar_prod_innerProductSpace_l2 {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] : InnerProductSpace ℝ (ℝ × H)

Helper for Proposition 9.42: the product Hilbert structure on ℝ × H is the textbook one ⟪(a, u), (b, v)⟫ = ab + ⟪u, v⟫.

@[implicit_reducible]

noncomputable def ERealFunction.perspective_prod_pseudoMetricSpace_l2 {H : Type u} [NormedAddCommGroup H] : PseudoMetricSpace ((ℝ × H) × ℝ)

Helper for Proposition 9.42: view ((ℝ × H) × ℝ) with the ℓ² product metric so Corollary 6.53 applies in the ambient Hilbert space of the perspective epigraph.

@[implicit_reducible]

noncomputable def ERealFunction.perspective_prod_normedAddCommGroup_l2 {H : Type u} [NormedAddCommGroup H] : NormedAddCommGroup ((ℝ × H) × ℝ)

Helper for Proposition 9.42: equip ((ℝ × H) × ℝ) with the ℓ² product norm.

@[implicit_reducible]

noncomputable def ERealFunction.perspective_prod_normedSpace_l2 {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] : NormedSpace ℝ ((ℝ × H) × ℝ)

Helper for Proposition 9.42: the ℓ² product norm on ((ℝ × H) × ℝ) is compatible with scalar multiplication.

theorem ERealFunction.perspective_prod_completeSpace_l2 {H : Type u} [NormedAddCommGroup H] [CompleteSpace H] : CompleteSpace ((ℝ × H) × ℝ)

Helper for Proposition 9.42: completeness of ((ℝ × H) × ℝ) for the ℓ² product metric again comes from its uniform equivalence with the corresponding WithLp product.

@[implicit_reducible]

noncomputable def ERealFunction.perspective_prod_innerProductSpace_l2 {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] : InnerProductSpace ℝ ((ℝ × H) × ℝ)

Helper for Proposition 9.42: the ambient Hilbert structure on ((ℝ × H) × ℝ) is the componentwise one from the textbook product space.

theorem ERealFunction.convex_epigraph_coe_of_convexOn_local {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {φ : H → ↑(Set.Ioi ⊥)} (hconv : ConvexOn φ (effectiveDomain φ)) : Convex ℝ (epigraph fun (x : H) => ↑(φ x))

Helper for Proposition 9.42: convexity on the effective domain of a ]-∞,+∞]-valued function yields convexity of its real-height epigraph after coercion to EReal.

theorem ERealFunction.mem_epigraph_toReal_of_mem_effectiveDomain {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {φ : H → ↑(Set.Ioi ⊥)} {x : H} (hx : x ∈ effectiveDomain φ) : (x, (↑(φ x)).toReal) ∈ epigraph fun (y : H) => ↑(φ y)

Helper for Proposition 9.42: every effective-domain point gives a canonical finite-height point of the real-height epigraph.

theorem ERealFunction.convex_perspectiveEpigraphSlice_of_convex_epigraph {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {F : H → EReal} (hF_conv : Convex ℝ (epigraph F)) : Convex ℝ (perspectiveEpigraphSlice F)

Helper for Proposition 9.42: the unit slice over a convex epigraph is convex.

theorem ERealFunction.isClosed_perspectiveEpigraphSlice_of_isClosed_epigraph {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {F : H → EReal} (hF_closed : IsClosed (epigraph F)) : IsClosed (perspectiveEpigraphSlice F)

Helper for Proposition 9.42: if the real-height epigraph of F is closed, then the fixed unit slice used for the perspective-cone description is also closed.

theorem ERealFunction.recessionCone_perspectiveEpigraphSlice_eq_zero_slice {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (F : H → EReal) (hF_nonempty : (epigraph F).Nonempty) : (perspectiveEpigraphSlice F).recessionCone = {p : (ℝ × H) × ℝ | p.1.1 = 0 ∧ (p.1.2, p.2) ∈ (epigraph F).recessionCone}

Helper for Proposition 9.42: the recession cone of the unit perspective slice consists precisely of the zero-height directions whose remaining coordinates lie in the recession cone of the original real-height epigraph.

theorem ERealFunction.epigraph_closedPerspectiveEReal_eq_perspective_union_zero_slice {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (φ : H → ↑(Set.Ioi ⊥)) (hdom : (effectiveDomain φ).Nonempty) : epigraph (closedPerspectiveEReal φ hdom) = epigraph (perspective fun (x : H) => ↑(φ x)) ∪ {p : (ℝ × H) × ℝ | p.1.1 = 0 ∧ (p.1.2, p.2) ∈ epigraph fun (y : H) => ↑(recessionFunction φ hdom y)}

Helper for Proposition 9.42: the epigraph of the closed perspective is the union of the ordinary perspective epigraph with the zero-height recession slice.

theorem ERealFunction.eq_of_epigraph_eq_of_forall_gt_bot {X : Type u} {f g : X → EReal} (hepigraph : epigraph f = epigraph g) (hf : ∀ (x : X), ⊥ < f x) : f = g

Helper for Proposition 9.42: equality of real-height epigraphs determines an EReal-valued function once one side is known never to take the value -∞.

theorem ERealFunction.lowerSemicontinuousEnvelope_perspective_eq_closedPerspectiveEReal {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (φ : H → ↑(Set.Ioi ⊥)) (hφ : φ ∈ Γ₀(H)) : lowerSemicontinuousEnvelope (perspective fun (x : H) => ↑(φ x)) = closedPerspectiveEReal φ ⋯

Proposition 9.42: for φ ∈ Γ₀(H), the lower semicontinuous envelope of the perspective of φ is the closed perspective obtained by inserting the recession function on the zero-height slice.

theorem ERealFunction.closedPerspective_mem_gammaZero {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (φ : H → ↑(Set.Ioi ⊥)) (hφ : φ ∈ Γ₀(H)) : closedPerspective φ ⋯ ∈ Γ₀(ℝ × H)

The closed perspective associated with a Γ₀(H) function belongs to Γ₀(ℝ × H).