@[reducible, inline]

noncomputable abbrev ERealFunction.prod_pseudoMetricSpace_l2 {H : Type u} {K : Type v} [NormedAddCommGroup H] [NormedAddCommGroup K] : PseudoMetricSpace (H × K)

Canonical raw-product ℓ² pseudometric bridge: view H × K with the metric transported from WithLp 2 (H × K). Downstream files activate it locally when they need the textbook Hilbert geometry on the raw product type.

@[reducible, inline]

noncomputable abbrev ERealFunction.prod_normedAddCommGroup_l2 {H : Type u} {K : Type v} [NormedAddCommGroup H] [NormedAddCommGroup K] : NormedAddCommGroup (H × K)

Canonical raw-product ℓ² norm bridge: equip H × K with the norm transported from WithLp 2 (H × K).

@[reducible, inline]

noncomputable abbrev ERealFunction.prod_seminormedAddCommGroup_l2 {H : Type u} {K : Type v} [NormedAddCommGroup H] [NormedAddCommGroup K] : SeminormedAddCommGroup (H × K)

Canonical raw-product ℓ² seminorm bridge on H × K. This is the primitive WithLp owner needed to derive the scalar-action structure.

@[implicit_reducible]

noncomputable def ERealFunction.prod_seminormedAddCommGroup_l2_inst {H : Type u} {K : Type v} [NormedAddCommGroup H] [NormedAddCommGroup K] : SeminormedAddCommGroup (H × K)

@[implicit_reducible]

noncomputable def ERealFunction.prod_normedAddCommGroup_l2_inst {H : Type u} {K : Type v} [NormedAddCommGroup H] [NormedAddCommGroup K] : NormedAddCommGroup (H × K)

@[reducible, inline]

noncomputable abbrev ERealFunction.prod_normedSpace_l2 {H : Type u} {K : Type v} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [NormedAddCommGroup K] [InnerProductSpace ℝ K] : NormedSpace ℝ (H × K)

Canonical raw-product ℓ² scalar-action bridge on H × K.

@[implicit_reducible]

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

@[reducible, inline]

noncomputable abbrev ERealFunction.prod_completeSpace_l2 {H : Type u} {K : Type v} [NormedAddCommGroup H] [NormedAddCommGroup K] [CompleteSpace H] [CompleteSpace K] : CompleteSpace (H × K)

Canonical raw-product ℓ² completeness bridge on H × K.

@[reducible, inline]

noncomputable abbrev ERealFunction.prod_innerProductSpace_l2 {H : Type u} {K : Type v} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [NormedAddCommGroup K] [InnerProductSpace ℝ K] : InnerProductSpace ℝ (H × K)

Canonical raw-product ℓ² Hilbert bridge on H × K, with inner product ⟪(u₁, v₁), (u₂, v₂)⟫ = ⟪u₁, u₂⟫ + ⟪v₁, v₂⟫.

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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

@[implicit_reducible]

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

theorem ERealFunction.convex_epigraph_of_mem_gammaZero {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {f : H → ↑(Set.Ioi ⊥)} (hf : f ∈ Γ₀(H)) : Convex ℝ (epigraph fun (y : H) => ↑(f y))

Helper for Proposition 9.18: Γ₀(H) convexity on the effective domain is equivalent to convexity of the real-height epigraph.

theorem ERealFunction.isChebyshev_epigraph_of_mem_gammaZero {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {f : H → ↑(Set.Ioi ⊥)} (hf : f ∈ Γ₀(H)) : IsChebyshev (epigraph fun (y : H) => ↑(f y))

The real-height epigraph of a Γ₀(H) function is a Chebyshev subset of H × ℝ.

theorem ERealFunction.eq_projectionPoint_epigraph_iff_max_le_and_variational_inequality_of_mem_gammaZero {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {f : H → ↑(Set.Ioi ⊥)} (hf : f ∈ Γ₀(H)) {x p : H} {ξ π : ℝ} : (p, π) = P[epigraph fun (y : H) => ↑(f y), ⋯] (x, ξ) ↔ max ↑ξ ↑(f p) ≤ ↑π ∧ ∀ y ∈ effectiveDomain f, inner ℝ (y - p) (x - p) + ((↑(f y)).toReal - π) * (ξ - π) ≤ 0

Proposition 9.18: for f ∈ Γ₀(H), a pair (p, π) is the metric projection of (x, ξ) onto the real-height epigraph of f if and only if π majorizes both ξ and f p, and the resulting variational inequality holds against every point of effectiveDomain f.