Mathlib.Topology.Algebra.Module.Multilinear.Topology

ContinuousMultilinearMap.toUniformOnFun definition

[TopologicalSpace F] (f : ContinuousMultilinearMap 𝕜 E F) : (Π i, E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F

Full source

/-- An auxiliary definition used to define topology on `ContinuousMultilinearMap 𝕜 E F`. -/
def toUniformOnFun [TopologicalSpace F] (f : ContinuousMultilinearMap 𝕜 E F) :
    (Π i, E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F :=
  UniformOnFun.ofFun _ f

Uniform convergence topology on continuous multilinear maps

Informal description

Given a continuous multilinear map $ f $ from $ \prod_i E_i $ to $ F $, where each $ E_i $ and $ F $ are topological vector spaces over a field $ \mathbb{K} $, the function `toUniformOnFun` maps $ f $ to the space of functions $ \prod_i E_i \to F $ equipped with the uniform structure of uniform convergence on all von Neumann bounded subsets of $ \prod_i E_i $.

ContinuousMultilinearMap.range_toUniformOnFun theorem

 [DecidableEq ι] [TopologicalSpace F] :
  range toUniformOnFun =
    {f : (Π i, E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F |
      Continuous (toFun _ f) ∧
        (∀ (m : Π i, E i) i x y, toFun _ f (update m i (x + y)) = toFun _ f (update m i x) + toFun _ f (update m i y)) ∧
          (∀ (m : Π i, E i) i (c : 𝕜) x, toFun _ f (update m i (c • x)) = c • toFun _ f (update m i x))}

Full source

lemma range_toUniformOnFun [DecidableEq ι] [TopologicalSpace F] :
    range toUniformOnFun =
      {f : (Π i, E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F |
        Continuous (toFun _ f) ∧
        (∀ (m : Π i, E i) i x y,
          toFun _ f (update m i (x + y)) = toFun _ f (update m i x) + toFun _ f (update m i y)) ∧
        (∀ (m : Π i, E i) i (c : 𝕜) x,
          toFun _ f (update m i (c • x)) = c • toFun _ f (update m i x))} := by
  ext f
  constructor
  · rintro ⟨f, rfl⟩
    exact ⟨f.cont, f.map_update_add, f.map_update_smul⟩
  · rintro ⟨hcont, hadd, hsmul⟩
    exact ⟨⟨⟨f, by intro; convert hadd, by intro; convert hsmul⟩, hcont⟩, rfl⟩

Characterization of the Range of Continuous Multilinear Maps in the Uniform Convergence Topology

Informal description

Let $\mathbb{K}$ be a normed field, $\iota$ a finite type, and $E_i$ for $i \in \iota$ and $F$ topological vector spaces over $\mathbb{K}$. The range of the map `toUniformOnFun`, which sends a continuous multilinear map $f \colon \prod_{i \in \iota} E_i \to F$ to the space of functions with the uniform structure of uniform convergence on von Neumann bounded subsets, is equal to the set of functions $f \colon \prod_{i \in \iota} E_i \to F$ such that: 1. $f$ is continuous, 2. For any $m \in \prod_{i \in \iota} E_i$, any $i \in \iota$, and any $x, y \in E_i$, we have \[ f(m[i \mapsto x + y]) = f(m[i \mapsto x]) + f(m[i \mapsto y]), \] 3. For any $m \in \prod_{i \in \iota} E_i$, any $i \in \iota$, any $c \in \mathbb{K}$, and any $x \in E_i$, we have \[ f(m[i \mapsto c \cdot x]) = c \cdot f(m[i \mapsto x]), \] where $m[i \mapsto v]$ denotes the function that updates the $i$-th component of $m$ to $v$ while keeping all other components unchanged.

ContinuousMultilinearMap.toUniformOnFun_toFun theorem

[TopologicalSpace F] (f : ContinuousMultilinearMap 𝕜 E F) : UniformOnFun.toFun _ f.toUniformOnFun = f

Full source

@[simp]
lemma toUniformOnFun_toFun [TopologicalSpace F] (f : ContinuousMultilinearMap 𝕜 E F) :
    UniformOnFun.toFun _ f.toUniformOnFun = f :=
  rfl

Uniform Convergence Construction Preserves Original Continuous Multilinear Map

Informal description

For any continuous multilinear map $f$ from $\prod_i E_i$ to $F$ (where each $E_i$ and $F$ are topological vector spaces over a field $\mathbb{K}$), the function obtained by applying the uniform convergence topology construction to $f$ and then converting back to an ordinary function is equal to $f$ itself. In other words, the composition of the uniform structure embedding and its inverse recovers the original map.

ContinuousMultilinearMap.instTopologicalSpace instance

[TopologicalSpace F] [IsTopologicalAddGroup F] : TopologicalSpace (ContinuousMultilinearMap 𝕜 E F)

Full source

instance instTopologicalSpace [TopologicalSpace F] [IsTopologicalAddGroup F] :
    TopologicalSpace (ContinuousMultilinearMap 𝕜 E F) :=
  .induced toUniformOnFun <|
    @UniformOnFun.topologicalSpace _ _ (IsTopologicalAddGroup.toUniformSpace F) _

Topological Space Structure on Continuous Multilinear Maps

Informal description

For any topological vector space $F$ over a field $\mathbb{K}$ where $F$ is a topological additive group, the space of continuous multilinear maps $\prod_i E_i \to F$ is equipped with a canonical topological space structure.

ContinuousMultilinearMap.instUniformSpace instance

[UniformSpace F] [IsUniformAddGroup F] : UniformSpace (ContinuousMultilinearMap 𝕜 E F)

Full source

instance instUniformSpace [UniformSpace F] [IsUniformAddGroup F] :
    UniformSpace (ContinuousMultilinearMap 𝕜 E F) :=
  .replaceTopology (.comap toUniformOnFun <| UniformOnFun.uniformSpace _ _ _) <| by
    rw [instTopologicalSpace, IsUniformAddGroup.toUniformSpace_eq]; rfl

Uniform Space Structure on Continuous Multilinear Maps

Informal description

For any uniform space $F$ that is also an additive uniform group, the space of continuous multilinear maps $\prod_i E_i \to F$ is equipped with a canonical uniform space structure.

ContinuousMultilinearMap.isUniformInducing_toUniformOnFun theorem

 : IsUniformInducing (toUniformOnFun : ContinuousMultilinearMap 𝕜 E F → ((Π i, E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F))

Full source

lemma isUniformInducing_toUniformOnFun :
    IsUniformInducing (toUniformOnFun :
      ContinuousMultilinearMap 𝕜 E F → ((Π i, E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F)) := ⟨rfl⟩

Uniform Inducing Property of the `toUniformOnFun` Map for Continuous Multilinear Maps

Informal description

The map `toUniformOnFun` from the space of continuous multilinear maps $\prod_i E_i \to F$ to the space of functions $\prod_i E_i \to F$ equipped with the uniform structure of uniform convergence on von Neumann bounded subsets is a uniform inducing map. That is, the uniformity on the space of continuous multilinear maps is induced by the uniformity of uniform convergence on von Neumann bounded subsets via this map.

ContinuousMultilinearMap.isUniformEmbedding_toUniformOnFun theorem

: IsUniformEmbedding (toUniformOnFun : ContinuousMultilinearMap 𝕜 E F → _)

Full source

lemma isUniformEmbedding_toUniformOnFun :
    IsUniformEmbedding (toUniformOnFun : ContinuousMultilinearMap 𝕜 E F → _) :=
  ⟨isUniformInducing_toUniformOnFun, DFunLike.coe_injective⟩

Uniform Embedding Property of `toUniformOnFun` for Continuous Multilinear Maps

Informal description

The map `toUniformOnFun` from the space of continuous multilinear maps $\prod_i E_i \to F$ to the space of functions $\prod_i E_i \to F$ equipped with the uniform structure of uniform convergence on von Neumann bounded subsets is a uniform embedding. That is, it is injective, uniformly continuous, and the uniformity on the space of continuous multilinear maps is induced by the uniformity of uniform convergence on von Neumann bounded subsets via this map.

ContinuousMultilinearMap.isEmbedding_toUniformOnFun theorem

 : IsEmbedding (toUniformOnFun : ContinuousMultilinearMap 𝕜 E F → ((Π i, E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F))

Full source

lemma isEmbedding_toUniformOnFun :
    IsEmbedding (toUniformOnFun : ContinuousMultilinearMap 𝕜 E F →
      ((Π i, E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F)) :=
  isUniformEmbedding_toUniformOnFun.isEmbedding

Topological Embedding Property of `toUniformOnFun` for Continuous Multilinear Maps

Informal description

The map `toUniformOnFun` from the space of continuous multilinear maps $\prod_i E_i \to F$ to the space of functions $\prod_i E_i \to F$ equipped with the uniform structure of uniform convergence on von Neumann bounded subsets is a topological embedding. That is, it is injective, continuous, and the topology on the space of continuous multilinear maps is induced by the topology of uniform convergence on von Neumann bounded subsets via this map.

ContinuousMultilinearMap.uniformContinuous_coe_fun theorem

 [∀ i, ContinuousSMul 𝕜 (E i)] : UniformContinuous (DFunLike.coe : ContinuousMultilinearMap 𝕜 E F → (Π i, E i) → F)

Full source

theorem uniformContinuous_coe_fun [∀ i, ContinuousSMul 𝕜 (E i)] :
    UniformContinuous (DFunLike.coe : ContinuousMultilinearMap 𝕜 E F → (Π i, E i) → F) :=
  (UniformOnFun.uniformContinuous_toFun isVonNBounded_covers).comp
    isUniformEmbedding_toUniformOnFun.uniformContinuous

Uniform Continuity of the Canonical Embedding for Continuous Multilinear Maps

Informal description

For any family of topological vector spaces $\{E_i\}_{i \in \iota}$ over a field $\mathbb{K}$ where the scalar multiplication $\mathbb{K} \times E_i \to E_i$ is continuous for each $i$, the canonical embedding of the space of continuous multilinear maps $\prod_i E_i \to F$ into the space of all functions $\prod_i E_i \to F$ is uniformly continuous.

ContinuousMultilinearMap.uniformContinuous_eval_const theorem

 [∀ i, ContinuousSMul 𝕜 (E i)] (x : Π i, E i) : UniformContinuous fun f : ContinuousMultilinearMap 𝕜 E F ↦ f x

Full source

theorem uniformContinuous_eval_const [∀ i, ContinuousSMul 𝕜 (E i)] (x : Π i, E i) :
    UniformContinuous fun f : ContinuousMultilinearMap 𝕜 E F ↦ f x :=
  uniformContinuous_pi.1 uniformContinuous_coe_fun x

Uniform Continuity of Evaluation at a Point for Continuous Multilinear Maps

Informal description

For any family of topological vector spaces $\{E_i\}_{i \in \iota}$ over a field $\mathbb{K}$ where the scalar multiplication $\mathbb{K} \times E_i \to E_i$ is continuous for each $i$, and for any fixed element $x \in \prod_i E_i$, the evaluation map $f \mapsto f(x)$ is uniformly continuous on the space of continuous multilinear maps $\prod_i E_i \to F$.

ContinuousMultilinearMap.instIsUniformAddGroup instance

: IsUniformAddGroup (ContinuousMultilinearMap 𝕜 E F)

Full source

instance instIsUniformAddGroup : IsUniformAddGroup (ContinuousMultilinearMap 𝕜 E F) :=
  let φ : ContinuousMultilinearMapContinuousMultilinearMap 𝕜 E F →+ (Π i, E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F :=
    { toFun := toUniformOnFun, map_add' := fun _ _ ↦ rfl, map_zero' := rfl }
  isUniformEmbedding_toUniformOnFun.isUniformAddGroup φ

Additive Uniform Group Structure on Continuous Multilinear Maps

Informal description

The space of continuous multilinear maps $\prod_i E_i \to F$ forms an additive uniform group, where the group operations (addition and negation) are uniformly continuous with respect to the uniform structure on the space of continuous multilinear maps.

ContinuousMultilinearMap.instUniformContinuousConstSMul instance

 {M : Type*} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜 M F] [ContinuousConstSMul M F] :
  UniformContinuousConstSMul M (ContinuousMultilinearMap 𝕜 E F)

Full source

instance instUniformContinuousConstSMul {M : Type*}
    [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜 M F] [ContinuousConstSMul M F] :
    UniformContinuousConstSMul M (ContinuousMultilinearMap 𝕜 E F) :=
  haveI := uniformContinuousConstSMul_of_continuousConstSMul M F
  isUniformEmbedding_toUniformOnFun.uniformContinuousConstSMul fun _ _ ↦ rfl

Uniform Continuity of Scalar Multiplication on Continuous Multilinear Maps

Informal description

For any monoid $M$ acting distributively on a topological vector space $F$ over a field $\mathbb{K}$, with the action commuting with the $\mathbb{K}$-action and being continuous for each fixed element of $M$, the space of continuous multilinear maps $\prod_i E_i \to F$ has uniformly continuous scalar multiplication by elements of $M$. That is, for each $c \in M$, the map $f \mapsto c \cdot f$ is uniformly continuous on the space of continuous multilinear maps.

ContinuousMultilinearMap.isUniformInducing_postcomp theorem

 {G : Type*} [AddCommGroup G] [UniformSpace G] [IsUniformAddGroup G] [Module 𝕜 G] (g : F →L[𝕜] G)
  (hg : IsUniformInducing g) :
  IsUniformInducing (g.compContinuousMultilinearMap : ContinuousMultilinearMap 𝕜 E F → ContinuousMultilinearMap 𝕜 E G)

Full source

theorem isUniformInducing_postcomp
    {G : Type*} [AddCommGroup G] [UniformSpace G] [IsUniformAddGroup G] [Module 𝕜 G]
    (g : F →L[𝕜] G) (hg : IsUniformInducing g) :
    IsUniformInducing (g.compContinuousMultilinearMap :
      ContinuousMultilinearMap 𝕜 E F → ContinuousMultilinearMap 𝕜 E G) := by
  rw [← isUniformInducing_toUniformOnFun.of_comp_iff]
  exact (UniformOnFun.postcomp_isUniformInducing hg).comp isUniformInducing_toUniformOnFun

Uniform Inducing Property of Post-Composition by a Uniform Inducing Linear Map on Continuous Multilinear Maps

Informal description

Let $G$ be an additive commutative group equipped with a uniform space structure making it an additive uniform group, and let $g : F \to G$ be a continuous linear map that is uniform inducing. Then the post-composition map \[ g \circ (\cdot) : \text{ContinuousMultilinearMap}(\mathbb{K}, E, F) \to \text{ContinuousMultilinearMap}(\mathbb{K}, E, G) \] is also uniform inducing, where both spaces of continuous multilinear maps are equipped with their canonical uniform structures.

ContinuousMultilinearMap.instCompleteSpace instance

[∀ i, IsTopologicalAddGroup (E i)] [SequentialSpace (Π i, E i)] : CompleteSpace (ContinuousMultilinearMap 𝕜 E F)

Full source

instance instCompleteSpace [∀ i, IsTopologicalAddGroup (E i)] [SequentialSpace (Π i, E i)] :
    CompleteSpace (ContinuousMultilinearMap 𝕜 E F) :=
  completeSpace <| .of_seq fun _u x hux ↦ (hux.isVonNBounded_range 𝕜).insert x

Completeness of Continuous Multilinear Maps on Sequential Product Spaces

Informal description

For any family of topological vector spaces $\{E_i\}_{i \in \iota}$ over a normed field $\mathbb{K}$ where each $E_i$ is an additive topological group and the product space $\prod_i E_i$ is sequential, the space of continuous multilinear maps $\text{ContinuousMultilinearMap}(\mathbb{K}, E, F)$ is complete with respect to its canonical uniform structure.

ContinuousMultilinearMap.isUniformEmbedding_restrictScalars theorem

: IsUniformEmbedding (restrictScalars 𝕜' : ContinuousMultilinearMap 𝕜 E F → ContinuousMultilinearMap 𝕜' E F)

Full source

theorem isUniformEmbedding_restrictScalars :
    IsUniformEmbedding
      (restrictScalars 𝕜' : ContinuousMultilinearMap 𝕜 E F → ContinuousMultilinearMap 𝕜' E F) := by
  letI : NontriviallyNormedField 𝕜 :=
    ⟨let ⟨x, hx⟩ := @NontriviallyNormedField.non_trivial 𝕜' _; ⟨algebraMap 𝕜' 𝕜 x, by simpa⟩⟩
  rw [← isUniformEmbedding_toUniformOnFun.of_comp_iff]
  convert isUniformEmbedding_toUniformOnFun using 4 with s
  exact ⟨fun h ↦ h.extend_scalars _, fun h ↦ h.restrict_scalars _⟩

Uniform Embedding Property of Scalar Restriction for Continuous Multilinear Maps

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}$ as a subfield of $\mathbb{K}'$ via a normed algebra structure. The restriction of scalars map from continuous $\mathbb{K}$-multilinear maps $\prod_i E_i \to F$ to continuous $\mathbb{K}'$-multilinear maps $\prod_i E_i \to F$ is a uniform embedding. That is, it is injective, uniformly continuous, and the uniformity on the space of $\mathbb{K}$-multilinear maps is induced by the uniformity on the space of $\mathbb{K}'$-multilinear maps via this map.

ContinuousMultilinearMap.uniformContinuous_restrictScalars theorem

: UniformContinuous (restrictScalars 𝕜' : ContinuousMultilinearMap 𝕜 E F → ContinuousMultilinearMap 𝕜' E F)

Full source

theorem uniformContinuous_restrictScalars :
    UniformContinuous
      (restrictScalars 𝕜' : ContinuousMultilinearMap 𝕜 E F → ContinuousMultilinearMap 𝕜' E F) :=
  (isUniformEmbedding_restrictScalars 𝕜').uniformContinuous

Uniform Continuity of Scalar Restriction for Continuous Multilinear Maps

Informal description

The restriction of scalars map from continuous $\mathbb{K}$-multilinear maps $\prod_i E_i \to F$ to continuous $\mathbb{K}'$-multilinear maps $\prod_i E_i \to F$ is uniformly continuous.

ContinuousMultilinearMap.instIsTopologicalAddGroup instance

: IsTopologicalAddGroup (ContinuousMultilinearMap 𝕜 E F)

Full source

instance instIsTopologicalAddGroup : IsTopologicalAddGroup (ContinuousMultilinearMap 𝕜 E F) :=
  letI := IsTopologicalAddGroup.toUniformSpace F
  haveI := isUniformAddGroup_of_addCommGroup (G := F)
  inferInstance

Topological Additive Group Structure on Continuous Multilinear Maps

Informal description

The space of continuous multilinear maps $\prod_i E_i \to F$ forms a topological additive group, where the group operations (addition and negation) are continuous with respect to the topology on the space of continuous multilinear maps.

ContinuousMultilinearMap.instContinuousConstSMul instance

 {M : Type*} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜 M F] [ContinuousConstSMul M F] :
  ContinuousConstSMul M (ContinuousMultilinearMap 𝕜 E F)

Full source

instance instContinuousConstSMul
    {M : Type*} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜 M F] [ContinuousConstSMul M F] :
    ContinuousConstSMul M (ContinuousMultilinearMap 𝕜 E F) := by
  letI := IsTopologicalAddGroup.toUniformSpace F
  haveI := isUniformAddGroup_of_addCommGroup (G := F)
  infer_instance

Continuous Scalar Multiplication on Continuous Multilinear Maps

Informal description

For any monoid $M$ acting distributively on a topological vector space $F$ over a field $\mathbb{K}$, with the action commuting with the $\mathbb{K}$-action and being continuous for each fixed element of $M$, the space of continuous multilinear maps $\prod_i E_i \to F$ has continuous scalar multiplication by elements of $M$. That is, for each $c \in M$, the map $f \mapsto c \cdot f$ is continuous on the space of continuous multilinear maps.

ContinuousMultilinearMap.instContinuousSMul instance

[ContinuousSMul 𝕜 F] : ContinuousSMul 𝕜 (ContinuousMultilinearMap 𝕜 E F)

Full source

instance instContinuousSMul [ContinuousSMul 𝕜 F] :
    ContinuousSMul 𝕜 (ContinuousMultilinearMap 𝕜 E F) :=
  letI := IsTopologicalAddGroup.toUniformSpace F
  haveI := isUniformAddGroup_of_addCommGroup (G := F)
  let φ : ContinuousMultilinearMapContinuousMultilinearMap 𝕜 E F →ₗ[𝕜] (Π i, E i) → F :=
    { toFun := (↑), map_add' := fun _ _ ↦ rfl, map_smul' := fun _ _ ↦ rfl }
  UniformOnFun.continuousSMul_induced_of_image_bounded _ _ _ _ φ
    isEmbedding_toUniformOnFun.isInducing fun _ _ hu ↦ hu.image_multilinear _

Continuous Scalar Multiplication on Continuous Multilinear Maps

Informal description

For any topological vector space $F$ over a field $\mathbb{K}$ with continuous scalar multiplication, the space of continuous multilinear maps $\prod_i E_i \to F$ is equipped with a continuous scalar multiplication operation by elements of $\mathbb{K}$.

ContinuousMultilinearMap.hasBasis_nhds_zero_of_basis theorem

 {ι : Type*} {p : ι → Prop} {b : ι → Set F} (h : (𝓝 (0 : F)).HasBasis p b) :
  (𝓝 (0 : ContinuousMultilinearMap 𝕜 E F)).HasBasis (fun Si : Set (Π i, E i) × ι => IsVonNBounded 𝕜 Si.1 ∧ p Si.2)
    fun Si => {f | MapsTo f Si.1 (b Si.2)}

Full source

theorem hasBasis_nhds_zero_of_basis {ι : Type*} {p : ι → Prop} {b : ι → Set F}
    (h : (𝓝 (0 : F)).HasBasis p b) :
    (𝓝 (0 : ContinuousMultilinearMap 𝕜 E F)).HasBasis
      (fun Si : SetSet (Π i, E i) × ι => IsVonNBoundedIsVonNBounded 𝕜 Si.1 ∧ p Si.2)
      fun Si => { f | MapsTo f Si.1 (b Si.2) } := by
  letI : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F
  haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
  rw [nhds_induced]
  refine (UniformOnFun.hasBasis_nhds_zero_of_basis _ ?_ ?_ h).comap DFunLike.coe
  · exact ⟨∅, isVonNBounded_empty _ _⟩
  · exact directedOn_of_sup_mem fun _ _ => Bornology.IsVonNBounded.union

Basis Characterization of Zero Neighborhoods in Continuous Multilinear Maps

Informal description

Let $F$ be a topological vector space over a field $\mathbb{K}$, and let $\mathcal{N}(0)$ be the neighborhood filter of zero in $F$ with a basis $\{b_i\}_{i \in \iota}$ indexed by a predicate $p$. Then the neighborhood filter of zero in the space of continuous multilinear maps $\prod_i E_i \to F$ has a basis consisting of sets of the form \[ \{f \mid f(S) \subseteq b_i\} \] where $S$ is a von Neumann bounded subset of $\prod_i E_i$ and $i \in \iota$ satisfies $p(i)$.

ContinuousMultilinearMap.hasBasis_nhds_zero theorem

 :
  (𝓝 (0 : ContinuousMultilinearMap 𝕜 E F)).HasBasis
    (fun SV : Set (Π i, E i) × Set F => IsVonNBounded 𝕜 SV.1 ∧ SV.2 ∈ 𝓝 0) fun SV => {f | MapsTo f SV.1 SV.2}

Full source

theorem hasBasis_nhds_zero :
    (𝓝 (0 : ContinuousMultilinearMap 𝕜 E F)).HasBasis
      (fun SV : SetSet (Π i, E i) × Set F => IsVonNBoundedIsVonNBounded 𝕜 SV.1 ∧ SV.2 ∈ 𝓝 0) fun SV =>
      { f | MapsTo f SV.1 SV.2 } :=
  hasBasis_nhds_zero_of_basis (Filter.basis_sets _)

Basis Characterization of Zero Neighborhoods in Continuous Multilinear Maps

Informal description

Let $\mathbb{K}$ be a normed field, and let $E_i$ and $F$ be topological vector spaces over $\mathbb{K}$. The neighborhood filter of zero in the space of continuous multilinear maps $\prod_i E_i \to F$ has a basis consisting of sets of the form \[ \{f \mid f(S) \subseteq V\} \] where $S$ is a von Neumann bounded subset of $\prod_i E_i$ and $V$ is a neighborhood of zero in $F$.

ContinuousMultilinearMap.instContinuousEvalConstForall instance

: ContinuousEvalConst (ContinuousMultilinearMap 𝕜 E F) (Π i, E i) F

Full source

instance : ContinuousEvalConst (ContinuousMultilinearMap 𝕜 E F) (Π i, E i) F where
  continuous_eval_const x :=
    let _ := IsTopologicalAddGroup.toUniformSpace F
    have _ := isUniformAddGroup_of_addCommGroup (G := F)
    (uniformContinuous_eval_const x).continuous

Continuity of Point Evaluation for Continuous Multilinear Maps

Informal description

For any family of topological vector spaces $\{E_i\}_{i \in \iota}$ over a field $\mathbb{K}$ and any topological vector space $F$ over $\mathbb{K}$, the space of continuous multilinear maps $\prod_i E_i \to F$ has the property that for any fixed element $x \in \prod_i E_i$, the evaluation map $f \mapsto f(x)$ is continuous.

ContinuousMultilinearMap.instT2Space instance

[T2Space F] : T2Space (ContinuousMultilinearMap 𝕜 E F)

Full source

instance instT2Space [T2Space F] : T2Space (ContinuousMultilinearMap 𝕜 E F) :=
  .of_injective_continuous DFunLike.coe_injective continuous_coeFun

Hausdorff Property of Continuous Multilinear Maps

Informal description

For any family of topological vector spaces $\{E_i\}_{i \in \iota}$ over a field $\mathbb{K}$ and any topological vector space $F$ over $\mathbb{K}$, if $F$ is a Hausdorff space, then the space of continuous multilinear maps $\prod_i E_i \to F$ is also a Hausdorff space.

ContinuousMultilinearMap.instT3Space instance

[T2Space F] : T3Space (ContinuousMultilinearMap 𝕜 E F)

Full source

instance instT3Space [T2Space F] : T3Space (ContinuousMultilinearMap 𝕜 E F) :=
  inferInstance

Hausdorff Target Implies T₃ Space for Continuous Multilinear Maps

Informal description

For any family of topological vector spaces $\{E_i\}_{i \in \iota}$ over a field $\mathbb{K}$ and any topological vector space $F$ over $\mathbb{K}$, if $F$ is a Hausdorff space, then the space of continuous multilinear maps $\prod_i E_i \to F$ is a T₃ space (i.e., a regular T₀ space).

ContinuousMultilinearMap.isEmbedding_restrictScalars theorem

: IsEmbedding (restrictScalars 𝕜' : ContinuousMultilinearMap 𝕜 E F → ContinuousMultilinearMap 𝕜' E F)

Full source

theorem isEmbedding_restrictScalars :
    IsEmbedding
      (restrictScalars 𝕜' : ContinuousMultilinearMap 𝕜 E F → ContinuousMultilinearMap 𝕜' E F) :=
  letI : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F
  haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
  (isUniformEmbedding_restrictScalars _).isEmbedding

Topological Embedding Property of Scalar Restriction for Continuous Multilinear Maps

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}$ as a subfield of $\mathbb{K}'$ via a normed algebra structure. The restriction of scalars map from continuous $\mathbb{K}$-multilinear maps $\prod_i E_i \to F$ to continuous $\mathbb{K}'$-multilinear maps $\prod_i E_i \to F$ is a topological embedding. That is, it is injective and the topology on the space of $\mathbb{K}$-multilinear maps is induced by the topology on the space of $\mathbb{K}'$-multilinear maps via this map.

ContinuousMultilinearMap.continuous_restrictScalars theorem

: Continuous (restrictScalars 𝕜' : ContinuousMultilinearMap 𝕜 E F → ContinuousMultilinearMap 𝕜' E F)

Full source

@[continuity, fun_prop]
theorem continuous_restrictScalars :
    Continuous
      (restrictScalars 𝕜' : ContinuousMultilinearMap 𝕜 E F → ContinuousMultilinearMap 𝕜' E F) :=
   isEmbedding_restrictScalars.continuous

Continuity of Scalar Restriction for Continuous Multilinear Maps

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}$ as a subfield of $\mathbb{K}'$ via a normed algebra structure. The restriction of scalars map from continuous $\mathbb{K}$-multilinear maps $\prod_i E_i \to F$ to continuous $\mathbb{K}'$-multilinear maps $\prod_i E_i \to F$ is continuous.

ContinuousMultilinearMap.restrictScalarsLinear definition

[ContinuousConstSMul 𝕜' F] : ContinuousMultilinearMap 𝕜 E F →L[𝕜'] ContinuousMultilinearMap 𝕜' E F

Full source

/-- `ContinuousMultilinearMap.restrictScalars` as a `ContinuousLinearMap`. -/
@[simps -fullyApplied apply]
def restrictScalarsLinear [ContinuousConstSMul 𝕜' F] :
    ContinuousMultilinearMapContinuousMultilinearMap 𝕜 E F →L[𝕜'] ContinuousMultilinearMap 𝕜' E F where
  toFun := restrictScalars 𝕜'
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

Continuous linear map induced by restriction of scalars on continuous multilinear maps

Informal description

Given normed fields $\mathbb{K}$ and $\mathbb{K}'$ with $\mathbb{K}$ as a subfield of $\mathbb{K}'$ via a normed algebra structure, and a topological vector space $F$ over $\mathbb{K}'$ with continuous scalar multiplication, the restriction of scalars operation that converts a continuous $\mathbb{K}$-multilinear map $\prod_i E_i \to F$ into a continuous $\mathbb{K}'$-multilinear map is itself a continuous linear map between the corresponding spaces of continuous multilinear maps.

ContinuousMultilinearMap.apply definition

[ContinuousConstSMul 𝕜 F] (m : Π i, E i) : ContinuousMultilinearMap 𝕜 E F →L[𝕜] F

Full source

/-- The application of a multilinear map as a `ContinuousLinearMap`. -/
def apply [ContinuousConstSMul 𝕜 F] (m : Π i, E i) : ContinuousMultilinearMapContinuousMultilinearMap 𝕜 E F →L[𝕜] F where
  toFun c := c m
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
  cont := continuous_eval_const m

Evaluation map for continuous multilinear maps at a fixed point

Informal description

For a fixed tuple of vectors $ m = (m_i)_{i \in \iota} $ in the product space $ \prod_i E_i $, the evaluation map that sends a continuous multilinear map $ c $ to its value $ c(m) $ is a continuous linear map from the space of continuous multilinear maps $ \text{ContinuousMultilinearMap}\, \mathbb{K}\, E\, F $ to $ F $.

ContinuousMultilinearMap.apply_apply theorem

[ContinuousConstSMul 𝕜 F] {m : Π i, E i} {c : ContinuousMultilinearMap 𝕜 E F} : apply 𝕜 E F m c = c m

Full source

@[simp]
lemma apply_apply [ContinuousConstSMul 𝕜 F] {m : Π i, E i} {c : ContinuousMultilinearMap 𝕜 E F} :
    apply 𝕜 E F m c = c m := rfl

Evaluation of Continuous Multilinear Maps at Fixed Point

Informal description

For any fixed tuple of vectors $m = (m_i)_{i \in \iota}$ in the product space $\prod_i E_i$ and any continuous multilinear map $c$ from $\prod_i E_i$ to $F$, the evaluation of the linear map $\text{apply}_{\mathbb{K},E,F}(m)$ at $c$ equals the evaluation of $c$ at $m$, i.e., $\text{apply}_{\mathbb{K},E,F}(m)(c) = c(m)$.

ContinuousMultilinearMap.hasSum_eval theorem

 {α : Type*} {p : α → ContinuousMultilinearMap 𝕜 E F} {q : ContinuousMultilinearMap 𝕜 E F} (h : HasSum p q)
  (m : Π i, E i) : HasSum (fun a => p a m) (q m)

Full source

theorem hasSum_eval {α : Type*} {p : α → ContinuousMultilinearMap 𝕜 E F}
    {q : ContinuousMultilinearMap 𝕜 E F} (h : HasSum p q) (m : Π i, E i) :
    HasSum (fun a => p a m) (q m) :=
  h.map (applyAddHom m) (continuous_eval_const m)

Summation of Evaluations of Continuous Multilinear Maps

Informal description

Let $\{p_a\}_{a \in \alpha}$ be a family of continuous multilinear maps from $\prod_{i} E_i$ to $F$ indexed by a type $\alpha$, and let $q$ be a continuous multilinear map. If the family $\{p_a\}$ has sum $q$ in the space of continuous multilinear maps, then for any fixed tuple $m = (m_i)_{i \in \iota}$ in $\prod_{i} E_i$, the family of evaluations $\{p_a(m)\}_{a \in \alpha}$ has sum $q(m)$ in $F$.

ContinuousMultilinearMap.tsum_eval theorem

 [T2Space F] {α : Type*} {p : α → ContinuousMultilinearMap 𝕜 E F} (hp : Summable p) (m : Π i, E i) :
  (∑' a, p a) m = ∑' a, p a m

Full source

theorem tsum_eval [T2Space F] {α : Type*} {p : α → ContinuousMultilinearMap 𝕜 E F} (hp : Summable p)
    (m : Π i, E i) : (∑' a, p a) m = ∑' a, p a m :=
  (hasSum_eval hp.hasSum m).tsum_eq.symm

Evaluation of Sum of Continuous Multilinear Maps Equals Sum of Evaluations

Informal description

Let $F$ be a Hausdorff topological space and $\{p_a\}_{a \in \alpha}$ be a summable family of continuous multilinear maps from $\prod_{i} E_i$ to $F$. For any fixed tuple $m = (m_i)_{i \in \iota}$ in $\prod_{i} E_i$, the evaluation of the sum of the family $\{p_a\}$ at $m$ equals the sum of the evaluations $\{p_a(m)\}_{a \in \alpha}$, i.e., \[ \left(\sum_{a} p_a\right)(m) = \sum_{a} p_a(m). \]