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.

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

@[deprecated ContinuousLinearMap.apply (since := "2026-08-21")]

def ContinuousLinearMap.evalL (𝕜 : Type u_1) {E' : Type u_6} (Fₗ' : Type u_11) [NontriviallyNormedField 𝕜] [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup Fₗ'] [Module 𝕜 Fₗ'] [TopologicalSpace Fₗ'] [IsNormableSpace 𝕜 Fₗ'] [IsNormableSpace 𝕜 E'] [IsTopologicalAddGroup Fₗ'] : E' →L[𝕜] (E' →L[𝕜] Fₗ') →L[𝕜] Fₗ'

Alias of ContinuousLinearMap.apply.

Equations

• ContinuousLinearMap.evalL = ContinuousLinearMap.apply

@[deprecated ContinuousLinearMap.apply_apply (since := "2026-08-21")]

theorem ContinuousLinearMap.evalL_apply {𝕜 : Type u_1} {E' : Type u_6} {Fₗ' : Type u_11} [NontriviallyNormedField 𝕜] [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] [AddCommGroup Fₗ'] [Module 𝕜 Fₗ'] [TopologicalSpace Fₗ'] [IsNormableSpace 𝕜 Fₗ'] [IsNormableSpace 𝕜 E'] [IsTopologicalAddGroup Fₗ'] (v : E') (f : E' →L[𝕜] Fₗ') : ((apply 𝕜 Fₗ') v) f = f v

Alias of ContinuousLinearMap.apply_apply.