Topology on continuous multilinear maps

In this file we define TopologicalSpace and UniformSpace structures on ContinuousMultilinearMap 𝕜 E F, where E i is a family of vector spaces over 𝕜 with topologies and F is a topological vector space.

def ContinuousMultilinearMap.toUniformOnFun {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (f : ContinuousMultilinearMap 𝕜 E F) : UniformOnFun ((i : ι) → E i) F {s : Set ((i : ι) → E i) | Bornology.IsVonNBounded 𝕜 s}

An auxiliary definition used to define topology on ContinuousMultilinearMap 𝕜 E F.

Equations

• f.toUniformOnFun = (UniformOnFun.ofFun {s : Set ((i : ι) → E i) | Bornology.IsVonNBounded 𝕜 s}) ⇑f

theorem ContinuousMultilinearMap.range_toUniformOnFun {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [DecidableEq ι] [TopologicalSpace F] : Set.range ContinuousMultilinearMap.toUniformOnFun = {f : UniformOnFun ((i : ι) → E i) F {s : Set ((i : ι) → E i) | Bornology.IsVonNBounded 𝕜 s} | Continuous ((UniformOnFun.toFun {s : Set ((i : ι) → E i) | Bornology.IsVonNBounded 𝕜 s}) f) ∧ (∀ (m : (i : ι) → E i) (i : ι) (x y : E i), (UniformOnFun.toFun {s : Set ((i : ι) → E i) | Bornology.IsVonNBounded 𝕜 s}) f (Function.update m i (x + y)) = (UniformOnFun.toFun {s : Set ((i : ι) → E i) | Bornology.IsVonNBounded 𝕜 s}) f (Function.update m i x) + (UniformOnFun.toFun {s : Set ((i : ι) → E i) | Bornology.IsVonNBounded 𝕜 s}) f (Function.update m i y)) ∧ ∀ (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x : E i), (UniformOnFun.toFun {s : Set ((i : ι) → E i) | Bornology.IsVonNBounded 𝕜 s}) f (Function.update m i (c • x)) = c • (UniformOnFun.toFun {s : Set ((i : ι) → E i) | Bornology.IsVonNBounded 𝕜 s}) f (Function.update m i x)}

@[simp]

theorem ContinuousMultilinearMap.toUniformOnFun_toFun {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] (f : ContinuousMultilinearMap 𝕜 E F) : (UniformOnFun.toFun {s : Set ((i : ι) → E i) | Bornology.IsVonNBounded 𝕜 s}) f.toUniformOnFun = ⇑f

instance ContinuousMultilinearMap.instTopologicalSpace {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] : TopologicalSpace (ContinuousMultilinearMap 𝕜 E F)

Equations

• One or more equations did not get rendered due to their size.

instance ContinuousMultilinearMap.instUniformSpace {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] : UniformSpace (ContinuousMultilinearMap 𝕜 E F)

Equations

• One or more equations did not get rendered due to their size.

theorem ContinuousMultilinearMap.isUniformInducing_toUniformOnFun {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] : IsUniformInducing ContinuousMultilinearMap.toUniformOnFun

theorem ContinuousMultilinearMap.isUniformEmbedding_toUniformOnFun {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] : IsUniformEmbedding ContinuousMultilinearMap.toUniformOnFun

@[deprecated ContinuousMultilinearMap.isUniformEmbedding_toUniformOnFun]

theorem ContinuousMultilinearMap.uniformEmbedding_toUniformOnFun {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] : IsUniformEmbedding ContinuousMultilinearMap.toUniformOnFun

Alias of ContinuousMultilinearMap.isUniformEmbedding_toUniformOnFun.

theorem ContinuousMultilinearMap.isEmbedding_toUniformOnFun {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] : IsEmbedding ContinuousMultilinearMap.toUniformOnFun

@[deprecated ContinuousMultilinearMap.isEmbedding_toUniformOnFun]

theorem ContinuousMultilinearMap.embedding_toUniformOnFun {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] : IsEmbedding ContinuousMultilinearMap.toUniformOnFun

Alias of ContinuousMultilinearMap.isEmbedding_toUniformOnFun.

theorem ContinuousMultilinearMap.uniformContinuous_coe_fun {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] : UniformContinuous DFunLike.coe

theorem ContinuousMultilinearMap.uniformContinuous_eval_const {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] (x : (i : ι) → E i) : UniformContinuous fun (f : ContinuousMultilinearMap 𝕜 E F) => f x

instance ContinuousMultilinearMap.instUniformAddGroup {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] : UniformAddGroup (ContinuousMultilinearMap 𝕜 E F)

Equations

• ⋯ = ⋯

instance ContinuousMultilinearMap.instUniformContinuousConstSMul {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] {M : Type u_5} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜 M F] [ContinuousConstSMul M F] : UniformContinuousConstSMul M (ContinuousMultilinearMap 𝕜 E F)

Equations

• ⋯ = ⋯

theorem ContinuousMultilinearMap.isUniformInducing_postcomp {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] {G : Type u_5} [AddCommGroup G] [UniformSpace G] [UniformAddGroup G] [Module 𝕜 G] (g : F →L[𝕜] G) (hg : IsUniformInducing ⇑g) : IsUniformInducing g.compContinuousMultilinearMap

theorem ContinuousMultilinearMap.completeSpace {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (h : RestrictGenTopology {s : Set ((i : ι) → E i) | Bornology.IsVonNBounded 𝕜 s}) : CompleteSpace (ContinuousMultilinearMap 𝕜 E F)

instance ContinuousMultilinearMap.instCompleteSpace {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] [∀ (i : ι), TopologicalAddGroup (E i)] [SequentialSpace ((i : ι) → E i)] : CompleteSpace (ContinuousMultilinearMap 𝕜 E F)

Equations

• ⋯ = ⋯

theorem ContinuousMultilinearMap.isUniformEmbedding_restrictScalars {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] (𝕜' : Type u_5) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [(i : ι) → Module 𝕜' (E i)] [∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] : IsUniformEmbedding (ContinuousMultilinearMap.restrictScalars 𝕜')

@[deprecated ContinuousMultilinearMap.isUniformEmbedding_restrictScalars]

theorem ContinuousMultilinearMap.uniformEmbedding_restrictScalars {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] (𝕜' : Type u_5) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [(i : ι) → Module 𝕜' (E i)] [∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] : IsUniformEmbedding (ContinuousMultilinearMap.restrictScalars 𝕜')

Alias of ContinuousMultilinearMap.isUniformEmbedding_restrictScalars.

theorem ContinuousMultilinearMap.uniformContinuous_restrictScalars {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [UniformSpace F] [UniformAddGroup F] (𝕜' : Type u_5) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [(i : ι) → Module 𝕜' (E i)] [∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] : UniformContinuous (ContinuousMultilinearMap.restrictScalars 𝕜')

instance ContinuousMultilinearMap.instTopologicalAddGroup {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] : TopologicalAddGroup (ContinuousMultilinearMap 𝕜 E F)

Equations

• ⋯ = ⋯

instance ContinuousMultilinearMap.instContinuousConstSMul {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] {M : Type u_5} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜 M F] [ContinuousConstSMul M F] : ContinuousConstSMul M (ContinuousMultilinearMap 𝕜 E F)

Equations

• ⋯ = ⋯

instance ContinuousMultilinearMap.instContinuousSMul {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousSMul 𝕜 F] : ContinuousSMul 𝕜 (ContinuousMultilinearMap 𝕜 E F)

Equations

• ⋯ = ⋯

theorem ContinuousMultilinearMap.hasBasis_nhds_zero_of_basis {𝕜 : Type u_1} {ι : Type u_2} {E : ι✝ → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι✝) → TopologicalSpace (E i)] [(i : ι✝) → AddCommGroup (E i)] [(i : ι✝) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] {ι : Type u_5} {p : ι → Prop} {b : ι → Set F} (h : (nhds 0).HasBasis p b) : (nhds 0).HasBasis (fun (Si : Set ((i : ι✝) → E i) × ι) => Bornology.IsVonNBounded 𝕜 Si.1 ∧ p Si.2) fun (Si : Set ((i : ι✝) → E i) × ι) => {f : ContinuousMultilinearMap 𝕜 E F | Set.MapsTo (⇑f) Si.1 (b Si.2)}

theorem ContinuousMultilinearMap.hasBasis_nhds_zero {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] : (nhds 0).HasBasis (fun (SV : Set ((i : ι) → E i) × Set F) => Bornology.IsVonNBounded 𝕜 SV.1 ∧ SV.2 ∈ nhds 0) fun (SV : Set ((i : ι) → E i) × Set F) => {f : ContinuousMultilinearMap 𝕜 E F | Set.MapsTo (⇑f) SV.1 SV.2}

instance ContinuousMultilinearMap.instContinuousEvalConstForall {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] : ContinuousEvalConst (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i) F

Equations

• ⋯ = ⋯

@[deprecated ContinuousEvalConst.continuous_eval_const]

theorem ContinuousMultilinearMap.continuous_eval_const {F : Type u_1} {α : outParam (Type u_2)} {X : outParam (Type u_3)} : ∀ {inst : FunLike F α X} {inst_1 : TopologicalSpace F} {inst_2 : TopologicalSpace X} [self : ContinuousEvalConst F α X] (x : α), Continuous fun (f : F) => f x

Alias of ContinuousEvalConst.continuous_eval_const.

@[deprecated ContinuousEvalConst.continuous_eval_const]

theorem ContinuousMultilinearMap.continuous_eval_left {F : Type u_1} {α : outParam (Type u_2)} {X : outParam (Type u_3)} : ∀ {inst : FunLike F α X} {inst_1 : TopologicalSpace F} {inst_2 : TopologicalSpace X} [self : ContinuousEvalConst F α X] (x : α), Continuous fun (f : F) => f x

Alias of ContinuousEvalConst.continuous_eval_const.

@[deprecated continuous_coeFun]

theorem ContinuousMultilinearMap.continuous_coe_fun {F : Type u_1} {α : Type u_2} {X : Type u_3} [FunLike F α X] [TopologicalSpace F] [TopologicalSpace X] [ContinuousEvalConst F α X] : Continuous DFunLike.coe

Alias of continuous_coeFun.

instance ContinuousMultilinearMap.instT2Space {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] [T2Space F] : T2Space (ContinuousMultilinearMap 𝕜 E F)

Equations

• ⋯ = ⋯

instance ContinuousMultilinearMap.instT3Space {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] [T2Space F] : T3Space (ContinuousMultilinearMap 𝕜 E F)

Equations

• ⋯ = ⋯

theorem ContinuousMultilinearMap.isEmbedding_restrictScalars {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] {𝕜' : Type u_5} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [(i : ι) → Module 𝕜' (E i)] [∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] : IsEmbedding (ContinuousMultilinearMap.restrictScalars 𝕜')

@[deprecated ContinuousMultilinearMap.isEmbedding_restrictScalars]

theorem ContinuousMultilinearMap.embedding_restrictScalars {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] {𝕜' : Type u_5} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [(i : ι) → Module 𝕜' (E i)] [∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] : IsEmbedding (ContinuousMultilinearMap.restrictScalars 𝕜')

Alias of ContinuousMultilinearMap.isEmbedding_restrictScalars.

theorem ContinuousMultilinearMap.continuous_restrictScalars {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] {𝕜' : Type u_5} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [(i : ι) → Module 𝕜' (E i)] [∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] : Continuous (ContinuousMultilinearMap.restrictScalars 𝕜')

@[simp]

theorem ContinuousMultilinearMap.restrictScalarsLinear_apply {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] (𝕜' : Type u_5) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [(i : ι) → Module 𝕜' (E i)] [∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] [ContinuousConstSMul 𝕜' F] : ⇑(ContinuousMultilinearMap.restrictScalarsLinear 𝕜') = ContinuousMultilinearMap.restrictScalars 𝕜'

def ContinuousMultilinearMap.restrictScalarsLinear {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] (𝕜' : Type u_5) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [(i : ι) → Module 𝕜' (E i)] [∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] [ContinuousConstSMul 𝕜' F] : ContinuousMultilinearMap 𝕜 E F →L[𝕜'] ContinuousMultilinearMap 𝕜' E F

ContinuousMultilinearMap.restrictScalars as a ContinuousLinearMap.

Equations

• ContinuousMultilinearMap.restrictScalarsLinear 𝕜' = { toFun := ContinuousMultilinearMap.restrictScalars 𝕜', map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

def ContinuousMultilinearMap.apply (𝕜 : Type u_1) {ι : Type u_2} (E : ι → Type u_3) (F : Type u_4) [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] [ContinuousConstSMul 𝕜 F] (m : (i : ι) → E i) : ContinuousMultilinearMap 𝕜 E F →L[𝕜] F

The application of a multilinear map as a ContinuousLinearMap.

Equations

• ContinuousMultilinearMap.apply 𝕜 E F m = { toFun := fun (c : ContinuousMultilinearMap 𝕜 E F) => c m, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

@[simp]

theorem ContinuousMultilinearMap.apply_apply {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] [ContinuousConstSMul 𝕜 F] {m : (i : ι) → E i} {c : ContinuousMultilinearMap 𝕜 E F} : (ContinuousMultilinearMap.apply 𝕜 E F m) c = c m

theorem ContinuousMultilinearMap.hasSum_eval {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] {α : Type u_5} {p : α → ContinuousMultilinearMap 𝕜 E F} {q : ContinuousMultilinearMap 𝕜 E F} (h : HasSum p q) (m : (i : ι) → E i) : HasSum (fun (a : α) => (p a) m) (q m)

theorem ContinuousMultilinearMap.tsum_eval {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [TopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] [T2Space F] {α : Type u_5} {p : α → ContinuousMultilinearMap 𝕜 E F} (hp : Summable p) (m : (i : ι) → E i) : (∑' (a : α), p a) m = ∑' (a : α), (p a) m