Building continuous bilinear maps in finite dimensions over complete fields

Given a complete nontrivially normed field 𝕜 and finite dimensional T₂ topological vector spaces over 𝕜, this file builds a continuous bilinear map from any bilinear function.

This applies in particular to evaluation of linear maps between such spaces.

Working with topological vector spaces instead of normed spaces is important for applications in the differential geometry part of Mathlib where we don’t want to fix a norm on tangent spaces for instance.

def LinearMap.toContinuousBilinearMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [FiniteDimensional 𝕜 E] [T2Space E] {F : Type u_3} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] [FiniteDimensional 𝕜 F] [T2Space F] {G : Type u_4} [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousSMul 𝕜 G] (f : E →ₗ[𝕜] F →ₗ[𝕜] G) : E →L[𝕜] F →L[𝕜] G

Building continuous bilinear maps from bilinear maps between finite dimensional topological vector spaces over a complete field.

Equations

• f.toContinuousBilinearMap = LinearMap.toContinuousLinearMap (IsLinearMap.mk' (fun (x : E) => LinearMap.toContinuousLinearMap (f x)) ⋯)

@[simp]

theorem LinearMap.toContinuousBilinearMap_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [FiniteDimensional 𝕜 E] [T2Space E] {F : Type u_3} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] [FiniteDimensional 𝕜 F] [T2Space F] {G : Type u_4} [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousSMul 𝕜 G] (f : E →ₗ[𝕜] F →ₗ[𝕜] G) (x : E) (y : F) : (f.toContinuousBilinearMap x) y = (f x) y

def IsBilinearMap.toContinuousBilinearMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [FiniteDimensional 𝕜 E] [T2Space E] {F : Type u_3} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] [FiniteDimensional 𝕜 F] [T2Space F] {G : Type u_4} [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousSMul 𝕜 G] {f : E → F → G} (h : IsBilinearMap 𝕜 f) : E →L[𝕜] F →L[𝕜] G

Building continuous bilinear maps from bilinear functions between finite dimensional topological vector spaces over a complete field.

Equations

• h.toContinuousBilinearMap = h.toLinearMap.toContinuousBilinearMap

@[simp]

theorem IsBilinearMap.toContinuousBilinearMap_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [FiniteDimensional 𝕜 E] [T2Space E] {F : Type u_3} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] [FiniteDimensional 𝕜 F] [T2Space F] {G : Type u_4} [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousSMul 𝕜 G] {f : E → F → G} (h : IsBilinearMap 𝕜 f) (x : E) (y : F) : (h.toContinuousBilinearMap x) y = f x y

def ContinuousLinearMap.evalL (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] (E : Type u_2) [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [FiniteDimensional 𝕜 E] [T2Space E] (F : Type u_3) [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] [FiniteDimensional 𝕜 F] [T2Space F] : E →L[𝕜] (E →L[𝕜] F) →L[𝕜] F

Evaluation of continuous linear maps as a continuous linear map in the case of finite dimensional topological vector spaces over a complete field. See also ContinuousLinearMap.apply for the case of normed spaces.

TODO: generalize the two constructions in the setting of maps from a bornological space to a locally convex one, or define a NormableSpace class to deduce this case from the normed case.

Equations

• ContinuousLinearMap.evalL 𝕜 E F = (↑LinearMap.toContinuousLinearMap.symm).flip.toContinuousBilinearMap

@[simp]

theorem ContinuousLinearMap.evalL_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [FiniteDimensional 𝕜 E] [T2Space E] {F : Type u_3} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] [FiniteDimensional 𝕜 F] [T2Space F] (x : E) (φ : E →L[𝕜] F) : ((evalL 𝕜 E F) x) φ = φ x