Mathlib.Analysis.LocallyConvex.BalancedCoreHull

balancedCore definition

(s : Set E)

Full source

/-- The largest balanced subset of `s`. -/
def balancedCore (s : Set E) :=
  ⋃₀ { t : Set E | Balanced 𝕜 t ∧ t ⊆ s }

Balanced core of a set

Informal description

The balanced core of a set $ s $ in a vector space $ E $ over a normed field $ \mathbb{K} $ is the largest balanced subset of $ s $, defined as the union of all balanced subsets $ t $ of $ s $.

balancedCoreAux definition

(s : Set E)

Full source

/-- Helper definition to prove `balanced_core_eq_iInter` -/
def balancedCoreAux (s : Set E) :=
  ⋂ (r : 𝕜) (_ : 1 ≤ ‖r‖), r • s

Auxiliary balanced core of a set

Informal description

For a set $ s $ in a vector space $ E $ over a normed field $ \mathbb{K} $, the auxiliary balanced core of $ s $ is defined as the intersection of all scaled sets $ r \cdot s $ where the scalar $ r \in \mathbb{K} $ satisfies $ \|r\| \geq 1 $.

balancedHull definition

(s : Set E)

Full source

/-- The smallest balanced superset of `s`. -/
def balancedHull (s : Set E) :=
  ⋃ (r : 𝕜) (_ : ‖r‖ ≤ 1), r • s

Balanced hull of a set

Informal description

The balanced hull of a set $ s $ in a vector space $ E $ over a normed field $ \mathbb{K} $ is the smallest balanced superset of $ s $, defined as the union of all scalar multiples $ r \cdot s $ where $ r \in \mathbb{K} $ satisfies $ \|r\| \leq 1 $.

balancedCore_subset theorem

(s : Set E) : balancedCore 𝕜 s ⊆ s

Full source

theorem balancedCore_subset (s : Set E) : balancedCorebalancedCore 𝕜 s ⊆ s :=
  sUnion_subset fun _ ht => ht.2

Balanced core is contained in the original set

Informal description

For any set $s$ in a vector space $E$ over a normed field $\mathbb{K}$, the balanced core of $s$ is a subset of $s$.

balancedCore_empty theorem

: balancedCore 𝕜 (∅ : Set E) = ∅

Full source

theorem balancedCore_empty : balancedCore 𝕜 (∅ : Set E) = ∅ :=
  eq_empty_of_subset_empty (balancedCore_subset _)

Balanced Core of Empty Set is Empty

Informal description

The balanced core of the empty set in a vector space $E$ over a normed field $\mathbb{K}$ is the empty set, i.e., $\text{balancedCore}_{\mathbb{K}}(\emptyset) = \emptyset$.

mem_balancedCore_iff theorem

: x ∈ balancedCore 𝕜 s ↔ ∃ t, Balanced 𝕜 t ∧ t ⊆ s ∧ x ∈ t

Full source

theorem mem_balancedCore_iff : x ∈ balancedCore 𝕜 sx ∈ balancedCore 𝕜 s ↔ ∃ t, Balanced 𝕜 t ∧ t ⊆ s ∧ x ∈ t := by
  simp_rw [balancedCore, mem_sUnion, mem_setOf_eq, and_assoc]

Characterization of Membership in the Balanced Core

Informal description

An element $x$ belongs to the balanced core of a set $s$ in a vector space $E$ over a normed field $\mathbb{K}$ if and only if there exists a balanced subset $t$ of $s$ such that $x \in t$.

smul_balancedCore_subset theorem

(s : Set E) {a : 𝕜} (ha : ‖a‖ ≤ 1) : a • balancedCore 𝕜 s ⊆ balancedCore 𝕜 s

Full source

theorem smul_balancedCore_subset (s : Set E) {a : 𝕜} (ha : ‖a‖ ≤ 1) :
    a • balancedCore 𝕜 s ⊆ balancedCore 𝕜 s := by
  rintro x ⟨y, hy, rfl⟩
  rw [mem_balancedCore_iff] at hy
  rcases hy with ⟨t, ht1, ht2, hy⟩
  exact ⟨t, ⟨ht1, ht2⟩, ht1 a ha (smul_mem_smul_set hy)⟩

Scalar Multiplication Preserves Balanced Core

Informal description

Let $E$ be a vector space over a normed field $\mathbb{K}$. For any subset $s \subseteq E$ and any scalar $a \in \mathbb{K}$ with $\|a\| \leq 1$, the scaled set $a \cdot \text{balancedCore}_{\mathbb{K}}(s)$ is contained in $\text{balancedCore}_{\mathbb{K}}(s)$.

balancedCore_balanced theorem

(s : Set E) : Balanced 𝕜 (balancedCore 𝕜 s)

Full source

theorem balancedCore_balanced (s : Set E) : Balanced 𝕜 (balancedCore 𝕜 s) := fun _ =>
  smul_balancedCore_subset s

Balanced Core is Balanced

Informal description

For any subset $s$ of a vector space $E$ over a normed field $\mathbb{K}$, the balanced core $\text{balancedCore}_{\mathbb{K}}(s)$ is a balanced set. That is, for every scalar $a \in \mathbb{K}$ with $\|a\| \leq 1$, we have $a \cdot \text{balancedCore}_{\mathbb{K}}(s) \subseteq \text{balancedCore}_{\mathbb{K}}(s)$.

Balanced.subset_balancedCore_of_subset theorem

(hs : Balanced 𝕜 s) (h : s ⊆ t) : s ⊆ balancedCore 𝕜 t

Full source

/-- The balanced core of `t` is maximal in the sense that it contains any balanced subset
`s` of `t`. -/
theorem Balanced.subset_balancedCore_of_subset (hs : Balanced 𝕜 s) (h : s ⊆ t) :
    s ⊆ balancedCore 𝕜 t :=
  subset_sUnion_of_mem ⟨hs, h⟩

Balanced Sets are Contained in Their Balanced Core

Informal description

Let $E$ be a vector space over a normed field $\mathbb{K}$. If $s$ is a balanced subset of $E$ and $s \subseteq t$ for some set $t \subseteq E$, then $s$ is contained in the balanced core of $t$.

Balanced.balancedCore_eq theorem

(h : Balanced 𝕜 s) : balancedCore 𝕜 s = s

Full source

lemma Balanced.balancedCore_eq (h : Balanced 𝕜 s) : balancedCore 𝕜 s = s :=
  le_antisymm (balancedCore_subset _) (h.subset_balancedCore_of_subset (subset_refl _))

Balanced Core of a Balanced Set Equals Itself

Informal description

If a set $s$ in a vector space $E$ over a normed field $\mathbb{K}$ is balanced, then its balanced core is equal to $s$ itself, i.e., $\text{balancedCore}_{\mathbb{K}}(s) = s$.

mem_balancedCoreAux_iff theorem

: x ∈ balancedCoreAux 𝕜 s ↔ ∀ r : 𝕜, 1 ≤ ‖r‖ → x ∈ r • s

Full source

theorem mem_balancedCoreAux_iff : x ∈ balancedCoreAux 𝕜 sx ∈ balancedCoreAux 𝕜 s ↔ ∀ r : 𝕜, 1 ≤ ‖r‖ → x ∈ r • s :=
  mem_iInter₂

Characterization of Membership in Auxiliary Balanced Core

Informal description

An element $x$ belongs to the auxiliary balanced core of a set $s$ in a vector space $E$ over a normed field $\mathbb{K}$ if and only if for every scalar $r \in \mathbb{K}$ with $\|r\| \geq 1$, the element $x$ is in the scaled set $r \cdot s$.

mem_balancedHull_iff theorem

: x ∈ balancedHull 𝕜 s ↔ ∃ r : 𝕜, ‖r‖ ≤ 1 ∧ x ∈ r • s

Full source

theorem mem_balancedHull_iff : x ∈ balancedHull 𝕜 sx ∈ balancedHull 𝕜 s ↔ ∃ r : 𝕜, ‖r‖ ≤ 1 ∧ x ∈ r • s := by
  simp [balancedHull]

Characterization of Balanced Hull Membership: $x \in \text{balancedHull}_{\mathbb{K}}(s) \leftrightarrow \exists r \in \mathbb{K}, \|r\| \leq 1 \land x \in r \cdot s$

Informal description

An element $x$ belongs to the balanced hull of a set $s$ in a vector space $E$ over a normed field $\mathbb{K}$ if and only if there exists a scalar $r \in \mathbb{K}$ with $\|r\| \leq 1$ such that $x \in r \cdot s$.

Balanced.balancedHull_subset_of_subset theorem

(ht : Balanced 𝕜 t) (h : s ⊆ t) : balancedHull 𝕜 s ⊆ t

Full source

/-- The balanced hull of `s` is minimal in the sense that it is contained in any balanced superset
`t` of `s`. -/
theorem Balanced.balancedHull_subset_of_subset (ht : Balanced 𝕜 t) (h : s ⊆ t) :
    balancedHullbalancedHull 𝕜 s ⊆ t := by
  intros x hx
  obtain ⟨r, hr, y, hy, rfl⟩ := mem_balancedHull_iff.1 hx
  exact ht.smul_mem hr (h hy)

Minimality of Balanced Hull: $\text{balancedHull}_{\mathbb{K}}(s) \subseteq t$ for any balanced superset $t$ of $s$

Informal description

Let $E$ be a vector space over a normed field $\mathbb{K}$. If $t$ is a balanced subset of $E$ containing a subset $s$, then the balanced hull of $s$ is contained in $t$.

balancedHull_mono theorem

(hst : s ⊆ t) : balancedHull 𝕜 s ⊆ balancedHull 𝕜 t

Full source

@[mono, gcongr]
theorem balancedHull_mono (hst : s ⊆ t) : balancedHullbalancedHull 𝕜 s ⊆ balancedHull 𝕜 t := by
  intro x hx
  rw [mem_balancedHull_iff] at *
  obtain ⟨r, hr₁, hr₂⟩ := hx
  use r
  exact ⟨hr₁, smul_set_mono hst hr₂⟩

Monotonicity of Balanced Hull: $s \subseteq t \Rightarrow \text{balancedHull}_{\mathbb{K}}(s) \subseteq \text{balancedHull}_{\mathbb{K}}(t)$

Informal description

For any two sets $s$ and $t$ in a vector space $E$ over a normed field $\mathbb{K}$, if $s \subseteq t$, then the balanced hull of $s$ is contained in the balanced hull of $t$, i.e., $\text{balancedHull}_{\mathbb{K}}(s) \subseteq \text{balancedHull}_{\mathbb{K}}(t)$.

balancedCore_zero_mem theorem

(hs : (0 : E) ∈ s) : (0 : E) ∈ balancedCore 𝕜 s

Full source

theorem balancedCore_zero_mem (hs : (0 : E) ∈ s) : (0 : E) ∈ balancedCore 𝕜 s :=
  mem_balancedCore_iff.2 ⟨0, balanced_zero, zero_subset.2 hs, Set.zero_mem_zero⟩

Zero Vector Belongs to Balanced Core if it Belongs to the Set

Informal description

If the zero vector $0$ belongs to a set $s$ in a vector space $E$ over a normed field $\mathbb{K}$, then $0$ also belongs to the balanced core of $s$.

balancedCore_nonempty_iff theorem

: (balancedCore 𝕜 s).Nonempty ↔ (0 : E) ∈ s

Full source

theorem balancedCore_nonempty_iff : (balancedCore 𝕜 s).Nonempty ↔ (0 : E) ∈ s :=
  ⟨fun h => zero_subset.1 <| (zero_smul_set h).superset.trans <|
    (balancedCore_balanced s (0 : 𝕜) <| norm_zero.trans_le zero_le_one).trans <|
      balancedCore_subset _,
    fun h => ⟨0, balancedCore_zero_mem h⟩⟩

Nonemptiness of Balanced Core Equivalent to Zero Vector in Set

Informal description

The balanced core of a set $s$ in a vector space $E$ over a normed field $\mathbb{K}$ is nonempty if and only if the zero vector $0$ belongs to $s$.

Balanced.zero_mem theorem

(hs : Balanced 𝕜 s) (hs_nonempty : s.Nonempty) : (0 : E) ∈ s

Full source

lemma Balanced.zero_mem (hs : Balanced 𝕜 s) (hs_nonempty : s.Nonempty) : (0 : E) ∈ s := by
  rw [← hs.balancedCore_eq] at hs_nonempty
  exact balancedCore_nonempty_iff.mp hs_nonempty

Zero Vector Belongs to Nonempty Balanced Sets

Informal description

For any nonempty balanced subset $s$ of a vector space $E$ over a normed field $\mathbb{K}$, the zero vector $0$ is an element of $s$.

subset_balancedHull theorem

[NormOneClass 𝕜] {s : Set E} : s ⊆ balancedHull 𝕜 s

Full source

theorem subset_balancedHull [NormOneClass 𝕜] {s : Set E} : s ⊆ balancedHull 𝕜 s := fun _ hx =>
  mem_balancedHull_iff.2 ⟨1, norm_one.le, _, hx, one_smul _ _⟩

Inclusion of Set in its Balanced Hull

Informal description

For any subset $s$ of a vector space $E$ over a normed field $\mathbb{K}$ where $\mathbb{K}$ has norm one class (i.e., $\|1\| = 1$), the set $s$ is contained in its balanced hull $\text{balancedHull}_{\mathbb{K}}(s)$. In other words, $s \subseteq \bigcup_{\|r\| \leq 1} r \cdot s$.

balancedHull.balanced theorem

(s : Set E) : Balanced 𝕜 (balancedHull 𝕜 s)

Full source

theorem balancedHull.balanced (s : Set E) : Balanced 𝕜 (balancedHull 𝕜 s) := by
  intro a ha
  simp_rw [balancedHull, smul_set_iUnion₂, subset_def, mem_iUnion₂]
  rintro x ⟨r, hr, hx⟩
  rw [← smul_assoc] at hx
  exact ⟨a • r, (norm_mul_le _ _).trans (mul_le_one₀ ha (norm_nonneg r) hr), hx⟩

Balanced Property of the Balanced Hull

Informal description

For any subset $s$ of a vector space $E$ over a normed field $\mathbb{K}$, the balanced hull of $s$ is a balanced set. That is, for every scalar $a \in \mathbb{K}$ with $\|a\| \leq 1$, the scaled set $a \cdot \text{balancedHull}(s)$ is contained in $\text{balancedHull}(s)$.

balancedHull_add_subset theorem

[NormOneClass 𝕜] {t : Set E} : balancedHull 𝕜 (s + t) ⊆ balancedHull 𝕜 s + balancedHull 𝕜 t

Full source

theorem balancedHull_add_subset [NormOneClass 𝕜] {t : Set E} :
    balancedHullbalancedHull 𝕜 (s + t) ⊆ balancedHull 𝕜 s + balancedHull 𝕜 t :=
  balancedHull_subset_of_subset (add (balancedHull.balanced _) (balancedHull.balanced _))
    (add_subset_add (subset_balancedHull _) (subset_balancedHull _))

Inclusion of Balanced Hull of Sum in Sum of Balanced Hulls

Informal description

Let $E$ be a vector space over a normed field $\mathbb{K}$ with $\|1\| = 1$. For any subsets $s$ and $t$ of $E$, the balanced hull of their Minkowski sum $s + t$ is contained in the Minkowski sum of their balanced hulls, i.e., \[ \text{balancedHull}_{\mathbb{K}}(s + t) \subseteq \text{balancedHull}_{\mathbb{K}}(s) + \text{balancedHull}_{\mathbb{K}}(t). \]

balancedCoreAux_empty theorem

: balancedCoreAux 𝕜 (∅ : Set E) = ∅

Full source

@[simp]
theorem balancedCoreAux_empty : balancedCoreAux 𝕜 (∅ : Set E) = ∅ := by
  simp_rw [balancedCoreAux, iInter₂_eq_empty_iff, smul_set_empty]
  exact fun _ => ⟨1, norm_one.ge, not_mem_empty _⟩

Auxiliary Balanced Core of Empty Set is Empty

Informal description

The auxiliary balanced core of the empty set in a vector space $E$ over a normed field $\mathbb{K}$ is the empty set, i.e., $\text{balancedCoreAux}_\mathbb{K}(\emptyset) = \emptyset$.

balancedCoreAux_subset theorem

(s : Set E) : balancedCoreAux 𝕜 s ⊆ s

Full source

theorem balancedCoreAux_subset (s : Set E) : balancedCoreAuxbalancedCoreAux 𝕜 s ⊆ s := fun x hx => by
  simpa only [one_smul] using mem_balancedCoreAux_iff.1 hx 1 norm_one.ge

Auxiliary Balanced Core is Subset of Original Set

Informal description

For any set $s$ in a vector space $E$ over a normed field $\mathbb{K}$, the auxiliary balanced core of $s$ is a subset of $s$, i.e., $\text{balancedCoreAux}_\mathbb{K}(s) \subseteq s$.

balancedCoreAux_balanced theorem

(h0 : (0 : E) ∈ balancedCoreAux 𝕜 s) : Balanced 𝕜 (balancedCoreAux 𝕜 s)

Full source

theorem balancedCoreAux_balanced (h0 : (0 : E) ∈ balancedCoreAux 𝕜 s) :
    Balanced 𝕜 (balancedCoreAux 𝕜 s) := by
  rintro a ha x ⟨y, hy, rfl⟩
  obtain rfl | h := eq_or_ne a 0
  · simp_rw [zero_smul, h0]
  rw [mem_balancedCoreAux_iff] at hy ⊢
  intro r hr
  have h'' : 1 ≤ ‖a⁻¹ • r‖ := by
    rw [norm_smul, norm_inv]
    exact one_le_mul_of_one_le_of_one_le ((one_le_inv₀ (norm_pos_iff.mpr h)).2 ha) hr
  have h' := hy (a⁻¹ • r) h''
  rwa [smul_assoc, mem_inv_smul_set_iff₀ h] at h'

Auxiliary Balanced Core is Balanced When Containing Zero

Informal description

Let $E$ be a vector space over a normed field $\mathbb{K}$ and $s$ a subset of $E$. If the zero vector $0$ belongs to the auxiliary balanced core of $s$, then this auxiliary balanced core is a balanced set in $E$.

balancedCoreAux_maximal theorem

(h : t ⊆ s) (ht : Balanced 𝕜 t) : t ⊆ balancedCoreAux 𝕜 s

Full source

theorem balancedCoreAux_maximal (h : t ⊆ s) (ht : Balanced 𝕜 t) : t ⊆ balancedCoreAux 𝕜 s := by
  refine fun x hx => mem_balancedCoreAux_iff.2 fun r hr => ?_
  rw [mem_smul_set_iff_inv_smul_mem₀ (norm_pos_iff.mp <| zero_lt_one.trans_le hr)]
  refine h (ht.smul_mem ?_ hx)
  rw [norm_inv]
  exact inv_le_one_of_one_le₀ hr

Maximality of Auxiliary Balanced Core for Balanced Subsets

Informal description

Let $E$ be a vector space over a normed field $\mathbb{K}$, and let $s$ and $t$ be subsets of $E$. If $t$ is a balanced subset of $s$ (i.e., $t \subseteq s$ and $t$ is balanced), then $t$ is contained in the auxiliary balanced core of $s$.

balancedCore_subset_balancedCoreAux theorem

: balancedCore 𝕜 s ⊆ balancedCoreAux 𝕜 s

Full source

theorem balancedCore_subset_balancedCoreAux : balancedCorebalancedCore 𝕜 s ⊆ balancedCoreAux 𝕜 s :=
  balancedCoreAux_maximal (balancedCore_subset s) (balancedCore_balanced s)

Inclusion of Balanced Core in Auxiliary Balanced Core

Informal description

For any subset $s$ of a vector space $E$ over a normed field $\mathbb{K}$, the balanced core of $s$ is contained in its auxiliary balanced core, i.e., $\text{balancedCore}_{\mathbb{K}}(s) \subseteq \text{balancedCoreAux}_{\mathbb{K}}(s)$.

balancedCore_eq_iInter theorem

(hs : (0 : E) ∈ s) : balancedCore 𝕜 s = ⋂ (r : 𝕜) (_ : 1 ≤ ‖r‖), r • s

Full source

theorem balancedCore_eq_iInter (hs : (0 : E) ∈ s) :
    balancedCore 𝕜 s = ⋂ (r : 𝕜) (_ : 1 ≤ ‖r‖), r • s := by
  refine balancedCore_subset_balancedCoreAux.antisymm ?_
  refine (balancedCoreAux_balanced ?_).subset_balancedCore_of_subset (balancedCoreAux_subset s)
  exact balancedCore_subset_balancedCoreAux (balancedCore_zero_mem hs)

Characterization of Balanced Core as Intersection of Scaled Sets

Informal description

For a subset $s$ of a vector space $E$ over a normed field $\mathbb{K}$ containing the zero vector, the balanced core of $s$ is equal to the intersection of all scaled sets $r \cdot s$ where the scalar $r \in \mathbb{K}$ satisfies $\|r\| \geq 1$. That is, \[ \text{balancedCore}_\mathbb{K}(s) = \bigcap_{\substack{r \in \mathbb{K} \\ \|r\| \geq 1}} r \cdot s. \]

subset_balancedCore theorem

(ht : (0 : E) ∈ t) (hst : ∀ a : 𝕜, ‖a‖ ≤ 1 → a • s ⊆ t) : s ⊆ balancedCore 𝕜 t

Full source

theorem subset_balancedCore (ht : (0 : E) ∈ t) (hst : ∀ a : 𝕜, ‖a‖ ≤ 1 → a • s ⊆ t) :
    s ⊆ balancedCore 𝕜 t := by
  rw [balancedCore_eq_iInter ht]
  refine subset_iInter₂ fun a ha ↦ ?_
  rw [subset_smul_set_iff₀ (norm_pos_iff.mp <| zero_lt_one.trans_le ha)]
  apply hst
  rw [norm_inv]
  exact inv_le_one_of_one_le₀ ha

Inclusion in Balanced Core under Scalar Multiplication Condition

Informal description

Let $E$ be a vector space over a normed field $\mathbb{K}$, and let $s, t$ be subsets of $E$ such that $0 \in t$. If for every scalar $a \in \mathbb{K}$ with $\|a\| \leq 1$, the scaled set $a \cdot s$ is contained in $t$, then $s$ is contained in the balanced core of $t$.

IsClosed.balancedCore theorem

(hU : IsClosed U) : IsClosed (balancedCore 𝕜 U)

Full source

protected theorem IsClosed.balancedCore (hU : IsClosed U) : IsClosed (balancedCore 𝕜 U) := by
  by_cases h : (0 : E) ∈ U
  · rw [balancedCore_eq_iInter h]
    refine isClosed_iInter fun a => ?_
    refine isClosed_iInter fun ha => ?_
    have ha' := lt_of_lt_of_le zero_lt_one ha
    rw [norm_pos_iff] at ha'
    exact isClosedMap_smul_of_ne_zero ha' U hU
  · have : balancedCore 𝕜 U = ∅ := by
      contrapose! h
      exact balancedCore_nonempty_iff.mp h
    rw [this]
    exact isClosed_empty

Closedness of the Balanced Core of a Closed Set

Informal description

For any closed subset $U$ of a topological vector space $E$ over a normed field $\mathbb{K}$, the balanced core of $U$ is also closed.

balancedCore_mem_nhds_zero theorem

(hU : U ∈ 𝓝 (0 : E)) : balancedCore 𝕜 U ∈ 𝓝 (0 : E)

Full source

theorem balancedCore_mem_nhds_zero (hU : U ∈ 𝓝 (0 : E)) : balancedCorebalancedCore 𝕜 U ∈ 𝓝 (0 : E) := by
  -- Getting neighborhoods of the origin for `0 : 𝕜` and `0 : E`
  obtain ⟨r, V, hr, hV, hrVU⟩ : ∃ (r : ℝ) (V : Set E),
      0 < r ∧ V ∈ 𝓝 (0 : E) ∧ ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U := by
    have h : Filter.Tendsto (fun x : 𝕜 × E => x.fst • x.snd) (𝓝 (0, 0)) (𝓝 0) :=
      continuous_smul.tendsto' (0, 0) _ (smul_zero _)
    simpa only [← Prod.exists', ← Prod.forall', ← and_imp, ← and_assoc, exists_prop] using
      h.basis_left (NormedAddCommGroup.nhds_zero_basis_norm_lt.prod_nhds (𝓝 _).basis_sets) U hU
  obtain ⟨y, hyr, hy₀⟩ : ∃ y : 𝕜, ‖y‖ < r ∧ y ≠ 0 :=
    Filter.nonempty_of_mem <|
      (nhdsWithin_hasBasis NormedAddCommGroup.nhds_zero_basis_norm_lt {0}{0}ᶜ).mem_of_mem hr
  have : y • V ∈ 𝓝 (0 : E) := (set_smul_mem_nhds_zero_iff hy₀).mpr hV
  -- It remains to show that `y • V ⊆ balancedCore 𝕜 U`
  refine Filter.mem_of_superset this (subset_balancedCore (mem_of_mem_nhds hU) fun a ha => ?_)
  rw [smul_smul]
  rintro _ ⟨z, hz, rfl⟩
  refine hrVU _ _ ?_ hz
  rw [norm_mul, ← one_mul r]
  exact mul_lt_mul' ha hyr (norm_nonneg y) one_pos

Balanced Core of a Zero Neighborhood is a Zero Neighborhood

Informal description

For any neighborhood $U$ of the zero vector in a topological vector space $E$ over a normed field $\mathbb{K}$, the balanced core of $U$ is also a neighborhood of zero.

nhds_basis_balanced theorem

: (𝓝 (0 : E)).HasBasis (fun s : Set E => s ∈ 𝓝 (0 : E) ∧ Balanced 𝕜 s) id

Full source

theorem nhds_basis_balanced :
    (𝓝 (0 : E)).HasBasis (fun s : Set E => s ∈ 𝓝 (0 : E)s ∈ 𝓝 (0 : E) ∧ Balanced 𝕜 s) id :=
  Filter.hasBasis_self.mpr fun s hs =>
    ⟨balancedCore 𝕜 s, balancedCore_mem_nhds_zero hs, balancedCore_balanced s,
      balancedCore_subset s⟩

Balanced Neighborhood Basis at Zero

Informal description

The neighborhood filter of the zero vector in a topological vector space $E$ over a normed field $\mathbb{K}$ has a basis consisting of balanced neighborhoods of zero. That is, for any neighborhood $U$ of $0 \in E$, there exists a balanced neighborhood $V \subseteq U$ of $0$.

nhds_basis_closed_balanced theorem

[RegularSpace E] : (𝓝 (0 : E)).HasBasis (fun s : Set E => s ∈ 𝓝 (0 : E) ∧ IsClosed s ∧ Balanced 𝕜 s) id

Full source

theorem nhds_basis_closed_balanced [RegularSpace E] :
    (𝓝 (0 : E)).HasBasis (fun s : Set E => s ∈ 𝓝 (0 : E)s ∈ 𝓝 (0 : E) ∧ IsClosed s ∧ Balanced 𝕜 s) id := by
  refine
    (closed_nhds_basis 0).to_hasBasis (fun s hs => ?_) fun s hs => ⟨s, ⟨hs.1, hs.2.1⟩, rfl.subset⟩
  refine ⟨balancedCore 𝕜 s, ⟨balancedCore_mem_nhds_zero hs.1, ?_⟩, balancedCore_subset s⟩
  exact ⟨hs.2.balancedCore, balancedCore_balanced s⟩

Closed Balanced Sets Form a Neighborhood Basis at Zero in Regular Spaces

Informal description

In a regular topological vector space $E$ over a normed field $\mathbb{K}$, the neighborhood filter $\mathcal{N}(0)$ of the zero vector has a basis consisting of closed, balanced sets. That is, for any neighborhood $U$ of $0$, there exists a closed, balanced neighborhood $V$ of $0$ such that $V \subseteq U$.

Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Main definitions

Main statements

Implementation details

References

Tags