theorem ERealFunction.dom_subset_dom_biconjugate_of_dom_conjugate_nonempty {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {f : H → EReal} (hdom : (dom (conjugate f)).Nonempty) : dom f ⊆ dom (conjugate (conjugate f))

Proposition 13.46 (1), left inclusion: if the Fenchel conjugate of an extended-real-valued function on a real Hilbert space has nonempty domain, then the domain of f is contained in the domain of f∗∗.

theorem ERealFunction.dom_biconjugate_subset_closure_dom_of_isConvex_of_dom_conjugate_nonempty {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {f : H → EReal} (hconv : IsConvex f) (hdom : (dom (conjugate f)).Nonempty) : dom (conjugate (conjugate f)) ⊆ closure (dom f)

Proposition 13.46 (1), right inclusion: for a convex extended-real-valued function on a real Hilbert space whose Fenchel conjugate has nonempty domain, the domain of f∗∗ is contained in the closure of the domain of f.

theorem ERealFunction.epigraph_biconjugate_eq_closure_epigraph_of_isConvex_of_dom_conjugate_nonempty {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {f : H → EReal} (hconv : IsConvex f) (hdom : (dom (conjugate f)).Nonempty) : epigraph (conjugate (conjugate f)) = closure (epigraph f)

Proposition 13.46 (2): for a convex extended-real-valued function on a real Hilbert space whose Fenchel conjugate has nonempty domain, equivalently which admits a continuous affine minorant, the epigraph of f∗∗ is the closure of the epigraph of f.

theorem ERealFunction.biconjugate_eq_liminfAt_of_isConvex_of_dom_conjugate_nonempty {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {f : H → EReal} (hconv : IsConvex f) (hdom : (dom (conjugate f)).Nonempty) (x : H) : conjugate (conjugate f) x = liminfAt f x

Proposition 13.46 (3): for a convex extended-real-valued function on a real Hilbert space whose Fenchel conjugate has nonempty domain, equivalently which admits a continuous affine minorant, the Fenchel biconjugate agrees pointwise with liminfAt f.