LinearMap.convexOn
theorem LinearMap.convexOn :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : OrderedAddCommMonoid Ξ²] [inst_3 : Module π E] [inst_4 : Module π Ξ²] (f : E ββ[π] Ξ²) {s : Set E},
Convex π s β ConvexOn π s βf
The theorem `LinearMap.convexOn` states that for any ordered semiring `π`, and any set `s` of elements of an additive commutative monoid `E` that form a module over `π`, if `s` is a convex set, then any linear map `f` from `E` to an ordered additive commutative monoid `Ξ²` that forms a module over `π` is a convex function on `s`. In simpler terms, a linear map from a convex set in one vector space to another vector space preserves the property of convexity. The term 'convex' here refers to the concept in mathematical analysis where, intuitively, a set is called convex if, given any two points in the set, the set contains the whole line segment that joins them. Similarly, a function is called 'convex' if the line segment joining any two points on the graph of the function lies above or on the graph.
More concisely: If `s` is a convex subset of an additive commutative monoid `E` that is a module over an ordered semiring `π`, then any linear map `f` from `E` to an ordered additive commutative monoid `Ξ²` that is also a module over `π` is a convex function on `s`.
|
ConvexOn.translate_right
theorem ConvexOn.translate_right :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : OrderedAddCommMonoid Ξ²] [inst_3 : Module π E] [inst_4 : SMul π Ξ²] {s : Set E} {f : E β Ξ²},
ConvexOn π s f β β (c : E), ConvexOn π ((fun z => c + z) β»ΒΉ' s) (f β fun z => c + z)
The theorem `ConvexOn.translate_right` states that for any ordered semiring `π`, types `E` and `Ξ²` where `E` is an additive commutative monoid, `Ξ²` is an ordered additive commutative monoid, `E` is a `π`-module, and `Ξ²` is a `π`-scalar multiplication space, if a function `f` from `E` to `Ξ²` is convex on a set `s` in `E`, then `f` composed with the translation function `c + z` is also convex on the preimage of `s` under the translation function. In other terms, right translation preserves the convexity of a function.
More concisely: If `f` is a convex function from an additive commutative monoid `E` to an ordered additive commutative monoid `Ξ²`, which is a `π`-module and a `π`-scalar multiplication space, then `f` composed with the translation function `c + z` is a convex function on the preimage of `s` under `c + z`, for any `c` in `E` and `z` in `π`.
|
convexOn_const
theorem convexOn_const :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : OrderedAddCommMonoid Ξ²] [inst_3 : SMul π E] [inst_4 : Module π Ξ²] {s : Set E} (c : Ξ²),
Convex π s β ConvexOn π s fun x => c
The theorem `convexOn_const` states that for any set `s` of elements of type `E` in a scalar multiplication space `π`, if `s` is convex, then the function `f` that maps each element `x` in `s` to a constant `c` of type `Ξ²` satisfies the property of being "convex on" `s`. In other words, if `s` is a convex set, then a constant function defined on this set is a convex function. This is true under the conditions that `π` is an ordered semiring, `E` is an additive commutative monoid, `Ξ²` is an ordered additive commutative monoid, and `π` has scalar multiplication actions on `E` and `Ξ²`.
More concisely: If `π` is an ordered semiring, `E` an additive commutative monoid, `Ξ²` an ordered additive commutative monoid, and `s β E` convex, then the constant function `f : s β Ξ²` defined by `f x = c` for all `x β s` and some constant `c β Ξ²`, is convex on `s`.
|
ConcaveOn.comp_linearMap
theorem ConcaveOn.comp_linearMap :
β {π : Type u_1} {E : Type u_2} {F : Type u_3} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : AddCommMonoid F] [inst_3 : OrderedAddCommMonoid Ξ²] [inst_4 : Module π E] [inst_5 : Module π F]
[inst_6 : SMul π Ξ²] {f : F β Ξ²} {s : Set F},
ConcaveOn π s f β β (g : E ββ[π] F), ConcaveOn π (βg β»ΒΉ' s) (f β βg)
The theorem `ConcaveOn.comp_linearMap` states that for all types `π`, `E`, `F`, and `Ξ²` where `π` is an ordered semiring, `E` and `F` are additive commutative monoids, `Ξ²` is an ordered additive commutative monoid, and there are scalar multiplications defined over `E`, `F`, and `Ξ²` with `π`, if a function `f` is concave on a set `s`, then the composition of `f` with any linear map `g` from `E` to `F` is also concave on the preimage of `s` under `g`. In other words, if `g` is a linear map and `f` is a concave function, then the function obtained by first applying `g` and then `f` is also concave.
More concisely: If `f` is a concave function and `g` is a linear map between two additive commutative monoids over an ordered semiring, then the composition `g β f` is concave on the preimage of the domain of `f` under `g`.
|
StrictConcaveOn.dual
theorem StrictConcaveOn.dual :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : OrderedAddCommMonoid Ξ²] [inst_3 : SMul π E] [inst_4 : SMul π Ξ²] {s : Set E} {f : E β Ξ²},
StrictConcaveOn π s f β StrictConvexOn π s (βOrderDual.toDual β f)
The theorem `StrictConcaveOn.dual` states that for any ordered semiring `π`, type `E` equipped with an addition commutative monoid structure, type `Ξ²` equipped with an ordered addition commutative monoid structure and both `E` and `Ξ²` having a scalar multiplication by `π`, if a function `f` from `E` to `Ξ²` is strictly concave on a set `s` of `E`, then the function obtained by applying the identity map to the dual order of `f` is strictly convex on the same set `s`. This shows a duality relationship between the concepts of strict concavity and strict convexity in the context of ordered semirings and ordered addition commutative monoids.
More concisely: If a function from an ordered semigroup equipped with an additive commutative monoid and scalar multiplication structure to another ordered semigroup with similar structures is strictly concave on a set, then its dual function is strictly convex on the same set.
|
StrictConvexOn.convexOn
theorem StrictConvexOn.convexOn :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : OrderedAddCommMonoid Ξ²] [inst_3 : Module π E] [inst_4 : Module π Ξ²] {s : Set E} {f : E β Ξ²},
StrictConvexOn π s f β ConvexOn π s f
The theorem `StrictConvexOn.convexOn` states that for any ordered semiring `π`, any set `s` of elements of type `E` with an addition operation, any function `f` from `E` to an ordered additively commutative monoid `Ξ²`, both `E` and `Ξ²` being modules over `π`, if the function `f` is strictly convex on the set `s`, then the function `f` is also convex on `s`. In mathematical terms, this means that if for all pairs of distinct points `x` and `y` in `s`, and all positive real numbers `a` and `b` such that `a + b = 1`, the inequality `f(a * x + b * y) < a * f(x) + b * f(y)` holds, then the function `f` is also convex, meaning that the inequality `f(a * x + b * y) β€ a * f(x) + b * f(y)` holds for all points `x` and `y` in `s` and all non-negative real numbers `a` and `b` such that `a + b = 1`.
More concisely: If a function `f` is strictly convex on a set `s` in an ordered semiring `π`, where `E` is the type of elements of `s` with an addition operation, and `Ξ²` is an ordered additively commutative monoid that `E` and `Ξ²` are modules over `π`, then `f` is convex on `s`.
|
ConcaveOn.dual
theorem ConcaveOn.dual :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : OrderedAddCommMonoid Ξ²] [inst_3 : SMul π E] [inst_4 : SMul π Ξ²] {s : Set E} {f : E β Ξ²},
ConcaveOn π s f β ConvexOn π s (βOrderDual.toDual β f)
The theorem `ConcaveOn.dual` states that for any ordered semiring `π`, types `E` and `Ξ²`, additive commutative monoid `E`, ordered additive commutative monoid `Ξ²`, and scalar multiplication on `E` and `Ξ²`, given a set `s` of type `E` and a function `f` from `E` to `Ξ²`, if the function `f` is concave on the set `s`, then the function `f` composed with the identity function to the `OrderDual` of `Ξ²` is convex on the set `s`. Here, `OrderDual` of a type is a type that reverses the order of elements in the original type.
More concisely: If `f` is a concave function from an additive commutative semigroup `E` to an ordered additive commutative monoid `Ξ²`, then the composition `f β id` with the order dual `OrderDual Ξ²` is a convex function on `E`.
|
LinearMap.concaveOn
theorem LinearMap.concaveOn :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : OrderedAddCommMonoid Ξ²] [inst_3 : Module π E] [inst_4 : Module π Ξ²] (f : E ββ[π] Ξ²) {s : Set E},
Convex π s β ConcaveOn π s βf
This theorem states that a linear map is concave on a convex set. More formally, for any ordered semiring `π`, any additive commutative monoid `E`, and any ordered additive commutative monoid `Ξ²`, if `f` is a linear map from `E` to `Ξ²`, and `s` is a convex set in `E`, then `f` is concave on `s`. Here, a function `f` is concave on a set `s` if for any two points `x` and `y` in `s` and for any two non-negative scalars `a` and `b` from `π` such that `a + b = 1`, the function value at the convex combination `a β’ x + b β’ y` is greater than or equal to the convex combination of the function values `a β’ f(x) + b β’ f(y)`.
More concisely: A linear map is concave on a convex set in the sense that for any two points in the set and any non-negative scalars summing to 1, the function value at their convex combination is greater than or equal to the convex combination of the function values at the original points.
|
LinearOrder.convexOn_of_lt
theorem LinearOrder.convexOn_of_lt :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : OrderedAddCommMonoid Ξ²] [inst_3 : Module π E] [inst_4 : Module π Ξ²] [inst_5 : LinearOrder E] {s : Set E}
{f : E β Ξ²},
Convex π s β
(β β¦x : Eβ¦,
x β s β
β β¦y : Eβ¦,
y β s β x < y β β β¦a b : πβ¦, 0 < a β 0 < b β a + b = 1 β f (a β’ x + b β’ y) β€ a β’ f x + b β’ f y) β
ConvexOn π s f
This theorem states that for a function defined on a convex set in a linearly ordered space (where the order and the algebraic structures may not be compatible), to demonstrate the function's convexity, it is enough to show the inequality `f (a β’ x + b β’ y) β€ a β’ f x + b β’ f y` for the case where `x < y` and `a`, `b` are positive. While `E = π` is the primary use-case, this theorem could also be applied, for instance, to `π^n` with a lexicographic order.
More concisely: For a function defined on a convex set in a linearly ordered space, convexity is proven by showing that `f (ax + by) β€ a*fx + b*fy` holds for positive `a, b` when `x < y`.
|
ConcaveOn.ge_on_segment
theorem ConcaveOn.ge_on_segment :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : LinearOrderedAddCommMonoid Ξ²] [inst_3 : SMul π E] [inst_4 : Module π Ξ²] [inst_5 : OrderedSMul π Ξ²]
{s : Set E} {f : E β Ξ²},
ConcaveOn π s f β β {x y z : E}, x β s β y β s β z β segment π x y β min (f x) (f y) β€ f z
The theorem `ConcaveOn.ge_on_segment` states that for any ordered semiring `π`, types `E` and `Ξ²` such that `E` is an additive commutative monoid, `Ξ²` is a linearly ordered additive commutative monoid, `π` is a scalar multiplier for `E` and `Ξ²`, and scalar multiplication of `π` and `Ξ²` is ordered, given a set `s` of type `E` and a function `f` from `E` to `Ξ²`, if `f` is concave on `s`, then for all `x`, `y`, and `z` of type `E` such that `x` and `y` belong to `s` and `z` belongs to the segment between `x` and `y`, the minimum of `f(x)` and `f(y)` is less than or equal to `f(z)`. In other words, a concave function on a segment is always greater than or equal to the minimum of its values at the endpoints of the segment.
More concisely: If `f` is a concave function on the set `s` in an ordered semiring, then for all `x`, `y` in `s` and `z` on the segment between `x` and `y`, we have `f(x) β€ f(z) β€ f(y)`.
|
neg_convexOn_iff
theorem neg_convexOn_iff :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : OrderedAddCommGroup Ξ²] [inst_3 : SMul π E] [inst_4 : Module π Ξ²] {s : Set E} {f : E β Ξ²},
ConvexOn π s (-f) β ConcaveOn π s f
The theorem `neg_convexOn_iff` states that for any set `s` and any function `f` from `E` to `Ξ²`, where `π` is an ordered semiring, `E` is an additive commutative monoid, `Ξ²` is an ordered additive commutative group, and `π` acts on `E` and `Ξ²` through scalar multiplication, the negative of the function `f` is convex on the set `s` if and only if the function `f` is concave on the set `s`. In other words, a function is concave exactly when its negation is convex.
More concisely: A function from an additive commutative monoid to an ordered additive commutative group over an ordered semiring is concave if and only if its negation is convex.
|
StrictConcaveOn.neg
theorem StrictConcaveOn.neg :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : OrderedAddCommGroup Ξ²] [inst_3 : SMul π E] [inst_4 : Module π Ξ²] {s : Set E} {f : E β Ξ²},
StrictConcaveOn π s f β StrictConvexOn π s (-f)
This theorem, termed `StrictConcaveOn.neg`, states that for any ordered semiring `π`, an additive commutative monoid `E`, an ordered additive commutative group `Ξ²`, a set `s` of elements of type `E`, and a function `f` mapping from `E` to `Ξ²`, if the function `f` is strictly concave on the set `s`, then the negation of this function, `-f`, is strictly convex on the same set `s`. In more mathematical terms, for a function to be strictly concave means that for any two distinct points in its domain, the function's value at the weighted average of these points is strictly less than the weighted average of the function values at these points. Strict convexity of a function is defined in the similar manner, but with the inequality reversed. Therefore, this theorem essentially provides a way of transforming a strictly concave function into a strictly convex one by taking its negation.
More concisely: If a function `f` mapping from an additive commutative monoid to an ordered additive commutative group is strictly concave on a set `s`, then the negation `-f` is strictly convex on `s`.
|
ConvexOn.convex_epigraph
theorem ConvexOn.convex_epigraph :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : OrderedAddCommMonoid Ξ²] [inst_3 : SMul π E] [inst_4 : Module π Ξ²] [inst_5 : OrderedSMul π Ξ²] {s : Set E}
{f : E β Ξ²}, ConvexOn π s f β Convex π {p | p.1 β s β§ f p.1 β€ p.2}
This theorem states that, for any ordered semiring `π`, any type `E` with an additive commutative monoid structure and a `π`-module structure, any type `Ξ²` with an ordered additive commutative monoid structure, a `π`-module structure, and an ordered `π`-scalar multiplication structure, a subset `s` of `E`, and a function `f` from `E` to `Ξ²`, if the function `f` is convex on the set `s` (`ConvexOn π s f`), then the epigraph of `f` on `s` (the set of points `(x, y)` such that `x` is in `s` and `y` is greater or equal to `f(x)`) is a convex set in `π`.
More concisely: For any ordered semiring `π`, if `f` is a convex function on a subset `s` of an additive commutative monoid `E` endowed with a `π`-module and an ordered `π`-scalar multiplication structure, then the epigraph of `f` on `s` is a convex set in `E Γ β`.
|
StrictConvexOn.eq_of_isMinOn
theorem StrictConvexOn.eq_of_isMinOn :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : LinearOrderedField π] [inst_1 : OrderedAddCommMonoid Ξ²]
[inst_2 : AddCommMonoid E] [inst_3 : SMul π E] [inst_4 : Module π Ξ²] [inst_5 : OrderedSMul π Ξ²] {f : E β Ξ²}
{s : Set E} {x y : E}, StrictConvexOn π s f β IsMinOn f s x β IsMinOn f s y β x β s β y β s β x = y
The theorem `StrictConvexOn.eq_of_isMinOn` states that for any strictly convex function `f` from a set `s` in a linearly ordered field `π`, if the function `f` has a global minimum on `s` at two different points `x` and `y`, then `x` and `y` must be the same. This means a strictly convex function can have at most one global minimum.
More concisely: In a strictly convex function over a linearly ordered field, there is at most one global minimum.
|
neg_concaveOn_iff
theorem neg_concaveOn_iff :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : OrderedAddCommGroup Ξ²] [inst_3 : SMul π E] [inst_4 : Module π Ξ²] {s : Set E} {f : E β Ξ²},
ConcaveOn π s (-f) β ConvexOn π s f
This theorem states that a function `-f`, where `f` maps elements from set `E` to `Ξ²`, is concave on a set `s` under the scalar multiplication of `π` if and only if the function `f` is convex on the set `s`. Here, `π` is an ordered semiring, `E` is an additive commutative monoid, and `Ξ²` is an ordered additive commutative group with a scalar multiplication structure and a module structure over `π`. The convexity or concavity of a function refers to the property that a line segment between any two points on the graph of the function lies above (for convex) or below (for concave) the graph.
More concisely: A function `f` from an additive commutative monoid `E` to an ordered additive commutative group `Ξ²` with a scalar multiplication structure and a module structure over an ordered semiring `π`, is concave on a set `s` if and only if it is convex on `s`.
|
ConcaveOn.ge_on_segment'
theorem ConcaveOn.ge_on_segment' :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : LinearOrderedAddCommMonoid Ξ²] [inst_3 : SMul π E] [inst_4 : Module π Ξ²] [inst_5 : OrderedSMul π Ξ²]
{s : Set E} {f : E β Ξ²},
ConcaveOn π s f β
β {x y : E}, x β s β y β s β β {a b : π}, 0 β€ a β 0 β€ b β a + b = 1 β min (f x) (f y) β€ f (a β’ x + b β’ y)
The theorem `ConcaveOn.ge_on_segment'` states that for any set `s` of elements of type `E` and any function `f` from `E` to `Ξ²`, if `f` is concave on `s`, then for any two elements `x` and `y` in `s` and any two scalars `a` and `b` from `π` that are non-negative and sum to 1, the minimum of `f(x)` and `f(y)` is less than or equal to `f` applied to the convex combination of `x` and `y` given by `a*x + b*y`. In terms of real-world meaning, it implies that for a concave function, the value of the function at any point inside a segment (a convex combination of two points) is always greater than or equal to the minimum value of the function at the endpoints of the segment.
More concisely: If `f` is a concave function on a set `s`, then for any `x, y in s` and `a, b in π` with `a β₯ 0`, `b β₯ 0`, and `a + b = 1`, we have `min {f(x), f(y)} β€ f(a*x + b*y)`.
|
StrictConcaveOn.inf
theorem StrictConcaveOn.inf :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : LinearOrderedAddCommMonoid Ξ²] [inst_3 : SMul π E] [inst_4 : Module π Ξ²] [inst_5 : OrderedSMul π Ξ²]
{s : Set E} {f g : E β Ξ²}, StrictConcaveOn π s f β StrictConcaveOn π s g β StrictConcaveOn π s (f β g)
The theorem `StrictConcaveOn.inf` states that for any ordered semiring `π`, any types `E` and `Ξ²` with `E` being a commutative additive monoid, `Ξ²` being a linearly ordered commutative additive monoid and a module over `π`, any set `s` of elements of type `E`, and any two functions `f` and `g` from `E` to `Ξ²`, if both `f` and `g` are strictly concave on `s`, then the pointwise minimum of `f` and `g`, denoted by `(f β g)`, is also strictly concave on `s`.
In simpler terms, the theorem ensures that taking the pointwise minimum of two strictly concave functions results in another strictly concave function. This property holds in the context of a semiring (a mathematical structure), and is crucial in various fields such as optimization and mathematical analysis.
More concisely: Given an ordered semiring π, a commutative additive monoid E, a linearly ordered commutative additive monoid and a π-module Ξ², if functions f and g from E to Ξ² are strictly concave, then their pointwise minimum (f β g) is also strictly concave on the set s.
|
StrictConvexOn.sup
theorem StrictConvexOn.sup :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : LinearOrderedAddCommMonoid Ξ²] [inst_3 : SMul π E] [inst_4 : Module π Ξ²] [inst_5 : OrderedSMul π Ξ²]
{s : Set E} {f g : E β Ξ²}, StrictConvexOn π s f β StrictConvexOn π s g β StrictConvexOn π s (f β g)
The theorem `StrictConvexOn.sup` states that if we have two strictly convex functions `f` and `g` defined on a set `s`, then the function `h` that is the pointwise maximum of `f` and `g` (denoted by `f β g`) is also strictly convex on `s`. This is valid for any ordered semiring `π`, additively commutative monoid `E`, linearly ordered additively commutative monoid `Ξ²` where `E` is a module over `π` and the multiplication operation in `Ξ²` is compatible with the ordering in `π`.
More concisely: If `f` and `g` are strictly convex functions on a set `s` in an ordered semiring `π`, where `E` is an additively commutative monoid, `Ξ²` is a linearly ordered additively commutative monoid with `E` a module over `π` and `Ξ²`'s multiplication compatible with `π`'s ordering, then their pointwise maximum `f β g` is also strictly convex on `s`.
|
StrictConvexOn.translate_left
theorem StrictConvexOn.translate_left :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCancelCommMonoid E]
[inst_2 : OrderedAddCommMonoid Ξ²] [inst_3 : Module π E] [inst_4 : SMul π Ξ²] {s : Set E} {f : E β Ξ²},
StrictConvexOn π s f β β (c : E), StrictConvexOn π ((fun z => c + z) β»ΒΉ' s) (f β fun z => z + c)
The theorem `StrictConvexOn.translate_left` states that left translation preserves the property of strict convexity for functions. In other words, for any ordered semiring `π`, any additive cancelable commutative monoid `E`, any ordered additive commutative monoid `Ξ²`, any module of `π` over `E`, and any scalar multiplication of `π` and `Ξ²` if a function `f` is strictly convex on a set `s` in `E`, then for any element `c` in `E`, the function `f` composed with the translation by `c` is strictly convex on the preimage of `s` under the addition by `c`. Here, a function is said to be strictly convex on a set if for any two distinct points in the set, the function value at any point in the open line segment between them is strictly less than the weighted average of the function values at the two points.
More concisely: If a function is strictly convex on a set in an additive commutative monoid, then translating the function by any element preserves strict convexity on the preimage of the set under addition with that element.
|
StrictConvexOn.add_convexOn
theorem StrictConvexOn.add_convexOn :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : OrderedCancelAddCommMonoid Ξ²] [inst_3 : SMul π E] [inst_4 : DistribMulAction π Ξ²] {s : Set E}
{f g : E β Ξ²}, StrictConvexOn π s f β ConvexOn π s g β StrictConvexOn π s (f + g)
The theorem `StrictConvexOn.add_convexOn` states that for any ordered semiring `π`, a set `s` of elements of type `E`, and two functions `f` and `g` from `E` to `Ξ²` such that `f` is strictly convex on `s` and `g` is convex on `s`, the function `f + g` (which represents the pointwise addition of `f` and `g`) is also strictly convex on `s`. Here, an ordered semiring is a mathematical structure with two operations that generalize the arithmetic operations of addition and multiplication, and a set `s` is strictly convex if for any two distinct points in `s`, all points on the line segment between them but not including the endpoints are inside `s`.
More concisely: If `π` is an ordered semiring, `s` is a strictly convex subset of `E`, and `f` and `g` are functions from `E` to `Ξ²` with `f` strictly convex on `s` and `g` convex on `s`, then `f + g` is strictly convex on `s`.
|
ConvexOn.comp_linearMap
theorem ConvexOn.comp_linearMap :
β {π : Type u_1} {E : Type u_2} {F : Type u_3} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : AddCommMonoid F] [inst_3 : OrderedAddCommMonoid Ξ²] [inst_4 : Module π E] [inst_5 : Module π F]
[inst_6 : SMul π Ξ²] {f : F β Ξ²} {s : Set F}, ConvexOn π s f β β (g : E ββ[π] F), ConvexOn π (βg β»ΒΉ' s) (f β βg)
This theorem states that if a function `g` is convex on a set `s`, then the composition of `g` with a linear function `f` is convex on the preimage of `s` under `f`. Here, `g` is a function from a type `E` to `F`, while `f` is a function from `F` to `Ξ²`. The types `E`, `F`, and `Ξ²` are modules over a semiring `π`, and `Ξ²` is furthermore an ordered additive commutative monoid. The convexity of a function on a set is defined in the context of an ordered semiring and the aforementioned module and monoid structures.
More concisely: If `g` is a convex function from `E` to `F` over an ordered semiring `π` with `E`, `F`, and `Ξ²` being `π`-modules and `Ξ²` an ordered additive commutative monoid, then the composition `g β f` is convex on the preimage `fβ»ΒΉ(s)` of a set `s` in `F` under `f`.
|
StrictConcaveOn.translate_left
theorem StrictConcaveOn.translate_left :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCancelCommMonoid E]
[inst_2 : OrderedAddCommMonoid Ξ²] [inst_3 : Module π E] [inst_4 : SMul π Ξ²] {s : Set E} {f : E β Ξ²},
StrictConcaveOn π s f β β (c : E), StrictConcaveOn π ((fun z => c + z) β»ΒΉ' s) (f β fun z => z + c)
The theorem `StrictConcaveOn.translate_left` states that for any ordered semiring `π`, any types `E` and `Ξ²` with the appropriate algebraic structures (specifically, `E` being an additive cancelable commutative monoid and `Ξ²` being an ordered additive commutative monoid, both with scalar multiplication by elements of `π`), any set `s` of elements of type `E`, and any function `f` from `E` to `Ξ²`, if the function `f` is strictly concave on the set `s`, then for any element `c` of type `E`, the function `f` composed with the function that adds `c` to its input is also strictly concave on the pre-image of `s` under the function that adds `c` to its input. In other words, left translation preserves strict concavity of functions.
More concisely: If `f` is a strictly concave function on a set `s` in an ordered semiring, then the function `g(x) = f(x + c)` is strictly concave on the set `{x : E | x + c β s}`, where `c` is an element in the semiring `π`.
|
StrictConcaveOn.lt_on_openSegment
theorem StrictConcaveOn.lt_on_openSegment :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : LinearOrderedAddCommMonoid Ξ²] [inst_3 : SMul π E] [inst_4 : Module π Ξ²] [inst_5 : OrderedSMul π Ξ²]
{s : Set E} {f : E β Ξ²},
StrictConcaveOn π s f β β {x y z : E}, x β s β y β s β x β y β z β openSegment π x y β min (f x) (f y) < f z
This theorem states that for any ordered semiring `π`, type `E` with an additive commutative monoid structure and scalar multiplication by `π`, and type `Ξ²` with a linearly ordered additive commutative monoid structure, a module structure, and ordered scalar multiplication by `π`, if a function `f` from `E` to `Ξ²` is strictly concave on a set `s`, then for any distinct elements `x` and `y` in `s`, and any element `z` in the open segment between `x` and `y`, the value of `f` at `z` is strictly greater than the minimum of the values of `f` at `x` and `y`.
In simpler terms, the theorem is saying that for a function that curves downwards, any point on the curve between two given points is always above the line connecting the two points.
More concisely: Given an ordered semiring `π`, an additive commutative monoid `E` with scalar multiplication by `π`, an ordered additive commutative monoid `Ξ²` with a module structure and ordered scalar multiplication by `π`, if `f` is a strictly concave function from `E` to `Ξ²` on a set `s`, then for any distinct `x, y` in `s` and any `z` in the open segment between `x` and `y`, `f(z) > min(f(x), f(y))`.
|
ConvexOn.le_on_segment
theorem ConvexOn.le_on_segment :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : LinearOrderedAddCommMonoid Ξ²] [inst_3 : SMul π E] [inst_4 : Module π Ξ²] [inst_5 : OrderedSMul π Ξ²]
{s : Set E} {f : E β Ξ²},
ConvexOn π s f β β {x y z : E}, x β s β y β s β z β segment π x y β f z β€ max (f x) (f y)
This theorem states that for any type `π`, `E`, and `Ξ²` with the required algebraic structures (an ordered semiring, an additive commutative monoid, a linearly ordered additive commutative monoid, and an ordered scalar multiplication respectively), a set `s` of type `E`, and a function `f` mapping from `E` to `Ξ²`, if the function `f` is convex on the set `s`, then for any elements `x`, `y`, and `z` of `E` such that `x` and `y` are in `s` and `z` is in the segment between `x` and `y`, the value of the function `f` at `z` is less than or equal to the maximum of the values of the function at `x` and `y`. In mathematical terms, if `f` is convex on a set `s`, then for any `x`, `y` in `s`, and `z` in the line segment joining `x` and `y`, `f(z) β€ max(f(x), f(y))`.
More concisely: If `f` is a convex function on a set `s` in an ordered semiring, then for any `x, y in s` and `z in [x, y]`, we have `f(z) β€ max(f(x), f(y))`.
|
ConcaveOn.comp_affineMap
theorem ConcaveOn.comp_affineMap :
β {π : Type u_1} {E : Type u_2} {F : Type u_3} {Ξ² : Type u_5} [inst : LinearOrderedField π]
[inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F] [inst_3 : OrderedAddCommMonoid Ξ²] [inst_4 : Module π E]
[inst_5 : Module π F] [inst_6 : SMul π Ξ²] {f : F β Ξ²} (g : E βα΅[π] F) {s : Set F},
ConcaveOn π s f β ConcaveOn π (βg β»ΒΉ' s) (f β βg)
This theorem states that if a function is concave on a set `s`, then it will remain concave when precomposed by an affine map. In other words, given a function `f` that is concave on a set `s`, and an affine transformation represented by `g`, the composition of `f` with `g` is also a concave function on the preimage of set `s` under `g`.
In mathematical terms, if `f` is concave on a set `s` and `g` is an affine map, then the function `(f β g)` is concave on the set `gβ»ΒΉ(s)`, where `gβ»ΒΉ(s)` is the preimage of `s` under `g`.
More concisely: If a concave function `f` is applied to an affine transformation `g` of its domain, the resulting composed function `(f β g)` is concave on the preimage `gβ»ΒΉ(s)` of the domain `s` under `g`.
|
neg_strictConvexOn_iff
theorem neg_strictConvexOn_iff :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : OrderedAddCommGroup Ξ²] [inst_3 : SMul π E] [inst_4 : Module π Ξ²] {s : Set E} {f : E β Ξ²},
StrictConvexOn π s (-f) β StrictConcaveOn π s f
This theorem states that for any ordered semiring `π`, any additive commutative monoid `E`, any ordered additive commutative group `Ξ²`, any scalar multiplication between `π` and `E`, any `π`-module `Ξ²`, any set `s` of type `E`, and any function `f` from `E` to `Ξ²`, the function `-f` is strictly convex on the set `s` if and only if `f` is strictly concave on the set `s`. In other words, negating a strictly concave function makes it strictly convex, and vice versa.
More concisely: For any ordered semiring `π`, additive commutative monoid `E`, ordered additive commutative group `Ξ²`, scalar multiplication between `π` and `E`, `π`-module `Ξ²`, set `s` of type `E`, and functions `f : E β Ξ²` with `-f` being the negation of `f`, `f` is strictly convex on `s` if and only if `-f` is strictly concave on `s`.
|
neg_strictConcaveOn_iff
theorem neg_strictConcaveOn_iff :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : OrderedAddCommGroup Ξ²] [inst_3 : SMul π E] [inst_4 : Module π Ξ²] {s : Set E} {f : E β Ξ²},
StrictConcaveOn π s (-f) β StrictConvexOn π s f
The theorem `neg_strictConcaveOn_iff` states that for a function `f` mapping elements of a set `s` in the type `E` to the type `Ξ²`, the negation of `f` is strictly concave if and only if `f` is strictly convex. Here, `π` is an ordered semiring, `E` is a type with a defined additive commutative monoid structure, `Ξ²` is a type with both ordered additive commutative group and `π`-module structures, and `s` is a subset of `E`. In terms of mathematics, a function is strictly concave if, at any two distinct points in the set, the function's value at the weighted average of the points is less than the weighted average of the function's values at those points. Conversely, a function is strictly convex if the inequality is reversed.
More concisely: The theorem `neg_strictConcaveOn_iff` in Lean 4 states that a function `f` mapping elements of a set `s` in an ordered semiring `π` with additive commutative monoid structure to a type `Ξ²` with ordered additive commutative group and `π`-module structures is negatively strictly concave if and only if it is positively strictly convex. That is, `f` satisfies `βa b in s, (a : π) * (b - a) / (1 : π) * (f a - f b) < 0` if and only if `-f` satisfies `βa b in s, (b - a) / (1 : π) * (f b - f a) > 0`.
|
ConvexOn.convex_le
theorem ConvexOn.convex_le :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : OrderedAddCommMonoid Ξ²] [inst_3 : SMul π E] [inst_4 : Module π Ξ²] [inst_5 : OrderedSMul π Ξ²] {s : Set E}
{f : E β Ξ²}, ConvexOn π s f β β (r : Ξ²), Convex π {x | x β s β§ f x β€ r}
The theorem `ConvexOn.convex_le` states that for any ordered semiring `π`, a set `E`, an ordered additively commutative monoid `Ξ²`, with a suitable scalar multiplication (as specified by `SMul π E`, `Module π Ξ²`, and `OrderedSMul π Ξ²`), a set `s` of type `E`, and a function `f` from `E` to `Ξ²`, if the function `f` is convex on the set `s`, then for any value `r` of type `Ξ²`, the subset of `s` where `f` is less than or equal to `r` is also a convex set.
In more informal terms, if a function is convex on a set, then the "level sets" of that function (the sets of points where the function value is below a certain level) are also convex.
More concisely: If a function is convex on a convex subset of an ordered semiring with respect to a suitable scalar multiplication, then the level sets of the function are also convex.
|
StrictConvexOn.translate_right
theorem StrictConvexOn.translate_right :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCancelCommMonoid E]
[inst_2 : OrderedAddCommMonoid Ξ²] [inst_3 : Module π E] [inst_4 : SMul π Ξ²] {s : Set E} {f : E β Ξ²},
StrictConvexOn π s f β β (c : E), StrictConvexOn π ((fun z => c + z) β»ΒΉ' s) (f β fun z => c + z)
The theorem `StrictConvexOn.translate_right` states that for all types `π`, `E` and `Ξ²`, where `π` is an ordered semiring, `E` is an add-cancel commutative monoid, `Ξ²` is an ordered add-commutative monoid, `π` is a module on `E`, and `π` is scalar multiply on `Ξ²`, if a function `f` is strictly convex on a set `s` of type `E`, then for every element `c` of type `E`, the function `f` remains strictly convex after being translated to the right by `c`. In other words, the strict convexity property of a function `f` is preserved under right translation. In set notation, the translated set is represented as `((fun z => c + z) β»ΒΉ' s)` and the translated function as `(f β fun z => c + z)`, where `β` denotes function composition.
More concisely: If `f` is a strictly convex function on a set `s` in an add-cancel commutative monoid `E`, over an ordered semiring `π` with module structure on `E` and scalar multiplication on an ordered add-commutative monoid `Ξ²`, then the translated function `f β (c +)` is strictly convex on the translated set `(c +)β»ΒΉ' s`, where `c` is an element in `E` and `(+)` denotes addition.
|
LinearOrder.strictConcaveOn_of_lt
theorem LinearOrder.strictConcaveOn_of_lt :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : OrderedAddCommMonoid Ξ²] [inst_3 : Module π E] [inst_4 : Module π Ξ²] [inst_5 : LinearOrder E] {s : Set E}
{f : E β Ξ²},
Convex π s β
(β β¦x : Eβ¦,
x β s β
β β¦y : Eβ¦,
y β s β x < y β β β¦a b : πβ¦, 0 < a β 0 < b β a + b = 1 β a β’ f x + b β’ f y < f (a β’ x + b β’ y)) β
StrictConcaveOn π s f
This theorem states that for a function defined on a convex set in a linearly ordered space (where the ordering and algebraic structures may not necessarily align), the function can be proven to be strictly concave if it satisfies the inequality `a β’ f(x) + b β’ f(y) < f(a β’ x + b β’ y)` for `x < y` and positive `a`, `b`. While this is primarily applicable when the domain `E` is the same as the base field `π`, it can also be extended to spaces like `π^n` with a lexicographic order. In essence, this theorem provides a condition under which a function is strictly concave on a given convex set.
More concisely: A real-valued function on a convex set of a linearly ordered space is strictly concave if for all x < y and positive a, b, the inequality a*x + b*y > x*f(x) + y*f(y) holds.
|
ConcaveOn.inf
theorem ConcaveOn.inf :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : LinearOrderedAddCommMonoid Ξ²] [inst_3 : SMul π E] [inst_4 : Module π Ξ²] [inst_5 : OrderedSMul π Ξ²]
{s : Set E} {f g : E β Ξ²}, ConcaveOn π s f β ConcaveOn π s g β ConcaveOn π s (f β g)
This theorem states that the pointwise minimum of two concave functions is also a concave function. In particular, if `f` and `g` are both concave functions on a set `s` with respect to a ordered semiring `π`, then the function `h` that maps each element `x` in `s` to the minimum of `f(x)` and `g(x)`, is also a concave function on `s` with respect to `π`. This is formalized in Lean 4 as `ConcaveOn π s f β ConcaveOn π s g β ConcaveOn π s (f β g)`, where `f β g` denotes the pointwise minimum of `f` and `g`.
More concisely: If `f` and `g` are concave functions on a set `s` with respect to an ordered semiring `π`, then their pointwise minimum `f β g` is also a concave function on `s` with respect to `π`.
|
ConcaveOn.neg
theorem ConcaveOn.neg :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : OrderedAddCommGroup Ξ²] [inst_3 : SMul π E] [inst_4 : Module π Ξ²] {s : Set E} {f : E β Ξ²},
ConcaveOn π s f β ConvexOn π s (-f)
The theorem `ConcaveOn.neg` states that for a given set `s` and a function `f` mapping elements from `E` to `Ξ²`, if `f` is concave on `s`, then the function `-f` (which is the negation of `f`) is convex on `s`. This theorem holds under certain conditions, such as `π` being an ordered semiring, `E` being an additive commutative monoid, `Ξ²` being an ordered additive commutative group, `E` being a scalar multiple under `π`, and `Ξ²` being a module over `π`.
More concisely: If `f` is concave on a set `s` in an ordered semiring `π`, then `-f` is convex on `s` provided that `E` is an additive commutative monoid, `Ξ²` is an ordered additive commutative group, `E` is a scalar multiple under `π`, and `Ξ²` is a module over `π`.
|
StrictConcaveOn.translate_right
theorem StrictConcaveOn.translate_right :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCancelCommMonoid E]
[inst_2 : OrderedAddCommMonoid Ξ²] [inst_3 : Module π E] [inst_4 : SMul π Ξ²] {s : Set E} {f : E β Ξ²},
StrictConcaveOn π s f β β (c : E), StrictConcaveOn π ((fun z => c + z) β»ΒΉ' s) (f β fun z => c + z)
The theorem states that the property of strict concavity is preserved under right translation. Specifically, for an arbitrary type `π` which is an ordered semiring, a type `E` which is an add-cancel-commutative monoid, and a type `Ξ²` that is an ordered-add-commutative monoid, if a function `f` from `E` to `Ξ²` is strictly concave on a certain set `s`, then for any element `c` of `E`, the function `f` composed with the operation of adding `c` is also strictly concave on the preimage of the set `s` under the operation of adding `c`.
In simpler terms, if a function has the property of being strictly concave on a set, and we shift every point in that set by the same amount (this is the right translation), the resulting function on the shifted set maintains the property of being strictly concave.
More concisely: If `f` is a strictly concave function from an add-cancel-commutative monoid `E` to an ordered-add-commutative monoid `Ξ²`, and `s` is a subset of `E`, then `f` composed with right translation by `c` in `E` is strictly concave on the preimage of `s` under right translation by `c`.
|
ConcaveOn.translate_left
theorem ConcaveOn.translate_left :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : OrderedAddCommMonoid Ξ²] [inst_3 : Module π E] [inst_4 : SMul π Ξ²] {s : Set E} {f : E β Ξ²},
ConcaveOn π s f β β (c : E), ConcaveOn π ((fun z => c + z) β»ΒΉ' s) (f β fun z => z + c)
The theorem `ConcaveOn.translate_left` states that for any given ordered semiring `π`, types `E` and `Ξ²`, where `E` forms an additive commutative monoid, `Ξ²` forms an ordered additive commutative monoid, `π` and `Ξ²` have a scalar multiplication operation, and `π` and `E` form a module, if a function `f` is concave on a set `s` of type `E`, then for any element `c` of type `E`, the function `f` remains concave on the set that results from translating every element of `s` by `c`. In other words, the left translation of the set `s` and the function `f` by the same element preserves the concavity of the function on the set. Here, a function is said to be concave on a set if the set is convex and for any two points in the set, the weighted average of the function values at these points is greater than or equal to the function value at the corresponding weighted average of the points.
More concisely: If `f` is concave on a convex set `s` in an additive commutative monoid `E` over an ordered semiring `π` with scalar multiplication, then `f` remains concave on the translated set `s + c`, where `c` is an element of `E`.
|
StrictConcaveOn.lt_on_open_segment'
theorem StrictConcaveOn.lt_on_open_segment' :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : LinearOrderedAddCommMonoid Ξ²] [inst_3 : SMul π E] [inst_4 : Module π Ξ²] [inst_5 : OrderedSMul π Ξ²]
{s : Set E} {f : E β Ξ²},
StrictConcaveOn π s f β
β {x y : E},
x β s β y β s β x β y β β {a b : π}, 0 < a β 0 < b β a + b = 1 β min (f x) (f y) < f (a β’ x + b β’ y)
The theorem `StrictConcaveOn.lt_on_open_segment'` states that for a given strictly concave function `f` on a set `s` of elements of type `E` (where types `E` and `Ξ²` have a specific algebraic structure), for any two distinct points `x` and `y` in `s`, and any two 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 greater than the minimum of the function values at `x` and `y`. In other words, a strictly concave function on an open segment is strictly lower-bounded by the minimum of its endpoints.
More concisely: For any strictly concave function $f$ on an open segment $s$ of real numbers and any distinct $x, y \in s$, there holds $f(ax+(1-a)y) < \min(fx, fy)$ for all $0 < a < 1$.
|
StrictConvexOn.lt_on_openSegment
theorem StrictConvexOn.lt_on_openSegment :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : LinearOrderedAddCommMonoid Ξ²] [inst_3 : SMul π E] [inst_4 : Module π Ξ²] [inst_5 : OrderedSMul π Ξ²]
{s : Set E} {f : E β Ξ²},
StrictConvexOn π s f β β {x y z : E}, x β s β y β s β x β y β z β openSegment π x y β f z < max (f x) (f y)
The theorem `StrictConvexOn.lt_on_openSegment` asserts that for any type `π` equipped with an ordered semiring structure, a type `E` equipped with an additive commutative monoid structure and scalar multiplication by `π`, and a type `Ξ²` equipped with a linearly ordered additive commutative monoid structure, a module structure over `π`, and an ordered scalar multiplication by `π`, if a function `f` from `E` to `Ξ²` is strictly convex on a set `s` of type `E`, then for any distinct `x` and `y` in `s` and any `z` in the open segment between `x` and `y`, the value of `f` at `z` is strictly less than the maximum of the values of `f` at `x` and `y`. In other words, a strictly convex function on an open segment is strictly upper-bounded by the maximum of its endpoints.
More concisely: If `f` is a strictly convex function on an open segment in the ordered semiring `π`-module `E` over the linearly ordered additive commutative monoid `Ξ²`, then `f(z) < max(f(x), f(y))` for any distinct `x, y` in the segment and any `z` in the open segment between `x` and `y`.
|
ConvexOn.neg
theorem ConvexOn.neg :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : OrderedAddCommGroup Ξ²] [inst_3 : SMul π E] [inst_4 : Module π Ξ²] {s : Set E} {f : E β Ξ²},
ConvexOn π s f β ConcaveOn π s (-f)
The theorem `ConvexOn.neg` states that for any ordered semiring `π`, a set `s` of elements of type `E`, and a function `f` from `E` to `Ξ²` where `Ξ²` is an ordered additively commutative group, if the function `f` is convex over the set `s`, then the function `-f` (the negation of `f`) is concave over the same set `s`. This means that if for any two points in the set, the function value at a weighted average of the points is no less than the weighted average of the function values at the two points (the property of convexity), then for the negated function `-f`, the function value at the weighted average of any two points in the set is no more than the weighted average of the function values at the two points (the property of concavity).
More concisely: If a function `f` from an ordered semiring to an ordered additively commutative group is convex over a set `s`, then the negation `-f` is concave over the same set `s`. That is, for all `x, y in s` and `r in [0, 1]`, we have `-f(rx + (1-r)y) <= r*-f(x) + (1-r)*(-f(y))`.
|
ConvexOn.le_on_segment'
theorem ConvexOn.le_on_segment' :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : LinearOrderedAddCommMonoid Ξ²] [inst_3 : SMul π E] [inst_4 : Module π Ξ²] [inst_5 : OrderedSMul π Ξ²]
{s : Set E} {f : E β Ξ²},
ConvexOn π s f β
β {x y : E}, x β s β y β s β β {a b : π}, 0 β€ a β 0 β€ b β a + b = 1 β f (a β’ x + b β’ y) β€ max (f x) (f y)
This theorem states that for any ordered semiring `π`, any type `E` with an additive commutative monoid structure, and any type `Ξ²` with a linearly ordered additive commutative monoid structure, if we have a function `f` from `E` to `Ξ²` that is convex on a set `s` of elements from `E`, then for any two elements `x` and `y` in `s` and any two non-negative elements `a` and `b` from `π` that sum to 1, the value of `f` at the point `a β’ x + b β’ y` (where `β’` denotes the scalar multiplication) is less than or equal to the maximum of the values of `f` at `x` and `y`. In other words, a convex function on a line segment does not exceed the maximum of its values at the endpoints of the segment.
More concisely: For any ordered semiring `π`, any additive commutative monoid `E`, any additive commutative monoid `Ξ²` with a total order, and any convex function `f` from `E` to `Ξ²` on a subset `s`, we have `f (a * x + b * y) β€ max (f x, f y)` for all `x, y β s` and `a, b β π` such that `a β₯ 0`, `b β₯ 0`, and `a + b = 1`.
|
ConvexOn.add
theorem ConvexOn.add :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : OrderedAddCommMonoid Ξ²] [inst_3 : SMul π E] [inst_4 : DistribMulAction π Ξ²] {s : Set E} {f g : E β Ξ²},
ConvexOn π s f β ConvexOn π s g β ConvexOn π s (f + g)
The theorem `ConvexOn.add` states that for any type `π` with an ordered semiring structure, another type `E` with an addition commutative monoid structure, and a third type `Ξ²` with an ordered addition commutative monoid structure, if `π` and `Ξ²` have scalar multiplication and `π` and `Ξ²` have a distributive multiplication action, then given a set `s` of elements of type `E` and two functions `f` and `g` from `E` to `Ξ²`, if both `f` and `g` are convex on `s`, then their pointwise sum `(f + g)` is also convex on `s`.
In other words, the sum of two convex functions on a given set is also a convex function on that set.
More concisely: If `π` is an ordered semiring, `E` is an additive commutative monoid, and `Ξ²` is an ordered additive commutative monoid with distributive multiplication actions of `π` over both `E` and `Ξ²`, then the pointwise sum of two convex functions from `E` to `Ξ²` is convex.
|
ConvexOn.translate_left
theorem ConvexOn.translate_left :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : OrderedAddCommMonoid Ξ²] [inst_3 : Module π E] [inst_4 : SMul π Ξ²] {s : Set E} {f : E β Ξ²},
ConvexOn π s f β β (c : E), ConvexOn π ((fun z => c + z) β»ΒΉ' s) (f β fun z => z + c)
The theorem `ConvexOn.translate_left` states that for any ordered semiring `π`, types `E` and `Ξ²`, where `E` is an additive commutative monoid module over `π`, `Ξ²` is an ordered additive commutative monoid that is also a semimodule over `π`, a set `s` of type `E`, and a function `f` from `E` to `Ξ²`, if the function `f` is convex on the set `s`, then for any element `c` of type `E`, the function `f` composed with the translation by `c`, is convex on the preimage of the set `s` under the translation by `c`. In other words, left translation preserves the convexity of functions.
More concisely: If `f` is a convex function on a set `s` in an additive commutative monoid module `E` over an ordered semiring, then the translated function `f(x + c)` is convex on the set `{x : E | x β s}`, where `c` is an element of `E`.
|
ConvexOn.sup
theorem ConvexOn.sup :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : LinearOrderedAddCommMonoid Ξ²] [inst_3 : SMul π E] [inst_4 : Module π Ξ²] [inst_5 : OrderedSMul π Ξ²]
{s : Set E} {f g : E β Ξ²}, ConvexOn π s f β ConvexOn π s g β ConvexOn π s (f β g)
This theorem states that given any ordered semiring `π`, a set `s` in some additive commutative monoid `E`, and two functions `f` and `g` from `E` to a linearly ordered additive commutative monoid `Ξ²` which is also a `π`-module and has an ordered scalar multiplication, if both `f` and `g` are convex on `s`, then the pointwise maximum of `f` and `g` is also convex on `s`. In other words, for any `x` and `y` in `s` and any non-negative scalars `a` and `b` in `π` such that `a + b = 1`, the maximum value of `f` and `g` at the point `a * x + b * y` is less than or equal to the linear combination `a * max(f(x), g(x)) + b * max(f(y), g(y))`. The `max` function is represented by the `β` operator.
More concisely: Given an ordered semiring `π`, a set `s` in some additive commutative monoid `E`, and functions `f` and `g` from `E` to a linearly ordered additive commutative `π`-module `Ξ²`, if `f` and `g` are convex on `s`, then the pointwise maximum of `f` and `g` is also convex on `s`, i.e., for all `x, y β s` and non-negative scalars `a, b β π` with `a + b = 1`, `a * f(x) + b * g(x) β€ max(a * f(x) + b * g(x), a * max(f(x), g(x)) + b * max(f(y), g(y)))`.
|
StrictConcaveOn.eq_of_isMaxOn
theorem StrictConcaveOn.eq_of_isMaxOn :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : LinearOrderedField π] [inst_1 : OrderedAddCommMonoid Ξ²]
[inst_2 : AddCommMonoid E] [inst_3 : SMul π E] [inst_4 : Module π Ξ²] [inst_5 : OrderedSMul π Ξ²] {f : E β Ξ²}
{s : Set E} {x y : E}, StrictConcaveOn π s f β IsMaxOn f s x β IsMaxOn f s y β x β s β y β s β x = y
The theorem `StrictConcaveOn.eq_of_isMaxOn` states that for any strictly concave function `f` on a set `s`, if two elements `x` and `y` in `s` are each a global maximum of `f` on `s`, then `x` must be equal to `y`. In other words, a strictly concave function can have at most one global maximum on a given set.
In more formal terms, given an ordered field `π`, additively commutative monoids `E` and `Ξ²` with a module structure of `π` on `Ξ²`, and an ordered scalar multiplication between `π` and `Ξ²`, if `f` is a function from `E` to `Ξ²` that is strictly concave on a set `s`, and `x` and `y` are points in `s` where `f` attains its maximum value on `s`, then `x` and `y` must be the same point.
More concisely: If `f` is a strictly concave function on a set `s`, then any two global maxima of `f` on `s` are equal.
|
StrictConvexOn.neg
theorem StrictConvexOn.neg :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : OrderedAddCommGroup Ξ²] [inst_3 : SMul π E] [inst_4 : Module π Ξ²] {s : Set E} {f : E β Ξ²},
StrictConvexOn π s f β StrictConcaveOn π s (-f)
This theorem, `StrictConvexOn.neg`, states that for any ordered semiring `π`, any type `E` with an addition operation defining it as a commutative monoid, any type `Ξ²` forming an ordered additive group, and any `s` of type `Set E`, if a function `f` mapping `E` to `Ξ²` is strictly convex on `s`, then the function `-f` is strictly concave on `s`. In other words, negating a strictly convex function results in a strictly concave function.
More concisely: If `f : E β Ξ²` is strictly convex on a set `s` in an ordered semiring `π` where `E` is a commutative monoid with additive structure, then `-f : E β Ξ²` is strictly concave on `s`.
|
ConcaveOn.translate_right
theorem ConcaveOn.translate_right :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : OrderedAddCommMonoid Ξ²] [inst_3 : Module π E] [inst_4 : SMul π Ξ²] {s : Set E} {f : E β Ξ²},
ConcaveOn π s f β β (c : E), ConcaveOn π ((fun z => c + z) β»ΒΉ' s) (f β fun z => c + z)
The theorem `ConcaveOn.translate_right` states that for any ordered semiring `π`, types `E` and `Ξ²` where `E` is an additive commutative monoid, `Ξ²` is an ordered additive commutative monoid and both `E` and `Ξ²` are scalar multiplicative under `π`, given a set `s` of type `E` and a function `f` mapping `E` to `Ξ²`, if the function `f` is concave on the set `s`, then for any element `c` of type `E`, the function `f` remains concave on the set obtained by right-translation of `s` by `c`. In other words, concavity is preserved under right-translation.
More concisely: If `f` is a concave function on a set `s` in an additive commutative monoid `E` over an ordered semiring `π`, where `E` is scalar multiplicative over `π` and `Ξ²` is an ordered additive commutative monoid, then `f` remains concave on the right-translated set `s + c`.
|
LinearOrder.strictConvexOn_of_lt
theorem LinearOrder.strictConvexOn_of_lt :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : OrderedAddCommMonoid Ξ²] [inst_3 : Module π E] [inst_4 : Module π Ξ²] [inst_5 : LinearOrder E] {s : Set E}
{f : E β Ξ²},
Convex π s β
(β β¦x : Eβ¦,
x β s β
β β¦y : Eβ¦,
y β s β x < y β β β¦a b : πβ¦, 0 < a β 0 < b β a + b = 1 β f (a β’ x + b β’ y) < a β’ f x + b β’ f y) β
StrictConvexOn π s f
This theorem states that for a function defined on a convex set in a linearly ordered space (where the order and the algebraic structures may not be compatible), it's sufficient to demonstrate the inequality `f(a * x + b * y) < a * f(x) + b * f(y)` for `x < y` alongside positive `a` and `b` to prove that the function is strictly convex. Even though the primary application of this theorem is when the domain `E` is the same as the field of scalars `π`, it can also be applied to more complex spaces, such as `π^n` with lexicographic order.
More concisely: Given a function `f` on a convex set in a linearly ordered space, if `f(a * x + b * y) < a * f(x) + b * f(y)` holds for all `x < y` and positive `a, b`, then `f` is strictly convex.
|
ConvexOn.comp_affineMap
theorem ConvexOn.comp_affineMap :
β {π : Type u_1} {E : Type u_2} {F : Type u_3} {Ξ² : Type u_5} [inst : LinearOrderedField π]
[inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F] [inst_3 : OrderedAddCommMonoid Ξ²] [inst_4 : Module π E]
[inst_5 : Module π F] [inst_6 : SMul π Ξ²] {f : F β Ξ²} (g : E βα΅[π] F) {s : Set F},
ConvexOn π s f β ConvexOn π (βg β»ΒΉ' s) (f β βg)
This theorem states that if a function is convex on a set `s`, it will remain convex even when precomposed with an affine transformation. In more detail, given a function `f` from type `F` to `Ξ²` which is convex on a set `s` of type `F`, and an affine transformation `g` from type `E` to `F`, the convexity of `f` is preserved when it is composed with `g` and applied to the preimage of `s` under `g`. This means that the function `f` β `g` is convex on the set `g`β»ΒΉ(`s`).
More concisely: If `f` is a convex function from `F` to `Ξ²` over a set `s` and `g` is an affine transformation from `E` to `F`, then the composite function `f β g` is convex over the preimage `gβ»ΒΉ(s)` in `E`.
|
LinearOrder.concaveOn_of_lt
theorem LinearOrder.concaveOn_of_lt :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : OrderedAddCommMonoid Ξ²] [inst_3 : Module π E] [inst_4 : Module π Ξ²] [inst_5 : LinearOrder E] {s : Set E}
{f : E β Ξ²},
Convex π s β
(β β¦x : Eβ¦,
x β s β
β β¦y : Eβ¦,
y β s β x < y β β β¦a b : πβ¦, 0 < a β 0 < b β a + b = 1 β a β’ f x + b β’ f y β€ f (a β’ x + b β’ y)) β
ConcaveOn π s f
The theorem `LinearOrder.concaveOn_of_lt` states that for a function defined on a convex set in a linearly ordered space, the function is concave if, for every pair of elements `x` and `y` in the set where `x` is less than `y`, and for every pair of positive real numbers `a` and `b` that sum to 1, the inequality `a β’ f(x) + b β’ f(y) β€ f(a β’ x + b β’ y)` holds. This theorem applies even when the order and algebraic structures of the space are not necessarily compatible. The primary application of this theorem is when the space is the set of real numbers, although it also applies to `β^n` with lexicographic order.
More concisely: A real-valued function defined on a linearly ordered set is concave if for any pair of elements x < y and any pair of positive real numbers a, b summing to 1, the inequality a * f(x) + b * f(y) β€ f(a * x + b * y) holds.
|
StrictConvexOn.lt_on_open_segment'
theorem StrictConvexOn.lt_on_open_segment' :
β {π : Type u_1} {E : Type u_2} {Ξ² : Type u_5} [inst : OrderedSemiring π] [inst_1 : AddCommMonoid E]
[inst_2 : LinearOrderedAddCommMonoid Ξ²] [inst_3 : SMul π E] [inst_4 : Module π Ξ²] [inst_5 : OrderedSMul π Ξ²]
{s : Set E} {f : E β Ξ²},
StrictConvexOn π s f β
β {x y : E},
x β s β y β s β x β y β β {a b : π}, 0 < a β 0 < b β a + b = 1 β f (a β’ x + b β’ y) < max (f x) (f y)
This theorem states that for any ordered semiring `π`, types `E` and `Ξ²` where `E` is an additively commutative monoid, `Ξ²` is a linearly ordered additive commutative monoid, `π` is a scalar multiplication on `E` and `Ξ²`, and `π` is an ordered scalar multiplication on `Ξ²`, if we have a set `s` of type `E` and a function `f` from `E` to `Ξ²` that exhibits strict convexity on set `s`, then for any two distinct elements `x` and `y` in `s` and any two positive scalars `a` and `b` from `π` that sum to 1, the value of the function `f` at the point `(aβ’x + bβ’y)` is less than the maximum of the function values at `x` and `y`. That is, a strictly convex function on an open segment is always strictly less than the maximum of its values at the segment endpoints.
More concisely: Given an ordered semiring `π`, an additively commutative monoid `E` with a strict convex function `f` from `E` to a linearly ordered additive commutative monoid `Ξ²`, and scalars `a, b β π` such that `a β₯ 0`, `b β₯ 0`, and `a + b = 1`, then `f(a * x + b * y) < max(f(x), f(y))` for any distinct `x, y β E`.
|