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.

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

    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.

      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, 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 : 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 ≤ ‖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 x, 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} :
        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) :
        balancedCoreAux 𝕜 s ⊆ s
        theorem balancedCoreAux_balanced {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} (h0 : 0 ∈ balancedCoreAux 𝕜 s) :
        Balanced 𝕜 (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) :
        t ⊆ balancedCoreAux 𝕜 s
        theorem balancedCore_subset_balancedCoreAux {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} :
        balancedCore 𝕜 s ⊆ balancedCoreAux 𝕜 s
        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‖ ≤ 1 → a • 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) :
        IsClosed (balancedCore 𝕜 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) :
        balancedCore 𝕜 U ∈ nhds 0
        theorem nhds_basis_balanced (𝕜 : Type u_1) (E : Type u_2) [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] :
        Filter.HasBasis (nhds 0) (fun s => 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] :
        Filter.HasBasis (nhds 0) (fun s => s ∈ nhds 0 ∧ IsClosed s ∧ Balanced 𝕜 s) id