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 sets.balanced_hull: The smallest balanced superset of a sets.
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.
References #
Tags #
balanced
def
balanced_core
(𝕜 : Type u_1)
{E : Type u_2}
[semi_normed_ring 𝕜]
[has_smul 𝕜 E]
(s : set E) :
set E
The largest balanced subset of s.
def
balanced_core_aux
(𝕜 : Type u_1)
{E : Type u_2}
[semi_normed_ring 𝕜]
[has_smul 𝕜 E]
(s : set E) :
set E
Helper definition to prove balanced_core_eq_Inter
theorem
balanced_core_subset
{𝕜 : Type u_1}
{E : Type u_2}
[semi_normed_ring 𝕜]
[has_smul 𝕜 E]
(s : set E) :
balanced_core 𝕜 s ⊆ s
theorem
balanced_core_empty
{𝕜 : Type u_1}
{E : Type u_2}
[semi_normed_ring 𝕜]
[has_smul 𝕜 E] :
balanced_core 𝕜 ∅ = ∅
theorem
smul_balanced_core_subset
{𝕜 : Type u_1}
{E : Type u_2}
[semi_normed_ring 𝕜]
[has_smul 𝕜 E]
(s : set E)
{a : 𝕜}
(ha : ‖a‖ ≤ 1) :
a • balanced_core 𝕜 s ⊆ balanced_core 𝕜 s
theorem
balanced_core_balanced
{𝕜 : Type u_1}
{E : Type u_2}
[semi_normed_ring 𝕜]
[has_smul 𝕜 E]
(s : set E) :
balanced 𝕜 (balanced_core 𝕜 s)
theorem
balanced.subset_core_of_subset
{𝕜 : Type u_1}
{E : Type u_2}
[semi_normed_ring 𝕜]
[has_smul 𝕜 E]
{s t : set E}
(hs : balanced 𝕜 s)
(h : s ⊆ t) :
s ⊆ balanced_core 𝕜 t
The balanced core of t is maximal in the sense that it contains any balanced subset
s of t.
theorem
balanced.hull_subset_of_subset
{𝕜 : Type u_1}
{E : Type u_2}
[semi_normed_ring 𝕜]
[has_smul 𝕜 E]
{s t : set E}
(ht : balanced 𝕜 t)
(h : s ⊆ t) :
balanced_hull 𝕜 s ⊆ 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}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
{s : set E}
(hs : 0 ∈ s) :
0 ∈ balanced_core 𝕜 s
theorem
balanced_core_nonempty_iff
{𝕜 : Type u_1}
{E : Type u_2}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
{s : set E} :
(balanced_core 𝕜 s).nonempty ↔ 0 ∈ s
theorem
subset_balanced_hull
(𝕜 : Type u_1)
{E : Type u_2}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
[norm_one_class 𝕜]
{s : set E} :
s ⊆ balanced_hull 𝕜 s
theorem
balanced_hull.balanced
{𝕜 : Type u_1}
{E : Type u_2}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
(s : set E) :
balanced 𝕜 (balanced_hull 𝕜 s)
@[simp]
theorem
balanced_core_aux_empty
{𝕜 : Type u_1}
{E : Type u_2}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E] :
balanced_core_aux 𝕜 ∅ = ∅
theorem
balanced_core_aux_subset
{𝕜 : Type u_1}
{E : Type u_2}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
(s : set E) :
balanced_core_aux 𝕜 s ⊆ s
theorem
balanced_core_aux_balanced
{𝕜 : Type u_1}
{E : Type u_2}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
{s : set E}
(h0 : 0 ∈ balanced_core_aux 𝕜 s) :
balanced 𝕜 (balanced_core_aux 𝕜 s)
theorem
balanced_core_aux_maximal
{𝕜 : Type u_1}
{E : Type u_2}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
{s t : set E}
(h : t ⊆ s)
(ht : balanced 𝕜 t) :
t ⊆ balanced_core_aux 𝕜 s
theorem
balanced_core_subset_balanced_core_aux
{𝕜 : Type u_1}
{E : Type u_2}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
{s : set E} :
balanced_core 𝕜 s ⊆ balanced_core_aux 𝕜 s
theorem
balanced_core_eq_Inter
{𝕜 : Type u_1}
{E : Type u_2}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
{s : set E}
(hs : 0 ∈ s) :
theorem
subset_balanced_core
{𝕜 : Type u_1}
{E : Type u_2}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
{s t : set E}
(ht : 0 ∈ t)
(hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t) :
s ⊆ balanced_core 𝕜 t
Topological properties #
@[protected]
theorem
is_closed.balanced_core
{𝕜 : Type u_1}
{E : Type u_2}
[nontrivially_normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[topological_space E]
[has_continuous_smul 𝕜 E]
{U : set E}
(hU : is_closed U) :
is_closed (balanced_core 𝕜 U)
theorem
balanced_core_mem_nhds_zero
{𝕜 : Type u_1}
{E : Type u_2}
[nontrivially_normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[topological_space E]
[has_continuous_smul 𝕜 E]
{U : set E}
(hU : U ∈ nhds 0) :
balanced_core 𝕜 U ∈ nhds 0
theorem
nhds_basis_balanced
(𝕜 : Type u_1)
(E : Type u_2)
[nontrivially_normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[topological_space E]
[has_continuous_smul 𝕜 E] :
theorem
nhds_basis_closed_balanced
(𝕜 : Type u_1)
(E : Type u_2)
[nontrivially_normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[topological_space E]
[has_continuous_smul 𝕜 E]
[regular_space E] :