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 balanced core and hull are implemented differently: for the core we take the obvious definition of the union over all balanced sets that are contained in s, whereas for the hull, we take the union over r • s, for r the scalars with ‖r‖ ≤ 1. We show that balancedHull has the defining properties of a hull in Balanced.balancedHull_subset_of_subset and subset_balancedHull. For the core we need slightly stronger assumptions to obtain a characterization 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 | Balanced 𝕜 t ∧ t ⊆ s}

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] (s : Set E) : Set E

The smallest balanced superset of s.

Equations

• balancedHull 𝕜 s = ⋃ (r : 𝕜) (_ : ‖r‖ ≤ 1), r • s

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

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, Balanced 𝕜 t ∧ t ⊆ s ∧ x ∈ t

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 balancedCore_balanced {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] (s : Set E) : Balanced 𝕜 (balancedCore 𝕜 s)

theorem Balanced.subset_balancedCore_of_subset {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] {s : Set E} {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 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 mem_balancedHull_iff {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] {s : Set E} {x : E} : x ∈ balancedHull 𝕜 s ↔ ∃ r x, x ∈ r • s

theorem Balanced.balancedHull_subset_of_subset {𝕜 : Type u_1} {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] {s : Set E} {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 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} : Set.Nonempty (balancedCore 𝕜 s) ↔ 0 ∈ s

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

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

@[simp]

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

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

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

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

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

theorem balancedCore_eq_iInter {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [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} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} {t : Set E} (ht : 0 ∈ t) (hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t) : s ⊆ balancedCore 𝕜 t

Topological properties

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

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

theorem nhds_basis_balanced (𝕜 : Type u_1) (E : Type u_2) [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] : Filter.HasBasis (nhds 0) (fun s => s ∈ nhds 0 ∧ Balanced 𝕜 s) id

theorem nhds_basis_closed_balanced (𝕜 : Type u_1) (E : Type u_2) [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] [RegularSpace E] : Filter.HasBasis (nhds 0) (fun s => s ∈ nhds 0 ∧ IsClosed s ∧ Balanced 𝕜 s) id