Documentation

Mathlib.Analysis.LocallyConvex.AbsConvex

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;
closedAbsConvexHull: the closed 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 absolutely convex hull of s;
closedAbsConvexHull_closure_eq_closedAbsConvexHull : the closed absolutely convex hull of the closure of s equals the closed absolutely 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) :

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)

Instances For

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 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)

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 𝕜) ⋯

Instances For

@[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

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 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 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 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 absConvex_closed_sInter {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] [AddCommMonoid E] [TopologicalSpace E] {S : Set (Set E)} (h : ∀ s ∈ S, AbsConvex 𝕜 s ∧ IsClosed s) :

AbsConvex 𝕜 (⋂₀ S) ∧ IsClosed (⋂₀ S)

def closedAbsConvexHull (𝕜 : Type u_1) {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] [AddCommMonoid E] [TopologicalSpace E] :

ClosureOperator (Set E)

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

Equations

closedAbsConvexHull 𝕜 = ClosureOperator.ofCompletePred (fun (s : Set E) => AbsConvex 𝕜 s ∧ IsClosed s) ⋯

Instances For

@[simp]

theorem closedAbsConvexHull_isClosed (𝕜 : Type u_1) {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] [AddCommMonoid E] [TopologicalSpace E] (s : Set E) :

(closedAbsConvexHull 𝕜).IsClosed s = (AbsConvex 𝕜 s ∧ IsClosed s)

theorem absConvex_convexClosedHull {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] [AddCommMonoid E] [TopologicalSpace E] {s : Set E} :

AbsConvex 𝕜 ((closedAbsConvexHull 𝕜) s)

theorem isClosed_closedAbsConvexHull {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] [AddCommMonoid E] [TopologicalSpace E] {s : Set E} :

IsClosed ((closedAbsConvexHull 𝕜) s)

theorem subset_closedAbsConvexHull {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] [AddCommMonoid E] [TopologicalSpace E] {s : Set E} :

s ⊆ (closedAbsConvexHull 𝕜) s

theorem closure_subset_closedAbsConvexHull {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] [AddCommMonoid E] [TopologicalSpace E] {s : Set E} :

closure s ⊆ (closedAbsConvexHull 𝕜) s

theorem closedAbsConvexHull_min {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] [AddCommMonoid E] [TopologicalSpace E] {s t : Set E} (hst : s ⊆ t) (h_conv : AbsConvex 𝕜 t) (h_closed : IsClosed t) :

(closedAbsConvexHull 𝕜) s ⊆ t

theorem absConvexHull_subset_closedAbsConvexHull {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] [AddCommMonoid E] [TopologicalSpace E] {s : Set E} :

(absConvexHull 𝕜) s ⊆ (closedAbsConvexHull 𝕜) s

@[simp]

theorem closedAbsConvexHull_closure_eq_closedAbsConvexHull {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] [SMul ℝ E] [AddCommMonoid E] [TopologicalSpace E] {s : Set E} :

(closedAbsConvexHull 𝕜) (closure s) = (closedAbsConvexHull 𝕜) s

theorem AbsConvex.closure {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [AddCommGroup E] [Module ℝ E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul ℝ E] [ContinuousSMul 𝕜 E] {s : Set E} (hs : AbsConvex 𝕜 s) :

AbsConvex 𝕜 (closure s)

theorem closedAbsConvexHull_eq_closure_absConvexHull {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [AddCommGroup E] [Module ℝ E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul ℝ E] [ContinuousSMul 𝕜 E] {s : Set E} :

(closedAbsConvexHull 𝕜) s = closure ((absConvexHull 𝕜) s)

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 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 u_2

The type of absolutely convex open sets.

Equations

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

Instances For

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) :

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)

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 ⋯ ⋯ ⋯

Instances For

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.