noncomputable def
ERealFunction.exactModulusOfConvexity
{H : Type u}
[NormedAddCommGroup H]
[NormedSpace ℝ H]
(f : H → ↑(Set.Ioi ⊥))
:
NNReal → EReal
Definition 10.11: for a proper convex ]-∞,+∞]-valued function, the exact modulus of
convexity assigns to each radius t ≥ 0 the infimum of the normalized Jensen gaps over all
effective-domain pairs at distance t and all coefficients α ∈ ]0,1[.
Instances For
theorem
ERealFunction.exactModulusOfConvexity_le_normalizedGap
{H : Type u}
[NormedAddCommGroup H]
[NormedSpace ℝ H]
(f : H → ↑(Set.Ioi ⊥))
{t : NNReal}
{x y : H}
(hx : x ∈ effectiveDomain f)
(hy : y ∈ effectiveDomain f)
(ht : ‖x - y‖₊ = t)
{α : ℝ}
(hα : α ∈ Set.Ioo 0 1)
:
exactModulusOfConvexity f t ≤ jensenGap f α x y / ↑(α * (1 - α))
The exact modulus of convexity is bounded above by every normalized Jensen gap realized at the given radius.