Balanced Core and Balanced Hull

Main definitions

• balancedCore: The largest balanced subset of a set s.
• balancedHull: The smallest balanced superset of a set s.

Main statements

• balancedCore_eq_iInter: Characterization of the balanced core as an intersection over subsets.
• nhds_basis_closed_balanced: The closed balanced sets form a basis of the neighborhood filter.

Implementation details

The balancedHull is defined as the ClosureOperator associated to the predicate Balanced 𝕜, i.e., as the intersection over all balanced sets containing s. The ClosureOperator API then provides most of the main results about the hull, e.g., subset_balancedHull and Balanced.balancedHull_subset_of_subset.

On the other hand, balancedCore 𝕜 s is defined directly as the union of all balanced subsets of s. This is exactly the ClosureOperator of Balanced 𝕜 on the order dual (Set E)ᵒᵈ, but there's not much support for such objects at this time in Mathlib.

Under slightly stronger assumptions, the hull can be described as the union over r • s, for r the scalars with ‖r‖ ≤ 1; this is balancedHull_eq_iUnion. Likewise, the core can be characterized as an intersection, this is balancedCore_eq_iInter.

References

• [Bourbaki, Topological Vector Spaces][bourbaki1987]

Tags

balanced

def balancedCore (𝕜 : Type u_1) {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] (s : Set E) : Set E

The largest balanced subset of s.

Equations

• balancedCore 𝕜 s = ⋃₀ {t : Set E | Balanced 𝕜 t ∧ t ⊆ s}

@[deprecated "Use balancedCore directly instead" (since := "2026-09-16")]

def balancedCoreAux (𝕜 : Type u_1) {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] (s : Set E) : Set E

Helper definition to prove balanced_core_eq_iInter

Equations

• balancedCoreAux 𝕜 s = ⋂ (r : 𝕜), ⋂ (_ : 1 ≤ ‖r‖), r • s

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

The smallest balanced superset of s.

Equations

• balancedHull 𝕜 = ClosureOperator.ofCompletePred (Balanced 𝕜) ⋯

theorem balancedCore_subset {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] (s : Set E) : balancedCore 𝕜 s ⊆ s

theorem balancedCore.balanced {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] (s : Set E) : Balanced 𝕜 (balancedCore 𝕜 s)

@[deprecated balancedCore.balanced (since := "2026-09-08")]

theorem balancedCore_balanced {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] (s : Set E) : Balanced 𝕜 (balancedCore 𝕜 s)

Alias of balancedCore.balanced.

theorem Balanced.subset_balancedCore_of_subset {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] {s t : Set E} (hs : Balanced 𝕜 s) (h : s ⊆ t) : s ⊆ balancedCore 𝕜 t

The balanced core of t is maximal in the sense that it contains any balanced subset s of t.

theorem balancedCore_mono {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] {s t : Set E} (hst : s ⊆ t) : balancedCore 𝕜 s ⊆ balancedCore 𝕜 t

theorem balancedCore_empty {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] : balancedCore 𝕜 ∅ = ∅

theorem mem_balancedCore_iff {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] {s : Set E} {x : E} : x ∈ balancedCore 𝕜 s ↔ ∃ (t : Set E), Balanced 𝕜 t ∧ t ⊆ s ∧ x ∈ t

@[deprecated "Use mem_balancedCore_iff directly" (since := "2026-09-16")]

theorem mem_balancedCoreAux_iff {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] {s : Set E} {x : E} : x ∈ balancedCoreAux 𝕜 s ↔ ∀ (r : 𝕜), 1 ≤ ‖r‖ → x ∈ r • s

theorem smul_balancedCore_subset {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] (s : Set E) {a : 𝕜} (ha : ‖a‖ ≤ 1) : a • balancedCore 𝕜 s ⊆ balancedCore 𝕜 s

theorem Balanced.balancedCore_eq {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] {s : Set E} (h : Balanced 𝕜 s) : balancedCore 𝕜 s = s

theorem balancedHull.balanced {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] (s : Set E) : Balanced 𝕜 ((balancedHull 𝕜) s)

theorem subset_balancedHull (𝕜 : Type u_1) {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] {s : Set E} : s ⊆ (balancedHull 𝕜) s

theorem Balanced.balancedHull_subset_of_subset {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] {s t : Set E} (ht : Balanced 𝕜 t) (h : s ⊆ t) : (balancedHull 𝕜) s ⊆ t

The balanced hull of s is minimal in the sense that it is contained in any balanced superset t of s.

theorem balancedHull_mono {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] {s t : Set E} (hst : s ⊆ t) : (balancedHull 𝕜) s ⊆ (balancedHull 𝕜) t

theorem balancedCore_zero_mem {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} (hs : 0 ∈ s) : 0 ∈ balancedCore 𝕜 s

theorem balancedCore_nonempty_iff {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} : (balancedCore 𝕜 s).Nonempty ↔ 0 ∈ s

theorem Balanced.zero_mem {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} (hs : Balanced 𝕜 s) (hs_nonempty : s.Nonempty) : 0 ∈ s

theorem balancedHull_eq_iUnion {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [NormOneClass 𝕜] (s : Set E) : (balancedHull 𝕜) s = ⋃ (r : 𝕜), ⋃ (_ : ‖r‖ ≤ 1), r • s

The balanced hull of s is the union of the sets r • s, for r a scalar with ‖r‖ ≤ 1.

theorem mem_balancedHull_iff {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} {x : E} [NormOneClass 𝕜] : x ∈ (balancedHull 𝕜) s ↔ ∃ (r : 𝕜), ‖r‖ ≤ 1 ∧ x ∈ r • s

theorem balancedHull_add_subset {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s t : Set E} : (balancedHull 𝕜) (s + t) ⊆ (balancedHull 𝕜) s + (balancedHull 𝕜) t

@[deprecated "Use balancedCore_empty directly" (since := "2026-09-16")]

theorem balancedCoreAux_empty {𝕜 : Type u_1} {E : Type u_2} [NormedDivisionRing 𝕜] [AddCommGroup E] [Module 𝕜 E] : balancedCoreAux 𝕜 ∅ = ∅

@[deprecated "Use balancedCore_subset directly" (since := "2026-09-16")]

theorem balancedCoreAux_subset {𝕜 : Type u_1} {E : Type u_2} [NormedDivisionRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (s : Set E) : balancedCoreAux 𝕜 s ⊆ s

@[deprecated "Use balancedCore.balanced directly" (since := "2026-09-16")]

theorem balancedCoreAux_balanced {𝕜 : Type u_1} {E : Type u_2} [NormedDivisionRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} (h0 : 0 ∈ balancedCoreAux 𝕜 s) : Balanced 𝕜 (balancedCoreAux 𝕜 s)

@[deprecated "Use Balanced.subset_balancedCore_of_subset directly" (since := "2026-09-16")]

theorem balancedCoreAux_maximal {𝕜 : Type u_1} {E : Type u_2} [NormedDivisionRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s t : Set E} (h : t ⊆ s) (ht : Balanced 𝕜 t) : t ⊆ balancedCoreAux 𝕜 s

@[deprecated "Use balancedCore directly instead of balancedCoreAux" (since := "2026-09-16")]

theorem balancedCore_subset_balancedCoreAux {𝕜 : Type u_1} {E : Type u_2} [NormedDivisionRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} : balancedCore 𝕜 s ⊆ balancedCoreAux 𝕜 s

theorem iInter_smul_subset {𝕜 : Type u_1} {E : Type u_2} [NormedDivisionRing 𝕜] [AddCommGroup E] [Module 𝕜 E] (s : Set E) : ⋂ (r : 𝕜), ⋂ (_ : 1 ≤ ‖r‖), r • s ⊆ s

theorem Balanced.subset_iInter_smul {𝕜 : Type u_1} {E : Type u_2} [NormedDivisionRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s t : Set E} (ht : Balanced 𝕜 t) (h : t ⊆ s) : t ⊆ ⋂ (r : 𝕜), ⋂ (_ : 1 ≤ ‖r‖), r • s

Any balanced subset of s is contained in ⋂ (r : 𝕜) (_ : 1 ≤ ‖r‖), r • s.

theorem balanced_iInter_smul {𝕜 : Type u_1} {E : Type u_2} [NormedDivisionRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} (hs : 0 ∈ s) : Balanced 𝕜 (⋂ (r : 𝕜), ⋂ (_ : 1 ≤ ‖r‖), r • s)

If s contains the origin, then ⋂ (r : 𝕜) (_ : 1 ≤ ‖r‖), r • s is balanced; by balancedCore_eq_iInter it is then the balanced core of s.

theorem balancedCore_eq_iInter {𝕜 : Type u_1} {E : Type u_2} [NormedDivisionRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} (hs : 0 ∈ s) : balancedCore 𝕜 s = ⋂ (r : 𝕜), ⋂ (_ : 1 ≤ ‖r‖), r • s

theorem subset_balancedCore {𝕜 : Type u_1} {E : Type u_2} [NormedDivisionRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s t : Set E} (ht : 0 ∈ t) (hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t) : s ⊆ balancedCore 𝕜 t

Topological properties

theorem IsOpen.balancedHull {𝕜 : Type u_1} {E : Type u_2} [NormedDivisionRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : IsOpen s) (hzero : 0 ∈ s) : IsOpen ((balancedHull 𝕜) s)

theorem IsClosed.balancedCore {𝕜 : Type u_1} {E : Type u_2} [NormedDivisionRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {U : Set E} [ContinuousSMul 𝕜 E] (hU : IsClosed U) : IsClosed (balancedCore 𝕜 U)

theorem balancedCore_mem_nhds_zero {𝕜 : Type u_1} {E : Type u_2} [NormedDivisionRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {U : Set E} [ContinuousSMul 𝕜 E] [(nhdsWithin 0 {0}ᶜ).NeBot] (hU : U ∈ nhds 0) : balancedCore 𝕜 U ∈ nhds 0

theorem nhds_basis_balanced (𝕜 : Type u_1) (E : Type u_2) [NormedDivisionRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] [(nhdsWithin 0 {0}ᶜ).NeBot] : (nhds 0).HasBasis (fun (s : Set E) => s ∈ nhds 0 ∧ Balanced 𝕜 s) id

theorem nhds_basis_open_balanced (𝕜 : Type u_1) (E : Type u_2) [NormedDivisionRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] [(nhdsWithin 0 {0}ᶜ).NeBot] : (nhds 0).HasBasis (fun (s : Set E) => s ∈ nhds 0 ∧ IsOpen s ∧ Balanced 𝕜 s) id

The open balanced sets form a basis of the neighborhood filter of the origin: the balanced hull of an open neighborhood of 0 is again open.

theorem nhds_basis_closed_balanced (𝕜 : Type u_1) (E : Type u_2) [NormedDivisionRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] [(nhdsWithin 0 {0}ᶜ).NeBot] [RegularSpace E] : (nhds 0).HasBasis (fun (s : Set E) => s ∈ nhds 0 ∧ IsClosed s ∧ Balanced 𝕜 s) id

The closed balanced sets form a basis of the neighborhood filter of the origin: the closure of a balanced neighborhood of 0 is again balanced.