convexOn_pow
theorem convexOn_pow :
∀ {𝕜 : Type u_1} [inst : LinearOrderedCommRing 𝕜] (n : ℕ), ConvexOn 𝕜 (Set.Ici 0) fun x => x ^ n
The theorem `convexOn_pow` states that for any natural number `n` and any type `𝕜` that forms a linear ordered commutative ring, the function `x^n` is convex on the interval `[0, +∞)`. In other words, for all non-negative real numbers `x` and `y`, and for all non-negative scalars `a` and `b` such that `a + b = 1`, the inequality `f(a*x + b*y) ≤ a*f(x) + b*f(y)` holds, where `f(x) = x^n`.
More concisely: For any commutative ring with a linear order `𝕜` and natural number `n`, the function `x => x^n` is convex on the interval `[0, +∞)`.
|
convexOn_zpow
theorem convexOn_zpow : ∀ {𝕜 : Type u_1} [inst : LinearOrderedField 𝕜] (n : ℤ), ConvexOn 𝕜 (Set.Ioi 0) fun x => x ^ n
The theorem `convexOn_zpow` states that for any integer `m`, the function `f(x) = x^m` is convex on the open interval `(0, +∞)`. Here, convexity means that for any two points in the interval and any two non-negative real numbers `a` and `b` that sum up to `1`, the value of the function at the point `a•x + b•y` (where `•` denotes scalar multiplication) is less than or equal to `a • f(x) + b • f(y)`. This holds for all types `𝕜` that form a linear ordered field.
More concisely: For any integer `m` and type `𝕜` forming a linear ordered field, the function `f(x) = x^m` is convex on the open interval `(0, +∞)`, i.e., for all `x, y ∈ (0, +∞)` and `a, b ∈ ℝ^+` with `a + b = 1`, `a * f(x) + b * f(y) ≥ f(a * x + b * y)`.
|
ConvexOn.smul'
theorem ConvexOn.smul' :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : LinearOrderedCommRing 𝕜] [inst_1 : LinearOrderedCommRing E]
[inst_2 : LinearOrderedAddCommGroup F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : Module E F]
[inst_6 : IsScalarTower 𝕜 E F] [inst_7 : SMulCommClass 𝕜 E F] [inst_8 : OrderedSMul 𝕜 F]
[inst_9 : OrderedSMul E F] {s : Set 𝕜} {f : 𝕜 → E} {g : 𝕜 → F},
ConvexOn 𝕜 s f →
ConvexOn 𝕜 s g →
(∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x) → (∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x) → MonovaryOn f g s → ConvexOn 𝕜 s (f • g)
This theorem, named `ConvexOn.smul'`, states that for any types `𝕜`, `E`, and `F` with the given algebraic structure (specifically, `𝕜` and `E` are linear ordered commutative rings, `F` is a linear ordered additive commutative group, `𝕜`, `E`, and `F` form modules and scalar towers, and there are ordered scalar multiplication structures defined on `𝕜` and `E` with `F`), if there is a set `s` in `𝕜` and two functions `f` and `g` from `𝕜` to `E` and `F` respectively, then if `f` and `g` are both convex on `s`, and for all `x` in `s`, `f(x)` and `g(x)` are non-negative, and moreover if `f` is monotonically increasing with `g` on `s`, then the function `f•g` (the scalar multiplication of `f` and `g`) is also convex on `s`. In simpler mathematical terms, under these conditions, the pointwise multiplication of two convex functions where one is monotonically increasing with the other, yields another convex function.
More concisely: If `𝕜` is a linear ordered commutative ring, `E` is a linear ordered additive commutative group, `F` is an ordered group, `𝕜` and `E` are modules and scalar towers over `F`, and `f: 𝕜 → E` and `g: 𝕜 → F` are convex functions on a set `s` in `𝕜` with `f(x)`, `g(x)` non-negative for all `x` in `s`, and `f` monotonically increasing with `g` on `s`, then the function `f•g: 𝕜 → F` defined as `f•g(x) := f(x)*g(x)` is convex on `s`.
|
Even.convexOn_pow
theorem Even.convexOn_pow :
∀ {𝕜 : Type u_1} [inst : LinearOrderedCommRing 𝕜] {n : ℕ}, Even n → ConvexOn 𝕜 Set.univ fun x => x ^ n
The theorem `Even.convexOn_pow` states that for any natural number `n` that is even, the function `x^n`, where `x` is any element from the set of all elements of a given type `𝕜` that forms a Linear Ordered Commutative Ring, is convex. In other words, for any even exponent, the power function is convex over the entire real line.
More concisely: For any even natural number `n` and any element `x` in a Linear Ordered Commutative Ring `𝕜`, the function `x ^ n` is convex.
|