theorem ERealFunction.coercive_tfae_lowerLevelSet_asymptoticSlope_affineLowerBound_conjugate {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (f : H → ↑(Set.Ioi ⊥)) (hf : f ∈ Γ₀(H)) : [Coercive (Function.asEReal f), ∀ (ξ : ℝ), Bornology.IsBounded (lowerLevelSet (Function.asEReal f) ξ), ↑0 < Filter.liminf (fun (x : H) => Function.asEReal f x / ↑‖x‖) (Filter.comap (fun (x : H) => ‖x‖) Filter.atTop), ∃ (α : ↑(Set.Ioi 0)) (β : ℝ), (Function.asEReal (scaledNormKernelOfPos α) + fun (x : H) => ↑β) ≤ Function.asEReal f, ∃ (ε : ↑(Set.Ioi 0)) (γ : ℝ), ∀ u ∈ Metric.closedBall 0 ↑ε, conjugate (Function.asEReal f) u ≤ ↑γ, 0 ∈ interior (dom (conjugate (Function.asEReal f)))].TFAE

Proposition 14.16: for f ∈ Γ₀(H), the following are equivalent: f is coercive; every real lower level set of f is bounded; the asymptotic quotient f(x) / ‖x‖ has strictly positive liminf at infinity; f admits a global affine lower bound of the form α ‖x‖ + β with α > 0; the Fenchel conjugate f* is bounded above on some closed ball around 0 (equivalently, on some neighborhood of 0); and 0 belongs to the interior of its domain.