strictConcaveOn_iff_slope_strict_anti_adjacent
theorem strictConcaveOn_iff_slope_strict_anti_adjacent :
∀ {𝕜 : Type u_1} [inst : LinearOrderedField 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
StrictConcaveOn 𝕜 s f ↔
Convex 𝕜 s ∧ ∀ ⦃x y z : 𝕜⦄, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) < (f y - f x) / (y - x)
The theorem `strictConcaveOn_iff_slope_strict_anti_adjacent` states that a function `f` mapping from a scalar field `𝕜` to `𝕜` is strictly concave on a set `s` if and only if the set `s` is convex and for any three points `x`, `y`, `z` (where `x < y < z`) belonging to `s`, the slope of the secant line of `f` on `[x, y]` is strictly greater than the slope of the secant line of `f` on `[x, z]`. Here, the slope of a secant line on `[a, b]` is defined as `(f b - f a) / (b - a)`. In simpler terms, a function is strictly concave if it curves downwards, and the steepness of the curve decreases as we move from left to right.
More concisely: A function is strictly concave on a convex set if and only if the slope of the secant line between any pair of distinct points in the set, in strictly decreasing order, satisfies the condition that the slope between the first and second points is strictly greater than the slope between the first and third points.
|
StrictConcaveOn.slope_anti_adjacent
theorem StrictConcaveOn.slope_anti_adjacent :
∀ {𝕜 : Type u_1} [inst : LinearOrderedField 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
StrictConcaveOn 𝕜 s f →
∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) < (f y - f x) / (y - x)
The theorem `StrictConcaveOn.slope_anti_adjacent` states that if a function `f : 𝕜 → 𝕜` is strictly concave on a set `s`, then for any three points `x`, `y`, and `z` in `s`, with `x` less than `y` and `y` less than `z`, the slope of the secant line of `f` on the interval `[x, y]` is strictly greater than the slope of the secant line of `f` on the interval `[y, z]`. In other words, as we move from `x` to `y` to `z`, the rate of change of `f` decreases, which is a characteristic property of strictly concave functions. Here, the slope of the secant line between two points `(a, f(a))` and `(b, f(b))` is defined as `(f(b) - f(a)) / (b - a)`.
More concisely: If `f : ℝ → ℝ` is strictly concave on a set `s ⊆ ℝ`, then for all `x < y < z` in `s`, the slope of `f` on the interval `[x, y]` is strictly greater than the slope of `f` on the interval `[y, z]`.
|
ConcaveOn.slope_anti_adjacent
theorem ConcaveOn.slope_anti_adjacent :
∀ {𝕜 : Type u_1} [inst : LinearOrderedField 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
ConcaveOn 𝕜 s f → ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)
This theorem states that if a function `f : 𝕜 → 𝕜` is concave on a set `s`, then for any three distinct points `x`, `y`, and `z` from the set `s` such that `x < y < z`, the slope of the secant line of the function `f` over the interval `[x, y]` is greater than or equal to the slope of the secant line of the function `f` over the interval `[y, z]`. In mathematical terms, it can be written as `(f z - f y) / (z - y) ≤ (f y - f x) / (y - x)` where the left side represents the slope of the secant line over `[y, z]` and the right side represents the slope of the secant line over `[x, y]`. This property is one of the defining characteristics of concave functions.
More concisely: For any concave function `f` and distinct points `x < y < z` in its domain, the slope of the secant line between `x` and `y` is less than or equal to the slope of the secant line between `y` and `z`. In mathematical notation, `(f y - f x) / (y - x) ≥ (f z - f y) / (z - y)`.
|
concaveOn_of_slope_anti_adjacent
theorem concaveOn_of_slope_anti_adjacent :
∀ {𝕜 : Type u_1} [inst : LinearOrderedField 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
Convex 𝕜 s →
(∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)) →
ConcaveOn 𝕜 s f
The theorem `concaveOn_of_slope_anti_adjacent` states that if for any three points `x`, `y`, and `z` in a convex set `s`, where `x < y < z`, the slope of the secant line of a function `f : 𝕜 → 𝕜` on the interval `[x, y]` is greater than the slope of the secant line of `f` on the interval `[x, z]`, then the function `f` is concave on `s`. In mathematical terms, if for all `x`, `y`, and `z` in `s` with `x < y < z`, the condition `(f z - f y) / (z - y) ≤ (f y - f x) / (y - x)` holds, then `f` is a concave function on `s`.
More concisely: If for all x, y, z in a convex set with x < y < z, the condition (f(z) - f(y)) / (z - y) <= (f(y) - f(x)) / (y - x) holds, then function f is concave on the set.
|
strictConvexOn_of_slope_strict_mono_adjacent
theorem strictConvexOn_of_slope_strict_mono_adjacent :
∀ {𝕜 : Type u_1} [inst : LinearOrderedField 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
Convex 𝕜 s →
(∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)) →
StrictConvexOn 𝕜 s f
This theorem states that if for a function `f` mapping a linear ordered field `𝕜` to `𝕜`, and for any three points `x`, `y`, and `z` in a convex set `s` of `𝕜` such that `x < y < z`, the slope of the secant line of `f` on the interval `[x, y]` is strictly less than the slope of the secant line of `f` on the interval `[x, z]`, then the function `f` is strictly convex on the set `s`. In mathematical terms, if the rate of change of `f` between `x` and `y` is less than the rate of change of `f` between `x` and `z`, then `f` is strictly convex.
More concisely: If for a function `f` over a linear ordered field `𝕜` mapping to itself, and for any `x < y < z` in a convex set `s`, the secant slope `(f(z) - f(x)) / (z - x)` is strictly less than the secant slope `(f(y) - f(x)) / (y - x)`, then `f` is strictly convex on `s`.
|
Mathlib.Analysis.Convex.Slope._auxLemma.1
theorem Mathlib.Analysis.Convex.Slope._auxLemma.1 :
∀ {K : Type u_3} [inst : DivisionMonoid K] [inst_1 : HasDistribNeg K] (a b : K), -(b / a) = -b / a
This theorem, `Mathlib.Analysis.Convex.Slope._auxLemma.1`, states that for any type `K` which has a division operation (making it a `DivisionMonoid`) and a negation operation that distributes over addition (`HasDistribNeg`), for any two elements `a` and `b` of that type, the negation of the fraction `b / a` is equal to the negation of `b` divided by `a`. In mathematical notation, it verifies the property - (b / a) = -b / a for all `a` and `b` in the set `K`.
More concisely: For any type `K` with division and negation operations satisfying distribution, the negation of the quotient `b / a` equals `-b / a` for all `a, b` in `K`.
|
StrictConvexOn.slope_strict_mono_adjacent
theorem StrictConvexOn.slope_strict_mono_adjacent :
∀ {𝕜 : Type u_1} [inst : LinearOrderedField 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
StrictConvexOn 𝕜 s f →
∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)
The theorem `StrictConvexOn.slope_strict_mono_adjacent` states that, for any strictly convex function `f` mapping from a type `𝕜` to `𝕜`, and for any three points `x`, `y`, and `z` within a set `s` of type `𝕜` such that `x < y < z`, the slope of the secant line of `f` on the interval `[x, y]` is strictly less than the slope of the secant line of `f` on `[x, z]`. Here the slope of the secant line from `x` to `y` is defined as `(f y - f x) / (y - x)`, and similarly for the secant line from `y` to `z`. This theorem underscores a key property of strictly convex functions, namely that the slope of the secant line increases strictly as we move along the domain of the function.
More concisely: For any strictly convex function `f` and points `x < y < z` in its domain, the slope of the secant line between `x` and `y` is strictly less than the slope of the secant line between `x` and `z`.
|
strictConvexOn_iff_slope_strict_mono_adjacent
theorem strictConvexOn_iff_slope_strict_mono_adjacent :
∀ {𝕜 : Type u_1} [inst : LinearOrderedField 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
StrictConvexOn 𝕜 s f ↔
Convex 𝕜 s ∧ ∀ ⦃x y z : 𝕜⦄, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)
The theorem `strictConvexOn_iff_slope_strict_mono_adjacent` states that a function `f` mapping from a type `𝕜` to `𝕜` is strictly convex on a set `s` of type `𝕜` if and only if the set `s` is convex and for any three points `x`, `y`, and `z` in `s` where `x < y < z`, the slope of the secant line of `f` on `[x, y]` is strictly less than the slope of the secant line of `f` on `[x, z]`. Here, the slope of a secant line between two points `(a, f(a))` and `(b, f(b))` is calculated as `(f(b) - f(a)) / (b - a)`.
More concisely: A function `f` is strictly convex on a convex set `s` if and only if the slope of the secant line between any pair of distinct points `x` and `y` in `s` with `x < y` satisfies the inequality `(f(y) - f(x)) / (y - x) < (f(z) - f(x)) / (z - x)` for all `z` in `s` with `x < z < y`.
|
concaveOn_iff_slope_anti_adjacent
theorem concaveOn_iff_slope_anti_adjacent :
∀ {𝕜 : Type u_1} [inst : LinearOrderedField 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
ConcaveOn 𝕜 s f ↔
Convex 𝕜 s ∧ ∀ ⦃x y z : 𝕜⦄, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)
The theorem `concaveOn_iff_slope_anti_adjacent` states that a function `f` from a set `𝕜` to itself is concave if and only if the set `𝕜` is convex and for any three points `x`, `y`, and `z` in `𝕜` such that `x < y < z`, the slope of the secant line of `f` on the interval `[x, y]` is greater than or equal to the slope of the secant line of `f` on the interval `[x, z]`. In mathematical terms, the slope is calculated as `(f z - f y) / (z - y)` and `(f y - f x) / (y - x)` respectively.
More concisely: A function from a convex set to itself is concave if and only if the slope of the secant line between any two points is greater than or equal to the slope of the secant line between any other pair of points in strictly increasing order.
|
ConvexOn.strict_mono_of_lt
theorem ConvexOn.strict_mono_of_lt :
∀ {𝕜 : Type u_1} [inst : LinearOrderedField 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
ConvexOn 𝕜 s f → ∀ {x y : 𝕜}, x ∈ s → x < y → f x < f y → StrictMonoOn f (s ∩ Set.Ici y)
The theorem states that if a function `f` is convex on a set `s` in a linearly ordered field, and if for two points `x` and `y` in `s` such that `x < y`, `f(x)` is less than `f(y)`, then `f` is strictly increasing (strictly monotone) on the intersection of `s` and the interval `[y, ∞)`. This means that for any two points `a` and `b` in `s ∩ [y, ∞)` where `a < b`, `f(a)` is less than `f(b)`.
More concisely: If a function `f` is convex and strictly increasing on a set `s` in a linearly ordered field, then it is strictly increasing on the intersection of `s` and the set `{x | x ≥ y}`, where `y` is any element in `s`.
|
ConvexOn.slope_mono_adjacent
theorem ConvexOn.slope_mono_adjacent :
∀ {𝕜 : Type u_1} [inst : LinearOrderedField 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
ConvexOn 𝕜 s f → ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
This theorem states that if a function `f : 𝕜 → 𝕜` is convex on a set `s`, then for any three points `x`, `y`, and `z` in `s` where `x < y < z`, the slope of the secant line of `f` on the interval `[x, y]` is less than or equal to the slope of the secant line of `f` on the interval `[y, z]`. In other words, this theorem is a formal statement of the property that the slope of the secant line of a convex function never decreases as we move from left to right.
More concisely: If `f` is a convex function on set `s` and `x < y < z` are in `s`, then the slope of `f` on the interval `[x, y]` is less than or equal to the slope of `f` on the interval `[y, z]`.
|
convexOn_of_slope_mono_adjacent
theorem convexOn_of_slope_mono_adjacent :
∀ {𝕜 : Type u_1} [inst : LinearOrderedField 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
Convex 𝕜 s →
(∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)) →
ConvexOn 𝕜 s f
This theorem states that for any three points `x < y < z` in a given set `s`, if the slope of the secant line of a function `f : 𝕜 → 𝕜` on the interval `[x, y]` is less than or equal to the slope of the secant line of `f` on the interval `[x, z]`, then the function `f` is convex on the set `s`. Here, convexity of the function `f` implies that for all `x` and `y` in `s` and for all scalars `a` and `b` such that `0 ≤ a`, `0 ≤ b`, and `a + b = 1`, it holds that `f (a • x + b • y) ≤ a • f x + b • f y`, where `•` denotes scalar multiplication.
More concisely: If for all `x < y < z` in a set `s` and for the function `f : 𝕜 → 𝕜`, the slope of `f` on the interval `[x, y]` is less than or equal to the slope on `[x, z]`, then `f` is convex on `s`, meaning `a • f x + b • f y ≤ f (a • x + b • y)` for all `x, y` in `s` and `0 ≤ a, b` with `a + b = 1`.
|
strictConcaveOn_of_slope_strict_anti_adjacent
theorem strictConcaveOn_of_slope_strict_anti_adjacent :
∀ {𝕜 : Type u_1} [inst : LinearOrderedField 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
Convex 𝕜 s →
(∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) < (f y - f x) / (y - x)) →
StrictConcaveOn 𝕜 s f
The theorem `strictConcaveOn_of_slope_strict_anti_adjacent` states that for any set `s` of type `𝕜` that is convex, if a function `f : 𝕜 → 𝕜` satisfies the condition that for any three points `x`, `y`, `z` in `s` such that `x < y < z`, the slope of the secant line of `f` on the interval `[x, y]` is strictly greater than the slope of the secant line of `f` on the interval `[x, z]`, then the function `f` is strictly concave on `s`. In other words, if the slope of the line connecting `f(y)` and `f(z)` is always less than the slope of the line connecting `f(x)` and `f(y)`, for `x < y < z` in the set, then `f` is strictly concave.
More concisely: If a convex set `s` and function `f : 𝕜 → 𝕜` satisfy the condition that for any distinct `x < y < z` in `s`, the slope of `f` on the interval `[x, y]` is strictly greater than the slope of `f` on the interval `[x, z]`, then `f` is strictly concave on `s`.
|
convexOn_iff_slope_mono_adjacent
theorem convexOn_iff_slope_mono_adjacent :
∀ {𝕜 : Type u_1} [inst : LinearOrderedField 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
ConvexOn 𝕜 s f ↔
Convex 𝕜 s ∧ ∀ ⦃x y z : 𝕜⦄, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
The theorem `convexOn_iff_slope_mono_adjacent` states that a function `f : 𝕜 → 𝕜` is convex on a set `s` if and only if `s` is a convex set and for any three points `x`, `y`, `z` in `s` where `x < y < z`, the slope of the secant line of `f` on the interval `[x, y]`, which is `(f y - f x) / (y - x)`, is less than or equal to the slope of the secant line of `f` on the interval `[y, z]`, which is `(f z - f y) / (z - y)`. This is a formal expression of the property that the function does not curve upwards, so that the slope of the secant line increases or stays the same as we move from left to right.
More concisely: A function `f : ℝ → ℝ` is convex on a set `s ⊆ ℝ` if and only if `s` is convex and for all `x < y < z` in `s`, the slope of the secant line of `f` on the interval `[x, y]` is less than or equal to that on `[y, z]`.
|