geometric_hahn_banach_closed_compact
theorem geometric_hahn_banach_closed_compact :
∀ {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : TopologicalAddGroup E]
[inst_3 : Module ℝ E] [inst_4 : ContinuousSMul ℝ E] {s t : Set E} [inst_5 : LocallyConvexSpace ℝ E],
Convex ℝ s →
IsClosed s → Convex ℝ t → IsCompact t → Disjoint s t → ∃ f u v, (∀ a ∈ s, f a < u) ∧ u < v ∧ ∀ b ∈ t, v < f b
The theorem `geometric_hahn_banach_closed_compact` is a variation of the Hahn-Banach theorem from functional analysis. It states that for any two disjoint convex sets `s` and `t` in a real vector space `E` equipped with a locally convex topology, where `s` is a closed set and `t` is a compact set, there exists a continuous linear functional `f` and real numbers `u` and `v` such that all values of `f` on `s` are less than `u`, `u` is less than `v`, and all values of `f` on `t` are greater than `v`. In other words, the functional `f` strongly separates the sets `s` and `t`.
More concisely: Given any two disjoint, closed (in a locally convex topology) and compact subsets `s` and `t` in a real vector space `E`, there exists a continuous linear functional `f` and real numbers `u < v` such that `f(s) < u` and `f(t) > v`.
|
iInter_halfspaces_eq
theorem iInter_halfspaces_eq :
∀ {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : TopologicalAddGroup E]
[inst_3 : Module ℝ E] [inst_4 : ContinuousSMul ℝ E] {s : Set E} [inst_5 : LocallyConvexSpace ℝ E],
Convex ℝ s → IsClosed s → ⋂ l, {x | ∃ y ∈ s, l x ≤ l y} = s
The theorem `iInter_halfspaces_eq` states that for any set `s` of type `E`, where `E` is a topological space, an additive commutative group, a topological additive group, a module over the real numbers, and a locally convex space with continuous scalar multiplication, if `s` is a convex and closed set, then `s` is equal to the intersection of all half-spaces that contain it. In this context, a half-space is defined as the set of all elements `x` such that there exists an element `y` in `s` for which `l x` is less than or equal to `l y`, where `l` is a linear functional.
More concisely: If `s` is a convex and closed subset of a topological space, additive commutative group, topological additive group, module over the real numbers, and locally convex space with continuous scalar multiplication, then `s` equals the intersection of all half-spaces containing it, where a half-space is the set of elements `x` such that there exists `y` in `s` with `l x ≤ l y` for some linear functional `l`.
|
geometric_hahn_banach_compact_closed
theorem geometric_hahn_banach_compact_closed :
∀ {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : TopologicalAddGroup E]
[inst_3 : Module ℝ E] [inst_4 : ContinuousSMul ℝ E] {s t : Set E} [inst_5 : LocallyConvexSpace ℝ E],
Convex ℝ s →
IsCompact s → Convex ℝ t → IsClosed t → Disjoint s t → ∃ f u v, (∀ a ∈ s, f a < u) ∧ u < v ∧ ∀ b ∈ t, v < f b
This is a version of the Hahn-Banach theorem. The theorem states that for any two disjoint convex sets `s` and `t` in a locally convex topological vector space over the real numbers ℝ, where `s` is compact and `t` is closed, there exists a continuous linear functional `f` and two real numbers `u` and `v` such that `f` strongly separates `s` and `t`. Strong separation is defined as all elements `a` of `s` being mapped by `f` to values less than `u`, all elements `b` of `t` being mapped to values greater than `v`, and `u` being less than `v`.
More concisely: Given any compact, convex set `s` and closed, convex set `t` in a locally convex topological vector space over the real numbers, there exists a continuous linear functional `f` and real numbers `u` < `v` such that `f(x)` < `u` for all `x` in `s` and `f(y)` > `v` for all `y` in `t`.
|
separate_convex_open_set
theorem separate_convex_open_set :
∀ {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : TopologicalAddGroup E]
[inst_3 : Module ℝ E] [inst_4 : ContinuousSMul ℝ E] {s : Set E},
0 ∈ s → Convex ℝ s → IsOpen s → ∀ {x₀ : E}, x₀ ∉ s → ∃ f, f x₀ = 1 ∧ ∀ x ∈ s, f x < 1
This theorem states that given a topological space `E` that has additional structures (it is a topological additive group and a module over the real numbers with continuous scalar multiplication), if we have a set `s` within this space such that `s` is a convex neighborhood of `0` and is open, then for any point `x₀` not in `s`, there exists a continuous linear functional `f` that maps `x₀` to 1 and every point in `s` to a value strictly less than 1.
More concisely: Given a topological additive group and real module `E` with continuous scalar multiplication, if `s` is an open, convex neighborhood of `0` in `E`, then there exists a continuous linear functional `f` such that `f(0) = 1` and `0 < f(x)` for all `x` in `s`, but `f(x₀) = 1` for some `x₀` not in `s`.
|
geometric_hahn_banach_open
theorem geometric_hahn_banach_open :
∀ {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : TopologicalAddGroup E]
[inst_3 : Module ℝ E] [inst_4 : ContinuousSMul ℝ E] {s t : Set E},
Convex ℝ s → IsOpen s → Convex ℝ t → Disjoint s t → ∃ f u, (∀ a ∈ s, f a < u) ∧ ∀ b ∈ t, u ≤ f b
The theorem `geometric_hahn_banach_open` is a variant of the Hahn-Banach theorem in Functional Analysis. It states that given two convex sets `s` and `t` in a real-valued topological vector space `E`, with `s` being open and `s` and `t` being disjoint, there exists a continuous linear functional `f` and a real number `u` such that for every element `a` in set `s`, `f a` is strictly less than `u` and for every element `b` in set `t`, `f b` is greater than or equal to `u`. In other words, the linear functional `f` separates the two disjoint convex sets `s` and `t` by assigning values from the entire real number line.
More concisely: Given two disjoint open convex sets `s` and `t` in a real-valued topological vector space `E`, there exists a continuous linear functional `f` and a real number `u` such that `f(a) < u` for all `a` in `s` and `f(b) >= u` for all `b` in `t`.
|
geometric_hahn_banach_point_point
theorem geometric_hahn_banach_point_point :
∀ {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : TopologicalAddGroup E]
[inst_3 : Module ℝ E] [inst_4 : ContinuousSMul ℝ E] {x y : E} [inst_5 : LocallyConvexSpace ℝ E]
[inst_6 : T1Space E], x ≠ y → ∃ f, f x < f y
This theorem, known as the point-point version of the geometric Hahn-Banach theorem, states that for any two distinct points `x` and `y` in a locally convex topological vector space `E` over the real numbers, there exists a continuous linear functional `f` such that `f(x)` is less than `f(y)`. This theorem provides a way to separate points in the space with a hyperplane. Note the space `E` must be equipped with the necessary structures, including an additive commutative group, a module over the reals, and a topological space where scalar multiplication is continuous.
More concisely: For any locally convex topological vector space over the real numbers and two distinct points, there exists a continuous linear functional separating them.
|