mathlib3 documentation

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 #

Main statements #

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.

Equations
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

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

The smallest balanced superset of s.

Equations
theorem balanced_core_subset {𝕜 : Type u_1} {E : Type u_2} [semi_normed_ring 𝕜] [has_smul 𝕜 E] (s : set E) :
theorem balanced_core_empty {𝕜 : Type u_1} {E : Type u_2} [semi_normed_ring 𝕜] [has_smul 𝕜 E] :
theorem mem_balanced_core_iff {𝕜 : Type u_1} {E : Type u_2} [semi_normed_ring 𝕜] [has_smul 𝕜 E] {s : set E} {x : E} :
x balanced_core 𝕜 s (t : set E), balanced 𝕜 t t s x t
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) :
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) :

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} [semi_normed_ring 𝕜] [has_smul 𝕜 E] {s : set E} {x : E} :
x balanced_core_aux 𝕜 s (r : 𝕜), 1 r x r s
theorem mem_balanced_hull_iff {𝕜 : Type u_1} {E : Type u_2} [semi_normed_ring 𝕜] [has_smul 𝕜 E] {s : set E} {x : E} :
x balanced_hull 𝕜 s (r : 𝕜) (hr : r 1), x r s
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) :

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) :
theorem balanced_core_nonempty_iff {𝕜 : Type u_1} {E : Type u_2} [semi_normed_ring 𝕜] [add_comm_group E] [module 𝕜 E] {s : set E} :
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} :
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] :
theorem balanced_core_aux_subset {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] (s : set E) :
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) :
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) :
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} :
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) :
balanced_core 𝕜 s = (r : 𝕜) (hr : 1 r), r 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) :

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) :
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) :
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] :
(nhds 0).has_basis (λ (s : set E), s nhds 0 balanced 𝕜 s) id
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] :
(nhds 0).has_basis (λ (s : set E), s nhds 0 is_closed s balanced 𝕜 s) id