# mathlib3documentation

analysis.locally_convex.balanced_core_hull

# Balanced Core and Balanced Hull #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## Main definitions #

• balanced_core: The largest balanced subset of a set s.
• balanced_hull: The smallest balanced superset of a set s.

## Main statements #

• balanced_core_eq_Inter: 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 balanced_hull has the defining properties of a hull in balanced.hull_minimal and subset_balanced_hull. For the core we need slightly stronger assumptions to obtain a characterization as an intersection, this is balanced_core_eq_Inter.

## Tags #

balanced

def balanced_core (𝕜 : Type u_1) {E : Type u_2} [ E] (s : set E) :
set E

The largest balanced subset of s.

Equations
def balanced_core_aux (𝕜 : Type u_1) {E : Type u_2} [ E] (s : set E) :
set E

Helper definition to prove balanced_core_eq_Inter

Equations
def balanced_hull (𝕜 : Type u_1) {E : Type u_2} [ E] (s : set E) :
set E

The smallest balanced superset of s.

Equations
theorem balanced_core_subset {𝕜 : Type u_1} {E : Type u_2} [ E] (s : set E) :
s
theorem balanced_core_empty {𝕜 : Type u_1} {E : Type u_2} [ E] :
theorem mem_balanced_core_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {s : set E} {x : E} :
x (t : set E), t t s x t
theorem smul_balanced_core_subset {𝕜 : Type u_1} {E : Type u_2} [ E] (s : set E) {a : 𝕜} (ha : a 1) :
a
theorem balanced_core_balanced {𝕜 : Type u_1} {E : Type u_2} [ E] (s : set E) :
s)
theorem balanced.subset_core_of_subset {𝕜 : Type u_1} {E : Type u_2} [ E] {s t : set E} (hs : s) (h : s t) :
s

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

theorem mem_balanced_core_aux_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {s : set E} {x : E} :
x (r : 𝕜), 1 r x r s
theorem mem_balanced_hull_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {s : set E} {x : E} :
x (r : 𝕜) (hr : r 1), x r s
theorem balanced.hull_subset_of_subset {𝕜 : Type u_1} {E : Type u_2} [ E] {s t : set E} (ht : t) (h : s t) :
t

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

theorem balanced_core_zero_mem {𝕜 : Type u_1} {E : Type u_2} [ E] {s : set E} (hs : 0 s) :
0
theorem balanced_core_nonempty_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {s : set E} :
s).nonempty 0 s
theorem subset_balanced_hull (𝕜 : Type u_1) {E : Type u_2} [ E] {s : set E} :
s
theorem balanced_hull.balanced {𝕜 : Type u_1} {E : Type u_2} [ E] (s : set E) :
s)
@[simp]
theorem balanced_core_aux_empty {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [ E] :
theorem balanced_core_aux_subset {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [ E] (s : set E) :
s
theorem balanced_core_aux_balanced {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [ E] {s : set E} (h0 : 0 ) :
s)
theorem balanced_core_aux_maximal {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [ E] {s t : set E} (h : t s) (ht : t) :
t
theorem balanced_core_subset_balanced_core_aux {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [ E] {s : set E} :
theorem balanced_core_eq_Inter {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [ E] {s : set E} (hs : 0 s) :
= (r : 𝕜) (hr : 1 r), r s
theorem subset_balanced_core {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [ E] {s t : set E} (ht : 0 t) (hst : (a : 𝕜), a 1 a s t) :
s

### Topological properties #

@[protected]
theorem is_closed.balanced_core {𝕜 : Type u_1} {E : Type u_2} [ E] [ E] {U : set E} (hU : is_closed U) :
theorem balanced_core_mem_nhds_zero {𝕜 : Type u_1} {E : Type u_2} [ E] [ E] {U : set E} (hU : U nhds 0) :
theorem nhds_basis_balanced (𝕜 : Type u_1) (E : Type u_2) [ E] [ E] :
(nhds 0).has_basis (λ (s : set E), s nhds 0 s) id
theorem nhds_basis_closed_balanced (𝕜 : Type u_1) (E : Type u_2) [ E] [ E]  :
(nhds 0).has_basis (λ (s : set E), s nhds 0 s) id