strictConvexOn_of_deriv2_pos'
theorem strictConvexOn_of_deriv2_pos' :
∀ {D : Set ℝ}, Convex ℝ D → ∀ {f : ℝ → ℝ}, ContinuousOn f D → (∀ x ∈ D, 0 < deriv^[2] f x) → StrictConvexOn ℝ D f
The theorem named `strictConvexOn_of_deriv2_pos'` states that, given a set `D` of real numbers that is convex, and a function `f` from the real numbers to the real numbers that is continuous on `D`, if the second derivative of `f` is strictly positive for every element in `D`, then `f` is strictly convex on `D`. In other words, if `f` changes its slope in a consistent manner (its second derivative is positive) over a convex set, then `f` forms a shape that is strictly convex, i.e., it curves upwards and any line segment between two points on the graph of `f` lies above the graph. Note that the requirement for `f` to have a second derivative is implicitly satisfied by the assumption that the second derivative is positive, except possibly at one point.
More concisely: If a continuous real-valued function defined on a convex set has strictly positive second derivative, then it is strictly convex.
|
Monotone.convexOn_univ_of_deriv
theorem Monotone.convexOn_univ_of_deriv :
∀ {f : ℝ → ℝ}, Differentiable ℝ f → Monotone (deriv f) → ConvexOn ℝ Set.univ f
The theorem states that if a function `f` from real numbers to real numbers is differentiable and its derivative `f'` is a monotone function on the real numbers, then `f` is a convex function. In other words, for any function `f` which is both differentiable and its derivative is monotone on the set of real numbers, the function `f` will exhibit convexity on the entire set of real numbers. Convexity here means that for any two points along `f`, the line segment connecting them lies above or on the graph of `f`.
More concisely: If a real-valued function `f` is differentiable and its derivative `f'` is a monotone increasing function, then `f` is convex (i.e., for all `x, y in R`, `(x - y) * (f(x) - f(y)) >= 0`).
|
concaveOn_of_deriv2_nonpos
theorem concaveOn_of_deriv2_nonpos :
∀ {D : Set ℝ},
Convex ℝ D →
∀ {f : ℝ → ℝ},
ContinuousOn f D →
DifferentiableOn ℝ f (interior D) →
DifferentiableOn ℝ (deriv f) (interior D) → (∀ x ∈ interior D, deriv^[2] f x ≤ 0) → ConcaveOn ℝ D f
The theorem `concaveOn_of_deriv2_nonpos` states that if a function `f` is continuous on a convex subset `D` of the real numbers, is differentiable twice on the interior of `D`, and its second derivative is nonpositive on the interior of `D`, then `f` is concave on `D`. Concavity here means that for any two points `x` and `y` in the set `D` and any `a` and `b` in the real numbers such that `a` and `b` are nonnegative and their sum is equal to one, the equation `a * f(x) + b * f(y) ≤ f(a * x + b * y)` holds true. The second derivative being nonpositive signifies the function `f` does not curve upwards.
More concisely: If a real-valued function `f` is continuous, twice differentiable with nonpositive second derivative on the interior of a convex set `D`, then `f` is concave on `D`, meaning `a * f(x) + b * f(y) ≤ f(a * x + b * y)` for all `x, y ∈ D` and `a, b ≥ 0` with `a + b = 1`.
|
StrictMonoOn.strictConvexOn_of_deriv
theorem StrictMonoOn.strictConvexOn_of_deriv :
∀ {D : Set ℝ},
Convex ℝ D → ∀ {f : ℝ → ℝ}, ContinuousOn f D → StrictMonoOn (deriv f) (interior D) → StrictConvexOn ℝ D f
The theorem states that if a function `f` is continuous on a convex subset `D` of real numbers, and the derivative of `f` is strictly increasing on the interior of `D`, then `f` is strictly convex on `D`. Notably, the theorem does not require `f` to be differentiable everywhere, because the strict increase of the derivative `f'` ensures differentiability at all but at most one point.
In mathematical terms, given a function `f: ℝ → ℝ` and a convex set `D ⊆ ℝ`, if `f` is continuous on `D` and `f'`(the derivative of `f`) is strictly monotone on the interior of `D`, then `f` is strictly convex on `D`. Strict convexity here means that for any two distinct points in `D`, the function value at any point inside the line segment connecting these two points is strictly less than the weighted average of the function values at the two points.
More concisely: If a continuous real-valued function on a convex set has a strictly increasing derivative on the set's interior, then the function is strictly convex on the set.
|
concaveOn_univ_of_deriv2_nonpos
theorem concaveOn_univ_of_deriv2_nonpos :
∀ {f : ℝ → ℝ},
Differentiable ℝ f → Differentiable ℝ (deriv f) → (∀ (x : ℝ), deriv^[2] f x ≤ 0) → ConcaveOn ℝ Set.univ f
The theorem `concaveOn_univ_of_deriv2_nonpos` states that if a function `f` from real numbers to real numbers is twice differentiable, and its second derivative is less than or equal to zero for all real numbers, then the function `f` is concave on the entire set of real numbers. In mathematical terms, if a function $f: \mathbb{R} \to \mathbb{R}$ satisfies $f''(x) \leq 0$ for all $x \in \mathbb{R}$, then $f$ is a concave function.
More concisely: If a twice-differentiable real-valued function has non-positive second derivative on the real numbers, then it is concave.
|
StrictAnti.strictConcaveOn_univ_of_deriv
theorem StrictAnti.strictConcaveOn_univ_of_deriv :
∀ {f : ℝ → ℝ}, Continuous f → StrictAnti (deriv f) → StrictConcaveOn ℝ Set.univ f
The theorem `StrictAnti.strictConcaveOn_univ_of_deriv` states that if a real-valued function `f` is continuous and its derivative `f'` is strictly antitone on the real numbers, then `f` is strictly concave on the set of all real numbers. The function `f` does not need to be differentiable since the strict antitonicity of `f'` ensures differentiability at all but at most one point.
More concisely: If a real-valued function is continuous with a strictly antitone derivative, then it is strictly concave on the real numbers.
|
strictConcaveOn_of_deriv2_neg'
theorem strictConcaveOn_of_deriv2_neg' :
∀ {D : Set ℝ},
Convex ℝ D → ∀ {f : ℝ → ℝ}, ContinuousOn f D → (∀ x ∈ D, deriv^[2] f x < 0) → StrictConcaveOn ℝ D f
The theorem `strictConcaveOn_of_deriv2_neg'` states that if we have a function `f` that is continuous on a convex subset `D` of the real numbers, and the second derivative of `f` is strictly negative for all points in `D`, then `f` is strictly concave on `D`. It should be noted that while this theorem does not explicitly require the function `f` to be twice differentiable, the condition of having a strictly negative second derivative inherently implies twice differentiability, with the possible exception of at most one point.
More concisely: If a continuous function on a convex subset of the real numbers has strictly negative second derivatives, then it is strictly concave.
|
MonotoneOn.convexOn_of_deriv
theorem MonotoneOn.convexOn_of_deriv :
∀ {D : Set ℝ},
Convex ℝ D →
∀ {f : ℝ → ℝ},
ContinuousOn f D → DifferentiableOn ℝ f (interior D) → MonotoneOn (deriv f) (interior D) → ConvexOn ℝ D f
The theorem states that if a function `f`, mapping real numbers to real numbers, satisfies the following conditions:
1. `f` is continuous on a convex set `D` in the set of real numbers.
2. `f` is differentiable on the interior of `D`.
3. The derivative of `f`, denoted as `f'` or `deriv f`, is a monotone function on the interior of `D`.
Then, the function `f` is convex on the set `D`. That is, for any two points in `D`, the function `f` evaluated at any point on the line segment between the two points (inclusive) is less than or equal to the weighted average of the function values at the two points, where the weights are the proportions of the line segment that the point divides it into.
More concisely: If a real-valued function `f` is continous on a convex set `D`, differentiable on the interior of `D`, and its derivative is a monotone function on the interior of `D`, then `f` is convex on `D`, meaning `f(tx+(1-t)y) <= tf(x) + (1-t)f(y)` for all `x, y in D` and `t in [0, 1]`.
|
convexOn_of_deriv2_nonneg
theorem convexOn_of_deriv2_nonneg :
∀ {D : Set ℝ},
Convex ℝ D →
∀ {f : ℝ → ℝ},
ContinuousOn f D →
DifferentiableOn ℝ f (interior D) →
DifferentiableOn ℝ (deriv f) (interior D) → (∀ x ∈ interior D, 0 ≤ deriv^[2] f x) → ConvexOn ℝ D f
The theorem states that if we have a function `f` that is continuous on a convex subset `D` of the real numbers, and this function is twice differentiable on the interior of `D`, with the second derivative being nonnegative within the interior of `D`, then the function `f` is convex on `D`. This theorem is a formalization of a well-known result in calculus and real analysis, establishing the connection between the convexity of a function and the sign of its second derivative.
More concisely: If a continuous function `f` on a convex subset `D` of the real numbers has a nonnegative second derivative on the interior of `D`, then `f` is convex on `D`.
|
convexOn_univ_of_deriv2_nonneg
theorem convexOn_univ_of_deriv2_nonneg :
∀ {f : ℝ → ℝ},
Differentiable ℝ f → Differentiable ℝ (deriv f) → (∀ (x : ℝ), 0 ≤ deriv^[2] f x) → ConvexOn ℝ Set.univ f
The theorem states that if a real-valued function `f` is twice differentiable on the real numbers `ℝ`, and the second derivative of `f` is nonnegative for all real numbers, then `f` is convex on the entire set of real numbers. In mathematical terms, if a function `f: ℝ → ℝ` satisfies `f''(x) ≥ 0` for all `x` in `ℝ`, and `f` is twice differentiable, then `f` is convex on `ℝ`. Convexity here means that for any two points `x` and `y` in the domain and any `a` and `b` in `ℝ` such that `a, b ≥ 0` and `a + b = 1`, we have `f(a * x + b * y) ≤ a * f(x) + b * f(y)`.
More concisely: If a real-valued function `f:` ℝ → ℝ is twice differentiable with nonnegative second derivative (i.e., `f''(x) ≥ 0` for all `x` in ℝ), then `f` is convex on the entire set of real numbers, meaning `a * f(x) + b * f(y) ≤ f(a * x + b * y)` for all `x, y` in ℝ and `a, b` in ℝ with `a, b ≥ 0` and `a + b = 1`.
|
strictConvexOn_of_deriv2_pos
theorem strictConvexOn_of_deriv2_pos :
∀ {D : Set ℝ},
Convex ℝ D → ∀ {f : ℝ → ℝ}, ContinuousOn f D → (∀ x ∈ interior D, 0 < deriv^[2] f x) → StrictConvexOn ℝ D f
The theorem `strictConvexOn_of_deriv2_pos` states the following: Given a set `D` in the real numbers `ℝ`, if `D` is a convex set and there exists a real-valued function `f` that is continuous on `D` and that its second derivative is positive on the interior of `D`, then this function `f` is strictly convex on `D`. Here, strict convexity means that for any two distinct points in `D`, the function's value at any point on the line segment connecting these two points is strictly less than the weighted average of the function's values at these points. It's worth noting that the theorem does not explicitly require the function to be twice differentiable because it is already implied by the existence of a strictly positive second derivative, except possibly at one point.
More concisely: If a continuous real-valued function defined on a convex set has a strictly positive second derivative on its interior, then it is strictly convex on that set.
|
convexOn_of_deriv2_nonneg'
theorem convexOn_of_deriv2_nonneg' :
∀ {D : Set ℝ},
Convex ℝ D →
∀ {f : ℝ → ℝ},
DifferentiableOn ℝ f D → DifferentiableOn ℝ (deriv f) D → (∀ x ∈ D, 0 ≤ deriv^[2] f x) → ConvexOn ℝ D f
The theorem `convexOn_of_deriv2_nonneg'` states that if we have a function `f` which is twice differentiable on an open convex set `D` that is a subset of real numbers (ℝ), and the second derivative of the function `f` is nonnegative on this set `D`, then the function `f` is convex on the set `D`. In other words, if a function's second derivative is always nonnegative over a convex set, then the function will always be convex over that set.
More concisely: If a twice-differentiable function on an open convex set has non-negative second derivative, then the function is convex on that set.
|
Antitone.concaveOn_univ_of_deriv
theorem Antitone.concaveOn_univ_of_deriv :
∀ {f : ℝ → ℝ}, Differentiable ℝ f → Antitone (deriv f) → ConcaveOn ℝ Set.univ f
The theorem `Antitone.concaveOn_univ_of_deriv` states that if a function `f` from real numbers to real numbers is differentiable and its derivative is antitone on the set of all real numbers (meaning that if `a` is less than or equal to `b`, then the derivative of `f` at `b` is less than or equal to the derivative of `f` at `a`), then `f` is concave on the universal set of real numbers. In other words, for any real numbers `x` and `y` and for any nonnegative real numbers `a` and `b` such that `a + b = 1`, the inequality `a * f(x) + b * f(y) ≤ f(a*x + b*y)` holds, which is the definition of the function `f` being concave.
More concisely: If a real-valued function is differentiable with antitone derivative, then it is concave on the universal set of real numbers. (That is, for all x, y in ℝ and nonnegative a, b with a + b = 1, a * f(x) + b * f(y) ≤ f(a*x + b*y).)
|
strictConcaveOn_of_deriv2_neg
theorem strictConcaveOn_of_deriv2_neg :
∀ {D : Set ℝ},
Convex ℝ D → ∀ {f : ℝ → ℝ}, ContinuousOn f D → (∀ x ∈ interior D, deriv^[2] f x < 0) → StrictConcaveOn ℝ D f
This theorem states that if a real-valued function `f` is continuous on a convex subset `D` of the real numbers, and its second derivative is strictly negative on the interior of `D`, then `f` is strictly concave on `D`. The condition of the second derivative being strictly negative is already implying the twice differentiability of `f` at all but possibly one point within `D`.
In other words, the theorem establishes a sufficient condition for a function to be strictly concave, which is the combination of the function being continuous, the domain being convex, and the second derivative being negative on the interior of the domain.
More concisely: If a real-valued, twice-differentiable function `f` is continuous on a convex subset `D` and has strictly negative second derivatives on the interior of `D`, then `f` is strictly concave on `D`.
|
StrictAntiOn.strictConcaveOn_of_deriv
theorem StrictAntiOn.strictConcaveOn_of_deriv :
∀ {D : Set ℝ},
Convex ℝ D → ∀ {f : ℝ → ℝ}, ContinuousOn f D → StrictAntiOn (deriv f) (interior D) → StrictConcaveOn ℝ D f
The theorem states that if a real-valued function `f` is continuous on a convex set `D` which is a subset of the real numbers, and the derivative `f'` of `f` is strictly decreasing on the interior of `D`, then `f` is strictly concave on `D`. This means `f` gets steeper as we move from left to right on the set `D`. Notably, the theorem does not require the function `f` to be differentiable everywhere, as this condition is ensured everywhere except maybe one point due to the strict decreasing property of `f'`.
More concisely: If a real-valued, continuous function `f` on a convex set `D` has a strictly decreasing derivative `f'` on the interior of `D`, then `f` is strictly concave on `D`.
|
strictConvexOn_univ_of_deriv2_pos
theorem strictConvexOn_univ_of_deriv2_pos :
∀ {f : ℝ → ℝ}, Continuous f → (∀ (x : ℝ), 0 < deriv^[2] f x) → StrictConvexOn ℝ Set.univ f
The theorem `strictConvexOn_univ_of_deriv2_pos` states that if a real-valued function `f` is continuous on the real numbers and its second derivative is strictly positive for all real numbers, then `f` is strictly convex on the real numbers. It is important to note that we do not explicitly require the function to be twice differentiable as this requirement is implied by the second derivative being strictly positive, possibly excluding at most one point. In mathematical terms, for a function `f: ℝ → ℝ`, if it is continuous and its second derivative `f''(x) > 0` for all `x` in `ℝ`, then `f` is strictly convex.
More concisely: If a real-valued function `f` is continuous on the real numbers and has strictly positive second derivative everywhere, then `f` is strictly convex.
|
strictConcaveOn_univ_of_deriv2_neg
theorem strictConcaveOn_univ_of_deriv2_neg :
∀ {f : ℝ → ℝ}, Continuous f → (∀ (x : ℝ), deriv^[2] f x < 0) → StrictConcaveOn ℝ Set.univ f
The theorem `strictConcaveOn_univ_of_deriv2_neg` states that if a function `f` mapping real numbers to real numbers is continuous, and its second derivative is strictly negative for all real numbers `x`, then the function `f` is strictly concave on the set of all real numbers. Note that the condition of the second derivative being strictly negative already implies that the function is twice differentiable, except possibly at one point. The concept of strict concavity here means that for all `x` and `y` in the set, and for all real numbers `a` and `b` strictly greater than 0 that sum to 1, the value of `f` at the weighted sum `a*x + b*y` is strictly less than the weighted sum of the values of `f` at `x` and `y`, i.e., `a*f(x) + b*f(y)`.
More concisely: If a real-valued function `f` is continuous and has strictly negative second derivative on the real numbers, then it is strictly concave on the set of all real numbers.
|
concaveOn_of_deriv2_nonpos'
theorem concaveOn_of_deriv2_nonpos' :
∀ {D : Set ℝ},
Convex ℝ D →
∀ {f : ℝ → ℝ},
DifferentiableOn ℝ f D → DifferentiableOn ℝ (deriv f) D → (∀ x ∈ D, deriv^[2] f x ≤ 0) → ConcaveOn ℝ D f
The theorem `concaveOn_of_deriv2_nonpos'` asserts that if a real-valued function `f` is twice differentiable on an open convex subset `D` of the real numbers, and if the second derivative of `f` is nonpositive on `D`, then `f` is concave on `D`. In other words, if the rate of change of the derivative of `f` (i.e., the second derivative) is less than or equal to zero at every point in `D`, implying that the function does not curve upwards, then the function exhibits the property of concavity on `D`. This is a mathematical statement about the properties and behavior of differentiable functions on convex sets.
More concisely: If a real-valued, twice differentiable function on an open convex set has nonpositive second derivatives, then it is concave on that set.
|
AntitoneOn.concaveOn_of_deriv
theorem AntitoneOn.concaveOn_of_deriv :
∀ {D : Set ℝ},
Convex ℝ D →
∀ {f : ℝ → ℝ},
ContinuousOn f D → DifferentiableOn ℝ f (interior D) → AntitoneOn (deriv f) (interior D) → ConcaveOn ℝ D f
This theorem asserts that if a real-valued function `f` adheres to certain conditions, then it is concave on a given set `D`. Specifically, those conditions are: the function `f` is continuous on a convex set `D` in the real numbers, the function `f` is differentiable within the interior of `D`, and the derivative of the function `f`, denoted `f'` or `deriv f`, is antitone (i.e., it preserves the order reversal) within the interior of `D`. If these conditions are satisfied, then the function `f` is concave on the set `D`.
More concisely: If a real-valued function `f` is continuous on a convex set `D`, differentiable on the interior of `D`, and its derivative is antitone on the interior of `D`, then `f` is concave on `D`.
|
StrictMono.strictConvexOn_univ_of_deriv
theorem StrictMono.strictConvexOn_univ_of_deriv :
∀ {f : ℝ → ℝ}, Continuous f → StrictMono (deriv f) → StrictConvexOn ℝ Set.univ f
The theorem `StrictMono.strictConvexOn_univ_of_deriv` states that if a function `f` mapping real numbers to real numbers is continuous, and its derivative `f'` is strictly monotone (i.e., as the input increases, the output of `f'` strictly increases as well), then `f` is strictly convex on the entire real line. Here, strict convexity means that for any two distinct points `x` and `y` in the domain, the function `f` at a weighted average of `x` and `y` is strictly less than the weighted average of `f(x)` and `f(y)`. This theorem does not require `f` to be differentiable everywhere since the strict monotonicity of `f'` ensures differentiability at all but at most one point.
More concisely: If a real-valued function is continuous and its derivative is strictly monotone, then it is strictly convex on the entire real line.
|