LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Analysis.Convex.Basic

`convex_halfspace_ge` theorem convex_halfspace_ge : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E] [inst_3 : OrderedAddCommMonoid β] [inst_4 : Module 𝕜 β] [inst_5 : OrderedSMul 𝕜 β] {f : E → β}, IsLinearMap 𝕜 f → ∀ (r : β), Convex 𝕜 {w \| r ≤ f w} The theorem `convex_halfspace_ge` states that for any ordered semiring `𝕜`, additive commutative monoid `E`, ordered additive commutative monoid `β`, and any functions `f` from `E` to `β` that are linear maps over the semiring `𝕜`, for any `r` in `β`, the set of all `w` in `E` such that `r` is less than or equal to `f(w)` is a convex set over the semiring `𝕜`. In short, the half-space defined by the linear function `f` and the value `r` is a convex set. More concisely: For any ordered semiring 𝕜, additive commutative monoid E, ordered additive commutative monoid β, and linear function f from E to β over semiring 𝕜, the half-space {w ∈ E \| r ≤ f(w)} is convex for any r ∈ β.
`Convex.translate_preimage_left` theorem Convex.translate_preimage_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E] {s : Set E}, Convex 𝕜 s → ∀ (z : E), Convex 𝕜 ((fun x => x + z) ⁻¹' s) This theorem states that if a set `s` in a vector space `E` over a semiring `𝕜` is convex, then the preimage of `s` under the translation map `x ↦ x + z` for any `z` in `E` is also convex. In other words, if a set is convex, then any translation of that set remains convex. This theorem is fundamental for translation invariance of convex sets in vector spaces. More concisely: If `s` is a convex subset of a vector space `E` over a semiring `𝕜`, then the translated set `{x + z \| x ∈ s}` is also convex for any `z` in `E`.
`convex_iInter` theorem convex_iInter : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : SMul 𝕜 E] {ι : Sort u_5} {s : ι → Set E}, (∀ (i : ι), Convex 𝕜 (s i)) → Convex 𝕜 (⋂ i, s i) The theorem `convex_iInter` states that for any ordered semiring `𝕜` and any additive commutative monoid `E` that supports scalar multiplication by `𝕜`, if we have an indexed collection `{s : ι → Set E}` of sets in E (each indexed by a type `ι`), and each of these sets is convex, then the intersection of all these sets is also convex. The convexity of a set here means that for any element `x` in the set, the set is star-convex at `x`. The concept of "star-convex at `x`" implies that for any point in the set, the entire line segment that connects this point and `x` is contained within the set. More concisely: Given an ordered semiring 𝕜 and an additive commutative monoid E with scalar multiplication, if each indexed collection {s : ι → Set E} of convex sets in E is star-convex at each point, then the intersection of all these sets is also star-convex.
`AffineSubspace.convex` theorem AffineSubspace.convex : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] (Q : AffineSubspace 𝕜 E), Convex 𝕜 ↑Q The theorem `AffineSubspace.convex` asserts that for any ordered ring `𝕜` and an additive commutative group `E` which is also a module over `𝕜`, any affine subspace `Q` of `E` is a convex set. In other words, for any two points `x` and `y` in `Q`, the entire line segment that joins `x` and `y` also lies in `Q`. More concisely: For any ordered ring `𝕜` and an additive commutative `𝕜`-module `E`, every affine subspace of `E` is a convex set.
`Convex.inter` theorem Convex.inter : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : SMul 𝕜 E] {s t : Set E}, Convex 𝕜 s → Convex 𝕜 t → Convex 𝕜 (s ∩ t) This theorem states that for any type 𝕜 with an ordered semiring structure, and any type E with an additive commutative monoid structure and a scalar multiplication by elements of 𝕜, if s and t are sets of elements of E and both are convex in the sense defined above (i.e., for any point x in the set, the set is star-convex with respect to x), then their intersection is also a convex set. In other words, the intersection of two convex sets is also convex. More concisely: Given types 𝕜 with an ordered semiring structure and E with an additive commutative monoid structure and scalar multiplication by elements of 𝕜, if s and t are convex subsets of E, then their intersection is also a convex subset.
`convex_singleton` theorem convex_singleton : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E] (c : E), Convex 𝕜 {c} This theorem, named `convex_singleton`, states that for any type `𝕜` which has a structure of `OrderedSemiring`, and any type `E` which has a `AddCommMonoid` and `Module 𝕜 E` structure (meaning that `E` is a module over `𝕜`), any singleton set `{c}` in `E` is a convex set. In simpler terms, for any scalar field `𝕜` and vector space `E` under operations of `𝕜`, a set containing only one point `c` in `E` is convex. This is because a convex set is defined as a set where, for any two points in the set, the entire line segment that joins them is also in the set. Since there is only one point in a singleton set, the condition is trivially satisfied, and thus a singleton set is convex. More concisely: A singleton set in an ordered semiring-valued module is convex.
`convex_iff_ordConnected` theorem convex_iff_ordConnected : ∀ {𝕜 : Type u_1} [inst : LinearOrderedField 𝕜] {s : Set 𝕜}, Convex 𝕜 s ↔ s.OrdConnected The theorem `convex_iff_ordConnected` establishes an equivalence between the convexity of a set and the ordered connectedness of that set, in the context of a linearly ordered field. Specifically, for every type `𝕜`, given that `𝕜` is a linearly ordered field and `s` is a set of `𝕜`, the set `s` is convex if and only if it is ordered connected. In other words, a set in a linearly ordered field is convex if every point between any two points in the set is also contained in the set. More concisely: A set in a linearly ordered field is convex if and only if it is ordered connected. (That is, a set is convex if every pair of its elements have every element between them also in the set.)
`Convex.vadd` theorem Convex.vadd : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E] {s : Set E}, Convex 𝕜 s → ∀ (z : E), Convex 𝕜 (z +ᵥ s) The theorem `Convex.vadd` states that for any ordered semiring `𝕜`, any additive commutative monoid `E` that also is a module over `𝕜`, and any set `s` of elements of `E` which is convex, the translated set `(z +ᵥ s)` is also convex for any element `z` of `E`. In other words, if `s` is a convex set in a vector space, then translating the set by adding a fixed vector `z` to all elements of the set retains the convexity property. More concisely: For any ordered semiring `𝕜`, additive commutative monoid `E` over `𝕜` that is an `𝕜`-module, and convex set `s` in `E`, the translated set `(z + s)` is convex for all `z` in `E`.
`Convex.prod` theorem Convex.prod : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : AddCommMonoid F] [inst_3 : SMul 𝕜 E] [inst_4 : SMul 𝕜 F] {s : Set E} {t : Set F}, Convex 𝕜 s → Convex 𝕜 t → Convex 𝕜 (s ×ˢ t) The theorem `Convex.prod` states that for any set `s` of elements of type `E` and any set `t` of elements of type `F`, if `s` and `t` are convex under a semiring `𝕜` (which is an ordered semiring and has scalar multiplication defined for both `E` and `F`), then the Cartesian product of `s` and `t` is also convex under `𝕜`. Here, a set is convex if any point in the set `s` is a star center of `s`, meaning that for any two points in `s`, the line segment that connects them is also entirely contained within `s`. In the context of this theorem, a Cartesian product of two sets is a set of all ordered pairs where the first element of each pair is from the first set and the second element is from the second set. More concisely: If sets `s` and `t` are convex under a semiring `𝕜` with ordered and scalar multiplication defined for types `E` and `F` respectively, then the Cartesian product `s × t` is also convex under `𝕜`.
`Convex.is_linear_preimage` theorem Convex.is_linear_preimage : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : AddCommMonoid F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] {s : Set F}, Convex 𝕜 s → ∀ {f : E → F}, IsLinearMap 𝕜 f → Convex 𝕜 (f ⁻¹' s) This theorem states that for any ordered semiring `𝕜` and any two types `E` and `F` that are additive commutative monoids and also `𝕜`-modules, if a set `s` of type `F` is convex, then the preimage of `s` under any linear map `f` from `E` to `F` is also convex. More concisely: Given an ordered semiring `𝕜`, if `E` and `F` are additive commutative `𝕜`-modules and `s ⊆ F` is a convex set, then the preimage `f⁻¹(s) ⊆ E` under any linear map `f : E → F` is also convex.
`convex_halfspace_le` theorem convex_halfspace_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E] [inst_3 : OrderedAddCommMonoid β] [inst_4 : Module 𝕜 β] [inst_5 : OrderedSMul 𝕜 β] {f : E → β}, IsLinearMap 𝕜 f → ∀ (r : β), Convex 𝕜 {w \| f w ≤ r} This theorem, named `convex_halfspace_le`, states that for any ordered semiring `𝕜`, any additive commutative monoid `E`, any ordered additive commutative monoid `β`, any `𝕜`-module `E`, any `𝕜`-module `β`, any `𝕜`-module `β` with a partial order compatible with scalar multiplication, any linear map `f` from `E` to `β`, and any element `r` of `β`, the set of elements `w` of `E` for which `f(w)` is less than or equal to `r` is a convex set in `E`. In simpler terms, it states that for any linear function mapping from one mathematical structure to another, the set of elements that map to a value less than or equal to a given value forms a convex set. This concept is frequently used in fields like optimization and computational geometry. More concisely: For any linear map from an additive commutative semigroup to an ordered additive commutative semigroup and any element in the image semigroup, the preimage under the map forms a convex set.
`convex_univ` theorem convex_univ : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : SMul 𝕜 E], Convex 𝕜 Set.univ This theorem asserts that for any ordered semiring `𝕜` and any additive commutative monoid `E` that also supports scalar multiplication with `𝕜`, the universal set of `E` is convex. In mathematical terms, the universal set of `E` (which includes all elements of `E`) is a convex set under the given algebraic structures. More concisely: Given an ordered semiring `𝕜` and an additive commutative monoid `E` with scalar multiplication, the universal set of `E` is a convex set.
`convex_Iio` theorem convex_Iio : ∀ {𝕜 : Type u_1} {β : Type u_4} [inst : OrderedSemiring 𝕜] [inst_1 : OrderedCancelAddCommMonoid β] [inst_2 : Module 𝕜 β] [inst_3 : OrderedSMul 𝕜 β] (r : β), Convex 𝕜 (Set.Iio r) The theorem `convex_Iio` states that for any instance of an ordered semiring `𝕜`, an ordered cancel additive commutative monoid `β`, a module over `𝕜` of `β`, and an ordered scalar multiplication of `𝕜` over `β`, and given any element `r` of type `β`, the left-infinite right-open interval (denoted by `Set.Iio r`) is a convex set with respect to `𝕜`. In other words, any left-infinite right-open interval forms a convex set in the context of the specified algebraic structures. More concisely: For any ordered semiring `𝕜`, ordered cancel additive commutative monoid `β`, module over `𝕜` of `β`, and ordered scalar multiplication of `𝕜` over `β`, the left-infinite right-open interval `Set.Iio r` of any element `r` in `β` is a convex set.
`convex_Ici` theorem convex_Ici : ∀ {𝕜 : Type u_1} {β : Type u_4} [inst : OrderedSemiring 𝕜] [inst_1 : OrderedAddCommMonoid β] [inst_2 : Module 𝕜 β] [inst_3 : OrderedSMul 𝕜 β] (r : β), Convex 𝕜 (Set.Ici r) This theorem, `convex_Ici`, states that for any ordered semiring `𝕜`, ordered additively commutative monoid `β`, module `𝕜 β` and ordered scalar multiplication `𝕜 β`, and for any real number `r`, the left-closed right-infinite interval `Set.Ici r` is a convex set. In other words, for any `r` in `β`, the set of all elements in `β` that are greater than or equal to `r`, forms a convex set under the conditions defined for `𝕜` and `β`. More concisely: For any ordered semiring `𝕜`, ordered additively commutative monoid `β`, and ordered scalar multiplication `𝕜 β`, the set `Set.Ici r` of elements in `β` greater than or equal to a real number `r` is a convex set.
`MonotoneOn.convex_ge` theorem MonotoneOn.convex_ge : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : OrderedSemiring 𝕜] [inst_1 : LinearOrderedAddCommMonoid E] [inst_2 : OrderedAddCommMonoid β] [inst_3 : Module 𝕜 E] [inst_4 : OrderedSMul 𝕜 E] {s : Set E} {f : E → β}, MonotoneOn f s → Convex 𝕜 s → ∀ (r : β), Convex 𝕜 {x \| x ∈ s ∧ r ≤ f x} The theorem `MonotoneOn.convex_ge` states that for any ordered semiring `𝕜`, linearly ordered additive commutative monoid `E`, and ordered additive commutative monoid `β`, with `E` being a module over `𝕜` and `𝕜` being able to scalar-multiply `E`, given a set `s` of type `E` and a function `f` mapping from `E` to `β`, if the function `f` is monotone on the set `s` and the set `s` itself is convex, then for any value `r` of type `β`, the set of all `x` from `s` such that `r` is less than or equal to `f(x)` is also convex. In simpler terms, this theorem is saying that the 'above-graph' of a monotone function over a convex set is also convex. More concisely: If `f` is a monotone function over a convex set `s` in an ordered additive commutative monoid `E`, then the level set `{x : s \| r ≤ f x}` is convex for any `r` in the ordered semiring `𝕜`.
`Convex.affine_image` theorem Convex.affine_image : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : OrderedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] {s : Set E} (f : E →ᵃ[𝕜] F), Convex 𝕜 s → Convex 𝕜 (⇑f '' s) The theorem 'Convex.affine_image' states that for any ordered ring `𝕜`, an additive commutative group `E`, another additive commutative group `F`, modules `E` and `F` over the ring `𝕜`, a set `s` of elements of `E`, and an affine map `f` from `E` to `F`, if the set `s` is convex, then the image of the set `s` under the affine map `f` is also convex. In other words, the image of a convex set under an affine transformation preserves its convexity. More concisely: If `s` is a convex subset of an additive commutative group `E` over an ordered ring `𝕜`, then the image of `s` under an affine map `f` from `E` to another additive commutative group `F` over `𝕜` is also a convex subset.
`MonotoneOn.convex_le` theorem MonotoneOn.convex_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : OrderedSemiring 𝕜] [inst_1 : LinearOrderedAddCommMonoid E] [inst_2 : OrderedAddCommMonoid β] [inst_3 : Module 𝕜 E] [inst_4 : OrderedSMul 𝕜 E] {s : Set E} {f : E → β}, MonotoneOn f s → Convex 𝕜 s → ∀ (r : β), Convex 𝕜 {x \| x ∈ s ∧ f x ≤ r} This theorem, `MonotoneOn.convex_le`, states that for any ordered semiring `𝕜`, any linear ordered additive commutative monoid `E`, any ordered additive commutative monoid `β`, any module `E` over `𝕜`, and any ordered scalar multiplication over `E`, given a set `s` of type `E` and a function `f` from `E` to `β`, if function `f` is monotone on set `s` and set `s` is convex in `𝕜`, then for any real number `r`, the set of all elements `x` in `s` such that `f(x)` is less than or equal to `r` is also convex in `𝕜`. In other words, any sub-level set of a monotone function on a convex set retains the convex property. More concisely: If a monotone function maps a convex set to an ordered additive commutative monoid, then the sub-level sets of the function are also convex.
`Convex.affine_preimage` theorem Convex.affine_preimage : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : OrderedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] (f : E →ᵃ[𝕜] F) {s : Set F}, Convex 𝕜 s → Convex 𝕜 (⇑f ⁻¹' s) The theorem `Convex.affine_preimage` states that for any ordered ring `𝕜`, and any two additively commutative groups `E` and `F` that are also modules over `𝕜`, if `f` is an affine map from `E` to `F` and `s` is a set in `F` that is convex, then the preimage of `s` under the map `f` (denoted `⇑f ⁻¹' s`) is also a convex set in `E`. In simpler terms, this theorem ensures that affine transformations preserve the convexity property of sets. More concisely: If `f` is an affine map from an additively commutative group `E` to another additively commutative group `F` that is also a module over an ordered ring `𝕜`, and `s` is a convex subset of `F`, then the preimage `f⁻¹(s)` is a convex subset of `E`.
`Convex.add` theorem Convex.add : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E] {s t : Set E}, Convex 𝕜 s → Convex 𝕜 t → Convex 𝕜 (s + t) The theorem `Convex.add` states that for any ordered semiring `𝕜` and any type `E` that forms an additive commutative monoid and is a `𝕜`-module, if `s` and `t` are two convex sets in `E`, then their Minkowski sum (denoted `s + t`), is also a convex set in `E`. In other words, the sum of two convex sets in a vector space over an ordered semiring is also a convex set in that vector space. More concisely: If `𝕜` is an ordered semiring, `E` is an additive commutative monoid and a `𝕜`-module, and `s` and `t` are convex sets in `E`, then their Minkowski sum `s + t` is also a convex set in `E`.
`convex_Iic` theorem convex_Iic : ∀ {𝕜 : Type u_1} {β : Type u_4} [inst : OrderedSemiring 𝕜] [inst_1 : OrderedAddCommMonoid β] [inst_2 : Module 𝕜 β] [inst_3 : OrderedSMul 𝕜 β] (r : β), Convex 𝕜 (Set.Iic r) This theorem states that for any given type `𝕜` which is an ordered semiring, type `β` which is an ordered additive commutative monoid, and also a module over `𝕜` with the scalar multiplication being ordered, and for any element `r` of type `β`, the set `Set.Iic r` is convex. In other words, an interval of the form `(-∞, r]` in the ordered additive commutative monoid `β` is a convex set under the scalar multiplication ordered semiring `𝕜`. More concisely: Given an ordered semiring `𝕜`, an ordered additive commutative monoid `β` that is a `𝕜`-module with ordered scalar multiplication, and an element `r` of `β`, the interval `Set.Iic r` is convex.
`Set.OrdConnected.convex` theorem Set.OrdConnected.convex : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : LinearOrderedAddCommMonoid E] [inst_2 : Module 𝕜 E] [inst_3 : OrderedSMul 𝕜 E] {s : Set E}, s.OrdConnected → Convex 𝕜 s The theorem `Set.OrdConnected.convex` states that for any type `𝕜` which forms an ordered semiring and another type `E` that is a linearly ordered additive commutative monoid with a `𝕜`-module structure and ordered scalar multiplication, if a set `s` of type `E` is ordinally connected, then `s` is also convex over the type `𝕜`. In other words, if `s` is such that for any two points in `s`, all points between them (in the order defined by `E`) are also in `s`, then for any two points in `s`, all points on the line segment between them (in the vector space structure defined by `𝕜` and `E`) are also in `s`. More concisely: If `s` is an ordinally connected subset of an additive commutative monoid `E` endowed with a `𝕜`-module structure and ordered scalar multiplication, then `s` is convex in the vector space structure defined by `𝕜` and `E`.
`Convex.segment_subset` theorem Convex.segment_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : SMul 𝕜 E] {s : Set E}, Convex 𝕜 s → ∀ {x y : E}, x ∈ s → y ∈ s → segment 𝕜 x y ⊆ s The theorem `Convex.segment_subset` states that for any ordered semiring `𝕜` and any additive commutative monoid `E` that is also a `𝕜`-module, if `s` is a convex set in `E`, then for any two elements `x` and `y` in `s`, the segment from `x` to `y` (which is defined as the set of all points `z` that can be expressed as `ax + by`, where `a` and `b` are nonnegative and sum to 1) is a subset of `s`. In other words, in a convex set, the entire line segment connecting any two points in the set also lies within the set. More concisely: In a convex set of an additive commutative monoid that is a module over an ordered semiring, any segment connecting two elements lies entirely within the set.
`convex_iff_pointwise_add_subset` theorem convex_iff_pointwise_add_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : SMul 𝕜 E] {s : Set E}, Convex 𝕜 s ↔ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • s + b • s ⊆ s This theorem provides an alternative definition for convexity of a set in terms of pointwise set operations. Specifically, it states that for any ordered semiring `𝕜` and any additive commutative monoid `E` that is a scalar multiple of `𝕜`, a set `s` of `E` is convex if and only if for any nonnegative elements `a` and `b` in `𝕜` such that `a + b = 1`, the sum of the scalar multiples `a • s` and `b • s` is a subset of `s`. Here, `a • s` and `b • s` represent the sets obtained by scaling every element of `s` by `a` and `b` respectively. More concisely: A set in an ordered semiring with respect to scalar multiplication by elements in the semiring with non-negative coefficients summing to 1 is convex if and only if the scaling of the set by each coefficient is a subset of the original set.
`Convex.set_combo_subset` theorem Convex.set_combo_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : SMul 𝕜 E] {s : Set E}, Convex 𝕜 s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • s + b • s ⊆ s This theorem provides an alternative definition of set convexity, in terms of pointwise set operations. More specifically, it asserts that for any ordered semiring `𝕜` and any set `s` in an additive commutative monoid `E` that is a scalar multiple of `𝕜`, if `s` is Convex in `𝕜`, then for any non-negative elements `a` and `b` in `𝕜` that sum up to 1, the set formed by pointwise addition of the scalar multiple of `s` by `a` and the scalar multiple of `s` by `b` is a subset of `s`. This is typically understood as any linear combination of points in a convex set, where the coefficients are non-negative and sum to 1, results in a point that's also inside the convex set. More concisely: For any ordered semiring `𝕜`, additive commutative monoid `E` with scalar multiplication, and convex set `s` in `E` that is a scalar multiple of `𝕜`, if `s` is convex, then for any non-negative `a, b ∈ 𝕜` with `a + b = 1`, the set `{as + bs : s ∈ s}` is a subset of `s`.
`convex_Ioi` theorem convex_Ioi : ∀ {𝕜 : Type u_1} {β : Type u_4} [inst : OrderedSemiring 𝕜] [inst_1 : OrderedCancelAddCommMonoid β] [inst_2 : Module 𝕜 β] [inst_3 : OrderedSMul 𝕜 β] (r : β), Convex 𝕜 (Set.Ioi r) This theorem, `convex_Ioi`, states that for any given ordered semiring `𝕜` and an ordered, cancellative, commutative additive monoid `β` that is a `𝕜`-module and has an ordered scalar multiplication, any left-open right-infinite interval `(r, ∞)` is a convex set. Essentially, it asserts that if you pick any two points in this interval, then the entire line segment between these two points also lies within the interval. More concisely: For any ordered semiring `𝕜`, ordered, cancellative, commutative additive monoid `β` that is a `𝕜`-module and has an ordered scalar multiplication, the left-open right-infinite interval `(r, ∞)` is a convex set in `β` with respect to `𝕜`.
`Convex.linear_preimage` theorem Convex.linear_preimage : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : AddCommMonoid F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] {s : Set F}, Convex 𝕜 s → ∀ (f : E →ₗ[𝕜] F), Convex 𝕜 (⇑f ⁻¹' s) The theorem `Convex.linear_preimage` states that for any ordered semiring `𝕜`, and any two additive commutative monoids `E` and `F` that also have a module structure over `𝕜`, if a set `s` in `F` is convex, then the preimage of `s` under any linear map `f` from `E` to `F` is also a convex set in `E`. In other words, the preimage of a convex set under a linear map is also convex. More concisely: Given an ordered semiring 𝕜, and additive commutative monoids E and F with a module structure over 𝕜, if s is a convex subset of F and f is a linear map from E to F, then the preimage of s under f is a convex subset of E.
`Convex.smul` theorem Convex.smul : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedCommSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E] {s : Set E}, Convex 𝕜 s → ∀ (c : 𝕜), Convex 𝕜 (c • s) The theorem `Convex.smul` states that for every ordered commutative semiring `𝕜`, every additive commutative monoid `E`, and every `𝕜`-module `E`, if a set `s` in `E` is convex, then the scaled set `c • s` is also convex. In other words, multiplying all elements of a convex set by a scalar yields another convex set. Here, "convex" means that for any two points in the set, the line segment that joins them stays completely within the set. More concisely: For every ordered commutative semiring 𝕜, every additive commutative monoid E made into a 𝕜-module, and convex set s in E, the scaled set c • s is also convex.
`convex_iff_div` theorem convex_iff_div : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {s : Set E}, Convex 𝕜 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → (a / (a + b)) • x + (b / (a + b)) • y ∈ s The theorem `convex_iff_div` provides an alternative definition of set convexity in terms of division. Specifically, it states that for any linear ordered field `𝕜` and any additively commutative group `E` that is also a `𝕜`-module, a set `s` of elements from `E` is convex if and only if for any elements `x` and `y` in `s` and any non-negative scalars `a` and `b` such that `a + b` is positive, the expression `(a / (a + b)) • x + (b / (a + b)) • y` is also an element of `s`. This definition is a precise way of saying that any point on the line segment connecting `x` and `y` (with `x` and `y` in `s`) is also in `s`, which captures the intuitive idea of a convex set. More concisely: A set of elements from an additively commutative group endowed with the structure of a module over a linear ordered field is convex if and only if for any of its elements x, y, and any non-negative scalars a and b with a + b > 0, the linear combination (a / (a + b) * x + b / (a + b) * y) is also an element of the set.
`Convex.ordConnected` theorem Convex.ordConnected : ∀ {𝕜 : Type u_1} [inst : LinearOrderedField 𝕜] {s : Set 𝕜}, Convex 𝕜 s → s.OrdConnected The theorem `Convex.ordConnected` states that for any type `𝕜` which is a `LinearOrderedField`, and any set `s` of type `Set 𝕜`, if `s` is convex then `s` is also order-connected. Here, a set is said to be convex if for any element `x` in the set, the set is star-convex at `x`. A set is said to be order-connected if for any two elements in the set, all elements between them are also in the set. More concisely: If `𝕜` is a LinearOrderedField and `s` is a convex subset of `Set 𝕜`, then `s` is order-connected.
`Convex.translate_preimage_right` theorem Convex.translate_preimage_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E] {s : Set E}, Convex 𝕜 s → ∀ (z : E), Convex 𝕜 ((fun x => z + x) ⁻¹' s) This theorem states that for any ordered semiring `𝕜`, type `E` that is an additive commutative monoid and a module over `𝕜`, and any set `s` of type `E`, if `s` is a convex set, then the preimage set of `s` under the translation by any element `z` of `E` (denoted by `(fun x => z + x) ⁻¹' s`) is also a convex set. In other words, translating a convex set by any amount does not change its convexity. More concisely: For any ordered semiring `𝕜`, additive commutative monoid and `𝕜`-module `E` type `E`, and convex set `s` of `E`, the translation of `s` by any element `z` in `E` (`(fun x => z + x) ⁻¹' s`) is also a convex set.
`convex_Icc` theorem convex_Icc : ∀ {𝕜 : Type u_1} {β : Type u_4} [inst : OrderedSemiring 𝕜] [inst_1 : OrderedAddCommMonoid β] [inst_2 : Module 𝕜 β] [inst_3 : OrderedSMul 𝕜 β] (r s : β), Convex 𝕜 (Set.Icc r s) The theorem `convex_Icc` states that for any ordered semiring `𝕜` and any ordered additive commutative monoid `β` which is a module over `𝕜` with an ordered scalar multiplication, the set interval from `r` to `s` (inclusive of both `r` and `s`) is a convex set. This means that for any two points in the interval, the line segment that joins them also lies completely within the interval. More concisely: For any ordered semiring `𝕜`, ordered additive commutative monoid `β` with an ordered scalar multiplication that is a `𝕜`-module, the interval from `r` to `s` in `β` is a convex set.

LeanAide GPT-4 documentation

Module: Mathlib.Analysis.Convex.Basic

convex_halfspace_ge

Convex.translate_preimage_left

theorem Convex.translate_preimage_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E] {s : Set E}, Convex 𝕜 s → ∀ (z : E), Convex 𝕜 ((fun x => x + z) ⁻¹' s)

convex_iInter

theorem convex_iInter : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : SMul 𝕜 E] {ι : Sort u_5} {s : ι → Set E}, (∀ (i : ι), Convex 𝕜 (s i)) → Convex 𝕜 (⋂ i, s i)

AffineSubspace.convex

theorem AffineSubspace.convex : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] (Q : AffineSubspace 𝕜 E), Convex 𝕜 ↑Q

Convex.inter

theorem Convex.inter : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : SMul 𝕜 E] {s t : Set E}, Convex 𝕜 s → Convex 𝕜 t → Convex 𝕜 (s ∩ t)

convex_singleton

theorem convex_singleton : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E] (c : E), Convex 𝕜 {c}

convex_iff_ordConnected

theorem convex_iff_ordConnected : ∀ {𝕜 : Type u_1} [inst : LinearOrderedField 𝕜] {s : Set 𝕜}, Convex 𝕜 s ↔ s.OrdConnected

Convex.vadd

theorem Convex.vadd : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E] {s : Set E}, Convex 𝕜 s → ∀ (z : E), Convex 𝕜 (z +ᵥ s)

Convex.prod

theorem Convex.prod : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : AddCommMonoid F] [inst_3 : SMul 𝕜 E] [inst_4 : SMul 𝕜 F] {s : Set E} {t : Set F}, Convex 𝕜 s → Convex 𝕜 t → Convex 𝕜 (s ×ˢ t)

Convex.is_linear_preimage

convex_halfspace_le

convex_univ

theorem convex_univ : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : SMul 𝕜 E], Convex 𝕜 Set.univ

convex_Iio

theorem convex_Iio : ∀ {𝕜 : Type u_1} {β : Type u_4} [inst : OrderedSemiring 𝕜] [inst_1 : OrderedCancelAddCommMonoid β] [inst_2 : Module 𝕜 β] [inst_3 : OrderedSMul 𝕜 β] (r : β), Convex 𝕜 (Set.Iio r)

convex_Ici

theorem convex_Ici : ∀ {𝕜 : Type u_1} {β : Type u_4} [inst : OrderedSemiring 𝕜] [inst_1 : OrderedAddCommMonoid β] [inst_2 : Module 𝕜 β] [inst_3 : OrderedSMul 𝕜 β] (r : β), Convex 𝕜 (Set.Ici r)

MonotoneOn.convex_ge

Convex.affine_image

theorem Convex.affine_image : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : OrderedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] {s : Set E} (f : E →ᵃ[𝕜] F), Convex 𝕜 s → Convex 𝕜 (⇑f '' s)

MonotoneOn.convex_le

Convex.affine_preimage

theorem Convex.affine_preimage : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : OrderedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] (f : E →ᵃ[𝕜] F) {s : Set F}, Convex 𝕜 s → Convex 𝕜 (⇑f ⁻¹' s)

Convex.add

theorem Convex.add : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E] {s t : Set E}, Convex 𝕜 s → Convex 𝕜 t → Convex 𝕜 (s + t)

convex_Iic

theorem convex_Iic : ∀ {𝕜 : Type u_1} {β : Type u_4} [inst : OrderedSemiring 𝕜] [inst_1 : OrderedAddCommMonoid β] [inst_2 : Module 𝕜 β] [inst_3 : OrderedSMul 𝕜 β] (r : β), Convex 𝕜 (Set.Iic r)

Set.OrdConnected.convex

theorem Set.OrdConnected.convex : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : LinearOrderedAddCommMonoid E] [inst_2 : Module 𝕜 E] [inst_3 : OrderedSMul 𝕜 E] {s : Set E}, s.OrdConnected → Convex 𝕜 s

Convex.segment_subset

theorem Convex.segment_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : SMul 𝕜 E] {s : Set E}, Convex 𝕜 s → ∀ {x y : E}, x ∈ s → y ∈ s → segment 𝕜 x y ⊆ s

convex_iff_pointwise_add_subset

theorem convex_iff_pointwise_add_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : SMul 𝕜 E] {s : Set E}, Convex 𝕜 s ↔ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • s + b • s ⊆ s

Convex.set_combo_subset

theorem Convex.set_combo_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : SMul 𝕜 E] {s : Set E}, Convex 𝕜 s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • s + b • s ⊆ s

convex_Ioi

theorem convex_Ioi : ∀ {𝕜 : Type u_1} {β : Type u_4} [inst : OrderedSemiring 𝕜] [inst_1 : OrderedCancelAddCommMonoid β] [inst_2 : Module 𝕜 β] [inst_3 : OrderedSMul 𝕜 β] (r : β), Convex 𝕜 (Set.Ioi r)

Convex.linear_preimage

Convex.smul

theorem Convex.smul : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedCommSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E] {s : Set E}, Convex 𝕜 s → ∀ (c : 𝕜), Convex 𝕜 (c • s)

convex_iff_div

Convex.ordConnected

theorem Convex.ordConnected : ∀ {𝕜 : Type u_1} [inst : LinearOrderedField 𝕜] {s : Set 𝕜}, Convex 𝕜 s → s.OrdConnected

Convex.translate_preimage_right

theorem Convex.translate_preimage_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E] {s : Set E}, Convex 𝕜 s → ∀ (z : E), Convex 𝕜 ((fun x => z + x) ⁻¹' s)

convex_Icc

theorem convex_Icc : ∀ {𝕜 : Type u_1} {β : Type u_4} [inst : OrderedSemiring 𝕜] [inst_1 : OrderedAddCommMonoid β] [inst_2 : Module 𝕜 β] [inst_3 : OrderedSMul 𝕜 β] (r s : β), Convex 𝕜 (Set.Icc r s)

`convex_halfspace_ge`

`Convex.translate_preimage_left`

`convex_iInter`

`AffineSubspace.convex`

`Convex.inter`

`convex_singleton`

`convex_iff_ordConnected`

`Convex.vadd`

`Convex.prod`

`Convex.is_linear_preimage`

`convex_halfspace_le`

`convex_univ`

`convex_Iio`

`convex_Ici`

`MonotoneOn.convex_ge`

`Convex.affine_image`

`MonotoneOn.convex_le`

`Convex.affine_preimage`

`Convex.add`

`convex_Iic`

`Set.OrdConnected.convex`

`Convex.segment_subset`

`convex_iff_pointwise_add_subset`

`Convex.set_combo_subset`

`convex_Ioi`

`Convex.linear_preimage`

`Convex.smul`

`convex_iff_div`

`Convex.ordConnected`

`Convex.translate_preimage_right`

`convex_Icc`