@[simp]
theorem
mem_S0On_iff
{E : Type u}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{Q : Set E}
{μ : ℝ}
{f : E → ℝ}
:
f ∈ S0On μ Q ↔ 0 < μ ∧ StrongConvexOn Q μ f
The source-facing notation 𝒮^0_μ(Q) is the set view of positive-parameter strong convexity
on Q.
theorem
StrongConvexOnClass.mu_pos
{E : Type u}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{Q : Set E}
{μ : ℝ}
{f : E → ℝ}
(hf : f ∈ S0On μ Q)
:
0 < μ
Membership in 𝒮^0_μ(Q) forces positivity of the fixed strong-convexity parameter.
theorem
StrongConvexOnClass.strongConvexOn
{E : Type u}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{Q : Set E}
{μ : ℝ}
{f : E → ℝ}
(hf : f ∈ S0On μ Q)
:
StrongConvexOn Q μ f
Membership in 𝒮^0_μ(Q) includes the canonical strong-convexity owner on Q.
theorem
StrongConvexOn.mem_S0On
{E : Type u}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{Q : Set E}
{μ : ℝ}
{f : E → ℝ}
(hμ : 0 < μ)
(hf : StrongConvexOn Q μ f)
:
f ∈ S0On μ Q
A positive strong-convexity witness gives source-facing membership in 𝒮^0_μ(Q).