theorem fenchelConjugate_realPart_isSelfConcordantBarrierOnWith {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → WithTop ℝ} {ν : NNReal} (hdual_gradient_eq_hessian_apply_self : ∀ ⦃s : E⦄, s ∈ extendedRealEffectiveDomain (fenchelDual f) → gradient (extendedRealRealPart (fenchelDual f)) s = (hessian (extendedRealRealPart (fenchelDual f)) s) s) (hsc : IsStandardSelfConcordantOn (extendedRealEffectiveDomain (fenchelDual f)) (extendedRealRealPart (fenchelDual f))) (hbound : ∀ s ∈ extendedRealEffectiveDomain (fenchelDual f), inner ℝ s ((hessian (extendedRealRealPart (fenchelDual f)) s) s) ≤ ↑ν) : IsSelfConcordantBarrierOnWith (extendedRealEffectiveDomain (fenchelDual f)) ν (extendedRealRealPart (fenchelDual f))

Proposition 5.3.4: let F_* = extendedRealRealPart (f⋆). Assume the canonical dual satisfies relation (5.1.34), namely ∇F_*(s) = ∇²F_*(s) s, is standard self-concordant on dom (f⋆), and obeys ⟪s, ∇²F_*(s) s⟫ ≤ ν on dom (f⋆). Then F_* is a ν-self-concordant barrier on its effective domain.