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 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

@[implicit_reducible]

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] [IsTopologicalAddGroup F] : TopologicalSpace (ContinuousMultilinearMap 𝕜 E F)

Equations

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

@[implicit_reducible]

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] [IsUniformAddGroup 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] [IsUniformAddGroup F] : IsUniformInducing 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] [IsUniformAddGroup F] : 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] [IsUniformAddGroup F] : Topology.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] [IsUniformAddGroup 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] [IsUniformAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] (x : (i : ι) → E i) : UniformContinuous fun (f : ContinuousMultilinearMap 𝕜 E F) => f x

instance ContinuousMultilinearMap.instIsUniformAddGroup {𝕜 : 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] [IsUniformAddGroup F] : IsUniformAddGroup (ContinuousMultilinearMap 𝕜 E 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] [IsUniformAddGroup F] {M : Type u_5} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜 M F] [ContinuousConstSMul M F] : UniformContinuousConstSMul M (ContinuousMultilinearMap 𝕜 E 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] [IsUniformAddGroup F] {G : Type u_5} [AddCommGroup G] [UniformSpace G] [IsUniformAddGroup 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] [IsUniformAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] (h : Topology.IsCoherentWith {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] [IsUniformAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] [ContinuousConstSMul 𝕜 F] [CompleteSpace F] [∀ (i : ι), IsTopologicalAddGroup (E i)] [SequentialSpace ((i : ι) → E i)] : CompleteSpace (ContinuousMultilinearMap 𝕜 E F)

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] [IsUniformAddGroup F] (𝕜' : Type u_5) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [(i : ι) → Module 𝕜' (E i)] [∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] : 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] [IsUniformAddGroup F] (𝕜' : Type u_5) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [(i : ι) → Module 𝕜' (E i)] [∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] : UniformContinuous (restrictScalars 𝕜')

instance ContinuousMultilinearMap.instIsTopologicalAddGroup {𝕜 : 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] [IsTopologicalAddGroup F] : IsTopologicalAddGroup (ContinuousMultilinearMap 𝕜 E 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] [IsTopologicalAddGroup 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] [IsTopologicalAddGroup 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] [IsTopologicalAddGroup 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] [IsTopologicalAddGroup 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}

theorem ContinuousMultilinearMap.eventually_nhds_zero_mapsTo {𝕜 : 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] [IsTopologicalAddGroup F] {s : Set ((i : ι) → E i)} (hs : Bornology.IsVonNBounded 𝕜 s) {U : Set F} (hu : U ∈ nhds 0) : ∀ᶠ (f : ContinuousMultilinearMap 𝕜 E F) in nhds 0, Set.MapsTo (⇑f) s U

theorem ContinuousMultilinearMap.isVonNBounded_image2_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] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] {S : Set (ContinuousMultilinearMap 𝕜 E F)} (hS : Bornology.IsVonNBounded 𝕜 S) {s : Set ((i : ι) → E i)} (hs : Bornology.IsVonNBounded 𝕜 s) : Bornology.IsVonNBounded 𝕜 (Set.image2 (fun (f : ContinuousMultilinearMap 𝕜 E F) (x : (i : ι) → E i) => f x) S s)

def ContinuousMultilinearMap.compContinuousLinearMapL {𝕜 : 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] [IsTopologicalAddGroup F] {E₁ : ι → Type u_5} [(i : ι) → TopologicalSpace (E₁ i)] [ContinuousConstSMul 𝕜 F] [(i : ι) → AddCommGroup (E₁ i)] [(i : ι) → Module 𝕜 (E₁ i)] (f : (i : ι) → E i →L[𝕜] E₁ i) : ContinuousMultilinearMap 𝕜 E₁ F →L[𝕜] ContinuousMultilinearMap 𝕜 E F

ContinuousMultilinearMap.compContinuousLinearMap as a bundled continuous linear map. Given a family of continuous linear maps f : Π i, E i →L[𝕜] E₁ i, this function returns a continuous linear maps between the spaces of continuous multilinear maps on Π i, E₁ i and on Π i, E i. The map sends g to the map given by v ↦ g (fun i ↦ f i (v i)).

Actually, the map is multilinear in f, see ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear.

For a version fixing g and varying f, see compContinuousLinearMapLRight.

Equations

• ContinuousMultilinearMap.compContinuousLinearMapL f = { toFun := fun (g : ContinuousMultilinearMap 𝕜 E₁ F) => g.compContinuousLinearMap f, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

@[simp]

theorem ContinuousMultilinearMap.compContinuousLinearMapL_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] [IsTopologicalAddGroup F] {E₁ : ι → Type u_5} [(i : ι) → TopologicalSpace (E₁ i)] [ContinuousConstSMul 𝕜 F] [(i : ι) → AddCommGroup (E₁ i)] [(i : ι) → Module 𝕜 (E₁ i)] (f : (i : ι) → E i →L[𝕜] E₁ i) (g : ContinuousMultilinearMap 𝕜 E₁ F) : (compContinuousLinearMapL f) g = g.compContinuousLinearMap f

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] [IsTopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] : ContinuousEvalConst (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i) F

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] [IsTopologicalAddGroup 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] [IsTopologicalAddGroup 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] [IsTopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] {𝕜' : Type u_5} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [(i : ι) → Module 𝕜' (E i)] [∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] : Topology.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] [IsTopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] {𝕜' : Type u_5} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [(i : ι) → Module 𝕜' (E i)] [∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] : Continuous (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] [IsTopologicalAddGroup 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 := ⋯ }

@[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] [IsTopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] (𝕜' : Type u_5) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [(i : ι) → Module 𝕜' (E i)] [∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] [ContinuousConstSMul 𝕜' F] : ⇑(restrictScalarsLinear 𝕜') = restrictScalars 𝕜'

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] [IsTopologicalAddGroup 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] [IsTopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] [ContinuousConstSMul 𝕜 F] {m : (i : ι) → E i} {c : ContinuousMultilinearMap 𝕜 E F} : (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] [IsTopologicalAddGroup 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] [IsTopologicalAddGroup 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

def ContinuousLinearMap.compContinuousMultilinearMapL (𝕜 : Type u_1) {ι : Type u_2} (E : ι → Type u_3) (F : Type u_4) (G : Type u_5) [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] : (F →L[𝕜] G) →L[𝕜] ContinuousMultilinearMap 𝕜 E F →L[𝕜] ContinuousMultilinearMap 𝕜 E G

ContinuousLinearMap.compContinuousMultilinearMap as a bundled continuous bilinear map.

Given a continuous linear map f : F →L[𝕜] G and a continuous multilinear map g from Π i, E i to F, this function returns f ∘ g as a continuous multilinear map.

With this order of arguments, the function is continuous in g (for each fixed f) and is continuous in f (as a function to the space of continuous linear maps). Note that for general topological vector spaces, it is not guaranteed to be continuous in (g, f).

Equations

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

@[simp]

theorem ContinuousLinearMap.compContinuousMultilinearMapL_apply {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} {G : Type u_5} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] (g : F →L[𝕜] G) (f : ContinuousMultilinearMap 𝕜 E F) : ((compContinuousMultilinearMapL 𝕜 E F G) g) f = g.compContinuousMultilinearMap f

def ContinuousLinearEquiv.continuousMultilinearMapCongrLeft {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {E₁ : ι → Type u_4} (F : Type u_5) [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [(i : ι) → TopologicalSpace (E₁ i)] [(i : ι) → AddCommGroup (E₁ i)] [(i : ι) → Module 𝕜 (E₁ i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] (f : (i : ι) → E i ≃L[𝕜] E₁ i) : ContinuousMultilinearMap 𝕜 E₁ F ≃L[𝕜] ContinuousMultilinearMap 𝕜 E F

ContinuousMultilinearMap.compContinuousLinearMap as a bundled continuous linear equiv. Given a family of continuous linear equivalences f : Π i, E i ≃L[𝕜] E₁ i, this function returns a continuous linear equivalence between the space of continuous multilinear maps with domain Π i, E i and codomain F and the space of multilinear maps with domain Π i, E₁ i and the same codomain, by composing the multilinear maps with f.

Equations

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

@[simp]

theorem ContinuousLinearEquiv.continuousMultilinearMapCongrLeft_symm {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {E₁ : ι → Type u_4} {F : Type u_5} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [(i : ι) → TopologicalSpace (E₁ i)] [(i : ι) → AddCommGroup (E₁ i)] [(i : ι) → Module 𝕜 (E₁ i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] (f : (i : ι) → E i ≃L[𝕜] E₁ i) : (continuousMultilinearMapCongrLeft F f).symm = continuousMultilinearMapCongrLeft F fun (i : ι) => (f i).symm

@[simp]

theorem ContinuousLinearEquiv.continuousMultilinearMapCongrLeft_apply {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {E₁ : ι → Type u_4} {F : Type u_5} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [(i : ι) → TopologicalSpace (E₁ i)] [(i : ι) → AddCommGroup (E₁ i)] [(i : ι) → Module 𝕜 (E₁ i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] (g : ContinuousMultilinearMap 𝕜 E₁ F) (f : (i : ι) → E i ≃L[𝕜] E₁ i) : (continuousMultilinearMapCongrLeft F f) g = g.compContinuousLinearMap fun (i : ι) => ↑(f i)

def ContinuousLinearEquiv.continuousMultilinearMapCongrRight {𝕜 : Type u_1} {ι : Type u_2} (E : ι → Type u_3) {F : Type u_5} {G : Type u_6} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] (g : F ≃L[𝕜] G) : ContinuousMultilinearMap 𝕜 E F ≃L[𝕜] ContinuousMultilinearMap 𝕜 E G

ContinuousLinearMap.compContinuousMultilinearMap as a bundled continuous linear equiv. Given a continuous linear equivalence g : F ≃L[𝕜] G, this function builds a continuous linear equivalence between the space of continuous multilinear maps with codomain F and the space of continuous multilinear maps with codomain G, by composing these maps with g or g.symm.

Equations

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

@[simp]

theorem ContinuousLinearEquiv.continuousMultilinearMapCongrRight_symm {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_5} {G : Type u_6} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] (g : F ≃L[𝕜] G) : (continuousMultilinearMapCongrRight E g).symm = continuousMultilinearMapCongrRight E g.symm

@[simp]

theorem ContinuousLinearEquiv.continuousMultilinearMapCongrRight_apply {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_5} {G : Type u_6} [NormedField 𝕜] [(i : ι) → TopologicalSpace (E i)] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] (g : F ≃L[𝕜] G) (f : ContinuousMultilinearMap 𝕜 E F) : (continuousMultilinearMapCongrRight E g) f = (↑g).compContinuousMultilinearMap f