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.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] : UniformEmbedding ContinuousMultilinearMap.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] : Embedding ContinuousMultilinearMap.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.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] [T2Space 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] [T2Space F] [∀ (i : ι), TopologicalAddGroup (E i)] [SequentialSpace ((i : ι) → E i)] : CompleteSpace (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}

theorem ContinuousMultilinearMap.continuous_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] [TopologicalSpace F] [TopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] (x : (i : ι) → E i) : Continuous fun (p : ContinuousMultilinearMap 𝕜 E F) => p x

@[deprecated ContinuousMultilinearMap.continuous_eval_const]

theorem ContinuousMultilinearMap.continuous_eval_left {𝕜 : 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)] (x : (i : ι) → E i) : Continuous fun (p : ContinuousMultilinearMap 𝕜 E F) => p x

Alias of ContinuousMultilinearMap.continuous_eval_const.

theorem ContinuousMultilinearMap.continuous_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] [TopologicalSpace F] [TopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] : Continuous DFunLike.coe

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

• ⋯ = ⋯

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