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
Instances For
    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
    Instances For
      def balancedHull (𝕜 : Type u_1) {E : Type u_2} [SeminormedRing 𝕜] [SMul 𝕜 E] (s : Set E) :
      Set E

      The smallest balanced superset of s.

      Equations
      Instances For
        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) :
        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 rx 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 : 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} :
        (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)
        @[simp]
        theorem balancedCoreAux_empty {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] :
        theorem balancedCoreAux_subset {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (s : Set E) :
        theorem balancedCoreAux_balanced {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} (h0 : 0 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) :
        theorem balancedCore_subset_balancedCoreAux {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} :
        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 1a 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) :
        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) :
        theorem nhds_basis_balanced (𝕜 : Type u_1) (E : Type u_2) [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] :
        (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) [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] [RegularSpace E] :
        (nhds 0).HasBasis (fun (s : Set E) => s nhds 0 IsClosed s Balanced 𝕜 s) id