Isbilinearmap

Mathlib/Analysis/Normed/Module/FiniteDimension.lean

@@ -680,3 +680,39 @@ theorem IsEquivalent.summable_iff {ι E : Type*} [NormedAddCommGroup E] [NormedS
 theorem IsEquivalent.summable_iff_nat {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
     [FiniteDimensional ℝ E] {f : ℕ → E} {g : ℕ → E} (h : f ~[atTop] g) : Summable f ↔ Summable g :=
   ⟨fun hf => summable_of_isEquivalent_nat hf h.symm, fun hg => summable_of_isEquivalent_nat hg h⟩
+
+
+def IsBilinearMap.toContinuousLinearMap
+    {𝕜 : Type*} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
+    {E : Type*} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E]
+    [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [FiniteDimensional 𝕜 E]
+    [T2Space E]
+    {F : Type*} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F]
+    [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] [FiniteDimensional 𝕜 F]
+    [T2Space F]
+    {G : Type*} [AddCommGroup G] [Module 𝕜 G] [TopologicalSpace G]
+    [IsTopologicalAddGroup G] [ContinuousSMul 𝕜 G]
+    {f : E → F → G} (h : IsBilinearMap 𝕜 f) : E →L[𝕜] F →L[𝕜] G :=
+  IsLinearMap.mk' (fun x : E ↦ h.toLinearMap x |>.toContinuousLinearMap)
+      (by constructor <;> (intros;simp)) |>.toContinuousLinearMap
+
+def isBilinearMap_evalL
+    (𝕜 : Type*) [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
+    (E : Type*) [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E]
+    [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [FiniteDimensional 𝕜 E]
+    [T2Space E]
+    (F : Type*) [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F]
+    [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] [FiniteDimensional 𝕜 F]
+    [T2Space F] :
+    IsBilinearMap 𝕜 (fun (e : E) (φ : E →L[𝕜] F) ↦ φ e) := by
+  constructor <;> simp
+
+def evalL
+    (𝕜 : Type*) [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
+    (E : Type*) [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E]
+    [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [FiniteDimensional 𝕜 E]
+    [T2Space E]
+    (F : Type*) [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F]
+    [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] [FiniteDimensional 𝕜 F]
+    [T2Space F] : E →L[𝕜] (E →L[𝕜] F) →L[𝕜] F :=
+  (isBilinearMap_evalL 𝕜 E F).toContinuousLinearMap

Mathlib/LinearAlgebra/BilinearMap.lean

@@ -431,6 +431,34 @@ variable (R M Nₗ) in
 /-- A shorthand for the type of `R`-bilinear `Nₗ`-valued maps on `M`. -/
 protected abbrev BilinMap : Type _ := M →ₗ[R] M →ₗ[R] Nₗ
 
+variable (R) in
+structure IsBilinearMap (R : Type*) {E F G : Type*} [Semiring R]
+    [AddCommMonoid E] [AddCommMonoid F] [AddCommMonoid G]
+    [Module R E] [Module R F] [Module R G] (f : E → F → G) : Prop where
+  add_left : ∀ (x₁ x₂ : E) (y : F), f (x₁ + x₂) y = f x₁ y + f x₂ y
+  smul_left : ∀ (c : R) (x : E) (y : F), f (c • x) y = c • f x y
+  add_right : ∀ (x : E) (y₁ y₂ : F), f x (y₁ + y₂) = f x y₁ + f x y₂
+  smul_right : ∀ (c : R) (x : E) (y : F), f x (c • y) = c • f x y
+
+lemma BilinMap.isBilinearMap (f : LinearMap.BilinMap R M Nₗ) :
+    IsBilinearMap R (f.toFun · : M → M → Nₗ) where
+  add_left := by intros; simp
+  add_right := by intros; simp
+  smul_left := by intros; simp
+  smul_right := by intros; simp
+
+def IsBilinearMap.toLinearMap {f : M → Pₗ → Qₗ} (hf : IsBilinearMap R f) :
+    M →ₗ[R] Pₗ →ₗ[R] Qₗ :=
+  LinearMap.mk₂ _ f hf.add_left hf.smul_left hf.add_right hf.smul_right
+
+def IsBilinearMap.toBilinMap {f : M → M → Mₗ} (hf : IsBilinearMap R f) :
+    LinearMap.BilinMap R M Mₗ :=
+  hf.toLinearMap
+
+variable (R M Mₗ) in
+lemma isBilinearMap_eval : IsBilinearMap R (fun (e : M) (φ : M →ₗ[R] Mₗ) ↦ φ e) := by
+  constructor <;> simp
+
 variable (R M) in
 /-- For convenience, a shorthand for the type of bilinear forms from `M` to `R`. -/
 protected abbrev BilinForm : Type _ := LinearMap.BilinMap R M R