Documentation

Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Balanced Core and Balanced Hull #

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 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 #

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
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
def balancedHull (๐•œ : Type u_1) {E : Type u_2} [SeminormedRing ๐•œ] [SMul ๐•œ E] (s : Set E) :
Set E

The smallest balanced superset of s.

Equations
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] :
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
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 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 : ๐•œ), โ€–rโ€– โ‰ค 1 โˆง x โˆˆ r โ€ข 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 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)
theorem balancedHull_add_subset {๐•œ : Type u_1} {E : Type u_2} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] {s : Set E} [NormOneClass ๐•œ] {t : Set E} :
balancedHull ๐•œ (s + t) โŠ† balancedHull ๐•œ s + balancedHull ๐•œ t
@[simp]
theorem balancedCoreAux_empty {๐•œ : Type u_1} {E : Type u_2} [NormedDivisionRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] :
theorem balancedCoreAux_subset {๐•œ : Type u_1} {E : Type u_2} [NormedDivisionRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] (s : Set E) :
balancedCoreAux ๐•œ s โŠ† s
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)
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
theorem balancedCore_subset_balancedCoreAux {๐•œ : Type u_1} {E : Type u_2} [NormedDivisionRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] {s : Set E} :
balancedCore ๐•œ s โŠ† balancedCoreAux ๐•œ 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 IsClosed.balancedCore {๐•œ : Type u_1} {E : Type u_2} [NormedDivisionRing ๐•œ] [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} [NormedDivisionRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] [TopologicalSpace E] [ContinuousSMul ๐•œ E] {U : Set 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_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