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
Instances For
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]
:
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]
:
Topology.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]
:
Topology.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]
:
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]
:
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 : Topology.RestrictGenTopology {s : Set ((i : ι) → E i) | Bornology.IsVonNBounded 𝕜 s})
:
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)]
:
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)]
:
@[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)]
:
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)]
:
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]
:
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)
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)
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
@[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✝¹ : TopologicalSpace F}
{inst✝² : TopologicalSpace X}
[self : ContinuousEvalConst F α X]
(x : α)
:
Continuous fun (f : F) => f x
@[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✝¹ : TopologicalSpace F}
{inst✝² : TopologicalSpace X}
[self : ContinuousEvalConst F α X]
(x : α)
:
Continuous fun (f : F) => f x
@[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)
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)
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]
:
@[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]
:
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]
:
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 := ⋯ }
Instances For
@[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]
:
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 := ⋯ }
Instances For
@[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