doc-next-gen

Mathlib.Analysis.LocallyConvex.Basic

Module docstring

{"# Local convexity

This file defines absorbent and balanced sets.

An absorbent set is one that \"surrounds\" the origin. The idea is made precise by requiring that any point belongs to all large enough scalings of the set. This is the vector world analog of a topological neighborhood of the origin.

A balanced set is one that is everywhere around the origin. This means that a • s ⊆ s for all a of norm less than 1.

Main declarations

For a module over a normed ring: * Absorbs: A set s absorbs a set t if all large scalings of s contain t. * Absorbent: A set s is absorbent if every point eventually belongs to all large scalings of s. * Balanced: A set s is balanced if a • s ⊆ s for all a of norm less than 1.

References

  • [H. H. Schaefer, Topological Vector Spaces][schaefer1966]

Tags

absorbent, balanced, locally convex, LCTVS "}

Balanced definition
(A : Set E)
Full source 
/-- A set `A` is balanced if `a • A` is contained in `A` whenever `a` has norm at most `1`. -/
def Balanced (A : Set E) :=
  ∀ a : 𝕜, ‖a‖ ≤ 1 → a • A ⊆ A
Balanced set
Informal description
A subset $A$ of a vector space $E$ over a normed field $\mathbb{K}$ is called *balanced* if for every scalar $a \in \mathbb{K}$ with $\|a\| \leq 1$, the scaled set $a \cdot A$ is contained in $A$.
absorbs_iff_norm theorem
: Absorbs 𝕜 A B ↔ ∃ r, ∀ c : 𝕜, r ≤ ‖c‖ → B ⊆ c • A
Full source 
lemma absorbs_iff_norm : AbsorbsAbsorbs 𝕜 A B ↔ ∃ r, ∀ c : 𝕜, r ≤ ‖c‖ → B ⊆ c • A :=
  Filter.atTop_basis.cobounded_of_norm.eventually_iff.trans <| by simp only [true_and]; rfl
Characterization of Absorption via Norm Condition
Informal description
Let $\mathbb{K}$ be a normed field and $E$ a vector space over $\mathbb{K}$. For subsets $A, B \subseteq E$, the set $A$ absorbs $B$ if and only if there exists a real number $r$ such that for every scalar $c \in \mathbb{K}$ with $\|c\| \geq r$, the set $B$ is contained in the scaled set $c \cdot A$.
Absorbs.exists_pos theorem
(h : Absorbs 𝕜 A B) : ∃ r > 0, ∀ c : 𝕜, r ≤ ‖c‖ → B ⊆ c • A
Full source 
lemma Absorbs.exists_pos (h : Absorbs 𝕜 A B) : ∃ r > 0, ∀ c : 𝕜, r ≤ ‖c‖ → B ⊆ c • A :=
  let ⟨r, hr₁, hr⟩ := (Filter.atTop_basis' 1).cobounded_of_norm.eventually_iff.1 h
  ⟨r, one_pos.trans_le hr₁, hr⟩
Existence of Positive Radius for Absorption
Informal description
If a set $A$ absorbs a set $B$ in a vector space over a normed field $\mathbb{K}$, then there exists a positive real number $r > 0$ such that for every scalar $c \in \mathbb{K}$ with $\|c\| \geq r$, the set $B$ is contained in the scaled set $c \cdot A$.
balanced_iff_smul_mem theorem
: Balanced 𝕜 s ↔ ∀ ⦃a : 𝕜⦄, ‖a‖ ≤ 1 → ∀ ⦃x : E⦄, x ∈ s → a • x ∈ s
Full source 
theorem balanced_iff_smul_mem : BalancedBalanced 𝕜 s ↔ ∀ ⦃a : 𝕜⦄, ‖a‖ ≤ 1 → ∀ ⦃x : E⦄, x ∈ s → a • x ∈ s :=
  forall₂_congr fun _a _ha => smul_set_subset_iff
Characterization of Balanced Sets via Scalar Multiplication
Informal description
A subset $s$ of a vector space $E$ over a normed field $\mathbb{K}$ is balanced if and only if for every scalar $a \in \mathbb{K}$ with $\|a\| \leq 1$ and every vector $x \in s$, the scaled vector $a \cdot x$ belongs to $s$.
balanced_iff_closedBall_smul theorem
: Balanced 𝕜 s ↔ Metric.closedBall (0 : 𝕜) 1 • s ⊆ s
Full source 
theorem balanced_iff_closedBall_smul : BalancedBalanced 𝕜 s ↔ Metric.closedBall (0 : 𝕜) 1 • s ⊆ s := by
  simp [balanced_iff_smul_mem, smul_subset_iff]
Characterization of Balanced Sets via Closed Unit Ball Scalar Multiplication
Informal description
A subset $s$ of a vector space $E$ over a normed field $\mathbb{K}$ is balanced if and only if the Minkowski product of the closed unit ball centered at $0$ in $\mathbb{K}$ with $s$ is contained in $s$, i.e., $\overline{B}(0, 1) \cdot s \subseteq s$.
balanced_empty theorem
: Balanced 𝕜 (∅ : Set E)
Full source 
@[simp]
theorem balanced_empty : Balanced 𝕜 (∅ : Set E) := fun _ _ => by rw [smul_set_empty]
Empty Set is Balanced
Informal description
The empty set $\emptyset$ in a vector space $E$ over a normed field $\mathbb{K}$ is balanced.
balanced_univ theorem
: Balanced 𝕜 (univ : Set E)
Full source 
@[simp]
theorem balanced_univ : Balanced 𝕜 (univ : Set E) := fun _a _ha => subset_univ _
Universal Set is Balanced
Informal description
The universal set $E$ in a vector space over a normed field $\mathbb{K}$ is balanced, meaning that for every scalar $a \in \mathbb{K}$ with $\|a\| \leq 1$, the scaled set $a \cdot E$ is contained in $E$.
Balanced.union theorem
(hA : Balanced 𝕜 A) (hB : Balanced 𝕜 B) : Balanced 𝕜 (A ∪ B)
Full source 
theorem Balanced.union (hA : Balanced 𝕜 A) (hB : Balanced 𝕜 B) : Balanced 𝕜 (A ∪ B) := fun _a ha =>
  smul_set_union.subset.trans <| union_subset_union (hA _ ha) <| hB _ ha
Union of Balanced Sets is Balanced
Informal description
Let $A$ and $B$ be balanced subsets of a vector space $E$ over a normed field $\mathbb{K}$. Then the union $A \cup B$ is also balanced.
Balanced.inter theorem
(hA : Balanced 𝕜 A) (hB : Balanced 𝕜 B) : Balanced 𝕜 (A ∩ B)
Full source 
theorem Balanced.inter (hA : Balanced 𝕜 A) (hB : Balanced 𝕜 B) : Balanced 𝕜 (A ∩ B) := fun _a ha =>
  smul_set_inter_subset.trans <| inter_subset_inter (hA _ ha) <| hB _ ha
Intersection of Balanced Sets is Balanced
Informal description
If two subsets $A$ and $B$ of a vector space $E$ over a normed field $\mathbb{K}$ are balanced, then their intersection $A \cap B$ is also balanced.
balanced_iUnion theorem
{f : ι → Set E} (h : ∀ i, Balanced 𝕜 (f i)) : Balanced 𝕜 (⋃ i, f i)
Full source 
theorem balanced_iUnion {f : ι → Set E} (h : ∀ i, Balanced 𝕜 (f i)) : Balanced 𝕜 (⋃ i, f i) :=
  fun _a ha => (smul_set_iUnion _ _).subset.trans <| iUnion_mono fun _ => h _ _ ha
Union of balanced sets is balanced
Informal description
Let $\{f_i\}_{i \in \iota}$ be a family of subsets of a vector space $E$ over a normed field $\mathbb{K}$. If each $f_i$ is balanced, then their union $\bigcup_{i \in \iota} f_i$ is also balanced.
balanced_iUnion₂ theorem
{f : ∀ i, κ i → Set E} (h : ∀ i j, Balanced 𝕜 (f i j)) : Balanced 𝕜 (⋃ (i) (j), f i j)
Full source 
theorem balanced_iUnion₂ {f : ∀ i, κ i → Set E} (h : ∀ i j, Balanced 𝕜 (f i j)) :
    Balanced 𝕜 (⋃ (i) (j), f i j) :=
  balanced_iUnion fun _ => balanced_iUnion <| h _
Union of Double-Indexed Balanced Sets is Balanced
Informal description
Let $E$ be a vector space over a normed field $\mathbb{K}$ and let $\{f_{i,j}\}_{i \in \iota, j \in \kappa_i}$ be a family of subsets of $E$. If for every $i$ and $j$, the subset $f_{i,j}$ is balanced, then the union $\bigcup_{i \in \iota} \bigcup_{j \in \kappa_i} f_{i,j}$ is also balanced.
Balanced.sInter theorem
{S : Set (Set E)} (h : ∀ s ∈ S, Balanced 𝕜 s) : Balanced 𝕜 (⋂₀ S)
Full source 
theorem Balanced.sInter {S : Set (Set E)} (h : ∀ s ∈ S, Balanced 𝕜 s) : Balanced 𝕜 (⋂₀ S) :=
  fun _ _ => (smul_set_sInter_subset ..).trans (fun _ _ => by aesop)
Intersection of Balanced Sets is Balanced
Informal description
Let $E$ be a vector space over a normed field $\mathbb{K}$ and let $S$ be a collection of subsets of $E$. If every set $s \in S$ is balanced, then the intersection $\bigcap S$ is also balanced.
balanced_iInter theorem
{f : ι → Set E} (h : ∀ i, Balanced 𝕜 (f i)) : Balanced 𝕜 (⋂ i, f i)
Full source 
theorem balanced_iInter {f : ι → Set E} (h : ∀ i, Balanced 𝕜 (f i)) : Balanced 𝕜 (⋂ i, f i) :=
  fun _a ha => (smul_set_iInter_subset _ _).trans <| iInter_mono fun _ => h _ _ ha
Intersection of Balanced Sets is Balanced
Informal description
Let $\{f_i\}_{i \in \iota}$ be a family of subsets of a vector space $E$ over a normed field $\mathbb{K}$. If each $f_i$ is balanced, then their intersection $\bigcap_{i \in \iota} f_i$ is also balanced.
balanced_iInter₂ theorem
{f : ∀ i, κ i → Set E} (h : ∀ i j, Balanced 𝕜 (f i j)) : Balanced 𝕜 (⋂ (i) (j), f i j)
Full source 
theorem balanced_iInter₂ {f : ∀ i, κ i → Set E} (h : ∀ i j, Balanced 𝕜 (f i j)) :
    Balanced 𝕜 (⋂ (i) (j), f i j) :=
  balanced_iInter fun _ => balanced_iInter <| h _
Intersection of Doubly-Indexed Balanced Sets is Balanced
Informal description
Let $E$ be a vector space over a normed field $\mathbb{K}$ and let $\{f_{i,j}\}_{i \in \iota, j \in \kappa_i}$ be a family of subsets of $E$. If for every $i$ and $j$, the set $f_{i,j}$ is balanced, then the intersection $\bigcap_{i,j} f_{i,j}$ is also balanced.
Balanced.mulActionHom_preimage theorem
[SMul 𝕜 F] {s : Set F} (hs : Balanced 𝕜 s) (f : E →[𝕜] F) : Balanced 𝕜 (f ⁻¹' s)
Full source 
theorem Balanced.mulActionHom_preimage [SMul 𝕜 F] {s : Set F} (hs : Balanced 𝕜 s)
    (f : E →[𝕜] F) : Balanced 𝕜 (f ⁻¹' s) := fun a ha x ⟨y,⟨hy₁,hy₂⟩⟩ => by
  rw [mem_preimage, ← hy₂, map_smul]
  exact hs a ha (smul_mem_smul_set hy₁)
Preimage of Balanced Set under Equivariant Linear Map is Balanced
Informal description
Let $E$ and $F$ be vector spaces over a normed field $\mathbb{K}$, with $F$ equipped with a scalar multiplication operation. If $s \subseteq F$ is a balanced set and $f : E \to F$ is a $\mathbb{K}$-equivariant linear map, then the preimage $f^{-1}(s)$ is a balanced subset of $E$.
Balanced.smul theorem
(a : 𝕝) (hs : Balanced 𝕜 s) : Balanced 𝕜 (a • s)
Full source 
theorem Balanced.smul (a : 𝕝) (hs : Balanced 𝕜 s) : Balanced 𝕜 (a • s) := fun _b hb =>
  (smul_comm _ _ _).subset.trans <| smul_set_mono <| hs _ hb
Scaled Balanced Set is Balanced
Informal description
Let $E$ be a vector space over a normed field $\mathbb{K}$ and let $s$ be a balanced subset of $E$. Then for any scalar $a \in \mathbb{K}$, the scaled set $a \cdot s$ is also balanced.
Balanced.neg theorem
: Balanced 𝕜 s → Balanced 𝕜 (-s)
Full source 
theorem Balanced.neg : Balanced 𝕜 s → Balanced 𝕜 (-s) :=
  forall₂_imp fun _ _ h => (smul_set_neg _ _).subset.trans <| neg_subset_neg.2 h
Negation Preserves Balanced Sets
Informal description
If a set $s$ in a vector space $E$ over a normed field $\mathbb{K}$ is balanced, then its negation $-s$ is also balanced.
Balanced.neg_mem_iff theorem
[NormOneClass 𝕜] (h : Balanced 𝕜 s) {x : E} : -x ∈ s ↔ x ∈ s
Full source 
theorem Balanced.neg_mem_iff [NormOneClass 𝕜] (h : Balanced 𝕜 s) {x : E} : -x ∈ s-x ∈ s ↔ x ∈ s :=
  ⟨fun hx ↦ by simpa using h.smul_mem (a := -1) (by simp) hx,
    fun hx ↦ by simpa using h.smul_mem (a := -1) (by simp) hx⟩
Characterization of Negation in Balanced Sets
Informal description
Let $E$ be a vector space over a normed field $\mathbb{K}$ with $\|1\| = 1$, and let $s \subseteq E$ be a balanced set. For any $x \in E$, the element $-x$ belongs to $s$ if and only if $x$ belongs to $s$.
Balanced.neg_eq theorem
[NormOneClass 𝕜] (h : Balanced 𝕜 s) : -s = s
Full source 
theorem Balanced.neg_eq [NormOneClass 𝕜] (h : Balanced 𝕜 s) : -s = s :=
  Set.ext fun _ ↦ h.neg_mem_iff
Negation Invariance of Balanced Sets: $-s = s$
Informal description
Let $E$ be a vector space over a normed field $\mathbb{K}$ with $\|1\| = 1$, and let $s \subseteq E$ be a balanced set. Then the negation of $s$ equals $s$, i.e., $-s = s$.
Balanced.add theorem
(hs : Balanced 𝕜 s) (ht : Balanced 𝕜 t) : Balanced 𝕜 (s + t)
Full source 
theorem Balanced.add (hs : Balanced 𝕜 s) (ht : Balanced 𝕜 t) : Balanced 𝕜 (s + t) := fun _a ha =>
  (smul_add _ _ _).subset.trans <| add_subset_add (hs _ ha) <| ht _ ha
Minkowski Sum of Balanced Sets is Balanced
Informal description
Let $E$ be a vector space over a normed field $\mathbb{K}$. If $s$ and $t$ are balanced subsets of $E$, then their Minkowski sum $s + t$ is also balanced.
Balanced.sub theorem
(hs : Balanced 𝕜 s) (ht : Balanced 𝕜 t) : Balanced 𝕜 (s - t)
Full source 
theorem Balanced.sub (hs : Balanced 𝕜 s) (ht : Balanced 𝕜 t) : Balanced 𝕜 (s - t) := by
  simp_rw [sub_eq_add_neg]
  exact hs.add ht.neg
Set Difference of Balanced Sets is Balanced
Informal description
Let $E$ be a vector space over a normed field $\mathbb{K}$. If $s$ and $t$ are balanced subsets of $E$, then their set difference $s - t$ is also balanced.
balanced_zero theorem
: Balanced 𝕜 (0 : Set E)
Full source 
theorem balanced_zero : Balanced 𝕜 (0 : Set E) := fun _a _ha => (smul_zero _).subset
Balancedness of the Zero Set
Informal description
The singleton set containing the zero vector $\{0\}$ in a vector space $E$ over a normed field $\mathbb{K}$ is balanced.
absorbs_iff_eventually_nhdsNE_zero theorem
: Absorbs 𝕜 s t ↔ ∀ᶠ c : 𝕜 in 𝓝[≠] 0, MapsTo (c • ·) t s
Full source 
theorem absorbs_iff_eventually_nhdsNE_zero :
    AbsorbsAbsorbs 𝕜 s t ↔ ∀ᶠ c : 𝕜 in 𝓝[≠] 0, MapsTo (c • ·) t s := by
  rw [absorbs_iff_eventually_cobounded_mapsTo, ← Filter.inv_cobounded₀]; rfl
Absorption Criterion via Punctured Neighborhood of Zero
Informal description
A set $s$ absorbs another set $t$ in a module $E$ over a normed ring $\mathbb{K}$ if and only if for all scalars $c$ in a punctured neighborhood of zero in $\mathbb{K}$, the scaled image of $t$ under $c \cdot (\cdot)$ is contained in $s$. In other words, $s$ absorbs $t$ precisely when there exists a neighborhood of zero (excluding zero itself) such that for all $c$ in this neighborhood, $c \cdot t \subseteq s$.
absorbent_iff_eventually_nhdsNE_zero theorem
: Absorbent 𝕜 s ↔ ∀ x : E, ∀ᶠ c : 𝕜 in 𝓝[≠] 0, c • x ∈ s
Full source 
theorem absorbent_iff_eventually_nhdsNE_zero :
    AbsorbentAbsorbent 𝕜 s ↔ ∀ x : E, ∀ᶠ c : 𝕜 in 𝓝[≠] 0, c • x ∈ s :=
  forall_congr' fun x ↦ by simp only [absorbs_iff_eventually_nhdsNE_zero, mapsTo_singleton]
Characterization of Absorbent Sets via Neighborhoods of Zero
Informal description
A set $s$ in a module $E$ over a normed ring $\mathbb{K}$ is absorbent if and only if for every point $x \in E$, there exists a neighborhood of zero (excluding zero itself) in $\mathbb{K}$ such that for all scalars $c$ in this neighborhood, the scaled point $c \cdot x$ belongs to $s$.
absorbs_iff_eventually_nhds_zero theorem
(h₀ : 0 ∈ s) : Absorbs 𝕜 s t ↔ ∀ᶠ c : 𝕜 in 𝓝 0, MapsTo (c • ·) t s
Full source 
theorem absorbs_iff_eventually_nhds_zero (h₀ : 0 ∈ s) :
    AbsorbsAbsorbs 𝕜 s t ↔ ∀ᶠ c : 𝕜 in 𝓝 0, MapsTo (c • ·) t s := by
  rw [← nhdsNE_sup_pure, Filter.eventually_sup, Filter.eventually_pure,
    ← absorbs_iff_eventually_nhdsNE_zero, and_iff_left]
  intro x _
  simpa only [zero_smul]
Absorption Criterion via Neighborhood of Zero for Sets Containing Origin
Informal description
Let $s$ be a subset of a module $E$ over a normed ring $\mathbb{K}$ containing the origin. Then $s$ absorbs another subset $t$ if and only if for all scalars $c$ in a neighborhood of zero in $\mathbb{K}$, the scaled image of $t$ under $c \cdot (\cdot)$ is contained in $s$. In other words, $s$ absorbs $t$ precisely when there exists a neighborhood of zero such that for all $c$ in this neighborhood, $c \cdot t \subseteq s$.
Balanced.smul_mono theorem
(hs : Balanced 𝕝 s) {a : 𝕝} (h : ‖a‖ ≤ ‖b‖) : a • s ⊆ b • s
Full source 
/-- Scalar multiplication (by possibly different types) of a balanced set is monotone. -/
theorem Balanced.smul_mono (hs : Balanced 𝕝 s) {a : 𝕝} (h : ‖a‖ ≤ ‖b‖) : a • s ⊆ b • s := by
  obtain rfl | hb := eq_or_ne b 0
  · rw [norm_zero, norm_le_zero_iff] at h
    simp only [h, ← image_smul, zero_smul, Subset.rfl]
  · calc
      a • s = b • (b⁻¹ • a) • s := by rw [smul_assoc, smul_inv_smul₀ hb]
      _ ⊆ b • s := smul_set_mono <| hs _ <| by
        rw [norm_smul, norm_inv, ← div_eq_inv_mul]
        exact div_le_one_of_le₀ h (norm_nonneg _)
Monotonicity of Scalar Multiplication for Balanced Sets: $\|a\| \leq \|b\| \implies a \cdot s \subseteq b \cdot s$
Informal description
Let $E$ be a vector space over a normed field $\mathbb{l}$ and let $s \subseteq E$ be a balanced set. For any scalars $a, b \in \mathbb{l}$ with $\|a\| \leq \|b\|$, the scaled set $a \cdot s$ is contained in $b \cdot s$.
Balanced.smul_mem_mono theorem
[SMulCommClass 𝕝 𝕜 E] (hs : Balanced 𝕝 s) {b : 𝕝} (ha : a • x ∈ s) (hba : ‖b‖ ≤ ‖a‖) : b • x ∈ s
Full source 
theorem Balanced.smul_mem_mono [SMulCommClass 𝕝 𝕜 E] (hs : Balanced 𝕝 s) {b : 𝕝}
    (ha : a • x ∈ s) (hba : ‖b‖ ≤ ‖a‖) : b • x ∈ s := by
  rcases eq_or_ne a 0 with rfl | ha₀
  · simp_all
  · calc
      (a⁻¹ • b) • a • x ∈ s := by
        refine hs.smul_mem ?_ ha
        rw [norm_smul, norm_inv, ← div_eq_inv_mul]
        exact div_le_one_of_le₀ hba (norm_nonneg _)
      (a⁻¹ • b) • a • x = b • x := by rw [smul_comm, smul_assoc, smul_inv_smul₀ ha₀]
Monotonicity of Scalar Multiplication in Balanced Sets
Informal description
Let $E$ be a vector space over a normed field $\mathbb{K}$ with an additional scalar multiplication by elements of $\mathbb{l}$ that commutes with the $\mathbb{K}$-action. If $s \subseteq E$ is a balanced set with respect to $\mathbb{l}$, and $a \in \mathbb{l}$ is such that $a \cdot x \in s$ for some $x \in E$, then for any $b \in \mathbb{l}$ with $\|b\| \leq \|a\|$, we have $b \cdot x \in s$.
Balanced.subset_smul theorem
(hs : Balanced 𝕜 s) (ha : 1 ≤ ‖a‖) : s ⊆ a • s
Full source 
theorem Balanced.subset_smul (hs : Balanced 𝕜 s) (ha : 1 ≤ ‖a‖) : s ⊆ a • s := by
  rw [← @norm_one 𝕜] at ha; simpa using hs.smul_mono ha
Inclusion of Balanced Set in Scaled Set for Large Scalars: $\|a\| \geq 1 \implies s \subseteq a \cdot s$
Informal description
Let $E$ be a vector space over a normed field $\mathbb{K}$ and let $s \subseteq E$ be a balanced set. For any scalar $a \in \mathbb{K}$ with $\|a\| \geq 1$, the set $s$ is contained in the scaled set $a \cdot s$.
Balanced.smul_congr theorem
(hs : Balanced 𝕜 s) (h : ‖a‖ = ‖b‖) : a • s = b • s
Full source 
theorem Balanced.smul_congr (hs : Balanced 𝕜 s) (h : ‖a‖ = ‖b‖) : a • s = b • s :=
  (hs.smul_mono h.le).antisymm (hs.smul_mono h.ge)
Equality of Scaled Balanced Sets for Equal Norm Scalars: $\|a\| = \|b\| \implies a \cdot s = b \cdot s$
Informal description
Let $E$ be a vector space over a normed field $\mathbb{K}$ and let $s \subseteq E$ be a balanced set. For any scalars $a, b \in \mathbb{K}$ with $\|a\| = \|b\|$, the scaled sets $a \cdot s$ and $b \cdot s$ are equal.
Balanced.smul_eq theorem
(hs : Balanced 𝕜 s) (ha : ‖a‖ = 1) : a • s = s
Full source 
theorem Balanced.smul_eq (hs : Balanced 𝕜 s) (ha : ‖a‖ = 1) : a • s = s :=
  (hs _ ha.le).antisymm <| hs.subset_smul ha.ge
Invariance of Balanced Set under Unit Norm Scaling: $\|a\| = 1 \implies a \cdot s = s$
Informal description
Let $E$ be a vector space over a normed field $\mathbb{K}$ and let $s \subseteq E$ be a balanced set. For any scalar $a \in \mathbb{K}$ with $\|a\| = 1$, the scaled set $a \cdot s$ is equal to $s$.
Balanced.absorbs_self theorem
(hs : Balanced 𝕜 s) : Absorbs 𝕜 s s
Full source 
/-- A balanced set absorbs itself. -/
theorem Balanced.absorbs_self (hs : Balanced 𝕜 s) : Absorbs 𝕜 s s :=
  .of_norm ⟨1, fun _ => hs.subset_smul⟩
Self-Absorption Property of Balanced Sets
Informal description
Let $E$ be a vector space over a normed field $\mathbb{K}$ and let $s \subseteq E$ be a balanced set. Then $s$ absorbs itself, meaning there exists a positive real number $r > 0$ such that for all scalars $a \in \mathbb{K}$ with $\|a\| \geq r$, we have $s \subseteq a \cdot s$.
Balanced.smul_mem_iff theorem
(hs : Balanced 𝕜 s) (h : ‖a‖ = ‖b‖) : a • x ∈ s ↔ b • x ∈ s
Full source 
theorem Balanced.smul_mem_iff (hs : Balanced 𝕜 s) (h : ‖a‖ = ‖b‖) : a • x ∈ sa • x ∈ s ↔ b • x ∈ s :=
  ⟨(hs.smul_mem_mono · h.ge), (hs.smul_mem_mono · h.le)⟩
Characterization of Membership in Balanced Sets via Scalar Norms
Informal description
Let $E$ be a vector space over a normed field $\mathbb{K}$ and let $s \subseteq E$ be a balanced set. For any two scalars $a, b \in \mathbb{K}$ with $\|a\| = \|b\|$, we have $a \cdot x \in s$ if and only if $b \cdot x \in s$.
absorbent_nhds_zero theorem
(hA : A ∈ 𝓝 (0 : E)) : Absorbent 𝕜 A
Full source 
/-- Every neighbourhood of the origin is absorbent. -/
theorem absorbent_nhds_zero (hA : A ∈ 𝓝 (0 : E)) : Absorbent 𝕜 A :=
  absorbent_iff_inv_smul.2 fun x ↦ Filter.tendsto_inv₀_cobounded.smul tendsto_const_nhds <| by
    rwa [zero_smul]
Neighborhoods of the Origin are Absorbent in Topological Vector Spaces
Informal description
For any neighborhood $A$ of the origin in a topological vector space $E$ over a normed field $\mathbb{K}$, the set $A$ is absorbent. That is, for every point $x \in E$, there exists a positive scalar $r > 0$ such that for all scalars $a \in \mathbb{K}$ with $\|a\| \geq r$, the point $x$ belongs to $a \cdot A$.
Balanced.zero_insert_interior theorem
(hA : Balanced 𝕜 A) : Balanced 𝕜 (insert 0 (interior A))
Full source 
/-- The union of `{0}` with the interior of a balanced set is balanced. -/
theorem Balanced.zero_insert_interior (hA : Balanced 𝕜 A) :
    Balanced 𝕜 (insert 0 (interior A)) := by
  intro a ha
  obtain rfl | h := eq_or_ne a 0
  · rw [zero_smul_set]
    exacts [subset_union_left, ⟨0, Or.inl rfl⟩]
  · rw [← image_smul, image_insert_eq, smul_zero]
    apply insert_subset_insert
    exact ((isOpenMap_smul₀ h).mapsTo_interior <| hA.smul_mem ha).image_subset
Balancedness of Zero Union Interior of a Balanced Set
Informal description
Let $E$ be a vector space over a normed field $\mathbb{K}$ and let $A \subseteq E$ be a balanced set. Then the set $\{0\} \cup \text{interior}(A)$ is also balanced.
Balanced.interior theorem
(hA : Balanced 𝕜 A) (h : (0 : E) ∈ interior A) : Balanced 𝕜 (interior A)
Full source 
/-- The interior of a balanced set is balanced if it contains the origin. -/
protected theorem Balanced.interior (hA : Balanced 𝕜 A) (h : (0 : E) ∈ interior A) :
    Balanced 𝕜 (interior A) := by
  rw [← insert_eq_self.2 h]
  exact hA.zero_insert_interior
Interior of a Balanced Set Containing the Origin is Balanced
Informal description
Let $E$ be a vector space over a normed field $\mathbb{K}$ and let $A \subseteq E$ be a balanced set. If the origin $0$ belongs to the interior of $A$, then the interior of $A$ is also balanced.
Balanced.convexHull theorem
(hs : Balanced 𝕜 s) : Balanced 𝕜 (convexHull ℝ s)
Full source 
protected theorem Balanced.convexHull (hs : Balanced 𝕜 s) : Balanced 𝕜 (convexHull ℝ s) := by
  suffices Convex ℝ { x | ∀ a : 𝕜, ‖a‖ ≤ 1 → a • x ∈ convexHull ℝ s } by
    rw [balanced_iff_smul_mem] at hs ⊢
    refine fun a ha x hx => convexHull_min ?_ this hx a ha
    exact fun y hy a ha => subset_convexHull ℝ s (hs ha hy)
  intro x hx y hy u v hu hv huv a ha
  simp only [smul_add, ← smul_comm]
  exact convex_convexHull ℝ s (hx a ha) (hy a ha) hu hv huv
Convex Hull of a Balanced Set is Balanced
Informal description
If $s$ is a balanced subset of a vector space $E$ over a normed field $\mathbb{K}$, then the convex hull of $s$ over $\mathbb{R}$ is also balanced over $\mathbb{K}$.
balanced_iff_neg_mem theorem
(hs : Convex ℝ s) : Balanced ℝ s ↔ ∀ ⦃x⦄, x ∈ s → -x ∈ s
Full source 
theorem balanced_iff_neg_mem (hs : Convex ℝ s) : BalancedBalanced ℝ s ↔ ∀ ⦃x⦄, x ∈ s → -x ∈ s := by
  refine ⟨fun h x => h.neg_mem_iff.2, fun h a ha => smul_set_subset_iff.2 fun x hx => ?_⟩
  rw [Real.norm_eq_abs, abs_le] at ha
  rw [show a = -((1 - a) / 2) + (a - -1) / 2 by ring, add_smul, neg_smul, ← smul_neg]
  exact hs (h hx) hx (div_nonneg (sub_nonneg_of_le ha.2) zero_le_two)
    (div_nonneg (sub_nonneg_of_le ha.1) zero_le_two) (by ring)
Characterization of Balanced Sets via Negation in Convex Sets
Informal description
Let $s$ be a convex subset of a real vector space. Then $s$ is balanced if and only if for every $x \in s$, the negation $-x$ also belongs to $s$.