ConvexOn.uniformConvexOn_zero
theorem ConvexOn.uniformConvexOn_zero :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set E} {f : E → ℝ},
ConvexOn ℝ s f → UniformConvexOn s 0 f
This theorem, known as `ConvexOn.uniformConvexOn_zero`, states that for any normed additive commutative group `E` with a normed space over the real numbers, and for any set `s` of `E` and any function `f` mapping `E` to the real numbers, if the function `f` is convex on the set `s`, then `f` is uniformly convex on the set `s` at the point zero. This is an alias of the reverse direction of the `uniformConvexOn_zero` property. In other words, convexity of a function over a set implies its uniform convexity at zero.
More concisely: If a real-valued function on a normed additive commutative group is convex on a set, then it is uniformly convex at zero on that set.
|
ConcaveOn.uniformConcaveOn_zero
theorem ConcaveOn.uniformConcaveOn_zero :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set E} {f : E → ℝ},
ConcaveOn ℝ s f → UniformConcaveOn s 0 f
This theorem, named `ConcaveOn.uniformConcaveOn_zero`, states that for any set `s` of elements of type `E`, where `E` is a normed additive commutative group and also a normed space over the real numbers, and for any function `f` from `E` to the real numbers, if the function `f` is concave on the set `s` with respect to the real numbers, then `f` is uniformly concave on `s` with a uniformity parameter of `0`. In other words, if `f` is a concave function on `s`, then it satisfies a stronger property of uniform concavity with `0` as the uniformity parameter.
More concisely: If `f` is a concave function on the set `s` of a normed additive commutative group `E`, then `f` is uniformly concave on `s` with a uniformity parameter of 0.
|