Absolutely convex sets

A set s in an commutative monoid E is called absolutely convex or disked if it is convex and balanced. The importance of absolutely convex sets comes from the fact that every locally convex topological vector space has a basis consisting of absolutely convex sets.

Main definitions

• absConvexHull: the absolutely convex hull of a set s is the smallest absolutely convex set containing s.
• gaugeSeminormFamily: the seminorm family induced by all open absolutely convex neighborhoods of zero.

Main statements

• absConvexHull_eq_convexHull_balancedHull: when the locally convex space is a module, the absolutely convex hull of a set s equals the convex hull of the balanced hull of s.
• convexHull_union_neg_eq_absConvexHull: the convex hull of s ∪ -s is the absolute convex hull of s.
• with_gaugeSeminormFamily: the topology of a locally convex space is induced by the family gaugeSeminormFamily.

Implementation notes

Mathlib's definition of Convex requires the scalars to be an OrderedSemiring whereas the definition of Balanced requires the scalars to be a SeminormedRing. Mathlib doesn't currently have a concept of a semi-normed ordered ring, so we define a set as AbsConvex if it is balanced over a SeminormedRing 𝕜 and convex over ℝ, assuming IsScalarTower ℝ 𝕜 E and SMulCommClass ℝ 𝕜 E where required.

Tags

disks, convex, balanced

def AbsConvex (𝕜 : Type u_1) {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] [AddCommMonoid E] (s : Set E) : Prop

A set is absolutely convex if it is balanced and convex. Mathlib's definition of Convex requires the scalars to be an OrderedSemiring whereas the definition of Balanced requires the scalars to be a SeminormedRing. Mathlib doesn't currently have a concept of a semi-normed ordered ring, so we define a set as AbsConvex if it is balanced over a SeminormedRing 𝕜 and convex over ℝ.

Equations

• AbsConvex 𝕜 s = (Balanced 𝕜 s ∧ Convex ℝ s)

theorem AbsConvex.empty {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] [AddCommMonoid E] : AbsConvex 𝕜 ∅

theorem AbsConvex.univ {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] [AddCommMonoid E] : AbsConvex 𝕜 Set.univ

theorem AbsConvex.inter {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] [AddCommMonoid E] {s : Set E} {t : Set E} (hs : AbsConvex 𝕜 s) (ht : AbsConvex 𝕜 t) : AbsConvex 𝕜 (s ∩ t)

theorem AbsConvex.sInter {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] [AddCommMonoid E] {S : Set (Set E)} (h : ∀ s ∈ S, AbsConvex 𝕜 s) : AbsConvex 𝕜 (⋂₀ S)

theorem AbsConvex.iInter {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] [AddCommMonoid E] {ι : Sort u_3} {s : ι → Set E} (h : ∀ (i : ι), AbsConvex 𝕜 (s i)) : AbsConvex 𝕜 (⋂ (i : ι), s i)

@[simp]

theorem absConvexHull_isClosed (𝕜 : Type u_1) {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] [AddCommMonoid E] (s : Set E) : (absConvexHull 𝕜).IsClosed s = AbsConvex 𝕜 s

def absConvexHull (𝕜 : Type u_1) {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] [AddCommMonoid E] : ClosureOperator (Set E)

The absolute convex hull of a set s is the minimal absolute convex set that includes s.

Equations

• absConvexHull 𝕜 = ClosureOperator.ofCompletePred (AbsConvex 𝕜) ⋯

theorem subset_absConvexHull {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] [AddCommMonoid E] {s : Set E} : s ⊆ (absConvexHull 𝕜) s

theorem absConvex_absConvexHull {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] [AddCommMonoid E] {s : Set E} : AbsConvex 𝕜 ((absConvexHull 𝕜) s)

theorem balanced_absConvexHull {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] [AddCommMonoid E] {s : Set E} : Balanced 𝕜 ((absConvexHull 𝕜) s)

theorem convex_absConvexHull {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] [AddCommMonoid E] {s : Set E} : Convex ℝ ((absConvexHull 𝕜) s)

theorem absConvexHull_eq_iInter (𝕜 : Type u_1) {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] [AddCommMonoid E] (s : Set E) : (absConvexHull 𝕜) s = ⋂ (t : Set E), ⋂ (_ : s ⊆ t), ⋂ (_ : AbsConvex 𝕜 t), t

theorem mem_absConvexHull_iff {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] [AddCommMonoid E] {s : Set E} {x : E} : x ∈ (absConvexHull 𝕜) s ↔ ∀ (t : Set E), s ⊆ t → AbsConvex 𝕜 t → x ∈ t

theorem absConvexHull_min {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] [AddCommMonoid E] {s : Set E} {t : Set E} : s ⊆ t → AbsConvex 𝕜 t → (absConvexHull 𝕜) s ⊆ t

theorem AbsConvex.absConvexHull_subset_iff {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] [AddCommMonoid E] {s : Set E} {t : Set E} (ht : AbsConvex 𝕜 t) : (absConvexHull 𝕜) s ⊆ t ↔ s ⊆ t

theorem absConvexHull_mono {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] [AddCommMonoid E] {s : Set E} {t : Set E} (hst : s ⊆ t) : (absConvexHull 𝕜) s ⊆ (absConvexHull 𝕜) t

theorem absConvexHull_eq_self {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] [AddCommMonoid E] {s : Set E} : (absConvexHull 𝕜) s = s ↔ AbsConvex 𝕜 s

theorem AbsConvex.absConvexHull_eq {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] [AddCommMonoid E] {s : Set E} : AbsConvex 𝕜 s → (absConvexHull 𝕜) s = s

Alias of the reverse direction of absConvexHull_eq_self.

@[simp]

theorem absConvexHull_univ {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] [AddCommMonoid E] : (absConvexHull 𝕜) Set.univ = Set.univ

@[simp]

theorem absConvexHull_empty {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] [AddCommMonoid E] : (absConvexHull 𝕜) ∅ = ∅

@[simp]

theorem absConvexHull_eq_empty {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] [AddCommMonoid E] {s : Set E} : (absConvexHull 𝕜) s = ∅ ↔ s = ∅

@[simp]

theorem absConvexHull_nonempty {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] [AddCommMonoid E] {s : Set E} : ((absConvexHull 𝕜) s).Nonempty ↔ s.Nonempty

theorem Set.Nonempty.absConvexHull {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] [AddCommMonoid E] {s : Set E} : s.Nonempty → ((absConvexHull 𝕜) s).Nonempty

Alias of the reverse direction of absConvexHull_nonempty.

theorem nhds_hasBasis_absConvex (𝕜 : Type u_1) (E : Type u_2) [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Module ℝ E] [SMulCommClass ℝ 𝕜 E] [TopologicalSpace E] [LocallyConvexSpace ℝ E] [ContinuousSMul 𝕜 E] : (nhds 0).HasBasis (fun (s : Set E) => s ∈ nhds 0 ∧ AbsConvex 𝕜 s) id

theorem nhds_hasBasis_absConvex_open (𝕜 : Type u_1) (E : Type u_2) [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [Module ℝ E] [SMulCommClass ℝ 𝕜 E] [TopologicalSpace E] [LocallyConvexSpace ℝ E] [ContinuousSMul 𝕜 E] [ContinuousSMul ℝ E] [TopologicalAddGroup E] : (nhds 0).HasBasis (fun (s : Set E) => 0 ∈ s ∧ IsOpen s ∧ AbsConvex 𝕜 s) id

theorem absConvexHull_add_subset (𝕜 : Type u_1) {E : Type u_2} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module ℝ E] [Module 𝕜 E] {s : Set E} {t : Set E} : (absConvexHull 𝕜) (s + t) ⊆ (absConvexHull 𝕜) s + (absConvexHull 𝕜) t

theorem absConvexHull_eq_convexHull_balancedHull (𝕜 : Type u_1) {E : Type u_2} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module ℝ E] [Module 𝕜 E] [SMulCommClass ℝ 𝕜 E] {s : Set E} : (absConvexHull 𝕜) s = (convexHull ℝ) (balancedHull 𝕜 s)

theorem balancedHull_convexHull_subseteq_absConvexHull (𝕜 : Type u_1) {E : Type u_2} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module ℝ E] [Module 𝕜 E] {s : Set E} : balancedHull 𝕜 ((convexHull ℝ) s) ⊆ (absConvexHull 𝕜) s

In general, equality doesn't hold here - e.g. consider s := {(-1, 1), (1, 1)} in ℝ².

theorem balancedHull_subset_convexHull_union_neg {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} : balancedHull ℝ s ⊆ (convexHull ℝ) (s ∪ -s)

@[simp]

theorem convexHull_union_neg_eq_absConvexHull {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} : (convexHull ℝ) (s ∪ -s) = (absConvexHull ℝ) s

theorem totallyBounded_absConvexHull (E : Type u_2) [AddCommGroup E] [Module ℝ E] {s : Set E} [UniformSpace E] [UniformAddGroup E] [lcs : LocallyConvexSpace ℝ E] [ContinuousSMul ℝ E] (hs : TotallyBounded s) : TotallyBounded ((absConvexHull ℝ) s)

def AbsConvexOpenSets (𝕜 : Type u_1) (E : Type u_2) [TopologicalSpace E] [AddCommMonoid E] [Zero E] [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] : Type (max 0 u_2)

The type of absolutely convex open sets.

Equations

• AbsConvexOpenSets 𝕜 E = { s : Set E // 0 ∈ s ∧ IsOpen s ∧ AbsConvex 𝕜 s }

noncomputable instance AbsConvexOpenSets.instCoeTC (𝕜 : Type u_1) (E : Type u_2) [TopologicalSpace E] [AddCommMonoid E] [Zero E] [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] : CoeTC (AbsConvexOpenSets 𝕜 E) (Set E)

Equations

• AbsConvexOpenSets.instCoeTC 𝕜 E = { coe := Subtype.val }

theorem AbsConvexOpenSets.coe_zero_mem {𝕜 : Type u_1} {E : Type u_2} [TopologicalSpace E] [AddCommMonoid E] [Zero E] [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] (s : AbsConvexOpenSets 𝕜 E) : 0 ∈ ↑s

theorem AbsConvexOpenSets.coe_isOpen {𝕜 : Type u_1} {E : Type u_2} [TopologicalSpace E] [AddCommMonoid E] [Zero E] [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] (s : AbsConvexOpenSets 𝕜 E) : IsOpen ↑s

theorem AbsConvexOpenSets.coe_nhds {𝕜 : Type u_1} {E : Type u_2} [TopologicalSpace E] [AddCommMonoid E] [Zero E] [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] (s : AbsConvexOpenSets 𝕜 E) : ↑s ∈ nhds 0

theorem AbsConvexOpenSets.coe_balanced {𝕜 : Type u_1} {E : Type u_2} [TopologicalSpace E] [AddCommMonoid E] [Zero E] [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] (s : AbsConvexOpenSets 𝕜 E) : Balanced 𝕜 ↑s

theorem AbsConvexOpenSets.coe_convex {𝕜 : Type u_1} {E : Type u_2} [TopologicalSpace E] [AddCommMonoid E] [Zero E] [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] (s : AbsConvexOpenSets 𝕜 E) : Convex ℝ ↑s

instance AbsConvexOpenSets.instNonempty (𝕜 : Type u_1) (E : Type u_2) [TopologicalSpace E] [AddCommMonoid E] [Zero E] [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] : Nonempty (AbsConvexOpenSets 𝕜 E)

Equations

• ⋯ = ⋯

noncomputable def gaugeSeminormFamily (𝕜 : Type u_1) (E : Type u_2) [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [Module ℝ E] [IsScalarTower ℝ 𝕜 E] [ContinuousSMul ℝ E] : SeminormFamily 𝕜 E (AbsConvexOpenSets 𝕜 E)

The family of seminorms defined by the gauges of absolute convex open sets.

Equations

• gaugeSeminormFamily 𝕜 E s = gaugeSeminorm ⋯ ⋯ ⋯

theorem gaugeSeminormFamily_ball {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [Module ℝ E] [IsScalarTower ℝ 𝕜 E] [ContinuousSMul ℝ E] (s : AbsConvexOpenSets 𝕜 E) : (gaugeSeminormFamily 𝕜 E s).ball 0 1 = ↑s

theorem with_gaugeSeminormFamily {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [Module ℝ E] [IsScalarTower ℝ 𝕜 E] [ContinuousSMul ℝ E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] [SMulCommClass ℝ 𝕜 E] [LocallyConvexSpace ℝ E] : WithSeminorms (gaugeSeminormFamily 𝕜 E)

The topology of a locally convex space is induced by the gauge seminorm family.