LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Analysis.Convex.Jensen

`ConcaveOn.min_le_of_mem_Icc` theorem ConcaveOn.min_le_of_mem_Icc : ∀ {𝕜 : Type u_1} {β : Type u_4} [inst : LinearOrderedField 𝕜] [inst_1 : LinearOrderedAddCommGroup β] [inst_2 : Module 𝕜 β] [inst_3 : OrderedSMul 𝕜 β] {f : 𝕜 → β} {x y z : 𝕜}, ConcaveOn 𝕜 (Set.Icc x y) f → z ∈ Set.Icc x y → min (f x) (f y) ≤ f z The theorem, referred to as the "Minimum principle" for concave functions on an interval, states that for any types `𝕜` and `β` where `𝕜` is a linear ordered field and `β` is a linear ordered additive commutative group, and for any function `f` from `𝕜` to `β`, with `x`, `y`, and `z` elements of `𝕜`: if `f` is concave on the closed interval from `x` to `y` (inclusive), and `z` is an element of this interval, then the minimum value of `f` at `x` and `f` at `y` is less than or equal to the value of `f` at `z`. In other words, for a concave function on a closed interval, the lowest value is attained at the endpoints of the interval. More concisely: For any concave function `f` from a linear ordered field `𝕜` to a linear ordered additive commutative group `β`, and for any `x`, `y` in `𝕜` with `x <= y`, if `f` is concave on the interval `[x, y]`, then `f x <= f z <= f y` for all `z` in `[x, y]`.
`ConvexOn.le_max_of_mem_Icc` theorem ConvexOn.le_max_of_mem_Icc : ∀ {𝕜 : Type u_1} {β : Type u_4} [inst : LinearOrderedField 𝕜] [inst_1 : LinearOrderedAddCommGroup β] [inst_2 : Module 𝕜 β] [inst_3 : OrderedSMul 𝕜 β] {f : 𝕜 → β} {x y z : 𝕜}, ConvexOn 𝕜 (Set.Icc x y) f → z ∈ Set.Icc x y → f z ≤ max (f x) (f y) The Maximum Principle theorem for convex functions posits that given a function `f` from a Linear Ordered Field `𝕜` to a Linear Ordered Additive Commutative Group `β`, if `f` is convex on the closed interval `[x, y]`, then for any point `z` in the interval `[x, y]`, the function value `f(z)` is less than or equal to the maximum of either `f(x)` or `f(y)`. In other words, a convex function reaches its maximum value at the endpoints of a closed interval. More concisely: If `f` is a convex function on the closed interval `[x, y]` in a Linear Ordered Field `𝕜`, then `f(z) ≤ max(f(x), f(y))` for all `z` in `[x, y]`.
`StrictConvexOn.map_sum_eq_iff'` theorem StrictConvexOn.map_sum_eq_iff' : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : OrderedAddCommGroup β] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 β] [inst_5 : OrderedSMul 𝕜 β] {s : Set E} {f : E → β} {t : Finset ι} {w : ι → 𝕜} {p : ι → E}, StrictConvexOn 𝕜 s f → (∀ i ∈ t, 0 ≤ w i) → (t.sum fun i => w i) = 1 → (∀ i ∈ t, p i ∈ s) → ((f (t.sum fun i => w i • p i) = t.sum fun i => w i • f (p i)) ↔ ∀ j ∈ t, w j ≠ 0 → p j = t.sum fun i => w i • p i) This theorem is the canonical form of the equality case of Jensen's inequality. For a strictly convex function `f` and nonnegative weights `w`, it states that the equality `f (∑ i in t, w i • p i) = ∑ i in t, w i • f (p i)` holds if and only if all points `p` with nonzero weight are identical, specifically equal to their center of mass with respect to `w`. This condition is under the assumptions that: the function `f` is strictly convex on a set `s`, the weights `w` are nonnegative, the sum of the weights is 1, and the points `p` belong to the set `s`. In essence, it gives a sufficient and necessary condition for the equality part of Jensen's inequality to hold for a strictly convex function. More concisely: For a strictly convex function and nonnegative, normalized weights, the equality in Jensen's inequality holds if and only if all nonzero weighted points have the same value, which is equal to their weighted average with respect to the given weights.
`ConvexOn.le_max_of_mem_segment` theorem ConvexOn.le_max_of_mem_segment : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : LinearOrderedAddCommGroup β] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 β] [inst_5 : OrderedSMul 𝕜 β] {f : E → β} {x y z : E}, ConvexOn 𝕜 (segment 𝕜 x y) f → z ∈ segment 𝕜 x y → f z ≤ max (f x) (f y) This is the Maximum Principle for convex functions on a segment. It states that for any linearly ordered field `𝕜`, any type `E` that is both an additive group and a `𝕜`-module, and any type `β` that is a linearly ordered additive group, a `𝕜`-module, and supports an order-preserving scalar multiplication, if a function `f` from `E` to `β` is convex on the segment from `x` to `y` (both of type `E`), then for any `z` in this segment, the value of `f` at `z` is less than or equal to the maximum of the values of `f` at `x` and `y`. In other words, if a function is convex on a segment, its maximum on that segment is achieved at one of the endpoints. More concisely: If `f` is a convex function on the segment between `x` and `y` in a linearly ordered field `𝕜`, an additive group and `𝕜`-module `E`, and `β` is a linearly ordered additive group, an `𝕜`-module, and supports order-preserving scalar multiplication, then `f(z) ≤ max(f(x), f(y))` for all `z` in the segment.
`ConcaveOn.le_map_sum` theorem ConcaveOn.le_map_sum : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : OrderedAddCommGroup β] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 β] [inst_5 : OrderedSMul 𝕜 β] {s : Set E} {f : E → β} {t : Finset ι} {w : ι → 𝕜} {p : ι → E}, ConcaveOn 𝕜 s f → (∀ i ∈ t, 0 ≤ w i) → (t.sum fun i => w i) = 1 → (∀ i ∈ t, p i ∈ s) → (t.sum fun i => w i • f (p i)) ≤ f (t.sum fun i => w i • p i) This is a version of the famous Jensen's inequality that applies to concave functions and finite sums. The theorem is formulated for a certain context defined by types `𝕜` (a linear ordered field), `E` (an additive commutative group), `β` (an ordered additive commutative group), and `ι` (an index type). Here, `s` is a set of type `E`, `f` is a function mapping elements of `E` to `β`, `t` is a finite set (or, a `Finset`) indexed by `ι`, `w` is a weight function on the index set, and `p` maps indices to elements of `E`. The theorem states that if `f` is concave on `s`, all weights are nonnegative and sum up to 1, and all the points `p i` lie in `s` for every index `i` in `t`, then the weighted sum of `f` over the points `p i` is less than or equal to `f` applied to the weighted sum of the points `p i`. This is a fundamental result about concave functions and provides a generalization of the concept that, for such functions, the graph lies below the chord joining any two points on it. More concisely: If `f` is a concave function on a set `s` in a linear ordered field, and `w` is a set of nonnegative weights summing to 1 with indices in a finite set `t`, then the weighted sum of `f(p i)` over `i` in `t` is less than or equal to `f(∑ i in t w i * p i)`.
`ConcaveOn.map_add_sum_le` theorem ConcaveOn.map_add_sum_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : OrderedAddCommGroup β] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 β] [inst_5 : OrderedSMul 𝕜 β] {s : Set E} {f : E → β} {t : Finset ι} {w : ι → 𝕜} {p : ι → E} {v : 𝕜} {q : E}, ConcaveOn 𝕜 s f → (∀ i ∈ t, 0 ≤ w i) → (v + t.sum fun i => w i) = 1 → (∀ i ∈ t, p i ∈ s) → 0 ≤ v → q ∈ s → (v • f q + t.sum fun i => w i • f (p i)) ≤ f (v • q + t.sum fun i => w i • p i) The theorem `ConcaveOn.map_add_sum_le` is a version of Jensen's inequality for concave functions, where an element plays a distinguished role. Given a linearly ordered field `𝕜`, an additively commutative group `E`, an ordered additively commutative group `β`, a module of `E` over `𝕜`, a module of `β` over `𝕜`, and an ordered scalar multiplication of `β` by `𝕜`, it states that if we have a function `f` that is concave on a set `s`, then for any finite set `t` and its associated weights `w` (all non-negative), any element `q` in `s` with non-negative weight `v`, and any mapping `p` from `t` to `s` which sums with `v` to `1`, the weighted sum of the function values at `q` and `p(i)` is less than or equal to the function value at the corresponding weighted sum of `q` and `p(i)`. More concisely: Given a concave function `f` on a set `s`, the weighted sum of `f` at elements `q` and `p(i)` in `s` with non-negative weights `v` and `w_i` that sum to `1`, satisfies `f(q * v + ∑(i in t) p(i) * w_i) ≤ f(q) * v + ∑(i in t) f(p(i)) * w_i`.
`StrictConvexOn.map_sum_lt` theorem StrictConvexOn.map_sum_lt : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : OrderedAddCommGroup β] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 β] [inst_5 : OrderedSMul 𝕜 β] {s : Set E} {f : E → β} {t : Finset ι} {w : ι → 𝕜} {p : ι → E}, StrictConvexOn 𝕜 s f → (∀ i ∈ t, 0 < w i) → (t.sum fun i => w i) = 1 → (∀ i ∈ t, p i ∈ s) → (∃ j ∈ t, ∃ k ∈ t, p j ≠ p k) → f (t.sum fun i => w i • p i) < t.sum fun i => w i • f (p i) This theorem states the strict Jensen inequality for a function that is strictly convex on a set. In more precise terms, given a type `𝕜` with a linear ordered field structure, a type `E` with an additive commutative group structure and a 𝕜-module structure, a type `β` with an ordered additive commutative group structure and a 𝕜-module structure, a set `s` in `E`, a function `f` from `E` to `β`, a finite set `t` indexed by type `ι`, a weight function `w` from `ι` to `𝕜`, and a point function `p` from `ι` to `E`, if the following conditions are satisfied: - The function `f` is strictly convex on the set `s`, - For every index in `t`, the corresponding weight is strictly positive, - The sum of all the weights is 1, - For every index in `t`, the corresponding point is in the set `s`, - There exist two different points in the set `t`, then the value of the function `f` at the weighted sum of the points is strictly less than the weighted sum of the function values at the points. This expresses the idea that, under these conditions, the function `f` lies strictly below the line segment connecting the points `(a, f(a))` and `(b, f(b))` for any points `a` and `b` in the set `s`. More concisely: If `f` is a strictly convex function on a set `s` in a real vector space, and `w` is a set of strictly positive weights summing to 1 with corresponding points `p` in `s`, then `∑(wi * f(pi)) < f(∑(wi * pi))`.
`StrictConvexOn.map_sum_eq_iff` theorem StrictConvexOn.map_sum_eq_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : OrderedAddCommGroup β] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 β] [inst_5 : OrderedSMul 𝕜 β] {s : Set E} {f : E → β} {t : Finset ι} {w : ι → 𝕜} {p : ι → E}, StrictConvexOn 𝕜 s f → (∀ i ∈ t, 0 < w i) → (t.sum fun i => w i) = 1 → (∀ i ∈ t, p i ∈ s) → ((f (t.sum fun i => w i • p i) = t.sum fun i => w i • f (p i)) ↔ ∀ j ∈ t, p j = t.sum fun i => w i • p i) This theorem corresponds to the canonical form of the equality case of Jensen's equality for a strictly convex function. Specifically, it states that for any strictly convex function `f` defined on a set `s`, and for any positive weights `w`, the equality `f (∑ i in t, w i • p i) = ∑ i in t, w i • f (p i)` holds if and only if all points `p` are equal. Furthermore, all these points must equal to their weighted average (or center of mass with respect to `w`). Here `∑ i in t, w i • p i` denotes the weighted sum of the points `p`, and `∑ i in t, w i • f (p i)` denotes the weighted sum of the function values `f(p)`. The weights `w` are assumed to be positive and sum up to 1, and the points `p` are assumed to lie in the set `s`. More concisely: For a strictly convex function `f` and positive weights `w` summing to 1 over a set `s`, the equality of the weighted sums of function values `∑ i in t, w i • f(p i)` and weighted sums of points `∑ i in t, w i • p i` holds if and only if all points `p` in `s` are equal and equal to their respective weighted averages.
`StrictConcaveOn.eq_of_map_sum_eq` theorem StrictConcaveOn.eq_of_map_sum_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : OrderedAddCommGroup β] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 β] [inst_5 : OrderedSMul 𝕜 β] {s : Set E} {f : E → β} {t : Finset ι} {w : ι → 𝕜} {p : ι → E}, StrictConcaveOn 𝕜 s f → (∀ i ∈ t, 0 < w i) → (t.sum fun i => w i) = 1 → (∀ i ∈ t, p i ∈ s) → (f (t.sum fun i => w i • p i) ≤ t.sum fun i => w i • f (p i)) → ∀ ⦃j : ι⦄, j ∈ t → ∀ ⦃k : ι⦄, k ∈ t → p j = p k This Lean theorem is a version of the equality case of Jensen's inequality for strictly concave functions. In mathematical terms, it states the following: For a strictly concave function `f` on a set `s` and positive weights `w` such that their sum equals one, if the function evaluated at the weighted sum of some points `p` in the set equals the weighted sum of the function values at these points, then all those points must be equal. In more detail, given a field `𝕜`, an additively commutative group `E`, an additively ordered commutative group `β`, and another type `ι`. Suppose `f` is a function from `E` to `β` and that `s` is a subset of `E`, `t` is a finite set of type `ι`, `w` is a function from `ι` to `𝕜` assigning weights, and `p` is a function from `ι` to `E` designating points. Assume that `f` is strictly concave on `s`, every weight is positive, the sum of weights is one, and every point is in `s`. If `f` evaluated at the weighted sum of points equals the weighted sum of `f` evaluated at those points, then any two points from set `t` are equal. More concisely: If `f` is a strictly concave function on a set `s`, and for some weights `w` summing to 1 and points `p` in `s`, we have `∑(w(i) f(p(i))) = f(∑(w(i) * p(i)))`, then all points `p(i)` are equal.*
`ConcaveOn.min_le_of_mem_segment` theorem ConcaveOn.min_le_of_mem_segment : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : LinearOrderedAddCommGroup β] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 β] [inst_5 : OrderedSMul 𝕜 β] {f : E → β} {x y z : E}, ConcaveOn 𝕜 (segment 𝕜 x y) f → z ∈ segment 𝕜 x y → min (f x) (f y) ≤ f z The theorem "ConcaveOn.min_le_of_mem_segment" states the minimum principle for concave functions on a segment. In the context of a function `f` from a vector space `E` over a field `𝕜` to an ordered additive commutative group `β`, if the function is concave in the segment `[x, y]` in `E`, then the minimum value of `f` over the segment `[x, y]` is attained at either `x` or `y`. For any point `z` in the segment `[x, y]`, the value of `f` at `z` is greater than or equal to the minimum of `f(x)` and `f(y)`. More concisely: If `f` is a concave function on the segment `[x, y]` in a vector space over a field, then the minimum value of `f` on this segment is attained at `x` or `y`, and for any `z` in the segment, `f(z)` is greater than or equal to both `f(x)` and `f(y)`.
`ConcaveOn.le_map_centerMass` theorem ConcaveOn.le_map_centerMass : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : OrderedAddCommGroup β] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 β] [inst_5 : OrderedSMul 𝕜 β] {s : Set E} {f : E → β} {t : Finset ι} {w : ι → 𝕜} {p : ι → E}, ConcaveOn 𝕜 s f → (∀ i ∈ t, 0 ≤ w i) → (0 < t.sum fun i => w i) → (∀ i ∈ t, p i ∈ s) → t.centerMass w (f ∘ p) ≤ f (t.centerMass w p) The theorem `ConcaveOn.le_map_centerMass` is a version of the Concave Jensen's Inequality. It states that for any types `𝕜`, `E`, `β`, `ι` with `𝕜` being a linear ordered field, `E` being an additive commutative group, `β` being an ordered additive commutative group, and `𝕜`, `β` being modules over `𝕜`, if a function `f` from `E` to `β` is concave on a set `s`, and for a finite set `t` with elements of type `ι`, if each element `i` of `t` has a corresponding weight `w i` that is non-negative, the sum of the weights is positive, and each `p i` maps to an element in `s`, then the center of mass of the function values `f ∘ p` weighted by `w` is less than or equal to the function value at the center of mass of `p` weighted by `w`. This theorem is a concrete manifestation of the intuitive idea that for concave functions, the function at the average is greater than or equal to the average of the function. More concisely: For a concave function `f` from an additive commutative group `E` to an ordered additive commutative group `β` over a linear ordered field `𝕜`, if `s` is a set of `E` with `f` being concave on `s`, and `t` is a finite set of `E` with non-negative weights `wi` summing to a positive value, and each `wi` maps to an element of `s`, then the center of mass of `f ∘ p` weighted by `wi` is less than or equal to `f` of the center of mass of `p` weighted by the sum of `wi`.
`ConcaveOn.exists_le_of_mem_convexHull` theorem ConcaveOn.exists_le_of_mem_convexHull : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : LinearOrderedAddCommGroup β] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 β] [inst_5 : OrderedSMul 𝕜 β] {s : Set E} {f : E → β}, ConcaveOn 𝕜 ((convexHull 𝕜) s) f → ∀ {x : E}, x ∈ (convexHull 𝕜) s → ∃ y ∈ s, f y ≤ f x The theorem "Minimum principle for concave functions" states that for any given function `f` which is concave on the convex hull of a set `s`, if a point `x` lies in the convex hull of `s`, then there exists a point `y` in `s` such that the value of the function `f` at `y` is less than or equal to the value of the function `f` at `x`. This principle essentially suggests that the minimum value of a concave function on the convex hull of a set is attained within the set itself. More concisely: If `f` is a concave function and `x` is in the convex hull of a set `s`, then there exists `y` in `s` such that `f(y) ≤ f(x)`.
`ConcaveOn.exists_le_of_centerMass` theorem ConcaveOn.exists_le_of_centerMass : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : LinearOrderedAddCommGroup β] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 β] [inst_5 : OrderedSMul 𝕜 β] {s : Set E} {f : E → β} {t : Finset ι} {w : ι → 𝕜} {p : ι → E}, ConcaveOn 𝕜 s f → (∀ i ∈ t, 0 ≤ w i) → (0 < t.sum fun i => w i) → (∀ i ∈ t, p i ∈ s) → ∃ i ∈ t, f (p i) ≤ f (t.centerMass w p) This theorem states that if a function `f` is concave on a set `s`, then there exists a point in `s` such that the value of the function at this point is less than or equal to the value of the function at the center of mass of points in `s`. Here, the center of mass is calculated with respect to a given finite set of indices `t`, a weight function `w` and point mapping `p`. The conditions for the theorem to hold include that all weights are non-negative, the sum of the weights is positive, and all points mapped by `p` are in set `s`. More concisely: If `f` is a concave function on a set `s` with center of mass calculated from a finite set of indices `t`, a weight function `w`, and point mapping `p`, then there exists a point in `s` with a function value less than or equal to the value at the center of mass.
`StrictConcaveOn.map_sum_eq_iff'` theorem StrictConcaveOn.map_sum_eq_iff' : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : OrderedAddCommGroup β] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 β] [inst_5 : OrderedSMul 𝕜 β] {s : Set E} {f : E → β} {t : Finset ι} {w : ι → 𝕜} {p : ι → E}, StrictConcaveOn 𝕜 s f → (∀ i ∈ t, 0 ≤ w i) → (t.sum fun i => w i) = 1 → (∀ i ∈ t, p i ∈ s) → ((f (t.sum fun i => w i • p i) = t.sum fun i => w i • f (p i)) ↔ ∀ j ∈ t, w j ≠ 0 → p j = t.sum fun i => w i • p i) This theorem presents the canonical form of the equality case of Jensen's inequality, specifically for a strictly concave function `f` and nonnegative weights `w`. The theorem states that the equality `f (∑ i in t, w i • p i) = ∑ i in t, w i • f (p i)` holds if and only if all points `p` with non-zero weight are equal, in particular, they are all equal to their center of mass with respect to `w`. This assertion is valid under the conditions that `f` is strictly concave on a set `s`, all weights `w i` are nonnegative for `i` in the finset `t`, the sum of all weights is `1`, and all points `p i` are in set `s` for `i` in the finset `t`. More concisely: The equality of the weighted sum and the weighted sum of functions for a strictly concave function holds if and only if the weights correspond to equal input values in the function's domain.
`StrictConcaveOn.lt_map_sum` theorem StrictConcaveOn.lt_map_sum : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : OrderedAddCommGroup β] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 β] [inst_5 : OrderedSMul 𝕜 β] {s : Set E} {f : E → β} {t : Finset ι} {w : ι → 𝕜} {p : ι → E}, StrictConcaveOn 𝕜 s f → (∀ i ∈ t, 0 < w i) → (t.sum fun i => w i) = 1 → (∀ i ∈ t, p i ∈ s) → (∃ j ∈ t, ∃ k ∈ t, p j ≠ p k) → (t.sum fun i => w i • f (p i)) < f (t.sum fun i => w i • p i) The theorem `StrictConcaveOn.lt_map_sum` is a statement about the strict Jensen inequality for strictly concave functions. If we have a strictly concave function `f` on a set `s` in a vector space `E` over a linearly ordered field `𝕜`, and we have an indexed family `(p i)` of points in `s` with corresponding strictly positive weights `(w i)`, then under the conditions that the sum of the weights is 1, and the family of points is non-constant, the inequality `(t.sum fun i => w i • f (p i)) < f (t.sum fun i => w i • p i)` holds. In other words, the weighted sum of the function values at the points is strictly less than the function value at the weighted sum of the points. More concisely: If `f` is a strictly concave function on a vector space over a linearly ordered field with a non-constant family of points `(p i)` and corresponding strictly positive weights `(w i)` such that the sum of the weights is 1, then `(∑ i, w i • f (p i)) < f (∑ i, w i • p i)`.
`ConvexOn.exists_ge_of_centerMass` theorem ConvexOn.exists_ge_of_centerMass : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : LinearOrderedAddCommGroup β] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 β] [inst_5 : OrderedSMul 𝕜 β] {s : Set E} {f : E → β} {t : Finset ι} {w : ι → 𝕜} {p : ι → E}, ConvexOn 𝕜 s f → (∀ i ∈ t, 0 ≤ w i) → (0 < t.sum fun i => w i) → (∀ i ∈ t, p i ∈ s) → ∃ i ∈ t, f (t.centerMass w p) ≤ f (p i) This theorem states that if a function `f` is convex on a set `s`, then there exists a point in the finset `t` such that the value of the function at the center of mass of the points in `s` is less than or equal to the value of the function at that point. A function is said to be convex on a set if for any two points in the set, the function's value at any point on the line segment connecting the two points is less than or equal to the weighted average of the function's values at the two points. The center of mass is calculated using a weight function `w` and a position function `p` from the elements of the set to the elements of `s`. The theorem assumes that all the weights are non-negative, the sum of the weights is positive, and every position is in the set `s`. More concisely: If `f` is a convex function on the finite set `s` with non-negative weights summing to positive value, then the center of mass of `s` with respect to `f` lies in `s` and satisfies `f(∫(x:s) w(x) dx) ≤ ∫(x:s) w(x) f(x) dx`.
`ConvexOn.map_add_sum_le` theorem ConvexOn.map_add_sum_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : OrderedAddCommGroup β] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 β] [inst_5 : OrderedSMul 𝕜 β] {s : Set E} {f : E → β} {t : Finset ι} {w : ι → 𝕜} {p : ι → E} {v : 𝕜} {q : E}, ConvexOn 𝕜 s f → (∀ i ∈ t, 0 ≤ w i) → (v + t.sum fun i => w i) = 1 → (∀ i ∈ t, p i ∈ s) → 0 ≤ v → q ∈ s → f (v • q + t.sum fun i => w i • p i) ≤ v • f q + t.sum fun i => w i • f (p i) The theorem `ConvexOn.map_add_sum_le` states the convex Jensen's inequality in the context where an element plays a distinguished role. It asserts that for a convex function `f` defined on a type `E` with values in a type `β`, both equipped with a scalar multiplication by elements from a type `𝕜`, if we have a set `s` from `E` where `f` is convex on, a finset `t`, a weight function `w` from the finset to `𝕜`, a point function `p` from the finset to the set `s`, a scalar `v` from `𝕜`, and a distinguished point `q` from the set `s`, such that the weights are nonnegative, their sum plus `v` is 1, and the points from the point function are in the set `s`, and `v` and `q` are nonnegative and in the set `s` respectively; then the value of the function `f` at the point `v • q + t.sum fun i => w i • p i` is less than or equal to `v • f q + t.sum fun i => w i • f (p i)`. This is a generalization of Jensen's inequality that includes a distinguished element and a finset of elements, each with a corresponding weight. More concisely: For a convex function `f` on a type `E` with scalar multiplication, if `s` is a convex subset of `E`, `t` is a finset of `E`, `w` is a weight function, `p` is a point function from `t` to `s`, `v` is a scalar, `q` is a distinguished point in `s`, and the weights `w` are nonnegative and sum to `1 + v`, then `f(vq + ∑(i ∈ t) w(i) p(i)) ≤ vf(q) + ∑(i ∈ t) w(i) f(p(i))`.
`ConvexOn.map_sum_le` theorem ConvexOn.map_sum_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : OrderedAddCommGroup β] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 β] [inst_5 : OrderedSMul 𝕜 β] {s : Set E} {f : E → β} {t : Finset ι} {w : ι → 𝕜} {p : ι → E}, ConvexOn 𝕜 s f → (∀ i ∈ t, 0 ≤ w i) → (t.sum fun i => w i) = 1 → (∀ i ∈ t, p i ∈ s) → f (t.sum fun i => w i • p i) ≤ t.sum fun i => w i • f (p i) This theorem states the Convex Jensen's Inequality in the context of finite sets. The inequality applies to a function `f` defined on a set `s` over which `f` is convex. Given a finite set `t`, weights `w` (where each weight is non-negative and the sum of all weights equals 1), and points `p` in set `s`, the value of the function `f` at the weighted sum of the points `p` is less than or equal to the weighted sum of the values of function `f` at each point `p`. In mathematical terms, the theorem states that if `f` is convex on `s`, then `f (∑_{i∈t} w_i * p_i) ≤ ∑_{i∈t} w_i * f(p_i)`. More concisely: If `f` is a convex function over a finite set `s`, then for any finite subset `t` of `s`, weights `w` summing to 1, and points `p` in `s`, we have `f (∑ₙₙₙₕₖ wₕ pₖ) ≤ ∑ₙₙₙₕₖ wₕ f(pₖ)`.
`StrictConcaveOn.map_sum_eq_iff` theorem StrictConcaveOn.map_sum_eq_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : OrderedAddCommGroup β] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 β] [inst_5 : OrderedSMul 𝕜 β] {s : Set E} {f : E → β} {t : Finset ι} {w : ι → 𝕜} {p : ι → E}, StrictConcaveOn 𝕜 s f → (∀ i ∈ t, 0 < w i) → (t.sum fun i => w i) = 1 → (∀ i ∈ t, p i ∈ s) → ((f (t.sum fun i => w i • p i) = t.sum fun i => w i • f (p i)) ↔ ∀ j ∈ t, p j = t.sum fun i => w i • p i) The theorem `StrictConcaveOn.map_sum_eq_iff` is a formalization of the equality case of Jensen's inequality for strictly concave functions. The theorem states that for any strictly concave function `f` on some set `s`, and for any positive weights `w`, the function value at the weighted sum of points `p` is equal to the weighted sum of the function values at `p` if and only if all points `p` are equal. More formally, `f (∑ i in t, w i • p i) = ∑ i in t, w i • f (p i)` if and only if `∀ j ∈ t, p j = ∑ i in t, w i • p i`. Here, the weights `w` are such that they are all positive, and their sum equals to `1`. In other words, the points `p` are equal to their center of mass with respect to the weights `w`. More concisely: For a strictly concave function `f` on a set `s` and positive weights `w` summing to 1, `f (∑ i in t, w i • p i) = ∑ i in t, w i • f (p i)` if and only if all points `p` are equal.
`ConvexOn.exists_ge_of_mem_convexHull` theorem ConvexOn.exists_ge_of_mem_convexHull : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : LinearOrderedAddCommGroup β] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 β] [inst_5 : OrderedSMul 𝕜 β] {s : Set E} {f : E → β}, ConvexOn 𝕜 ((convexHull 𝕜) s) f → ∀ {x : E}, x ∈ (convexHull 𝕜) s → ∃ y ∈ s, f x ≤ f y The Maximum Principle for convex functions states that, given a function `f` that is convex on the convex hull of a set `s`, any local maximum of `f` on the convex hull of `s` must be contained within `s` itself. In other words, for any element `x` in the convex hull of `s`, there exists an element `y` in `s` such that the value of `f` at `x` is less than or equal to the value of `f` at `y`. This theorem is applicable under certain conditions, including that the underlying field is a linear ordered field, the space `E` has an addition operation that forms an abelian group, and `β` is a linear ordered additive commutative group that can be scaled by elements of the field. More concisely: Given a convex function `f` on a convex set `s` over a linear ordered field, any local maximum of `f` on the convex hull of `s` lies in `s`.
`ConvexOn.map_centerMass_le` theorem ConvexOn.map_centerMass_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : OrderedAddCommGroup β] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 β] [inst_5 : OrderedSMul 𝕜 β] {s : Set E} {f : E → β} {t : Finset ι} {w : ι → 𝕜} {p : ι → E}, ConvexOn 𝕜 s f → (∀ i ∈ t, 0 ≤ w i) → (0 < t.sum fun i => w i) → (∀ i ∈ t, p i ∈ s) → f (t.centerMass w p) ≤ t.centerMass w (f ∘ p) The theorem `ConvexOn.map_centerMass_le` is a statement of Jensen's inequality in the context of convex functions. It states that for any types `𝕜, E, β, ι`, given a linear ordered field `𝕜`, an additive commutative group `E`, an ordered additive commutative group `β`, modules `𝕜 E` and `𝕜 β`, an ordered scalar multiplication `𝕜 β`, a set `s` of type `E`, a function `f` from `E` to `β`, a finite set `t` of type `ι`, a function `w` mapping each element of `t` to `𝕜`, and a function `p` mapping each element of `t` to `E`, if `f` is convex on `s`, `w i` is non-negative for every `i` in `t`, the sum of `w i` for `i` in `t` is positive, and `p i` is in `s` for every `i` in `t`, then the value of `f` at the center of mass of `t` (weighted by `w` and positioned by `p`) is less than or equal to the center of mass of `t` (weighted by `w` and positioned by `f ∘ p`). This captures the intuitive geometric meaning of convexity: the function evaluated at the center of mass is no more than the center of mass of the function values. More concisely: For any convex function `f` on a set `s` with respect to a finite set of weights `w` and positions `p`, the weighted center of mass of `f(p(i))` is less than or equal to the weighted center of mass of `f` evaluated at the center of mass of the positions.
`StrictConvexOn.eq_of_le_map_sum` theorem StrictConvexOn.eq_of_le_map_sum : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : OrderedAddCommGroup β] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 β] [inst_5 : OrderedSMul 𝕜 β] {s : Set E} {f : E → β} {t : Finset ι} {w : ι → 𝕜} {p : ι → E}, StrictConvexOn 𝕜 s f → (∀ i ∈ t, 0 < w i) → (t.sum fun i => w i) = 1 → (∀ i ∈ t, p i ∈ s) → (t.sum fun i => w i • f (p i)) ≤ f (t.sum fun i => w i • p i) → ∀ ⦃j : ι⦄, j ∈ t → ∀ ⦃k : ι⦄, k ∈ t → p j = p k This theorem is a form of the equality case of Jensen's inequality applicable to strictly convex functions. It states that given a strictly convex function `f` on a set `s` and a finite set of points `p` in `s` with corresponding positive weights `w` such that the sum of the weights is `1`, if the weighted sum of `f` at each of these points is less than or equal to `f` at the weighted sum of the points, then all the points `p` are equal to each other. In other words, if the sum of the weights applied to `f` evaluated at each point is equal to or less than `f` evaluated at the point represented by the weighted average of the `p` points, this implies that all the `p` points are the same. More concisely: If a strictly convex function `f` on a set `s` and a finite set of points `p` in `s` with positive weights `w` summing to 1 satisfy the weighted sum of `f` at each `p` being less than or equal to `f` at the weighted average of `p`, then all points `p` are equal.

LeanAide GPT-4 documentation

Module: Mathlib.Analysis.Convex.Jensen

`ConcaveOn.min_le_of_mem_Icc`

`ConvexOn.le_max_of_mem_Icc`

`StrictConvexOn.map_sum_eq_iff'`

`ConvexOn.le_max_of_mem_segment`

`ConcaveOn.le_map_sum`

`ConcaveOn.map_add_sum_le`

`StrictConvexOn.map_sum_lt`

`StrictConvexOn.map_sum_eq_iff`

`StrictConcaveOn.eq_of_map_sum_eq`

`ConcaveOn.min_le_of_mem_segment`

`ConcaveOn.le_map_centerMass`

`ConcaveOn.exists_le_of_mem_convexHull`

`ConcaveOn.exists_le_of_centerMass`

`StrictConcaveOn.map_sum_eq_iff'`

`StrictConcaveOn.lt_map_sum`

`ConvexOn.exists_ge_of_centerMass`

`ConvexOn.map_add_sum_le`

`ConvexOn.map_sum_le`

`StrictConcaveOn.map_sum_eq_iff`

`ConvexOn.exists_ge_of_mem_convexHull`

`ConvexOn.map_centerMass_le`

`StrictConvexOn.eq_of_le_map_sum`