theorem
strictlyQuasiconvex_norm
{H : Type u}
[NormedAddCommGroup H]
[NormedSpace ℝ H]
[StrictConvexSpace ℝ H]
:
On a strictly convex real normed space, the norm is strictly quasiconvex.
theorem
strictlyQuasiconvex_norm_rpow
{H : Type u}
[NormedAddCommGroup H]
[NormedSpace ℝ H]
[StrictConvexSpace ℝ H]
(p : ℝ)
(hp : 0 < p)
:
ERealFunction.StrictlyQuasiconvex (Function.asEReal (Function.toEReal fun (x : H) => ‖x‖ ^ p))
Example 10.31 (1): clause (i). For p > 0, the norm-power function is strictly
quasiconvex.
theorem
not_convexOn_univ_norm_rpow_of_lt_one
{H : Type u}
[NormedAddCommGroup H]
[NormedSpace ℝ H]
[Nontrivial H]
(p : ℝ)
(hp : 0 < p)
(hp1 : p < 1)
:
¬ConvexOn ℝ Set.univ fun (x : H) => ‖x‖ ^ p
Example 10.31 (2): clause (ii), first part. If H is nontrivial and 0 < p < 1, then the
norm-power function is not convex on the whole space.
theorem
not_uniformlyQuasiconvex_norm_rpow_of_lt_one
{H : Type u}
[NormedAddCommGroup H]
[NormedSpace ℝ H]
[Nontrivial H]
(p : ℝ)
(hp : 0 < p)
(hp1 : p < 1)
:
¬∃ (φ : NNReal → EReal),
ERealFunction.UniformlyQuasiconvex (Function.asEReal (Function.toEReal fun (x : H) => ‖x‖ ^ p)) φ
Example 10.31 (3): clause (ii), second part. If H is nontrivial and 0 < p < 1, then the
norm-power function is not uniformly quasiconvex.