Local convexity

This file defines absorbent and balanced sets.

An absorbent set is one that "surrounds" the origin. The idea is made precise by requiring that any point belongs to all large enough scalings of the set. This is the vector world analog of a topological neighborhood of the origin.

A balanced set is one that is everywhere around the origin. This means that a • s ⊆ s for all a of norm less than 1.

Main declarations

For a module over a normed ring:

• Absorbs: A set s absorbs a set t if all large scalings of s contain t.
• Absorbent: A set s is absorbent if every point eventually belongs to all large scalings of s.
• Balanced: A set s is balanced if a • s ⊆ s for all a of norm less than 1.

References

• [H. H. Schaefer, Topological Vector Spaces][schaefer1966]

Tags

absorbent, balanced, locally convex, LCTVS

def Balanced (𝕜 : Type u_1) {E : Type u_3} [SeminormedRing 𝕜] [SMul 𝕜 E] (A : Set E) : Prop

A set A is balanced if a • A is contained in A whenever a has norm at most 1.

Equations

• Balanced 𝕜 A = ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • A ⊆ A

theorem absorbs_iff_norm {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [SMul 𝕜 E] {A : Set E} {B : Set E} : Absorbs 𝕜 A B ↔ ∃ (r : ℝ), ∀ (c : 𝕜), r ≤ ‖c‖ → B ⊆ c • A

theorem Absorbs.of_norm {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [SMul 𝕜 E] {A : Set E} {B : Set E} : (∃ (r : ℝ), ∀ (c : 𝕜), r ≤ ‖c‖ → B ⊆ c • A) → Absorbs 𝕜 A B

Alias of the reverse direction of absorbs_iff_norm.

theorem Absorbs.exists_pos {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [SMul 𝕜 E] {A : Set E} {B : Set E} (h : Absorbs 𝕜 A B) : ∃ r > 0, ∀ (c : 𝕜), r ≤ ‖c‖ → B ⊆ c • A

theorem balanced_iff_smul_mem {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [SMul 𝕜 E] {s : Set E} : Balanced 𝕜 s ↔ ∀ ⦃a : 𝕜⦄, ‖a‖ ≤ 1 → ∀ ⦃x : E⦄, x ∈ s → a • x ∈ s

theorem Balanced.smul_mem {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [SMul 𝕜 E] {s : Set E} : Balanced 𝕜 s → ∀ ⦃a : 𝕜⦄, ‖a‖ ≤ 1 → ∀ ⦃x : E⦄, x ∈ s → a • x ∈ s

Alias of the forward direction of balanced_iff_smul_mem.

theorem balanced_iff_closedBall_smul {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [SMul 𝕜 E] {s : Set E} : Balanced 𝕜 s ↔ Metric.closedBall 0 1 • s ⊆ s

@[simp]

theorem balanced_empty {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [SMul 𝕜 E] : Balanced 𝕜 ∅

@[simp]

theorem balanced_univ {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [SMul 𝕜 E] : Balanced 𝕜 Set.univ

theorem Balanced.union {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [SMul 𝕜 E] {A : Set E} {B : Set E} (hA : Balanced 𝕜 A) (hB : Balanced 𝕜 B) : Balanced 𝕜 (A ∪ B)

theorem Balanced.inter {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [SMul 𝕜 E] {A : Set E} {B : Set E} (hA : Balanced 𝕜 A) (hB : Balanced 𝕜 B) : Balanced 𝕜 (A ∩ B)

theorem balanced_iUnion {𝕜 : Type u_1} {E : Type u_3} {ι : Sort u_4} [SeminormedRing 𝕜] [SMul 𝕜 E] {f : ι → Set E} (h : ∀ (i : ι), Balanced 𝕜 (f i)) : Balanced 𝕜 (⋃ (i : ι), f i)

theorem balanced_iUnion₂ {𝕜 : Type u_1} {E : Type u_3} {ι : Sort u_4} {κ : ι → Sort u_5} [SeminormedRing 𝕜] [SMul 𝕜 E] {f : (i : ι) → κ i → Set E} (h : ∀ (i : ι) (j : κ i), Balanced 𝕜 (f i j)) : Balanced 𝕜 (⋃ (i : ι), ⋃ (j : κ i), f i j)

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

theorem balanced_iInter {𝕜 : Type u_1} {E : Type u_3} {ι : Sort u_4} [SeminormedRing 𝕜] [SMul 𝕜 E] {f : ι → Set E} (h : ∀ (i : ι), Balanced 𝕜 (f i)) : Balanced 𝕜 (⋂ (i : ι), f i)

theorem balanced_iInter₂ {𝕜 : Type u_1} {E : Type u_3} {ι : Sort u_4} {κ : ι → Sort u_5} [SeminormedRing 𝕜] [SMul 𝕜 E] {f : (i : ι) → κ i → Set E} (h : ∀ (i : ι) (j : κ i), Balanced 𝕜 (f i j)) : Balanced 𝕜 (⋂ (i : ι), ⋂ (j : κ i), f i j)

theorem Balanced.smul {𝕜 : Type u_1} {𝕝 : Type u_2} {E : Type u_3} [SeminormedRing 𝕜] [SMul 𝕜 E] {s : Set E} [SMul 𝕝 E] [SMulCommClass 𝕜 𝕝 E] (a : 𝕝) (hs : Balanced 𝕜 s) : Balanced 𝕜 (a • s)

theorem Balanced.neg {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} : Balanced 𝕜 s → Balanced 𝕜 (-s)

@[simp]

theorem balanced_neg {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} : Balanced 𝕜 (-s) ↔ Balanced 𝕜 s

theorem Balanced.neg_mem_iff {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} [NormOneClass 𝕜] (h : Balanced 𝕜 s) {x : E} : -x ∈ s ↔ x ∈ s

theorem Balanced.neg_eq {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} [NormOneClass 𝕜] (h : Balanced 𝕜 s) : -s = s

theorem Balanced.add {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} {t : Set E} (hs : Balanced 𝕜 s) (ht : Balanced 𝕜 t) : Balanced 𝕜 (s + t)

theorem Balanced.sub {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} {t : Set E} (hs : Balanced 𝕜 s) (ht : Balanced 𝕜 t) : Balanced 𝕜 (s - t)

theorem balanced_zero {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] : Balanced 𝕜 0

theorem absorbs_iff_eventually_nhdsWithin_zero {𝕜 : Type u_1} {E : Type u_3} [NormedDivisionRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} {t : Set E} : Absorbs 𝕜 s t ↔ ∀ᶠ (c : 𝕜) in nhdsWithin 0 {0}ᶜ, Set.MapsTo (fun (x : E) => c • x) t s

theorem Absorbs.eventually_nhdsWithin_zero {𝕜 : Type u_1} {E : Type u_3} [NormedDivisionRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} {t : Set E} : Absorbs 𝕜 s t → ∀ᶠ (c : 𝕜) in nhdsWithin 0 {0}ᶜ, Set.MapsTo (fun (x : E) => c • x) t s

Alias of the forward direction of absorbs_iff_eventually_nhdsWithin_zero.

theorem absorbent_iff_eventually_nhdsWithin_zero {𝕜 : Type u_1} {E : Type u_3} [NormedDivisionRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} : Absorbent 𝕜 s ↔ ∀ (x : E), ∀ᶠ (c : 𝕜) in nhdsWithin 0 {0}ᶜ, c • x ∈ s

theorem Absorbent.eventually_nhdsWithin_zero {𝕜 : Type u_1} {E : Type u_3} [NormedDivisionRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} : Absorbent 𝕜 s → ∀ (x : E), ∀ᶠ (c : 𝕜) in nhdsWithin 0 {0}ᶜ, c • x ∈ s

Alias of the forward direction of absorbent_iff_eventually_nhdsWithin_zero.

theorem absorbs_iff_eventually_nhds_zero {𝕜 : Type u_1} {E : Type u_3} [NormedDivisionRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} {t : Set E} (h₀ : 0 ∈ s) : Absorbs 𝕜 s t ↔ ∀ᶠ (c : 𝕜) in nhds 0, Set.MapsTo (fun (x : E) => c • x) t s

theorem Absorbs.eventually_nhds_zero {𝕜 : Type u_1} {E : Type u_3} [NormedDivisionRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} {t : Set E} (h : Absorbs 𝕜 s t) (h₀ : 0 ∈ s) : ∀ᶠ (c : 𝕜) in nhds 0, Set.MapsTo (fun (x : E) => c • x) t s

theorem Balanced.smul_mono {𝕜 : Type u_1} {𝕝 : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedRing 𝕝] [NormedSpace 𝕜 𝕝] [AddCommGroup E] [Module 𝕜 E] [SMulWithZero 𝕝 E] [IsScalarTower 𝕜 𝕝 E] {s : Set E} (hs : Balanced 𝕝 s) {a : 𝕝} {b : 𝕜} (h : ‖a‖ ≤ ‖b‖) : a • s ⊆ b • s

Scalar multiplication (by possibly different types) of a balanced set is monotone.

theorem Balanced.smul_mem_mono {𝕜 : Type u_1} {𝕝 : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedRing 𝕝] [NormedSpace 𝕜 𝕝] [AddCommGroup E] [Module 𝕜 E] [SMulWithZero 𝕝 E] [IsScalarTower 𝕜 𝕝 E] {s : Set E} {x : E} [SMulCommClass 𝕝 𝕜 E] (hs : Balanced 𝕝 s) {a : 𝕜} {b : 𝕝} (ha : a • x ∈ s) (hba : ‖b‖ ≤ ‖a‖) : b • x ∈ s

theorem Balanced.subset_smul {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {A : Set E} {a : 𝕜} (hA : Balanced 𝕜 A) (ha : 1 ≤ ‖a‖) : A ⊆ a • A

theorem Balanced.smul_congr {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {A : Set E} {a : 𝕜} {b : 𝕜} (hs : Balanced 𝕜 A) (h : ‖a‖ = ‖b‖) : a • A = b • A

theorem Balanced.smul_eq {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {A : Set E} {a : 𝕜} (hA : Balanced 𝕜 A) (ha : ‖a‖ = 1) : a • A = A

theorem Balanced.absorbs_self {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {A : Set E} (hA : Balanced 𝕜 A) : Absorbs 𝕜 A A

A balanced set absorbs itself.

theorem Balanced.smul_mem_iff {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} {x : E} {a : 𝕜} {b : 𝕜} (hs : Balanced 𝕜 s) (h : ‖a‖ = ‖b‖) : a • x ∈ s ↔ b • x ∈ s

@[deprecated Balanced.smul_mem_iff]

theorem Balanced.mem_smul_iff {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} {x : E} {a : 𝕜} {b : 𝕜} (hs : Balanced 𝕜 s) (h : ‖a‖ = ‖b‖) : a • x ∈ s ↔ b • x ∈ s

Alias of Balanced.smul_mem_iff.

theorem absorbent_nhds_zero {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {A : Set E} [TopologicalSpace E] [ContinuousSMul 𝕜 E] (hA : A ∈ nhds 0) : Absorbent 𝕜 A

Every neighbourhood of the origin is absorbent.

theorem Balanced.zero_insert_interior {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {A : Set E} [TopologicalSpace E] [ContinuousSMul 𝕜 E] (hA : Balanced 𝕜 A) : Balanced 𝕜 (insert 0 (interior A))

The union of {0} with the interior of a balanced set is balanced.

@[deprecated Balanced.zero_insert_interior]

theorem balanced_zero_union_interior {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {A : Set E} [TopologicalSpace E] [ContinuousSMul 𝕜 E] (hA : Balanced 𝕜 A) : Balanced 𝕜 (0 ∪ interior A)

theorem Balanced.interior {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {A : Set E} [TopologicalSpace E] [ContinuousSMul 𝕜 E] (hA : Balanced 𝕜 A) (h : 0 ∈ interior A) : Balanced 𝕜 (interior A)

The interior of a balanced set is balanced if it contains the origin.

theorem Balanced.closure {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {A : Set E} [TopologicalSpace E] [ContinuousSMul 𝕜 E] (hA : Balanced 𝕜 A) : Balanced 𝕜 (closure A)

@[deprecated Absorbent.zero_mem]

theorem Absorbent.zero_mem' {𝕜 : Type u_1} {E : Type u_3} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} (hs : Absorbent 𝕜 s) : 0 ∈ s

theorem Balanced.convexHull {𝕜 : Type u_1} {E : Type u_3} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} [Module ℝ E] [SMulCommClass ℝ 𝕜 E] (hs : Balanced 𝕜 s) : Balanced 𝕜 ((convexHull ℝ) s)

@[deprecated Balanced.convexHull]

theorem balanced_convexHull_of_balanced {𝕜 : Type u_1} {E : Type u_3} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} [Module ℝ E] [SMulCommClass ℝ 𝕜 E] (hs : Balanced 𝕜 s) : Balanced 𝕜 ((convexHull ℝ) s)

Alias of Balanced.convexHull.

theorem balanced_iff_neg_mem {E : Type u_3} [AddCommGroup E] [Module ℝ E] {s : Set E} (hs : Convex ℝ s) : Balanced ℝ s ↔ ∀ ⦃x : E⦄, x ∈ s → -x ∈ s