IsMaxOn.of_isLocalMax_of_convex_univ
theorem IsMaxOn.of_isLocalMax_of_convex_univ :
∀ {E : Type u_1} {β : Type u_2} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : Module ℝ E]
[inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul ℝ E] [inst_5 : OrderedAddCommGroup β]
[inst_6 : Module ℝ β] [inst_7 : OrderedSMul ℝ β] {f : E → β} {a : E},
IsLocalMax f a → ConcaveOn ℝ Set.univ f → ∀ (x : E), f x ≤ f a
This theorem states that if a function has a local maximum at a point and the function is concave on the entire domain, then that local maximum is also a global maximum. More formally, for a function `f` from a set `E` to a set `β`, where `E` is an additive commutative group with a topology and a real-number module structure, and `β` is an ordered additive commutative group with a real-number module structure, if `f` has a local maximum at a point `a` and `f` is concave on the entire domain of `E`, then for every point `x` in `E`, the value of `f` at `x` is less than or equal to the value of `f` at `a`. The concavity of `f` and the existence of a local maximum together ensure that no other point in the domain of `f` can have a higher function value than `a`.
More concisely: If a concave function attains a local maximum at a point, then that point is a global maximum.
|
IsMinOn.of_isLocalMinOn_of_convexOn
theorem IsMinOn.of_isLocalMinOn_of_convexOn :
∀ {E : Type u_1} {β : Type u_2} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : Module ℝ E]
[inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul ℝ E] [inst_5 : OrderedAddCommGroup β]
[inst_6 : Module ℝ β] [inst_7 : OrderedSMul ℝ β] {s : Set E} {f : E → β} {a : E},
a ∈ s → IsLocalMinOn f s a → ConvexOn ℝ s f → IsMinOn f s a
This theorem states that if `a` is a point in a set `s`, and `f` is a function from `E` to `β` that has a local minimum at `a` and is convex on `s`, then `a` is a global minimum on `s`. In other words, if a function is convex on a set and has a local minimum at a point within this set, then this local minimum is also a global minimum within that set. Here, `E` is a type equipped with an addition operation forming a commutative group, a topology, a module structure over the real numbers, and a continuous scalar multiplication. `β` is a type that forms an ordered additive commutative group and a module over the real numbers with an ordered scalar multiplication.
More concisely: If `f` is a convex function with a local minimum at `a` in the set `s`, then `a` is the global minimum of `f` on `s`.
|
IsMinOn.of_isLocalMin_of_convex_univ
theorem IsMinOn.of_isLocalMin_of_convex_univ :
∀ {E : Type u_1} {β : Type u_2} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : Module ℝ E]
[inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul ℝ E] [inst_5 : OrderedAddCommGroup β]
[inst_6 : Module ℝ β] [inst_7 : OrderedSMul ℝ β] {f : E → β} {a : E},
IsLocalMin f a → ConvexOn ℝ Set.univ f → ∀ (x : E), f a ≤ f x
The theorem `IsMinOn.of_isLocalMin_of_convex_univ` states that for any function `f` mapping from a type `E` to a type `β`, where `E` is an additive commutative group with a continuous scalar multiplication operation, a topological space, and a topological additive group, and `β` is an ordered additive commutative group with a scalar multiplication operation, if `f` has a local minimum at a point `a` and `f` is convex on the universal set of `E`, then `f` has a global minimum at `a`. In other words, for all elements `x` of `E`, the value of `f` at `a` is less than or equal to the value of `f` at `x`.
More concisely: If a function `f` mapping from an additive commutative group `E` (with continuous scalar multiplication, topological space, and topological additive group structure) to an ordered additive commutative group `β` with scalar multiplication has a local minimum at `a` and is convex on `E`'s universal set, then `a` is a global minimum of `f`.
|
IsMinOn.of_isLocalMinOn_of_convexOn_Icc
theorem IsMinOn.of_isLocalMinOn_of_convexOn_Icc :
∀ {β : Type u_2} [inst : OrderedAddCommGroup β] [inst_1 : Module ℝ β] [inst_2 : OrderedSMul ℝ β] {f : ℝ → β}
{a b : ℝ}, a < b → IsLocalMinOn f (Set.Icc a b) a → ConvexOn ℝ (Set.Icc a b) f → IsMinOn f (Set.Icc a b) a
This theorem states that if `f` is a real-valued function that has a local minimum at `a` within a closed interval from `a` to `b` (`a` and `b` are real numbers with `a` less than `b`), and `f` is convex on this closed interval, then `f` actually has a global minimum at `a` on this closed interval. In other words, if `f` is convex and has a local minimum at the left endpoint of a closed interval, then this local minimum is also a global minimum on that interval.
More concisely: If a real-valued, convex function `f` has a local minimum at `a` within a closed interval [`a`, `b`], then `a` is the global minimum of `f` on that interval.
|
IsMaxOn.of_isLocalMaxOn_of_concaveOn
theorem IsMaxOn.of_isLocalMaxOn_of_concaveOn :
∀ {E : Type u_1} {β : Type u_2} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : Module ℝ E]
[inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul ℝ E] [inst_5 : OrderedAddCommGroup β]
[inst_6 : Module ℝ β] [inst_7 : OrderedSMul ℝ β] {s : Set E} {f : E → β} {a : E},
a ∈ s → IsLocalMaxOn f s a → ConcaveOn ℝ s f → IsMaxOn f s a
The theorem `IsMaxOn.of_isLocalMaxOn_of_concaveOn` states that for a given set `s` and a function `f` mapping from a certain type `E` to another type `β` (with `E` being a topological additive group and a real vector space, and `β` being an ordered additive commutative group and a real vector space), if an element `a` in `s` is a local maximum of the function `f` and the function `f` is concave on set `s`, then `a` is also a global maximum of the function `f` restricted to the set `s`.
In other words, if a point is a local maximum of a concave function on a certain set, then this point is also a global maximum on this set.
More concisely: If a local maximum of a concave function lies in a set, then it is the global maximum of that function on that set.
|