Mathlib.Analysis.LocallyConvex.WithSeminorms

SeminormFamily abbrev

Full source

/-- An abbreviation for indexed families of seminorms. This is mainly to allow for dot-notation. -/
abbrev SeminormFamily :=
  ι → Seminorm 𝕜 E

Indexed Family of Seminorms

Informal description

An abbreviation for indexed families of seminorms on a vector space $E$ over a field $\mathbb{K}$, where $\iota$ is the indexing set. This notation is primarily introduced to enable dot-notation for operations on such families.

SeminormFamily.basisSets definition

(p : SeminormFamily 𝕜 E ι) : Set (Set E)

Full source

/-- The sets of a filter basis for the neighborhood filter of 0. -/
def basisSets (p : SeminormFamily 𝕜 E ι) : Set (Set E) :=
  ⋃ (s : Finset ι) (r) (_ : 0 < r), singleton (ball (s.sup p) (0 : E) r)

Basis sets of seminorm balls centered at 0

Informal description

The collection of all open balls centered at 0 with respect to the seminorms in the family $ p $, where each ball is defined by a finite subset of seminorms $ s \subseteq \iota $ and a positive radius $ r > 0 $. Specifically, a set $ U \subseteq E $ belongs to `basisSets` if and only if there exists a finite subset $ s \subseteq \iota $ and a positive real number $ r > 0 $ such that $ U $ is the ball $ \{ x \in E \mid \sup_{i \in s} p_i(x) < r \} $ centered at 0.

SeminormFamily.basisSets_iff theorem

{U : Set E} : U ∈ p.basisSets ↔ ∃ (i : Finset ι) (r : ℝ), 0 < r ∧ U = ball (i.sup p) 0 r

Full source

theorem basisSets_iff {U : Set E} :
    U ∈ p.basisSetsU ∈ p.basisSets ↔ ∃ (i : Finset ι) (r : ℝ), 0 < r ∧ U = ball (i.sup p) 0 r := by
  simp only [basisSets, mem_iUnion, exists_prop, mem_singleton_iff]

Characterization of Basis Sets in Seminorm Family

Informal description

A subset $U$ of a vector space $E$ belongs to the basis sets of the seminorm family $p$ if and only if there exists a finite subset $i \subseteq \iota$ and a positive real number $r > 0$ such that $U$ is the open ball centered at $0$ with radius $r$ with respect to the seminorm $\sup_{j \in i} p_j$.

SeminormFamily.basisSets_mem theorem

(i : Finset ι) {r : ℝ} (hr : 0 < r) : (i.sup p).ball 0 r ∈ p.basisSets

Full source

theorem basisSets_mem (i : Finset ι) {r : ℝ} (hr : 0 < r) : (i.sup p).ball 0 r ∈ p.basisSets :=
  (basisSets_iff _).mpr ⟨i, _, hr, rfl⟩

Membership of Seminorm Ball in Basis Sets

Informal description

For any finite subset $i$ of the index set $\iota$ and any positive real number $r > 0$, the open ball centered at $0$ with radius $r$ with respect to the seminorm $\sup_{j \in i} p_j$ is a member of the basis sets of the seminorm family $p$.

SeminormFamily.basisSets_singleton_mem theorem

(i : ι) {r : ℝ} (hr : 0 < r) : (p i).ball 0 r ∈ p.basisSets

Full source

theorem basisSets_singleton_mem (i : ι) {r : ℝ} (hr : 0 < r) : (p i).ball 0 r ∈ p.basisSets :=
  (basisSets_iff _).mpr ⟨{i}, _, hr, by rw [Finset.sup_singleton]⟩

Membership of Single Seminorm Ball in Basis Sets

Informal description

For any index $i$ in the indexing set $\iota$ and any positive real number $r > 0$, the open ball centered at $0$ with radius $r$ with respect to the seminorm $p_i$ is a member of the basis sets of the seminorm family $p$.

SeminormFamily.basisSets_nonempty theorem

[Nonempty ι] : p.basisSets.Nonempty

Full source

theorem basisSets_nonempty [Nonempty ι] : p.basisSets.Nonempty := by
  let i := Classical.arbitrary ι
  refine nonempty_def.mpr ⟨(p i).ball 0 1, ?_⟩
  exact p.basisSets_singleton_mem i zero_lt_one

Nonemptiness of Basis Sets for Seminorm Family with Nonempty Index Set

Informal description

For any nonempty indexing set $\iota$, the collection of basis sets of the seminorm family $p$ is nonempty. That is, there exists at least one open ball centered at $0$ defined by a finite subset of seminorms in $p$ and a positive radius.

SeminormFamily.basisSets_intersect theorem

(U V : Set E) (hU : U ∈ p.basisSets) (hV : V ∈ p.basisSets) : ∃ z ∈ p.basisSets, z ⊆ U ∩ V

Full source

theorem basisSets_intersect (U V : Set E) (hU : U ∈ p.basisSets) (hV : V ∈ p.basisSets) :
    ∃ z ∈ p.basisSets, z ⊆ U ∩ V := by
  classical
    rcases p.basisSets_iff.mp hU with ⟨s, r₁, hr₁, hU⟩
    rcases p.basisSets_iff.mp hV with ⟨t, r₂, hr₂, hV⟩
    use ((s ∪ t).sup p).ball 0 (min r₁ r₂)
    refine ⟨p.basisSets_mem (s ∪ t) (lt_min_iff.mpr ⟨hr₁, hr₂⟩), ?_⟩
    rw [hU, hV, ball_finset_sup_eq_iInter _ _ _ (lt_min_iff.mpr ⟨hr₁, hr₂⟩),
      ball_finset_sup_eq_iInter _ _ _ hr₁, ball_finset_sup_eq_iInter _ _ _ hr₂]
    exact
      Set.subset_inter
        (Set.iInter₂_mono' fun i hi =>
          ⟨i, Finset.subset_union_left hi, ball_mono <| min_le_left _ _⟩)
        (Set.iInter₂_mono' fun i hi =>
          ⟨i, Finset.subset_union_right hi, ball_mono <| min_le_right _ _⟩)

Intersection Property of Seminorm Basis Sets

Informal description

For any two sets $U$ and $V$ in the basis sets of a seminorm family $p$ on a vector space $E$, there exists a basis set $z$ such that $z$ is contained in the intersection $U \cap V$.

SeminormFamily.basisSets_zero theorem

(U) (hU : U ∈ p.basisSets) : (0 : E) ∈ U

Full source

theorem basisSets_zero (U) (hU : U ∈ p.basisSets) : (0 : E) ∈ U := by
  rcases p.basisSets_iff.mp hU with ⟨ι', r, hr, hU⟩
  rw [hU, mem_ball_zero, map_zero]
  exact hr

Zero Vector Belongs to Every Basis Set of Seminorm Family

Informal description

For any set $U$ in the basis sets of a seminorm family $p$ on a vector space $E$, the zero vector $0 \in E$ is contained in $U$.

SeminormFamily.basisSets_add theorem

(U) (hU : U ∈ p.basisSets) : ∃ V ∈ p.basisSets, V + V ⊆ U

Full source

theorem basisSets_add (U) (hU : U ∈ p.basisSets) :
    ∃ V ∈ p.basisSets, V + V ⊆ U := by
  rcases p.basisSets_iff.mp hU with ⟨s, r, hr, hU⟩
  use (s.sup p).ball 0 (r / 2)
  refine ⟨p.basisSets_mem s (div_pos hr zero_lt_two), ?_⟩
  refine Set.Subset.trans (ball_add_ball_subset (s.sup p) (r / 2) (r / 2) 0 0) ?_
  rw [hU, add_zero, add_halves]

Minkowski Sum Property of Seminorm Basis Sets

Informal description

For any set $U$ in the basis sets of a seminorm family $p$ on a vector space $E$, there exists another basis set $V$ such that the Minkowski sum $V + V$ is contained in $U$.

SeminormFamily.basisSets_neg theorem

(U) (hU' : U ∈ p.basisSets) : ∃ V ∈ p.basisSets, V ⊆ (fun x : E => -x) ⁻¹' U

Full source

theorem basisSets_neg (U) (hU' : U ∈ p.basisSets) :
    ∃ V ∈ p.basisSets, V ⊆ (fun x : E => -x) ⁻¹' U := by
  rcases p.basisSets_iff.mp hU' with ⟨s, r, _, hU⟩
  rw [hU, neg_preimage, neg_ball (s.sup p), neg_zero]
  exact ⟨U, hU', Eq.subset hU⟩

Existence of Negation-Compatible Basis Set in Seminorm Family

Informal description

For any set $U$ in the basis sets of a seminorm family $p$ on a vector space $E$, there exists another basis set $V$ such that $V$ is contained in the preimage of $U$ under the negation map $x \mapsto -x$.

SeminormFamily.addGroupFilterBasis definition

[Nonempty ι] : AddGroupFilterBasis E

Full source

/-- The `addGroupFilterBasis` induced by the filter basis `Seminorm.basisSets`. -/
protected def addGroupFilterBasis [Nonempty ι] : AddGroupFilterBasis E :=
  addGroupFilterBasisOfComm p.basisSets p.basisSets_nonempty p.basisSets_intersect p.basisSets_zero
    p.basisSets_add p.basisSets_neg

Additive group filter basis induced by seminorm family

Informal description

The additive group filter basis on a vector space $E$ induced by the filter basis of open seminorm balls centered at 0, where the family of seminorms is indexed by a nonempty set $\iota$. This construction ensures compatibility with the additive group structure of $E$, providing a basis for the topology where the neighborhoods of 0 are generated by the seminorm balls.

SeminormFamily.basisSets_smul_right theorem

(v : E) (U : Set E) (hU : U ∈ p.basisSets) : ∀ᶠ x : 𝕜 in 𝓝 0, x • v ∈ U

Full source

theorem basisSets_smul_right (v : E) (U : Set E) (hU : U ∈ p.basisSets) :
    ∀ᶠ x : 𝕜 in 𝓝 0, x • v ∈ U := by
  rcases p.basisSets_iff.mp hU with ⟨s, r, hr, hU⟩
  rw [hU, Filter.eventually_iff]
  simp_rw [(s.sup p).mem_ball_zero, map_smul_eq_mul]
  by_cases h : 0 < (s.sup p) v
  · simp_rw [(lt_div_iff₀ h).symm]
    rw [← _root_.ball_zero_eq]
    exact Metric.ball_mem_nhds 0 (div_pos hr h)
  simp_rw [le_antisymm (not_lt.mp h) (apply_nonneg _ v), mul_zero, hr]
  exact IsOpen.mem_nhds isOpen_univ (mem_univ 0)

Scalar Multiplication of Vector in Seminorm Basis Sets is Eventually in Basis Set

Informal description

For any vector $v$ in a vector space $E$ and any set $U$ in the basis sets of a seminorm family $p$ on $E$, there exists a neighborhood $V$ of $0$ in the scalar field $\mathbb{K}$ such that for all $x \in V$, the scalar multiple $x \cdot v$ belongs to $U$.

SeminormFamily.basisSets_smul theorem

(U) (hU : U ∈ p.basisSets) : ∃ V ∈ 𝓝 (0 : 𝕜), ∃ W ∈ p.addGroupFilterBasis.sets, V • W ⊆ U

Full source

theorem basisSets_smul (U) (hU : U ∈ p.basisSets) :
    ∃ V ∈ 𝓝 (0 : 𝕜), ∃ W ∈ p.addGroupFilterBasis.sets, V • W ⊆ U := by
  rcases p.basisSets_iff.mp hU with ⟨s, r, hr, hU⟩
  refine ⟨Metric.ball 0 √r, Metric.ball_mem_nhds 0 (Real.sqrt_pos.mpr hr), ?_⟩
  refine ⟨(s.sup p).ball 0 √r, p.basisSets_mem s (Real.sqrt_pos.mpr hr), ?_⟩
  refine Set.Subset.trans (ball_smul_ball (s.sup p) √r √r) ?_
  rw [hU, Real.mul_self_sqrt (le_of_lt hr)]

Existence of Scalar and Neighborhood for Seminorm Basis Sets

Informal description

For any set $U$ in the basis sets of the seminorm family $p$ on a vector space $E$ over a field $\mathbb{K}$, there exists a neighborhood $V$ of $0$ in $\mathbb{K}$ and a set $W$ in the additive group filter basis of $E$ such that the scalar multiplication $V \cdot W$ is contained in $U$.

SeminormFamily.basisSets_smul_left theorem

 (x : 𝕜) (U : Set E) (hU : U ∈ p.basisSets) : ∃ V ∈ p.addGroupFilterBasis.sets, V ⊆ (fun y : E => x • y) ⁻¹' U

Full source

theorem basisSets_smul_left (x : 𝕜) (U : Set E) (hU : U ∈ p.basisSets) :
    ∃ V ∈ p.addGroupFilterBasis.sets, V ⊆ (fun y : E => x • y) ⁻¹' U := by
  rcases p.basisSets_iff.mp hU with ⟨s, r, hr, hU⟩
  rw [hU]
  by_cases h : x ≠ 0
  · rw [(s.sup p).smul_ball_preimage 0 r x h, smul_zero]
    use (s.sup p).ball 0 (r / ‖x‖)
    exact ⟨p.basisSets_mem s (div_pos hr (norm_pos_iff.mpr h)), Subset.rfl⟩
  refine ⟨(s.sup p).ball 0 r, p.basisSets_mem s hr, ?_⟩
  simp only [not_ne_iff.mp h, Set.subset_def, mem_ball_zero, hr, mem_univ, map_zero, imp_true_iff,
    preimage_const_of_mem, zero_smul]

Existence of Scalar Multiplication Preimage in Seminorm Basis Sets

Informal description

For any scalar $x$ in the field $\mathbb{K}$ and any set $U$ in the basis sets of the seminorm family $p$ on a vector space $E$, there exists a neighborhood $V$ of $0$ in the additive group filter basis induced by $p$ such that $V$ is contained in the preimage of $U$ under the scalar multiplication map $y \mapsto x \cdot y$.

SeminormFamily.moduleFilterBasis definition

: ModuleFilterBasis 𝕜 E

Full source

/-- The `moduleFilterBasis` induced by the filter basis `Seminorm.basisSets`. -/
protected def moduleFilterBasis : ModuleFilterBasis 𝕜 E where
  toAddGroupFilterBasis := p.addGroupFilterBasis
  smul' := p.basisSets_smul _
  smul_left' := p.basisSets_smul_left
  smul_right' := p.basisSets_smul_right

Module filter basis induced by seminorm family

Informal description

The module filter basis on a vector space $E$ over a field $\mathbb{K}$ induced by a family of seminorms $p : \iota \to \text{Seminorm}\, \mathbb{K}\, E$. This is constructed from the additive group filter basis generated by the open seminorm balls centered at 0, and satisfies the additional properties: 1. For any set $U$ in the basis, there exist a neighborhood $V$ of $0$ in $\mathbb{K}$ and a set $W$ in the additive group filter basis such that $V \cdot W \subseteq U$. 2. For any scalar $x \in \mathbb{K}$ and any basis set $U$, there exists a set $V$ in the additive group filter basis contained in the preimage of $U$ under scalar multiplication by $x$. 3. For any vector $v \in E$ and any basis set $U$, scalar multiples $x \cdot v$ belong to $U$ for all $x$ in some neighborhood of $0$ in $\mathbb{K}$.

SeminormFamily.filter_eq_iInf theorem

(p : SeminormFamily 𝕜 E ι) : p.moduleFilterBasis.toFilterBasis.filter = ⨅ i, (𝓝 0).comap (p i)

Full source

theorem filter_eq_iInf (p : SeminormFamily 𝕜 E ι) :
    p.moduleFilterBasis.toFilterBasis.filter = ⨅ i, (𝓝 0).comap (p i) := by
  refine le_antisymm (le_iInf fun i => ?_) ?_
  · rw [p.moduleFilterBasis.toFilterBasis.hasBasis.le_basis_iff
        (Metric.nhds_basis_ball.comap _)]
    intro ε hε
    refine ⟨(p i).ball 0 ε, ?_, ?_⟩
    · rw [← (Finset.sup_singleton : _ = p i)]
      exact p.basisSets_mem {i} hε
    · rw [id, (p i).ball_zero_eq_preimage_ball]
  · rw [p.moduleFilterBasis.toFilterBasis.hasBasis.ge_iff]
    rintro U (hU : U ∈ p.basisSets)
    rcases p.basisSets_iff.mp hU with ⟨s, r, hr, rfl⟩
    rw [id, Seminorm.ball_finset_sup_eq_iInter _ _ _ hr, s.iInter_mem_sets]
    exact fun i _ =>
      Filter.mem_iInf_of_mem i
        ⟨Metric.ball 0 r, Metric.ball_mem_nhds 0 hr,
          Eq.subset (p i).ball_zero_eq_preimage_ball.symm⟩

Filter Characterization of Seminorm-Induced Topology at Zero

Informal description

For a family of seminorms $p$ on a vector space $E$ over a field $\mathbb{K}$, the filter generated by the module filter basis associated to $p$ is equal to the infimum over all indices $i$ of the preimage filters of the neighborhood filter of $0$ under each seminorm $p_i$. In other words, the filter of neighborhoods of $0$ in the topology induced by the seminorm family $p$ is given by $\bigwedge_i p_i^{-1}(\mathcal{N}(0))$, where $\mathcal{N}(0)$ denotes the neighborhood filter of $0$ in $\mathbb{R}$.

SeminormFamily.basisSets_mem_nhds theorem

 {𝕜 E ι : Type*} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] (p : SeminormFamily 𝕜 E ι)
  (hp : ∀ i, Continuous (p i)) (U : Set E) (hU : U ∈ p.basisSets) : U ∈ 𝓝 (0 : E)

Full source

/-- If a family of seminorms is continuous, then their basis sets are neighborhoods of zero. -/
lemma basisSets_mem_nhds {𝕜 E ι : Type*} [NormedField 𝕜]
    [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] (p : SeminormFamily 𝕜 E ι)
    (hp : ∀ i, Continuous (p i)) (U : Set E) (hU : U ∈ p.basisSets) : U ∈ 𝓝 (0 : E) := by
  obtain ⟨s, r, hr, rfl⟩ := p.basisSets_iff.mp hU
  clear hU
  refine Seminorm.ball_mem_nhds ?_ hr
  classical
  induction s using Finset.induction_on
  case empty => simpa using continuous_zero
  case insert a s _ hs =>
    simp only [Finset.sup_insert, coe_sup]
    exact Continuous.max (hp a) hs

Basis Sets of Continuous Seminorms are Neighborhoods of Zero

Informal description

Let $E$ be a topological vector space over a normed field $\mathbb{K}$ with topology induced by a family of seminorms $p : \iota \to \text{Seminorm}\, \mathbb{K}\, E$. If each seminorm $p_i$ is continuous, then every basis set $U \in p.\text{basisSets}$ (i.e., every open seminorm ball centered at 0) is a neighborhood of 0 in $E$.

Seminorm.IsBounded definition

(p : ι → Seminorm 𝕜 E) (q : ι' → Seminorm 𝕜₂ F) (f : E →ₛₗ[σ₁₂] F) : Prop

Full source

/-- The proposition that a linear map is bounded between spaces with families of seminorms. -/
def IsBounded (p : ι → Seminorm 𝕜 E) (q : ι' → Seminorm 𝕜₂ F) (f : E →ₛₗ[σ₁₂] F) : Prop :=
  ∀ i, ∃ s : Finset ι, ∃ C : ℝ≥0, (q i).comp f ≤ C • s.sup p

Boundedness of a semilinear map between seminormed spaces

Informal description

Given two families of seminorms $p : \iota \to \text{Seminorm}\, \mathbb{K}\, E$ and $q : \iota' \to \text{Seminorm}\, \mathbb{K}_2\, F$ on vector spaces $E$ and $F$ respectively, a semilinear map $f : E \to F$ is called *bounded* if for every seminorm $q_i$ in the family $q$, there exists a finite subset $s \subseteq \iota$ and a constant $C \geq 0$ such that the composition $q_i \circ f$ is bounded by $C$ times the supremum of the seminorms $\{p_j\}_{j \in s}$.

Seminorm.isBounded_const theorem

 (ι' : Type*) [Nonempty ι'] {p : ι → Seminorm 𝕜 E} {q : Seminorm 𝕜₂ F} (f : E →ₛₗ[σ₁₂] F) :
  IsBounded p (fun _ : ι' => q) f ↔ ∃ (s : Finset ι) (C : ℝ≥0), q.comp f ≤ C • s.sup p

Full source

theorem isBounded_const (ι' : Type*) [Nonempty ι'] {p : ι → Seminorm 𝕜 E} {q : Seminorm 𝕜₂ F}
    (f : E →ₛₗ[σ₁₂] F) :
    IsBoundedIsBounded p (fun _ : ι' => q) f ↔ ∃ (s : Finset ι) (C : ℝ≥0), q.comp f ≤ C • s.sup p := by
  simp only [IsBounded, forall_const]

Boundedness of Semilinear Maps with Constant Seminorm Family

Informal description

Let $E$ and $F$ be vector spaces over normed fields $\mathbb{K}$ and $\mathbb{K}_2$ respectively, equipped with families of seminorms $p : \iota \to \text{Seminorm}\, \mathbb{K}\, E$ and a single seminorm $q$ on $F$. For a semilinear map $f : E \to F$, the following are equivalent: 1. $f$ is bounded with respect to the families $p$ and the constant family $\lambda \_. q$ (where $\iota'$ is any nonempty index type). 2. There exists a finite subset $s \subseteq \iota$ and a constant $C \geq 0$ such that the composition $q \circ f$ is bounded by $C$ times the supremum of the seminorms $\{p_j\}_{j \in s}$.

Seminorm.const_isBounded theorem

 (ι : Type*) [Nonempty ι] {p : Seminorm 𝕜 E} {q : ι' → Seminorm 𝕜₂ F} (f : E →ₛₗ[σ₁₂] F) :
  IsBounded (fun _ : ι => p) q f ↔ ∀ i, ∃ C : ℝ≥0, (q i).comp f ≤ C • p

Full source

theorem const_isBounded (ι : Type*) [Nonempty ι] {p : Seminorm 𝕜 E} {q : ι' → Seminorm 𝕜₂ F}
    (f : E →ₛₗ[σ₁₂] F) : IsBoundedIsBounded (fun _ : ι => p) q f ↔ ∀ i, ∃ C : ℝ≥0, (q i).comp f ≤ C • p := by
  constructor <;> intro h i
  · rcases h i with ⟨s, C, h⟩
    exact ⟨C, le_trans h (smul_le_smul (Finset.sup_le fun _ _ => le_rfl) le_rfl)⟩
  use {Classical.arbitrary ι}
  simp only [h, Finset.sup_singleton]

Boundedness Criterion for Semilinear Maps with Constant Seminorm Family

Informal description

Let $E$ and $F$ be vector spaces over fields $\mathbb{K}$ and $\mathbb{K}_2$ respectively, equipped with a single seminorm $p$ on $E$ and a family of seminorms $q : \iota' \to \text{Seminorm}\, \mathbb{K}_2\, F$ on $F$. Given a semilinear map $f : E \to F$, the following are equivalent: 1. $f$ is bounded with respect to the constant family of seminorms $(p)_{i \in \iota}$ (where $\iota$ is nonempty) and the family $q$. 2. For every index $i \in \iota'$, there exists a constant $C \geq 0$ such that the composition $(q_i) \circ f$ is bounded by $C \cdot p$.

Seminorm.isBounded_sup theorem

 {p : ι → Seminorm 𝕜 E} {q : ι' → Seminorm 𝕜₂ F} {f : E →ₛₗ[σ₁₂] F} (hf : IsBounded p q f) (s' : Finset ι') :
  ∃ (C : ℝ≥0) (s : Finset ι), (s'.sup q).comp f ≤ C • s.sup p

Full source

theorem isBounded_sup {p : ι → Seminorm 𝕜 E} {q : ι' → Seminorm 𝕜₂ F} {f : E →ₛₗ[σ₁₂] F}
    (hf : IsBounded p q f) (s' : Finset ι') :
    ∃ (C : ℝ≥0) (s : Finset ι), (s'.sup q).comp f ≤ C • s.sup p := by
  classical
    obtain rfl | _ := s'.eq_empty_or_nonempty
    · exact ⟨1, ∅, by simp [Seminorm.bot_eq_zero]⟩
    choose fₛ fC hf using hf
    use s'.card • s'.sup fC, Finset.biUnion s' fₛ
    have hs : ∀ i : ι', i ∈ s' → (q i).comp f ≤ s'.sup fC • (Finset.biUnion s' fₛ).sup p := by
      intro i hi
      refine (hf i).trans (smul_le_smul ?_ (Finset.le_sup hi))
      exact Finset.sup_mono (Finset.subset_biUnion_of_mem fₛ hi)
    refine (comp_mono f (finset_sup_le_sum q s')).trans ?_
    simp_rw [← pullback_apply, map_sum, pullback_apply]
    refine (Finset.sum_le_sum hs).trans ?_
    rw [Finset.sum_const, smul_assoc]

Boundedness of Semilinear Maps under Supremum Seminorms

Informal description

Let $E$ and $F$ be vector spaces over normed fields $\mathbb{K}$ and $\mathbb{K}_2$ respectively, equipped with families of seminorms $p : \iota \to \text{Seminorm}\, \mathbb{K}\, E$ and $q : \iota' \to \text{Seminorm}\, \mathbb{K}_2\, F$. Given a bounded semilinear map $f : E \to F$ (i.e., $f$ satisfies the condition $\text{IsBounded}\, p\, q\, f$) and any finite subset $s' \subseteq \iota'$, there exists a constant $C \geq 0$ and a finite subset $s \subseteq \iota$ such that the composition of the supremum seminorm $\sup_{i \in s'} q_i$ with $f$ is bounded by $C$ times the supremum seminorm $\sup_{j \in s} p_j$.

WithSeminorms structure

(p : SeminormFamily 𝕜 E ι) [topology : TopologicalSpace E]

Full source

/-- The proposition that the topology of `E` is induced by a family of seminorms `p`. -/
structure WithSeminorms (p : SeminormFamily 𝕜 E ι) [topology : TopologicalSpace E] : Prop where
  topology_eq_withSeminorms : topology = p.moduleFilterBasis.topology

Topology induced by a family of seminorms

Informal description

The structure `WithSeminorms p` asserts that the topology on a vector space `E` over a field `𝕜` is induced by a family of seminorms `p : ι → Seminorm 𝕜 E`, where `ι` is an indexing set. This means that the topology is generated by the open balls defined by the seminorms in the family `p`.

WithSeminorms.withSeminorms_eq theorem

{p : SeminormFamily 𝕜 E ι} [t : TopologicalSpace E] (hp : WithSeminorms p) : t = p.moduleFilterBasis.topology

Full source

theorem WithSeminorms.withSeminorms_eq {p : SeminormFamily 𝕜 E ι} [t : TopologicalSpace E]
    (hp : WithSeminorms p) : t = p.moduleFilterBasis.topology :=
  hp.1

Equality of Topologies Induced by Seminorm Family and Module Filter Basis

Informal description

Let $E$ be a vector space over a field $\mathbb{K}$ equipped with a family of seminorms $p : \iota \to \text{Seminorm}\, \mathbb{K}\, E$. If the topology on $E$ is induced by this family of seminorms (i.e., `WithSeminorms p` holds), then the topology coincides with the one generated by the module filter basis associated to $p$.

WithSeminorms.topologicalAddGroup theorem

(hp : WithSeminorms p) : IsTopologicalAddGroup E

Full source

theorem WithSeminorms.topologicalAddGroup (hp : WithSeminorms p) : IsTopologicalAddGroup E := by
  rw [hp.withSeminorms_eq]
  exact AddGroupFilterBasis.isTopologicalAddGroup _

Topological Additive Group Structure Induced by Seminorms

Informal description

Let $E$ be a vector space over a field $\mathbb{K}$ equipped with a topology induced by a family of seminorms $p : \iota \to \text{Seminorm}\, \mathbb{K}\, E$. Then $E$ forms a topological additive group under this topology.

WithSeminorms.continuousSMul theorem

(hp : WithSeminorms p) : ContinuousSMul 𝕜 E

Full source

theorem WithSeminorms.continuousSMul (hp : WithSeminorms p) : ContinuousSMul 𝕜 E := by
  rw [hp.withSeminorms_eq]
  exact ModuleFilterBasis.continuousSMul _

Continuity of Scalar Multiplication in Seminorm-Induced Topology

Informal description

Let $E$ be a vector space over a field $\mathbb{K}$ equipped with a topology induced by a family of seminorms $p : \iota \to \text{Seminorm}\, \mathbb{K}\, E$. Then the scalar multiplication operation $\mathbb{K} \times E \to E$ is continuous.

WithSeminorms.hasBasis theorem

(hp : WithSeminorms p) : (𝓝 (0 : E)).HasBasis (fun s : Set E => s ∈ p.basisSets) id

Full source

theorem WithSeminorms.hasBasis (hp : WithSeminorms p) :
    (𝓝 (0 : E)).HasBasis (fun s : Set E => s ∈ p.basisSets) id := by
  rw [congr_fun (congr_arg (@nhds E) hp.1) 0]
  exact AddGroupFilterBasis.nhds_zero_hasBasis _

Neighborhood Basis at Zero in a Seminorm-Induced Topology

Informal description

Let $E$ be a vector space over a field $\mathbb{K}$ equipped with a topology induced by a family of seminorms $p : \iota \to \text{Seminorm}\, \mathbb{K}\, E$. Then the neighborhood filter of $0$ in $E$ has a basis consisting of the sets in `p.basisSets`, i.e., the sets of the form $\{x \in E \mid \sup_{i \in s} p_i(x) < r\}$ for some finite subset $s \subseteq \iota$ and $r > 0$.

WithSeminorms.hasBasis_zero_ball theorem

 (hp : WithSeminorms p) : (𝓝 (0 : E)).HasBasis (fun sr : Finset ι × ℝ => 0 < sr.2) fun sr => (sr.1.sup p).ball 0 sr.2

Full source

theorem WithSeminorms.hasBasis_zero_ball (hp : WithSeminorms p) :
    (𝓝 (0 : E)).HasBasis
    (fun sr : FinsetFinset ι × ℝ => 0 < sr.2) fun sr => (sr.1.sup p).ball 0 sr.2 := by
  refine ⟨fun V => ?_⟩
  simp only [hp.hasBasis.mem_iff, SeminormFamily.basisSets_iff, Prod.exists]
  constructor
  · rintro ⟨-, ⟨s, r, hr, rfl⟩, hV⟩
    exact ⟨s, r, hr, hV⟩
  · rintro ⟨s, r, hr, hV⟩
    exact ⟨_, ⟨s, r, hr, rfl⟩, hV⟩

Neighborhood basis at zero in seminorm-induced topology via finite seminorm subsets

Informal description

Let $E$ be a vector space over a field $\mathbb{K}$ equipped with a topology induced by a family of seminorms $p = (p_i)_{i \in \iota}$. Then the neighborhood filter of $0$ in $E$ has a basis consisting of all open balls $\{x \in E \mid \max_{i \in s} p_i(x) < r\}$ centered at 0, where $s$ ranges over all finite subsets of $\iota$ and $r$ ranges over all positive real numbers.

WithSeminorms.hasBasis_ball theorem

 (hp : WithSeminorms p) {x : E} :
  (𝓝 (x : E)).HasBasis (fun sr : Finset ι × ℝ => 0 < sr.2) fun sr => (sr.1.sup p).ball x sr.2

Full source

theorem WithSeminorms.hasBasis_ball (hp : WithSeminorms p) {x : E} :
    (𝓝 (x : E)).HasBasis
    (fun sr : FinsetFinset ι × ℝ => 0 < sr.2) fun sr => (sr.1.sup p).ball x sr.2 := by
  have : IsTopologicalAddGroup E := hp.topologicalAddGroup
  rw [← map_add_left_nhds_zero]
  convert hp.hasBasis_zero_ball.map (x + ·) using 1
  ext sr : 1
  -- Porting note: extra type ascriptions needed on `0`
  have : (sr.fst.sup p).ball (x +ᵥ (0 : E)) sr.snd = x +ᵥ (sr.fst.sup p).ball 0 sr.snd :=
    Eq.symm (Seminorm.vadd_ball (sr.fst.sup p))
  rwa [vadd_eq_add, add_zero] at this

Neighborhood Basis via Seminorm Balls in Seminorm-Induced Topology

Informal description

Let $E$ be a vector space over a field $\mathbb{K}$ equipped with a topology induced by a family of seminorms $p = (p_i)_{i \in \iota}$. For any point $x \in E$, the neighborhood filter $\mathcal{N}(x)$ has a basis consisting of all open balls $\{y \in E \mid \max_{i \in s} p_i(y - x) < r\}$, where $s$ ranges over all finite subsets of $\iota$ and $r$ ranges over all positive real numbers.

WithSeminorms.mem_nhds_iff theorem

(hp : WithSeminorms p) (x : E) (U : Set E) : U ∈ 𝓝 x ↔ ∃ s : Finset ι, ∃ r > 0, (s.sup p).ball x r ⊆ U

Full source

/-- The `x`-neighbourhoods of a space whose topology is induced by a family of seminorms
are exactly the sets which contain seminorm balls around `x`. -/
theorem WithSeminorms.mem_nhds_iff (hp : WithSeminorms p) (x : E) (U : Set E) :
    U ∈ 𝓝 xU ∈ 𝓝 x ↔ ∃ s : Finset ι, ∃ r > 0, (s.sup p).ball x r ⊆ U := by
  rw [hp.hasBasis_ball.mem_iff, Prod.exists]

Characterization of Neighborhoods in Seminorm-Induced Topology

Informal description

Let $E$ be a vector space over a field $\mathbb{K}$ equipped with a topology induced by a family of seminorms $(p_i)_{i \in \iota}$. For any point $x \in E$ and any subset $U \subseteq E$, $U$ is a neighborhood of $x$ if and only if there exists a finite subset $s \subseteq \iota$ and a positive real number $r > 0$ such that the open ball $\{y \in E \mid \max_{i \in s} p_i(y - x) < r\}$ is contained in $U$.

WithSeminorms.isOpen_iff_mem_balls theorem

(hp : WithSeminorms p) (U : Set E) : IsOpen U ↔ ∀ x ∈ U, ∃ s : Finset ι, ∃ r > 0, (s.sup p).ball x r ⊆ U

Full source

/-- The open sets of a space whose topology is induced by a family of seminorms
are exactly the sets which contain seminorm balls around all of their points. -/
theorem WithSeminorms.isOpen_iff_mem_balls (hp : WithSeminorms p) (U : Set E) :
    IsOpenIsOpen U ↔ ∀ x ∈ U, ∃ s : Finset ι, ∃ r > 0, (s.sup p).ball x r ⊆ U := by
  simp_rw [← WithSeminorms.mem_nhds_iff hp _ U, isOpen_iff_mem_nhds]

Characterization of Open Sets in Seminorm-Induced Topology

Informal description

Let $E$ be a vector space over a field $\mathbb{K}$ equipped with a topology induced by a family of seminorms $(p_i)_{i \in \iota}$. A subset $U \subseteq E$ is open if and only if for every point $x \in U$, there exists a finite subset $s \subseteq \iota$ and a positive real number $r > 0$ such that the open ball $\{y \in E \mid \max_{i \in s} p_i(y - x) < r\}$ is contained in $U$.

WithSeminorms.T1_of_separating theorem

(hp : WithSeminorms p) (h : ∀ x, x ≠ 0 → ∃ i, p i x ≠ 0) : T1Space E

Full source

/-- A separating family of seminorms induces a T₁ topology. -/
theorem WithSeminorms.T1_of_separating (hp : WithSeminorms p)
    (h : ∀ x, x ≠ 0 → ∃ i, p i x ≠ 0) : T1Space E := by
  have := hp.topologicalAddGroup
  refine IsTopologicalAddGroup.t1Space _ ?_
  rw [← isOpen_compl_iff, hp.isOpen_iff_mem_balls]
  rintro x (hx : x ≠ 0)
  obtain ⟨i, pi_nonzero⟩ := h x hx
  refine ⟨{i}, p i x, by positivity, subset_compl_singleton_iff.mpr ?_⟩
  rw [Finset.sup_singleton, mem_ball, zero_sub, map_neg_eq_map, not_lt]

Separating Seminorm Family Induces $T_1$ Topology

Informal description

Let $E$ be a vector space over a field $\mathbb{K}$ equipped with a topology induced by a separating family of seminorms $(p_i)_{i \in \iota}$ (i.e., for every nonzero $x \in E$, there exists $i \in \iota$ such that $p_i(x) \neq 0$). Then $E$ is a $T_1$ topological space.

WithSeminorms.separating_of_T1 theorem

[T1Space E] (hp : WithSeminorms p) (x : E) (hx : x ≠ 0) : ∃ i, p i x ≠ 0

Full source

/-- A family of seminorms inducing a T₁ topology is separating. -/
theorem WithSeminorms.separating_of_T1 [T1Space E] (hp : WithSeminorms p) (x : E) (hx : x ≠ 0) :
    ∃ i, p i x ≠ 0 := by
  have := ((t1Space_TFAE E).out 0 9).mp (inferInstanceAs <| T1Space E)
  by_contra! h
  refine hx (this ?_)
  rw [hp.hasBasis_zero_ball.specializes_iff]
  rintro ⟨s, r⟩ (hr : 0 < r)
  simp only [ball_finset_sup_eq_iInter _ _ _ hr, mem_iInter₂, mem_ball_zero, h, hr, forall_true_iff]

Separating Property of Seminorms in $T_1$ Topological Vector Spaces

Informal description

Let $E$ be a topological vector space whose topology is induced by a family of seminorms $p = (p_i)_{i \in \iota}$. If $E$ is a $T_1$ space, then for any nonzero vector $x \in E$, there exists an index $i \in \iota$ such that $p_i(x) \neq 0$. In other words, the family of seminorms is separating.

WithSeminorms.separating_iff_T1 theorem

(hp : WithSeminorms p) : (∀ x, x ≠ 0 → ∃ i, p i x ≠ 0) ↔ T1Space E

Full source

/-- A family of seminorms is separating iff it induces a T₁ topology. -/
theorem WithSeminorms.separating_iff_T1 (hp : WithSeminorms p) :
    (∀ x, x ≠ 0 → ∃ i, p i x ≠ 0) ↔ T1Space E := by
  refine ⟨WithSeminorms.T1_of_separating hp, ?_⟩
  intro
  exact WithSeminorms.separating_of_T1 hp

Equivalence of Separating Seminorm Family and $T_1$ Topology in Seminorm-Induced Spaces

Informal description

Let $E$ be a topological vector space whose topology is induced by a family of seminorms $(p_i)_{i \in \iota}$. Then the family of seminorms is separating (i.e., for every nonzero $x \in E$, there exists $i \in \iota$ such that $p_i(x) \neq 0$) if and only if $E$ is a $T_1$ space.

WithSeminorms.tendsto_nhds' theorem

 (hp : WithSeminorms p) (u : F → E) {f : Filter F} (y₀ : E) :
  Filter.Tendsto u f (𝓝 y₀) ↔ ∀ (s : Finset ι) (ε), 0 < ε → ∀ᶠ x in f, s.sup p (u x - y₀) < ε

Full source

/-- Convergence along filters for `WithSeminorms`.

Variant with `Finset.sup`. -/
theorem WithSeminorms.tendsto_nhds' (hp : WithSeminorms p) (u : F → E) {f : Filter F} (y₀ : E) :
    Filter.TendstoFilter.Tendsto u f (𝓝 y₀) ↔
    ∀ (s : Finset ι) (ε), 0 < ε → ∀ᶠ x in f, s.sup p (u x - y₀) < ε := by
  simp [hp.hasBasis_ball.tendsto_right_iff]

Convergence Criterion in Seminorm-Induced Topology via Finite Suprema

Informal description

Let $E$ be a topological vector space whose topology is induced by a family of seminorms $p = (p_i)_{i \in \iota}$. For a function $u : F \to E$, a filter $f$ on $F$, and a point $y_0 \in E$, the function $u$ tends to $y_0$ along the filter $f$ if and only if for every finite subset $s \subset \iota$ and every $\epsilon > 0$, there exists an event in $f$ beyond which $\max_{i \in s} p_i(u(x) - y_0) < \epsilon$ holds for all $x$ in that event.

WithSeminorms.tendsto_nhds theorem

 (hp : WithSeminorms p) (u : F → E) {f : Filter F} (y₀ : E) :
  Filter.Tendsto u f (𝓝 y₀) ↔ ∀ i ε, 0 < ε → ∀ᶠ x in f, p i (u x - y₀) < ε

Full source

/-- Convergence along filters for `WithSeminorms`. -/
theorem WithSeminorms.tendsto_nhds (hp : WithSeminorms p) (u : F → E) {f : Filter F} (y₀ : E) :
    Filter.TendstoFilter.Tendsto u f (𝓝 y₀) ↔ ∀ i ε, 0 < ε → ∀ᶠ x in f, p i (u x - y₀) < ε := by
  rw [hp.tendsto_nhds' u y₀]
  exact
    ⟨fun h i => by simpa only [Finset.sup_singleton] using h {i}, fun h s ε hε =>
      (s.eventually_all.2 fun i _ => h i ε hε).mono fun _ => finset_sup_apply_lt hε⟩

Convergence in Seminorm-Induced Topology via Individual Seminorms

Informal description

Let $E$ be a topological vector space whose topology is induced by a family of seminorms $p = (p_i)_{i \in \iota}$. For a function $u : F \to E$, a filter $f$ on $F$, and a point $y_0 \in E$, the function $u$ tends to $y_0$ along the filter $f$ if and only if for every seminorm $p_i$ in the family and every $\epsilon > 0$, there exists an event in $f$ beyond which $p_i(u(x) - y_0) < \epsilon$ holds for all $x$ in that event.

WithSeminorms.tendsto_nhds_atTop theorem

 (hp : WithSeminorms p) (u : F → E) (y₀ : E) :
  Filter.Tendsto u Filter.atTop (𝓝 y₀) ↔ ∀ i ε, 0 < ε → ∃ x₀, ∀ x, x₀ ≤ x → p i (u x - y₀) < ε

Full source

/-- Limit `→ ∞` for `WithSeminorms`. -/
theorem WithSeminorms.tendsto_nhds_atTop (hp : WithSeminorms p) (u : F → E) (y₀ : E) :
    Filter.TendstoFilter.Tendsto u Filter.atTop (𝓝 y₀) ↔
    ∀ i ε, 0 < ε → ∃ x₀, ∀ x, x₀ ≤ x → p i (u x - y₀) < ε := by
  rw [hp.tendsto_nhds u y₀]
  exact forall₃_congr fun _ _ _ => Filter.eventually_atTop

Convergence at Infinity in Seminorm-Induced Topology

Informal description

Let $E$ be a topological vector space whose topology is induced by a family of seminorms $p = (p_i)_{i \in \iota}$. For a function $u : F \to E$ and a point $y_0 \in E$, the function $u$ tends to $y_0$ as $x \to \infty$ if and only if for every seminorm $p_i$ in the family and every $\epsilon > 0$, there exists a threshold $x_0$ such that for all $x \geq x_0$, the seminorm $p_i(u(x) - y_0) < \epsilon$.

SeminormFamily.withSeminorms_of_nhds theorem

 [IsTopologicalAddGroup E] (p : SeminormFamily 𝕜 E ι) (h : 𝓝 (0 : E) = p.moduleFilterBasis.toFilterBasis.filter) :
  WithSeminorms p

Full source

theorem SeminormFamily.withSeminorms_of_nhds [IsTopologicalAddGroup E] (p : SeminormFamily 𝕜 E ι)
    (h : 𝓝 (0 : E) = p.moduleFilterBasis.toFilterBasis.filter) : WithSeminorms p := by
  refine
    ⟨IsTopologicalAddGroup.ext inferInstance p.addGroupFilterBasis.isTopologicalAddGroup ?_⟩
  rw [AddGroupFilterBasis.nhds_zero_eq]
  exact h

Topology Induced by Seminorms via Neighborhood Filter Condition

Informal description

Let $E$ be a topological vector space over a field $\mathbb{K}$ with a topology that makes addition continuous (i.e., $E$ is a topological additive group). Given a family of seminorms $p : \iota \to \text{Seminorm}\, \mathbb{K}\, E$ indexed by $\iota$, if the neighborhood filter of $0$ in $E$ is equal to the filter generated by the module filter basis associated with $p$, then the topology on $E$ is induced by the family of seminorms $p$.

SeminormFamily.withSeminorms_of_hasBasis theorem

 [IsTopologicalAddGroup E] (p : SeminormFamily 𝕜 E ι) (h : (𝓝 (0 : E)).HasBasis (fun s : Set E => s ∈ p.basisSets) id) :
  WithSeminorms p

Full source

theorem SeminormFamily.withSeminorms_of_hasBasis [IsTopologicalAddGroup E]
    (p : SeminormFamily 𝕜 E ι) (h : (𝓝 (0 : E)).HasBasis (fun s : Set E => s ∈ p.basisSets) id) :
    WithSeminorms p :=
  p.withSeminorms_of_nhds <|
    Filter.HasBasis.eq_of_same_basis h p.addGroupFilterBasis.toFilterBasis.hasBasis

Topology Induced by Seminorms via Basis Condition

Informal description

Let $E$ be a topological vector space over a field $\mathbb{K}$ with a topology that makes addition continuous (i.e., $E$ is a topological additive group). Given a family of seminorms $p = (p_i)_{i \in \iota}$ on $E$, if the neighborhood filter of $0$ in $E$ has a basis consisting of the sets in `p.basisSets` (i.e., the open seminorm balls centered at 0), then the topology on $E$ is induced by the family of seminorms $p$.

SeminormFamily.withSeminorms_iff_nhds_eq_iInf theorem

 [IsTopologicalAddGroup E] (p : SeminormFamily 𝕜 E ι) : WithSeminorms p ↔ (𝓝 (0 : E)) = ⨅ i, (𝓝 0).comap (p i)

Full source

theorem SeminormFamily.withSeminorms_iff_nhds_eq_iInf [IsTopologicalAddGroup E]
    (p : SeminormFamily 𝕜 E ι) : WithSeminormsWithSeminorms p ↔ (𝓝 (0 : E)) = ⨅ i, (𝓝 0).comap (p i) := by
  rw [← p.filter_eq_iInf]
  refine ⟨fun h => ?_, p.withSeminorms_of_nhds⟩
  rw [h.topology_eq_withSeminorms]
  exact AddGroupFilterBasis.nhds_zero_eq _

Characterization of Seminorm-Induced Topology via Neighborhood Filters at Zero

Informal description

Let $E$ be a topological vector space over a field $\mathbb{K}$ with a topology that makes addition continuous (i.e., $E$ is a topological additive group). Given a family of seminorms $p = (p_i)_{i \in \iota}$ on $E$, the topology on $E$ is induced by $p$ if and only if the neighborhood filter of $0$ in $E$ equals the infimum over $i \in \iota$ of the preimage filters of the neighborhood filter of $0$ in $\mathbb{R}$ under each seminorm $p_i$. In other words, $\text{WithSeminorms}\, p$ holds precisely when $\mathcal{N}_E(0) = \bigwedge_{i \in \iota} p_i^{-1}(\mathcal{N}_{\mathbb{R}}(0))$, where $\mathcal{N}_E(0)$ and $\mathcal{N}_{\mathbb{R}}(0)$ denote the neighborhood filters of $0$ in $E$ and $\mathbb{R}$, respectively.

SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf theorem

 [IsTopologicalAddGroup E] (p : SeminormFamily 𝕜 E ι) :
  WithSeminorms p ↔ t = ⨅ i, (p i).toSeminormedAddCommGroup.toUniformSpace.toTopologicalSpace

Full source

/-- The topology induced by a family of seminorms is exactly the infimum of the ones induced by
each seminorm individually. We express this as a characterization of `WithSeminorms p`. -/
theorem SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf [IsTopologicalAddGroup E]
    (p : SeminormFamily 𝕜 E ι) :
    WithSeminormsWithSeminorms p ↔
      t = ⨅ i, (p i).toSeminormedAddCommGroup.toUniformSpace.toTopologicalSpace := by
  rw [p.withSeminorms_iff_nhds_eq_iInf,
    IsTopologicalAddGroup.ext_iff inferInstance (topologicalAddGroup_iInf fun i => inferInstance),
    nhds_iInf]
  congrm _ = ⨅ i, ?_
  exact @comap_norm_nhds_zero _ (p i).toSeminormedAddGroup

Topology Induced by Seminorms as Infimum of Individual Topologies

Informal description

Let $E$ be a topological vector space over a field $\mathbb{K}$ with a topology that makes addition continuous (i.e., $E$ is a topological additive group). Given a family of seminorms $p = (p_i)_{i \in \iota}$ on $E$, the topology on $E$ is induced by $p$ if and only if the topology $\tau$ on $E$ equals the infimum of the topologies induced by each seminorm $p_i$ (where each $p_i$ is viewed as inducing a topology via its associated seminormed additive commutative group structure). In other words, $\text{WithSeminorms}\, p$ holds precisely when $\tau = \bigwedge_{i \in \iota} \tau_i$, where $\tau_i$ is the topology induced by the seminorm $p_i$.

WithSeminorms.continuous_seminorm theorem

{p : SeminormFamily 𝕜 E ι} (hp : WithSeminorms p) (i : ι) : Continuous (p i)

Full source

theorem WithSeminorms.continuous_seminorm {p : SeminormFamily 𝕜 E ι} (hp : WithSeminorms p)
    (i : ι) : Continuous (p i) := by
  have := hp.topologicalAddGroup
  rw [p.withSeminorms_iff_topologicalSpace_eq_iInf.mp hp]
  exact continuous_iInf_dom (@continuous_norm _ (p i).toSeminormedAddGroup)

Continuity of Seminorms in Seminorm-Induced Topology

Informal description

Let $E$ be a vector space over a field $\mathbb{K}$ equipped with a topology induced by a family of seminorms $p = (p_i)_{i \in \iota}$. Then for each index $i \in \iota$, the seminorm $p_i : E \to \mathbb{R}$ is a continuous function.

SeminormFamily.withSeminorms_iff_uniformSpace_eq_iInf theorem

 [u : UniformSpace E] [IsUniformAddGroup E] (p : SeminormFamily 𝕜 E ι) :
  WithSeminorms p ↔ u = ⨅ i, (p i).toSeminormedAddCommGroup.toUniformSpace

Full source

/-- The uniform structure induced by a family of seminorms is exactly the infimum of the ones
induced by each seminorm individually. We express this as a characterization of
`WithSeminorms p`. -/
theorem SeminormFamily.withSeminorms_iff_uniformSpace_eq_iInf [u : UniformSpace E]
    [IsUniformAddGroup E] (p : SeminormFamily 𝕜 E ι) :
    WithSeminormsWithSeminorms p ↔ u = ⨅ i, (p i).toSeminormedAddCommGroup.toUniformSpace := by
  rw [p.withSeminorms_iff_nhds_eq_iInf,
    IsUniformAddGroup.ext_iff inferInstance (isUniformAddGroup_iInf fun i => inferInstance),
    UniformSpace.toTopologicalSpace_iInf, nhds_iInf]
  congrm _ = ⨅ i, ?_
  exact @comap_norm_nhds_zero _ (p i).toAddGroupSeminorm.toSeminormedAddGroup

Uniform Structure Characterization of Seminorm-Induced Topology

Informal description

Let $E$ be a topological vector space over a field $\mathbb{K}$ equipped with a uniform structure $u$ that makes addition uniformly continuous (i.e., $E$ is a uniform additive group). Given a family of seminorms $p = (p_i)_{i \in \iota}$ on $E$, the topology on $E$ is induced by $p$ if and only if the uniform structure $u$ on $E$ is equal to the infimum of the uniform structures induced by each seminorm $p_i$ individually. In other words, $\text{WithSeminorms}\, p$ holds precisely when the uniform structure $u$ on $E$ satisfies $u = \bigwedge_{i \in \iota} u_i$, where $u_i$ is the uniform structure induced by the seminorm $p_i$.

norm_withSeminorms theorem

 (𝕜 E) [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : WithSeminorms fun _ : Fin 1 => normSeminorm 𝕜 E

Full source

/-- The topology of a `NormedSpace 𝕜 E` is induced by the seminorm `normSeminorm 𝕜 E`. -/
theorem norm_withSeminorms (𝕜 E) [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] :
    WithSeminorms fun _ : Fin 1 => normSeminorm 𝕜 E := by
  let p : SeminormFamily 𝕜 E (Fin 1) := fun _ => normSeminorm 𝕜 E
  refine
    ⟨SeminormedAddCommGroup.toIsTopologicalAddGroup.ext
        p.addGroupFilterBasis.isTopologicalAddGroup ?_⟩
  refine Filter.HasBasis.eq_of_same_basis Metric.nhds_basis_ball ?_
  rw [← ball_normSeminorm 𝕜 E]
  refine
    Filter.HasBasis.to_hasBasis p.addGroupFilterBasis.nhds_zero_hasBasis ?_ fun r hr =>
      ⟨(normSeminorm 𝕜 E).ball 0 r, p.basisSets_singleton_mem 0 hr, rfl.subset⟩
  rintro U (hU : U ∈ p.basisSets)
  rcases p.basisSets_iff.mp hU with ⟨s, r, hr, hU⟩
  use r, hr
  rw [hU, id]
  by_cases h : s.Nonempty
  · rw [Finset.sup_const h]
  rw [Finset.not_nonempty_iff_eq_empty.mp h, Finset.sup_empty, ball_bot _ hr]
  exact Set.subset_univ _

Norm Topology is Induced by the Norm Seminorm

Informal description

For a normed space $E$ over a normed field $\mathbb{K}$, the topology on $E$ is induced by the single seminorm $\| \cdot \|_{\mathbb{K}, E}$, where $\| \cdot \|_{\mathbb{K}, E}$ is the norm seminorm associated with the normed space structure on $E$.

WithSeminorms.isVonNBounded_iff_finset_seminorm_bounded theorem

 {s : Set E} (hp : WithSeminorms p) : Bornology.IsVonNBounded 𝕜 s ↔ ∀ I : Finset ι, ∃ r > 0, ∀ x ∈ s, I.sup p x < r

Full source

theorem WithSeminorms.isVonNBounded_iff_finset_seminorm_bounded {s : Set E} (hp : WithSeminorms p) :
    Bornology.IsVonNBoundedBornology.IsVonNBounded 𝕜 s ↔ ∀ I : Finset ι, ∃ r > 0, ∀ x ∈ s, I.sup p x < r := by
  rw [hp.hasBasis.isVonNBounded_iff]
  constructor
  · intro h I
    simp only [id] at h
    specialize h ((I.sup p).ball 0 1) (p.basisSets_mem I zero_lt_one)
    rcases h.exists_pos with ⟨r, hr, h⟩
    obtain ⟨a, ha⟩ := NormedField.exists_lt_norm 𝕜 r
    specialize h a (le_of_lt ha)
    rw [Seminorm.smul_ball_zero (norm_pos_iff.1 <| hr.trans ha), mul_one] at h
    refine ⟨‖a‖, lt_trans hr ha, ?_⟩
    intro x hx
    specialize h hx
    exact (Finset.sup I p).mem_ball_zero.mp h
  intro h s' hs'
  rcases p.basisSets_iff.mp hs' with ⟨I, r, hr, hs'⟩
  rw [id, hs']
  rcases h I with ⟨r', _, h'⟩
  simp_rw [← (I.sup p).mem_ball_zero] at h'
  refine Absorbs.mono_right ?_ h'
  exact (Finset.sup I p).ball_zero_absorbs_ball_zero hr

Characterization of von Neumann bounded sets via finite seminorm bounds

Informal description

Let $E$ be a topological vector space over a field $\mathbb{K}$ with topology induced by a family of seminorms $p : \iota \to \text{Seminorm}\, \mathbb{K}\, E$. A subset $s \subseteq E$ is von Neumann bounded if and only if for every finite subset $I \subseteq \iota$, there exists a positive real number $r > 0$ such that $\sup_{i \in I} p_i(x) < r$ for all $x \in s$.

WithSeminorms.image_isVonNBounded_iff_finset_seminorm_bounded theorem

 (f : G → E) {s : Set G} (hp : WithSeminorms p) :
  Bornology.IsVonNBounded 𝕜 (f '' s) ↔ ∀ I : Finset ι, ∃ r > 0, ∀ x ∈ s, I.sup p (f x) < r

Full source

theorem WithSeminorms.image_isVonNBounded_iff_finset_seminorm_bounded (f : G → E) {s : Set G}
    (hp : WithSeminorms p) :
    Bornology.IsVonNBoundedBornology.IsVonNBounded 𝕜 (f '' s) ↔
      ∀ I : Finset ι, ∃ r > 0, ∀ x ∈ s, I.sup p (f x) < r := by
  simp_rw [hp.isVonNBounded_iff_finset_seminorm_bounded, Set.forall_mem_image]

Image von Neumann Boundedness via Finite Seminorm Bounds

Informal description

Let $E$ be a topological vector space over a field $\mathbb{K}$ with topology induced by a family of seminorms $p : \iota \to \text{Seminorm}\, \mathbb{K}\, E$. For a function $f : G \to E$ and a subset $s \subseteq G$, the image $f(s)$ is von Neumann bounded in $E$ if and only if for every finite subset $I \subseteq \iota$, there exists a positive real number $r > 0$ such that $\sup_{i \in I} p_i(f(x)) < r$ for all $x \in s$.

WithSeminorms.isVonNBounded_iff_seminorm_bounded theorem

{s : Set E} (hp : WithSeminorms p) : Bornology.IsVonNBounded 𝕜 s ↔ ∀ i : ι, ∃ r > 0, ∀ x ∈ s, p i x < r

Full source

theorem WithSeminorms.isVonNBounded_iff_seminorm_bounded {s : Set E} (hp : WithSeminorms p) :
    Bornology.IsVonNBoundedBornology.IsVonNBounded 𝕜 s ↔ ∀ i : ι, ∃ r > 0, ∀ x ∈ s, p i x < r := by
  rw [hp.isVonNBounded_iff_finset_seminorm_bounded]
  constructor
  · intro hI i
    convert hI {i}
    rw [Finset.sup_singleton]
  intro hi I
  by_cases hI : I.Nonempty
  · choose r hr h using hi
    have h' : 0 < I.sup' hI r := by
      rcases hI with ⟨i, hi⟩
      exact lt_of_lt_of_le (hr i) (Finset.le_sup' r hi)
    refine ⟨I.sup' hI r, h', fun x hx => finset_sup_apply_lt h' fun i hi => ?_⟩
    refine lt_of_lt_of_le (h i x hx) ?_
    simp only [Finset.le_sup'_iff, exists_prop]
    exact ⟨i, hi, (Eq.refl _).le⟩
  simp only [Finset.not_nonempty_iff_eq_empty.mp hI, Finset.sup_empty, coe_bot, Pi.zero_apply,
    exists_prop]
  exact ⟨1, zero_lt_one, fun _ _ => zero_lt_one⟩

Characterization of von Neumann bounded sets via seminorm bounds

Informal description

Let $E$ be a topological vector space over a field $\mathbb{K}$ with topology induced by a family of seminorms $(p_i)_{i \in \iota}$. A subset $s \subseteq E$ is von Neumann bounded if and only if for every seminorm $p_i$ in the family, there exists a positive real number $r > 0$ such that $p_i(x) < r$ for all $x \in s$.

WithSeminorms.image_isVonNBounded_iff_seminorm_bounded theorem

 (f : G → E) {s : Set G} (hp : WithSeminorms p) :
  Bornology.IsVonNBounded 𝕜 (f '' s) ↔ ∀ i : ι, ∃ r > 0, ∀ x ∈ s, p i (f x) < r

Full source

theorem WithSeminorms.image_isVonNBounded_iff_seminorm_bounded (f : G → E) {s : Set G}
    (hp : WithSeminorms p) :
    Bornology.IsVonNBoundedBornology.IsVonNBounded 𝕜 (f '' s) ↔ ∀ i : ι, ∃ r > 0, ∀ x ∈ s, p i (f x) < r := by
  simp_rw [hp.isVonNBounded_iff_seminorm_bounded, Set.forall_mem_image]

Image von Neumann Boundedness via Seminorm Bounds

Informal description

Let $E$ be a topological vector space over a field $\mathbb{K}$ with topology induced by a family of seminorms $(p_i)_{i \in \iota}$. For a function $f : G \to E$ and a subset $s \subseteq G$, the image $f(s)$ is von Neumann bounded in $E$ if and only if for every seminorm $p_i$ in the family, there exists a positive real number $r > 0$ such that $p_i(f(x)) < r$ for all $x \in s$.

Seminorm.continuous_of_continuous_comp theorem

 {q : SeminormFamily 𝕝₂ F ι'} [TopologicalSpace E] [IsTopologicalAddGroup E] [TopologicalSpace F] (hq : WithSeminorms q)
  (f : E →ₛₗ[τ₁₂] F) (hf : ∀ i, Continuous ((q i).comp f)) : Continuous f

Full source

theorem continuous_of_continuous_comp {q : SeminormFamily 𝕝₂ F ι'} [TopologicalSpace E]
    [IsTopologicalAddGroup E] [TopologicalSpace F] (hq : WithSeminorms q)
    (f : E →ₛₗ[τ₁₂] F) (hf : ∀ i, Continuous ((q i).comp f)) : Continuous f := by
  have : IsTopologicalAddGroup F := hq.topologicalAddGroup
  refine continuous_of_continuousAt_zero f ?_
  simp_rw [ContinuousAt, f.map_zero, q.withSeminorms_iff_nhds_eq_iInf.mp hq, Filter.tendsto_iInf,
    Filter.tendsto_comap_iff]
  intro i
  convert (hf i).continuousAt.tendsto
  exact (map_zero _).symm

Continuity of Semilinear Maps via Continuous Compositions with Seminorms

Informal description

Let $E$ and $F$ be topological vector spaces over fields $\mathbb{K}_1$ and $\mathbb{K}_2$ respectively, with $E$ equipped with a topology that makes it a topological additive group. Suppose the topology on $F$ is induced by a family of seminorms $q = (q_i)_{i \in \iota'}$. Given a semilinear map $f \colon E \to F$ (with respect to some ring homomorphism $\tau_{12} \colon \mathbb{K}_1 \to \mathbb{K}_2$), if for every seminorm $q_i$ in the family $q$, the composition $q_i \circ f$ is continuous, then $f$ itself is continuous.

Seminorm.continuous_iff_continuous_comp theorem

 {q : SeminormFamily 𝕜₂ F ι'} [TopologicalSpace E] [IsTopologicalAddGroup E] [TopologicalSpace F] (hq : WithSeminorms q)
  (f : E →ₛₗ[σ₁₂] F) : Continuous f ↔ ∀ i, Continuous ((q i).comp f)

Full source

theorem continuous_iff_continuous_comp {q : SeminormFamily 𝕜₂ F ι'} [TopologicalSpace E]
    [IsTopologicalAddGroup E] [TopologicalSpace F] (hq : WithSeminorms q) (f : E →ₛₗ[σ₁₂] F) :
    ContinuousContinuous f ↔ ∀ i, Continuous ((q i).comp f) :=
  ⟨fun h i => (hq.continuous_seminorm i).comp h, continuous_of_continuous_comp hq f⟩

Continuity Criterion for Semilinear Maps via Seminorm Compositions

Informal description

Let $E$ and $F$ be topological vector spaces over fields $\mathbb{K}_1$ and $\mathbb{K}_2$ respectively, where $E$ is equipped with a topology making it a topological additive group. Suppose the topology on $F$ is induced by a family of seminorms $(q_i)_{i \in \iota'}$. Given a $\sigma_{12}$-semilinear map $f \colon E \to F$, the following are equivalent: 1. $f$ is continuous. 2. For every seminorm $q_i$ in the family, the composition $q_i \circ f$ is continuous.

Seminorm.continuous_from_bounded theorem

 {p : SeminormFamily 𝕝 E ι} {q : SeminormFamily 𝕝₂ F ι'} {_ : TopologicalSpace E} (hp : WithSeminorms p)
  {_ : TopologicalSpace F} (hq : WithSeminorms q) (f : E →ₛₗ[τ₁₂] F) (hf : Seminorm.IsBounded p q f) : Continuous f

Full source

theorem continuous_from_bounded {p : SeminormFamily 𝕝 E ι} {q : SeminormFamily 𝕝₂ F ι'}
    {_ : TopologicalSpace E} (hp : WithSeminorms p) {_ : TopologicalSpace F} (hq : WithSeminorms q)
    (f : E →ₛₗ[τ₁₂] F) (hf : Seminorm.IsBounded p q f) : Continuous f := by
  have : IsTopologicalAddGroup E := hp.topologicalAddGroup
  refine continuous_of_continuous_comp hq _ fun i => ?_
  rcases hf i with ⟨s, C, hC⟩
  rw [← Seminorm.finset_sup_smul] at hC
  -- Note: we deduce continuouty of `s.sup (C • p)` from that of `∑ i ∈ s, C • p i`.
  -- The reason is that there is no `continuous_finset_sup`, and even if it were we couldn't
  -- really use it since `ℝ` is not an `OrderBot`.
  refine Seminorm.continuous_of_le ?_ (hC.trans <| Seminorm.finset_sup_le_sum _ _)
  change Continuous (fun x ↦ Seminorm.coeFnAddMonoidHom _ _ (∑ i ∈ s, C • p i) x)
  simp_rw [map_sum, Finset.sum_apply]
  exact (continuous_finset_sum _ fun i _ ↦ (hp.continuous_seminorm i).const_smul (C : ℝ))

Continuity of Bounded Semilinear Maps Between Seminorm-Induced Spaces

Informal description

Let $E$ and $F$ be topological vector spaces over fields $\mathbb{K}_1$ and $\mathbb{K}_2$ respectively, with topologies induced by families of seminorms $p = (p_i)_{i \in \iota}$ and $q = (q_j)_{j \in \iota'}$. Given a $\tau_{12}$-semilinear map $f \colon E \to F$, if $f$ is bounded with respect to the seminorm families $p$ and $q$, then $f$ is continuous.

Seminorm.cont_withSeminorms_normedSpace theorem

 (F) [SeminormedAddCommGroup F] [NormedSpace 𝕝₂ F] [TopologicalSpace E] {p : ι → Seminorm 𝕝 E} (hp : WithSeminorms p)
  (f : E →ₛₗ[τ₁₂] F) (hf : ∃ (s : Finset ι) (C : ℝ≥0), (normSeminorm 𝕝₂ F).comp f ≤ C • s.sup p) : Continuous f

Full source

theorem cont_withSeminorms_normedSpace (F) [SeminormedAddCommGroup F] [NormedSpace 𝕝₂ F]
    [TopologicalSpace E] {p : ι → Seminorm 𝕝 E} (hp : WithSeminorms p)
    (f : E →ₛₗ[τ₁₂] F) (hf : ∃ (s : Finset ι) (C : ℝ≥0), (normSeminorm 𝕝₂ F).comp f ≤ C • s.sup p) :
    Continuous f := by
  rw [← Seminorm.isBounded_const (Fin 1)] at hf
  exact continuous_from_bounded hp (norm_withSeminorms 𝕝₂ F) f hf

Continuity of Bounded Semilinear Maps from Seminorm-Induced Space to Normed Space

Informal description

Let $E$ be a topological vector space over a field $\mathbb{K}_1$ with topology induced by a family of seminorms $p = (p_i)_{i \in \iota}$, and let $F$ be a seminormed additive commutative group over a field $\mathbb{K}_2$ equipped with the norm topology. Given a $\tau_{12}$-semilinear map $f \colon E \to F$, if there exists a finite subset $s \subseteq \iota$ and a constant $C \geq 0$ such that the composition of the norm seminorm on $F$ with $f$ is bounded by $C$ times the supremum of the seminorms $\{p_j\}_{j \in s}$, then $f$ is continuous.

WithSeminorms.equicontinuous_TFAE theorem

 {κ : Type*} {q : SeminormFamily 𝕜₂ F ι'} [UniformSpace E] [IsUniformAddGroup E] [u : UniformSpace F]
  [hu : IsUniformAddGroup F] (hq : WithSeminorms q) [ContinuousSMul 𝕜 E] (f : κ → E →ₛₗ[σ₁₂] F) :
  TFAE
    [EquicontinuousAt ((↑) ∘ f) 0, Equicontinuous ((↑) ∘ f), UniformEquicontinuous ((↑) ∘ f),
      ∀ i, ∃ p : Seminorm 𝕜 E, Continuous p ∧ ∀ k, (q i).comp (f k) ≤ p,
      ∀ i, BddAbove (range fun k ↦ (q i).comp (f k)) ∧ Continuous (⨆ k, (q i).comp (f k))]

Full source

/-- Let `E` and `F` be two topological vector spaces over a `NontriviallyNormedField`, and assume
that the topology of `F` is generated by some family of seminorms `q`. For a family `f` of linear
maps from `E` to `F`, the following are equivalent:
* `f` is equicontinuous at `0`.
* `f` is equicontinuous.
* `f` is uniformly equicontinuous.
* For each `q i`, the family of seminorms `k ↦ (q i) ∘ (f k)` is bounded by some continuous
  seminorm `p` on `E`.
* For each `q i`, the seminorm `⊔ k, (q i) ∘ (f k)` is well-defined and continuous.

In particular, if you can determine all continuous seminorms on `E`, that gives you a complete
characterization of equicontinuity for linear maps from `E` to `F`. For example `E` and `F` are
both normed spaces, you get `NormedSpace.equicontinuous_TFAE`. -/
protected theorem _root_.WithSeminorms.equicontinuous_TFAE {κ : Type*}
    {q : SeminormFamily 𝕜₂ F ι'} [UniformSpace E] [IsUniformAddGroup E] [u : UniformSpace F]
    [hu : IsUniformAddGroup F] (hq : WithSeminorms q) [ContinuousSMul 𝕜 E]
    (f : κ → E →ₛₗ[σ₁₂] F) : TFAE
    [ EquicontinuousAt ((↑) ∘ f) 0,
      Equicontinuous ((↑) ∘ f),
      UniformEquicontinuous ((↑) ∘ f),
      ∀ i, ∃ p : Seminorm 𝕜 E, Continuous p ∧ ∀ k, (q i).comp (f k) ≤ p,
      ∀ i, BddAbove (range fun k ↦ (q i).comp (f k)) ∧ Continuous (⨆ k, (q i).comp (f k)) ] := by
  -- We start by reducing to the case where the target is a seminormed space
  rw [q.withSeminorms_iff_uniformSpace_eq_iInf.mp hq, uniformEquicontinuous_iInf_rng,
      equicontinuous_iInf_rng, equicontinuousAt_iInf_rng]
  refine forall_tfae [_, _, _, _, _] fun i ↦ ?_
  let _ : SeminormedAddCommGroup F := (q i).toSeminormedAddCommGroup
  clear u hu hq
  -- Now we can prove the equivalence in this setting
  simp only [List.map]
  tfae_have 1 → 3 := uniformEquicontinuous_of_equicontinuousAt_zero f
  tfae_have 3 → 2 := UniformEquicontinuous.equicontinuous
  tfae_have 2 → 1 := fun H ↦ H 0
  tfae_have 3 → 5
  | H => by
    have : ∀ᶠ x in 𝓝 0, ∀ k, q i (f k x) ≤ 1 := by
      filter_upwards [Metric.equicontinuousAt_iff_right.mp (H.equicontinuous 0) 1 one_pos]
        with x hx k
      simpa using (hx k).le
    have bdd : BddAbove (range fun k ↦ (q i).comp (f k)) :=
      Seminorm.bddAbove_of_absorbent (absorbent_nhds_zero this)
        (fun x hx ↦ ⟨1, forall_mem_range.mpr hx⟩)
    rw [← Seminorm.coe_iSup_eq bdd]
    refine ⟨bdd, Seminorm.continuous' (r := 1) ?_⟩
    filter_upwards [this] with x hx
    simpa only [closedBall_iSup bdd _ one_pos, mem_iInter, mem_closedBall_zero] using hx
  tfae_have 5 → 4 := fun H ↦ ⟨⨆ k, (q i).comp (f k), Seminorm.coe_iSup_eq H.1 ▸ H.2, le_ciSup H.1⟩
  tfae_have 4 → 1 -- This would work over any `NormedField`
  | ⟨p, hp, hfp⟩ =>
    Metric.equicontinuousAt_of_continuity_modulus p (map_zero p ▸ hp.tendsto 0) _ <|
      Eventually.of_forall fun x k ↦ by simpa using hfp k x
  tfae_finish

Equicontinuity Characterization for Families of Linear Maps in Seminormed Spaces

Informal description

Let $E$ and $F$ be topological vector spaces over a nontrivially normed field $\mathbb{K}$, with $F$ equipped with a family of seminorms $q = (q_i)_{i \in \iota'}$ inducing its topology. Let $\kappa$ be an index set and $f = (f_k)_{k \in \kappa}$ be a family of linear maps $f_k : E \to F$. The following statements are equivalent: 1. The family $f$ is equicontinuous at $0$. 2. The family $f$ is equicontinuous. 3. The family $f$ is uniformly equicontinuous. 4. For each seminorm $q_i$, there exists a continuous seminorm $p$ on $E$ such that $q_i \circ f_k \leq p$ for all $k \in \kappa$. 5. For each seminorm $q_i$, the family $(q_i \circ f_k)_{k \in \kappa}$ is bounded above and the seminorm $\sup_{k \in \kappa} (q_i \circ f_k)$ is continuous.

WithSeminorms.uniformEquicontinuous_iff_exists_continuous_seminorm theorem

 {κ : Type*} {q : SeminormFamily 𝕜₂ F ι'} [UniformSpace E] [IsUniformAddGroup E] [u : UniformSpace F]
  [IsUniformAddGroup F] (hq : WithSeminorms q) [ContinuousSMul 𝕜 E] (f : κ → E →ₛₗ[σ₁₂] F) :
  UniformEquicontinuous ((↑) ∘ f) ↔ ∀ i, ∃ p : Seminorm 𝕜 E, Continuous p ∧ ∀ k, (q i).comp (f k) ≤ p

Full source

theorem _root_.WithSeminorms.uniformEquicontinuous_iff_exists_continuous_seminorm {κ : Type*}
    {q : SeminormFamily 𝕜₂ F ι'} [UniformSpace E] [IsUniformAddGroup E] [u : UniformSpace F]
    [IsUniformAddGroup F] (hq : WithSeminorms q) [ContinuousSMul 𝕜 E]
    (f : κ → E →ₛₗ[σ₁₂] F) :
    UniformEquicontinuousUniformEquicontinuous ((↑) ∘ f) ↔
    ∀ i, ∃ p : Seminorm 𝕜 E, Continuous p ∧ ∀ k, (q i).comp (f k) ≤ p :=
  (hq.equicontinuous_TFAE f).out 2 3

Uniform Equicontinuity Characterization via Continuous Seminorms

Informal description

Let $E$ and $F$ be topological vector spaces over a field $\mathbb{K}$, where $F$ is equipped with a family of seminorms $q = (q_i)_{i \in \iota'}$ inducing its topology. Let $\kappa$ be an index set and $f = (f_k)_{k \in \kappa}$ be a family of linear maps $f_k : E \to F$. Then the family $f$ is uniformly equicontinuous if and only if for each seminorm $q_i$ in $F$, there exists a continuous seminorm $p$ on $E$ such that $q_i \circ f_k \leq p$ for all $k \in \kappa$.

WithSeminorms.uniformEquicontinuous_iff_bddAbove_and_continuous_iSup theorem

 {κ : Type*} {q : SeminormFamily 𝕜₂ F ι'} [UniformSpace E] [IsUniformAddGroup E] [u : UniformSpace F]
  [IsUniformAddGroup F] (hq : WithSeminorms q) [ContinuousSMul 𝕜 E] (f : κ → E →ₛₗ[σ₁₂] F) :
  UniformEquicontinuous ((↑) ∘ f) ↔ ∀ i, BddAbove (range fun k ↦ (q i).comp (f k)) ∧ Continuous (⨆ k, (q i).comp (f k))

Full source

theorem _root_.WithSeminorms.uniformEquicontinuous_iff_bddAbove_and_continuous_iSup {κ : Type*}
    {q : SeminormFamily 𝕜₂ F ι'} [UniformSpace E] [IsUniformAddGroup E] [u : UniformSpace F]
    [IsUniformAddGroup F] (hq : WithSeminorms q) [ContinuousSMul 𝕜 E]
    (f : κ → E →ₛₗ[σ₁₂] F) :
    UniformEquicontinuousUniformEquicontinuous ((↑) ∘ f) ↔ ∀ i,
    BddAbove (range fun k ↦ (q i).comp (f k)) ∧
      Continuous (⨆ k, (q i).comp (f k)) :=
  (hq.equicontinuous_TFAE f).out 2 4

Uniform Equicontinuity Characterization via Boundedness and Continuity of Supremum Seminorms

Informal description

Let $E$ and $F$ be topological vector spaces over a field $\mathbb{K}$, where $F$ is equipped with a family of seminorms $q = (q_i)_{i \in \iota'}$ inducing its topology. Let $\kappa$ be an index set and $f = (f_k)_{k \in \kappa}$ be a family of linear maps $f_k : E \to F$. Then the family $f$ is uniformly equicontinuous if and only if for each seminorm $q_i$, the family $(q_i \circ f_k)_{k \in \kappa}$ is bounded above and the seminorm $\sup_{k \in \kappa} (q_i \circ f_k)$ is continuous on $E$.

WithSeminorms.congr theorem

 {p : SeminormFamily 𝕜 E ι} {q : SeminormFamily 𝕜 E ι'} [t : TopologicalSpace E] (hp : WithSeminorms p)
  (hpq : Seminorm.IsBounded p q LinearMap.id) (hqp : Seminorm.IsBounded q p LinearMap.id) : WithSeminorms q

Full source

/-- Two families of seminorms `p` and `q` on the same space generate the same topology
if each `p i` is bounded by some `C • Finset.sup s q` and vice-versa.

We formulate these boundedness assumptions as `Seminorm.IsBounded q p LinearMap.id` (and
vice-versa) to reuse the API. Furthermore, we don't actually state it as an equality of topologies
but as a way to deduce `WithSeminorms q` from `WithSeminorms p`, since this should be more
useful in practice. -/
protected theorem congr {p : SeminormFamily 𝕜 E ι} {q : SeminormFamily 𝕜 E ι'}
    [t : TopologicalSpace E] (hp : WithSeminorms p) (hpq : Seminorm.IsBounded p q LinearMap.id)
    (hqp : Seminorm.IsBounded q p LinearMap.id) : WithSeminorms q := by
  constructor
  rw [hp.topology_eq_withSeminorms]
  clear hp t
  refine le_antisymm ?_ ?_ <;>
  rw [← continuous_id_iff_le] <;>
  refine continuous_from_bounded (.mk (topology := _) rfl) (.mk (topology := _) rfl)
    LinearMap.id (by assumption)

Equivalence of Topologies Induced by Mutually Bounded Seminorm Families

Informal description

Let $E$ be a vector space over a field $\mathbb{K}$ with two families of seminorms $p = (p_i)_{i \in \iota}$ and $q = (q_j)_{j \in \iota'}$. Suppose the topology on $E$ is induced by the family $p$ (i.e., `WithSeminorms p` holds). If the identity map $\text{id} \colon E \to E$ is bounded with respect to both $(p,q)$ and $(q,p)$ (i.e., for each $q_j$ there exists a finite subset $s \subseteq \iota$ and $C > 0$ such that $q_j \leq C \sup_{i \in s} p_i$, and vice versa), then the topology is also induced by the family $q$ (i.e., `WithSeminorms q` holds).

WithSeminorms.finset_sups theorem

 {p : SeminormFamily 𝕜 E ι} [TopologicalSpace E] (hp : WithSeminorms p) : WithSeminorms (fun s : Finset ι ↦ s.sup p)

Full source

protected theorem finset_sups {p : SeminormFamily 𝕜 E ι} [TopologicalSpace E]
    (hp : WithSeminorms p) : WithSeminorms (fun s : Finset ι ↦ s.sup p) := by
  refine hp.congr ?_ ?_
  · intro s
    refine ⟨s, 1, ?_⟩
    rw [one_smul]
    rfl
  · intro i
    refine ⟨{{i}}, 1, ?_⟩
    rw [Finset.sup_singleton, Finset.sup_singleton, one_smul]
    rfl

Topology induced by finite suprema of seminorms

Informal description

Let $E$ be a vector space over a field $\mathbb{K}$ equipped with a family of seminorms $p = (p_i)_{i \in \iota}$ that induces the topology on $E$. Then the topology on $E$ is also induced by the family of seminorms obtained by taking the supremum over finite subsets of $\iota$, i.e., $\left( \sup_{i \in s} p_i \right)_{s \in \text{Finset}(\iota)}$.

WithSeminorms.partial_sups theorem

 [Preorder ι] [LocallyFiniteOrderBot ι] {p : SeminormFamily 𝕜 E ι} [TopologicalSpace E] (hp : WithSeminorms p) :
  WithSeminorms (fun i ↦ (Finset.Iic i).sup p)

Full source

protected theorem partial_sups [Preorder ι] [LocallyFiniteOrderBot ι] {p : SeminormFamily 𝕜 E ι}
    [TopologicalSpace E] (hp : WithSeminorms p) : WithSeminorms (fun i ↦ (Finset.Iic i).sup p) := by
  refine hp.congr ?_ ?_
  · intro i
    refine ⟨Finset.Iic i, 1, ?_⟩
    rw [one_smul]
    rfl
  · intro i
    refine ⟨{i}, 1, ?_⟩
    rw [Finset.sup_singleton, one_smul]
    exact (Finset.le_sup (Finset.mem_Iic.mpr le_rfl) : p i ≤ (Finset.Iic i).sup p)

Topology Induced by Partial Suprema of Seminorms

Informal description

Let $\iota$ be a preorder with a locally finite order and a bottom element, and let $E$ be a topological vector space over a field $\mathbb{K}$ whose topology is induced by a family of seminorms $p = (p_i)_{i \in \iota}$ (i.e., `WithSeminorms p` holds). Then the topology is also induced by the family of seminorms obtained by taking the supremum over all seminorms $p_j$ with $j \leq i$ for each $i \in \iota$, i.e., $\sup_{j \in \text{Iic}(i)} p_j$, where $\text{Iic}(i)$ denotes the set $\{j \in \iota \mid j \leq i\}$.

WithSeminorms.congr_equiv theorem

 {p : SeminormFamily 𝕜 E ι} [t : TopologicalSpace E] (hp : WithSeminorms p) (e : ι' ≃ ι) : WithSeminorms (p ∘ e)

Full source

protected theorem congr_equiv {p : SeminormFamily 𝕜 E ι} [t : TopologicalSpace E]
    (hp : WithSeminorms p) (e : ι' ≃ ι) : WithSeminorms (p ∘ e) := by
  refine hp.congr ?_ ?_ <;>
  intro i <;>
  [use {e i}, 1; use {e.symm i}, 1] <;>
  simp

Topology Induced by Seminorm Family is Preserved under Index Equivalence

Informal description

Let $E$ be a vector space over a field $\mathbb{K}$ with a topology induced by a family of seminorms $p = (p_i)_{i \in \iota}$ (i.e., `WithSeminorms p` holds). Given an equivalence $e : \iota' \simeq \iota$ between indexing sets, the topology on $E$ is also induced by the family of seminorms $p \circ e = (p_{e(j)})_{j \in \iota'}$ (i.e., `WithSeminorms (p \circ e)` holds).

Seminorm.map_eq_zero_of_norm_zero theorem

(q : Seminorm 𝕜 F) (hq : Continuous q) {x : F} (hx : ‖x‖ = 0) : q x = 0

Full source

/-- In a semi-`NormedSpace`, a continuous seminorm is zero on elements of norm `0`. -/
lemma map_eq_zero_of_norm_zero (q : Seminorm 𝕜 F)
    (hq : Continuous q) {x : F} (hx : ‖x‖ = 0) : q x = 0 :=
  (map_zero q) ▸
    ((specializes_iff_mem_closure.mpr <| mem_closure_zero_iff_norm.mpr hx).map hq).eq.symm

Continuous Seminorm Vanishes on Zero-Norm Elements

Informal description

Let $F$ be a seminormed space over a field $\mathbb{K}$, and let $q$ be a continuous seminorm on $F$. For any element $x \in F$ with zero norm (i.e., $\|x\| = 0$), the seminorm $q$ evaluated at $x$ is zero, i.e., $q(x) = 0$.

Seminorm.bound_of_continuous_normedSpace theorem

(q : Seminorm 𝕜 F) (hq : Continuous q) : ∃ C, 0 < C ∧ (∀ x : F, q x ≤ C * ‖x‖)

Full source

/-- Let `F` be a semi-`NormedSpace` over a `NontriviallyNormedField`, and let `q` be a
seminorm on `F`. If `q` is continuous, then it is uniformly controlled by the norm, that is there
is some `C > 0` such that `∀ x, q x ≤ C * ‖x‖`.
The continuity ensures boundedness on a ball of some radius `ε`. The nontriviality of the
norm is then used to rescale any element into an element of norm in `[ε/C, ε[`, thus with a
controlled image by `q`. The control of `q` at the original element follows by rescaling. -/
lemma bound_of_continuous_normedSpace (q : Seminorm 𝕜 F)
    (hq : Continuous q) : ∃ C, 0 < C ∧ (∀ x : F, q x ≤ C * ‖x‖) := by
  have hq' : Tendsto q (𝓝 0) (𝓝 0) := map_zero q ▸ hq.tendsto 0
  rcases NormedAddCommGroup.nhds_zero_basis_norm_lt.mem_iff.mp (hq' <| Iio_mem_nhds one_pos)
    with ⟨ε, ε_pos, hε⟩
  rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩
  have : 0 < ‖c‖ / ε := by positivity
  refine ⟨‖c‖ / ε, this, fun x ↦ ?_⟩
  by_cases hx : ‖x‖ = 0
  · rw [hx, mul_zero]
    exact le_of_eq (map_eq_zero_of_norm_zero q hq hx)
  · refine (normSeminorm 𝕜 F).bound_of_shell q ε_pos hc (fun x hle hlt ↦ ?_) hx
    refine (le_of_lt <| show q x < _ from hε hlt).trans ?_
    rwa [← div_le_iff₀' this, one_div_div]

Continuous Seminorm is Bounded by Norm

Informal description

Let $F$ be a seminormed space over a nontrivially normed field $\mathbb{K}$, and let $q$ be a continuous seminorm on $F$. Then there exists a constant $C > 0$ such that for all $x \in F$, the seminorm $q(x)$ is bounded by $C$ times the norm of $x$, i.e., $q(x) \leq C \|x\|$.

Seminorm.bound_of_continuous theorem

 [Nonempty ι] [t : TopologicalSpace E] (hp : WithSeminorms p) (q : Seminorm 𝕜 E) (hq : Continuous q) :
  ∃ s : Finset ι, ∃ C : ℝ≥0, C ≠ 0 ∧ q ≤ C • s.sup p

Full source

/-- Let `E` be a topological vector space (over a `NontriviallyNormedField`) whose topology is
generated by some family of seminorms `p`, and let `q` be a seminorm on `E`. If `q` is continuous,
then it is uniformly controlled by *finitely many* seminorms of `p`, that is there
is some finset `s` of the index set and some `C > 0` such that `q ≤ C • s.sup p`. -/
lemma bound_of_continuous [Nonempty ι] [t : TopologicalSpace E] (hp : WithSeminorms p)
    (q : Seminorm 𝕜 E) (hq : Continuous q) :
    ∃ s : Finset ι, ∃ C : ℝ≥0, C ≠ 0 ∧ q ≤ C • s.sup p := by
  -- The continuity of `q` gives us a finset `s` and a real `ε > 0`
  -- such that `hε : (s.sup p).ball 0 ε ⊆ q.ball 0 1`.
  rcases hp.hasBasis.mem_iff.mp (ball_mem_nhds hq one_pos) with ⟨V, hV, hε⟩
  rcases p.basisSets_iff.mp hV with ⟨s, ε, ε_pos, rfl⟩
  -- Now forget that `E` already had a topology and view it as the (semi)normed space
  -- `(E, s.sup p)`.
  clear hp hq t
  let _ : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup
  let _ : NormedSpace 𝕜 E := { norm_smul_le := fun a b ↦ le_of_eq (map_smul_eq_mul (s.sup p) a b) }
  -- The inclusion `hε` tells us exactly that `q` is *still* continuous for this new topology
  have : Continuous q :=
    Seminorm.continuous (r := 1) (mem_of_superset (Metric.ball_mem_nhds _ ε_pos) hε)
  -- Hence we can conclude by applying `bound_of_continuous_normedSpace`.
  rcases bound_of_continuous_normedSpace q this with ⟨C, C_pos, hC⟩
  exact ⟨s, ⟨C, C_pos.le⟩, fun H ↦ C_pos.ne.symm (congr_arg NNReal.toReal H), hC⟩

Continuous Seminorm is Bounded by Finitely Many Seminorms

Informal description

Let $E$ be a topological vector space over a nontrivially normed field $\mathbb{K}$, whose topology is induced by a family of seminorms $p : \iota \to \text{Seminorm}\, \mathbb{K}\, E$. If $q$ is a continuous seminorm on $E$, then there exists a finite subset $s \subseteq \iota$ and a positive constant $C > 0$ such that $q(x) \leq C \sup_{i \in s} p_i(x)$ for all $x \in E$.

WithSeminorms.toLocallyConvexSpace theorem

{p : SeminormFamily 𝕜 E ι} (hp : WithSeminorms p) : LocallyConvexSpace ℝ E

Full source

theorem WithSeminorms.toLocallyConvexSpace {p : SeminormFamily 𝕜 E ι} (hp : WithSeminorms p) :
    LocallyConvexSpace ℝ E := by
  have := hp.topologicalAddGroup
  apply ofBasisZero ℝ E id fun s => s ∈ p.basisSets
  · rw [hp.1, AddGroupFilterBasis.nhds_eq _, AddGroupFilterBasis.N_zero]
    exact FilterBasis.hasBasis _
  · intro s hs
    change s ∈ Set.iUnion _ at hs
    simp_rw [Set.mem_iUnion, Set.mem_singleton_iff] at hs
    rcases hs with ⟨I, r, _, rfl⟩
    exact convex_ball _ _ _

Locally Convex Space Structure Induced by Seminorms

Informal description

Let $E$ be a vector space over a field $\mathbb{K}$ equipped with a topology induced by a family of seminorms $p : \iota \to \text{Seminorm}\, \mathbb{K}\, E$. Then $E$ is a locally convex space over $\mathbb{R}$ under this topology.

NormedSpace.toLocallyConvexSpace' theorem

[NormedSpace 𝕜 E] [Module ℝ E] [IsScalarTower ℝ 𝕜 E] : LocallyConvexSpace ℝ E

Full source

/-- Not an instance since `𝕜` can't be inferred. See `NormedSpace.toLocallyConvexSpace` for a
slightly weaker instance version. -/
theorem NormedSpace.toLocallyConvexSpace' [NormedSpace 𝕜 E] [Module ℝ E] [IsScalarTower ℝ 𝕜 E] :
    LocallyConvexSpace ℝ E :=
  (norm_withSeminorms 𝕜 E).toLocallyConvexSpace

Locally Convex Structure on Normed Spaces with Real Scalar Multiplication

Informal description

For any normed space $E$ over a normed field $\mathbb{K}$ that is also a real vector space with compatible scalar multiplication (i.e., $\mathbb{R}$ and $\mathbb{K}$ actions commute), the space $E$ is locally convex when equipped with the topology induced by its norm.

NormedSpace.toLocallyConvexSpace instance

[NormedSpace ℝ E] : LocallyConvexSpace ℝ E

Full source

/-- See `NormedSpace.toLocallyConvexSpace'` for a slightly stronger version which is not an
instance. -/
instance NormedSpace.toLocallyConvexSpace [NormedSpace ℝ E] : LocallyConvexSpace ℝ E :=
  NormedSpace.toLocallyConvexSpace' ℝ

Normed Spaces over Reals are Locally Convex

Informal description

Every normed space $E$ over the real numbers $\mathbb{R}$ is a locally convex space when equipped with the topology induced by its norm.

SeminormFamily.comp definition

(q : SeminormFamily 𝕜₂ F ι) (f : E →ₛₗ[σ₁₂] F) : SeminormFamily 𝕜 E ι

Full source

/-- The family of seminorms obtained by composing each seminorm by a linear map. -/
def SeminormFamily.comp (q : SeminormFamily 𝕜₂ F ι) (f : E →ₛₗ[σ₁₂] F) : SeminormFamily 𝕜 E ι :=
  fun i => (q i).comp f

Composition of a seminorm family with a semilinear map

Informal description

Given an indexed family of seminorms $ q $ on a vector space $ F $ over a field $ \mathbb{K}_2 $, and a semilinear map $ f : E \to F $ (where $ E $ is a vector space over $ \mathbb{K} $), the composition $ q \circ f $ defines a new indexed family of seminorms on $ E $, where each seminorm in the family is obtained by composing the corresponding seminorm in $ q $ with $ f $.

SeminormFamily.comp_apply theorem

(q : SeminormFamily 𝕜₂ F ι) (i : ι) (f : E →ₛₗ[σ₁₂] F) : q.comp f i = (q i).comp f

Full source

theorem SeminormFamily.comp_apply (q : SeminormFamily 𝕜₂ F ι) (i : ι) (f : E →ₛₗ[σ₁₂] F) :
    q.comp f i = (q i).comp f :=
  rfl

Composition of Seminorm Family with Semilinear Map Preserves Individual Seminorms

Informal description

Given an indexed family of seminorms $ q $ on a vector space $ F $ over a field $ \mathbb{K}_2 $, a semilinear map $ f : E \to F $ (where $ E $ is a vector space over $ \mathbb{K} $), and an index $ i \in \iota $, the $ i $-th seminorm in the composed family $ q \circ f $ is equal to the composition of the $ i $-th seminorm $ q_i $ with $ f $. That is, $ (q \circ f)_i = q_i \circ f $.

SeminormFamily.finset_sup_comp theorem

(q : SeminormFamily 𝕜₂ F ι) (s : Finset ι) (f : E →ₛₗ[σ₁₂] F) : (s.sup q).comp f = s.sup (q.comp f)

Full source

theorem SeminormFamily.finset_sup_comp (q : SeminormFamily 𝕜₂ F ι) (s : Finset ι)
    (f : E →ₛₗ[σ₁₂] F) : (s.sup q).comp f = s.sup (q.comp f) := by
  ext x
  rw [Seminorm.comp_apply, Seminorm.finset_sup_apply, Seminorm.finset_sup_apply]
  rfl

Supremum of Seminorms Commutes with Composition

Informal description

Let $q$ be a family of seminorms on a vector space $F$ over a field $\mathbb{K}_2$, indexed by a set $\iota$. For any finite subset $s \subseteq \iota$ and any semilinear map $f \colon E \to F$ (where $E$ is a vector space over $\mathbb{K}$), the composition of the pointwise supremum seminorm $\sup_{i \in s} q_i$ with $f$ is equal to the pointwise supremum of the compositions $(q_i \circ f)_{i \in s}$. In other words, $(\sup_{i \in s} q_i) \circ f = \sup_{i \in s} (q_i \circ f)$.

LinearMap.withSeminorms_induced theorem

 [hι : Nonempty ι] {q : SeminormFamily 𝕜₂ F ι} (hq : WithSeminorms q) (f : E →ₛₗ[σ₁₂] F) :
  WithSeminorms (topology := induced f inferInstance) (q.comp f)

Full source

theorem LinearMap.withSeminorms_induced [hι : Nonempty ι] {q : SeminormFamily 𝕜₂ F ι}
    (hq : WithSeminorms q) (f : E →ₛₗ[σ₁₂] F) :
    WithSeminorms (topology := induced f inferInstance) (q.comp f) := by
  have := hq.topologicalAddGroup
  let _ : TopologicalSpace E := induced f inferInstance
  have : IsTopologicalAddGroup E := topologicalAddGroup_induced f
  rw [(q.comp f).withSeminorms_iff_nhds_eq_iInf, nhds_induced, map_zero,
    q.withSeminorms_iff_nhds_eq_iInf.mp hq, Filter.comap_iInf]
  refine iInf_congr fun i => ?_
  exact Filter.comap_comap

Induced Topology via Semilinear Map Coincides with Seminorm-Induced Topology

Informal description

Let $E$ and $F$ be vector spaces over fields $\mathbb{K}$ and $\mathbb{K}_2$ respectively, with $\sigma_{12} \colon \mathbb{K} \to \mathbb{K}_2$ a field homomorphism. Let $\iota$ be a nonempty indexing set and $q = (q_i)_{i \in \iota}$ a family of seminorms on $F$ inducing its topology. Given a $\sigma_{12}$-semilinear map $f \colon E \to F$, the topology on $E$ induced by $f$ (i.e., the coarsest topology making $f$ continuous) is equal to the topology induced by the family of seminorms $(q_i \circ f)_{i \in \iota}$.

Topology.IsInducing.withSeminorms theorem

 [hι : Nonempty ι] {q : SeminormFamily 𝕜₂ F ι} (hq : WithSeminorms q) [TopologicalSpace E] {f : E →ₛₗ[σ₁₂] F}
  (hf : IsInducing f) : WithSeminorms (q.comp f)

Full source

lemma Topology.IsInducing.withSeminorms [hι : Nonempty ι] {q : SeminormFamily 𝕜₂ F ι}
    (hq : WithSeminorms q) [TopologicalSpace E] {f : E →ₛₗ[σ₁₂] F} (hf : IsInducing f) :
    WithSeminorms (q.comp f) := by
  rw [hf.eq_induced]
  exact f.withSeminorms_induced hq

Inducing Semilinear Maps Preserve Seminorm-Induced Topology

Informal description

Let $E$ and $F$ be vector spaces over fields $\mathbb{K}$ and $\mathbb{K}_2$ respectively, with $\sigma_{12} \colon \mathbb{K} \to \mathbb{K}_2$ a field homomorphism. Let $\iota$ be a nonempty indexing set and $q = (q_i)_{i \in \iota}$ a family of seminorms on $F$ that induces its topology. Given a $\sigma_{12}$-semilinear map $f \colon E \to F$ that is inducing (i.e., the topology on $E$ is the coarsest making $f$ continuous), then the topology on $E$ is induced by the family of seminorms $(q_i \circ f)_{i \in \iota}$.

SeminormFamily.sigma definition

{κ : ι → Type*} (p : (i : ι) → SeminormFamily 𝕜 E (κ i)) : SeminormFamily 𝕜 E ((i : ι) × κ i)

Full source

/-- (Disjoint) union of seminorm families. -/
protected def SeminormFamily.sigma {κ : ι → Type*} (p : (i : ι) → SeminormFamily 𝕜 E (κ i)) :
    SeminormFamily 𝕜 E ((i : ι) × κ i) :=
  fun ⟨i, k⟩ => p i k

Disjoint union of seminorm families

Informal description

Given an indexed family of seminorm families $(p_i)_{i \in \iota}$, where each $p_i$ is a seminorm family on a vector space $E$ over a field $\mathbb{K}$ indexed by $\kappa_i$, the disjoint union $\Sigma p$ is a seminorm family on $E$ indexed by the disjoint union $\Sigma_{i \in \iota} \kappa_i$. For each pair $(i, k) \in \Sigma_{i \in \iota} \kappa_i$, the seminorm $(\Sigma p)_{(i,k)}$ is defined as $(p_i)_k$.

withSeminorms_iInf theorem

 {κ : ι → Type*} [Nonempty ((i : ι) × κ i)] [∀ i, Nonempty (κ i)] {p : (i : ι) → SeminormFamily 𝕜 E (κ i)}
  {t : ι → TopologicalSpace E} (hp : ∀ i, WithSeminorms (topology := t i) (p i)) :
  WithSeminorms (topology := ⨅ i, t i) (SeminormFamily.sigma p)

Full source

theorem withSeminorms_iInf {κ : ι → Type*} [Nonempty ((i : ι) × κ i)] [∀ i, Nonempty (κ i)]
    {p : (i : ι) → SeminormFamily 𝕜 E (κ i)} {t : ι → TopologicalSpace E}
    (hp : ∀ i, WithSeminorms (topology := t i) (p i)) :
    WithSeminorms (topology := ⨅ i, t i) (SeminormFamily.sigma p) := by
  have : ∀ i, @IsTopologicalAddGroup E (t i) _ :=
    fun i ↦ @WithSeminorms.topologicalAddGroup _ _ _ _ _ _ _ (t i) _ (hp i)
  have : @IsTopologicalAddGroup E (⨅ i, t i) _ := topologicalAddGroup_iInf inferInstance
  simp_rw [@SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf _ _ _ _ _ _ _ (_)] at hp ⊢
  rw [iInf_sigma]
  exact iInf_congr hp

Infimum of Seminorm-Induced Topologies is Induced by Disjoint Union of Seminorm Families

Informal description

Let $\mathbb{K}$ be a field, $E$ a vector space over $\mathbb{K}$, and $\iota$ an indexing set. For each $i \in \iota$, let $\kappa_i$ be a nonempty type and $p_i : \kappa_i \to \text{Seminorm}\, \mathbb{K}\, E$ a family of seminorms on $E$ indexed by $\kappa_i$. Suppose that for each $i$, the topology $t_i$ on $E$ is induced by the seminorm family $p_i$. Then the topology on $E$ given by the infimum $\bigwedge_{i \in \iota} t_i$ is induced by the disjoint union seminorm family $\Sigma p$ on $E$ indexed by $\Sigma_{i \in \iota} \kappa_i$.

withSeminorms_pi theorem

 {κ : ι → Type*} {E : ι → Type*} [∀ i, AddCommGroup (E i)] [∀ i, Module 𝕜 (E i)] [∀ i, TopologicalSpace (E i)]
  [Nonempty ((i : ι) × κ i)] [∀ i, Nonempty (κ i)] {p : (i : ι) → SeminormFamily 𝕜 (E i) (κ i)}
  (hp : ∀ i, WithSeminorms (p i)) : WithSeminorms (SeminormFamily.sigma (fun i ↦ (p i).comp (LinearMap.proj i)))

Full source

theorem withSeminorms_pi {κ : ι → Type*} {E : ι → Type*}
    [∀ i, AddCommGroup (E i)] [∀ i, Module 𝕜 (E i)] [∀ i, TopologicalSpace (E i)]
    [Nonempty ((i : ι) × κ i)] [∀ i, Nonempty (κ i)] {p : (i : ι) → SeminormFamily 𝕜 (E i) (κ i)}
    (hp : ∀ i, WithSeminorms (p i)) :
    WithSeminorms (SeminormFamily.sigma (fun i ↦ (p i).comp (LinearMap.proj i))) :=
  withSeminorms_iInf fun i ↦ (LinearMap.proj i).withSeminorms_induced (hp i)

Product Topology Induced by Disjoint Union of Seminorm Families

Informal description

Let $\mathbb{K}$ be a field, $\iota$ an indexing set, and for each $i \in \iota$, let $E_i$ be a vector space over $\mathbb{K}$ equipped with a topology induced by a family of seminorms $p_i : \kappa_i \to \text{Seminorm}\, \mathbb{K}\, E_i$. Suppose that for each $i$, the topology on $E_i$ is induced by $p_i$, and that $\kappa_i$ is nonempty. Then the product topology on $\prod_{i \in \iota} E_i$ is induced by the disjoint union of the seminorm families $(p_i \circ \text{proj}_i)_{i \in \iota}$, where $\text{proj}_i$ is the projection map from the product space to $E_i$.

WithSeminorms.firstCountableTopology theorem

(hp : WithSeminorms p) : FirstCountableTopology E

Full source

/-- If the topology of a space is induced by a countable family of seminorms, then the topology
is first countable. -/
theorem WithSeminorms.firstCountableTopology (hp : WithSeminorms p) :
    FirstCountableTopology E := by
  have := hp.topologicalAddGroup
  let _ : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
  have : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
  have : (𝓝 (0 : E)).IsCountablyGenerated := by
    rw [p.withSeminorms_iff_nhds_eq_iInf.mp hp]
    exact Filter.iInf.isCountablyGenerated _
  have : (uniformity E).IsCountablyGenerated := IsUniformAddGroup.uniformity_countably_generated
  exact UniformSpace.firstCountableTopology E

First countability of seminorm-induced topology for countable families

Informal description

Let $E$ be a topological vector space over a field $\mathbb{K}$ whose topology is induced by a countable family of seminorms $(p_i)_{i \in \iota}$. Then $E$ satisfies the first countability axiom, meaning every point in $E$ has a countable neighborhood basis.

Mathlib.Analysis.LocallyConvex.WithSeminorms

Main definitions

Main statements

Continuity of semilinear maps

Tags