strictConvexOn_zpow
theorem strictConvexOn_zpow : ∀ {m : ℤ}, m ≠ 0 → m ≠ 1 → StrictConvexOn ℝ (Set.Ioi 0) fun x => x ^ m
The theorem `strictConvexOn_zpow` states that for any integer `m` that is not `0` or `1`, the function `f(x) = x^m` is strictly convex on the interval `(0, +∞)`. In other words, for any two distinct points `x` and `y` in the interval `(0, +∞)`, and any two positive real numbers `a` and `b` such that `a + b = 1`, we have that `f(a*x + b*y) < a*f(x) + b*f(y)`. Here, `f(a*x + b*y)` is the function value at the convex combination of `x` and `y`, and `a*f(x) + b*f(y)` is the same convex combination of the function values at `x` and `y`. This property is a strict version of the definition of convexity, meaning that the function lies strictly below the line segment connecting `(x, f(x))` and `(y, f(y))` for any `x` and `y` in the interval `(0, +∞)`.
More concisely: For any integer `m` not equal to `0` or `1`, the function `x => x^m` is strictly convex on the interval `(0, +∞)`, meaning that for any distinct `x, y` in this interval and any `a, b > 0 with a + b = 1`, `(a*x^m + b*y^m) < a*x^m + b*y^m`.
|
strictConvexOn_pow
theorem strictConvexOn_pow : ∀ {n : ℕ}, 2 ≤ n → StrictConvexOn ℝ (Set.Ici 0) fun x => x ^ n
The theorem `strictConvexOn_pow` states that the function `x^n`, where `n` is a natural number, is strictly convex on the interval [0, +∞). This holds for all `n` that are greater than or equal to 2. In mathematical terms, for any two distinct points `x` and `y` in the interval [0, +∞) and for any positive real numbers `a` and `b` such that `a + b = 1`, the value of the function at the point `a*x + b*y` is strictly less than `a*f(x) + b*f(y)`, where `f(x)` is `x^n`.
More concisely: For all natural numbers `n` ≥ 2 and any distinct `x, y` in the interval [0, +∞), the function `x mapsto x^n` is strictly convex, i.e., `(a*x + b*y)^n < a*x^n + b*y^n` for all `a, b` in the open unit interval with `a + b = 1`.
|
Even.strictConvexOn_pow
theorem Even.strictConvexOn_pow : ∀ {n : ℕ}, Even n → n ≠ 0 → StrictConvexOn ℝ Set.univ fun x => x ^ n
The theorem `Even.strictConvexOn_pow` states that for any natural number `n` that is both even and non-zero, the function `f(x) = x^n` is strictly convex on the entire real line. In other words, for any distinct numbers `x` and `y` in the real line and any positive real numbers `a` and `b` such that `a + b = 1`, the inequality `f(ax + by) < af(x) + bf(y)` holds.
More concisely: For any even and non-zero natural number `n`, the function `x => x^n` is strictly convex on the real line, i.e., for all distinct `x` and `y` in the real line and `0 < a, b < 1` with `a + b = 1`, `(x^n * b + y^n * a) < (x^n * a + x^n * b + y^n * b + y^n * a)`.
|