noncomputable def ERealFunction.quadraticPerspectivePlusSquare : ℝ × ℝ → ↑(Set.Ioi ⊥)

Example 17.13: the counterexample function on ℝ² is f(ξ,η)=η^2+η^2/ξ for ξ > 0 and η ≥ 0, f(0,0)=0, and f=+∞ otherwise.

@[simp]

theorem ERealFunction.quadraticPerspectivePlusSquare_apply (p : ℝ × ℝ) : ↑(quadraticPerspectivePlusSquare p) = if 0 < p.1 ∧ 0 ≤ p.2 then ↑(p.2 ^ 2 + p.2 ^ 2 / p.1) else if p = (0, 0) then 0 else ⊤

Coercing the Example 17.13 function to EReal recovers its explicit piecewise formula.

theorem ERealFunction.quadraticPerspective_openFormula_contDiffOn : ContDiffOn ℝ 2 (fun (p : ℝ × ℝ) => p.2 ^ 2 + p.2 ^ 2 / p.1) (Set.Ioi 0 ×ˢ Set.Ioi 0)

The open-domain formula h(ξ,η)=η^2+η^2/ξ is twice Fréchet differentiable on ℝ_{++}^2 = ]0,+∞[ × ]0,+∞[.

theorem ERealFunction.quadraticPerspectivePlusSquare_mem_gammaZero : quadraticPerspectivePlusSquare ∈ Γ₀(ℝ × ℝ)

The Example 17.13 counterexample belongs to Γ₀(ℝ × ℝ).

theorem ERealFunction.quadraticPerspectivePlusSquare_not_strictlyConvex : ¬StrictlyConvex quadraticPerspectivePlusSquare

The Example 17.13 counterexample is not strictly convex.