From 815dc0aa172a2d0f55be035fe341336992902af6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Micha=C5=82=20Pacholski?= <mpacholski@google.com>
Date: Mon, 13 Jul 2026 21:32:12 +0200
Subject: [PATCH 01/30] =?UTF-8?q?feat(Topology/Algebra/Module/Spaces/Conti?=
 =?UTF-8?q?nuousLinearMap):=20add=20`toLinearMap=E2=82=81=E2=82=82=5Fadd`?=
 =?UTF-8?q?=20and=20`toLinearMap=E2=82=81=E2=82=82=5Fsmul`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Prove that the projection `toLinearMap₁₂` (which strips the topology from a continuous semibilinear map) preserves addition and scalar multiplication, and mark both lemmas with `@[simp]`.
---
 .../Algebra/Module/Spaces/ContinuousLinearMap.lean   | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
index f0a3681fab4122..5df1420e60bd4d 100644
--- a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
+++ b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
@@ -313,6 +313,18 @@ lemma toLinearMap₁₂_inj (L₁ L₂ : E →SL[σ₁₃] F →SL[σ₂₃] G)
     L₁.toLinearMap₁₂ = L₂.toLinearMap₁₂ ↔ L₁ = L₂ :=
   toLinearMap₁₂_injective.eq_iff
 
+@[simp]
+lemma toLinearMap₁₂_add (L₁ L₂ : E →SL[σ₁₃] F →SL[σ₂₃] G) :
+    (L₁ + L₂).toLinearMap₁₂ = L₁.toLinearMap₁₂ + L₂.toLinearMap₁₂ := by
+  ext x y
+  rfl
+
+@[simp]
+lemma toLinearMap₁₂_smul (c : 𝕜₃) (L : E →SL[σ₁₃] F →SL[σ₂₃] G) :
+    (c • L).toLinearMap₁₂ = c • L.toLinearMap₁₂ := by
+  ext x y
+  rfl
+
 end AddCommMonoid
 
 section Nonsemilinear

From 136d68436734b9d8d9bed26a61b0a41847c32dff Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Micha=C5=82=20Pacholski?= <mpacholski@google.com>
Date: Tue, 14 Jul 2026 17:00:06 +0200
Subject: [PATCH 02/30] =?UTF-8?q?feat(ContinuousLinearMap)=20`toLinearMap?=
 =?UTF-8?q?=E2=82=81=E2=82=82`=20as=20a=20linear=20map?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .../Module/Spaces/ContinuousLinearMap.lean    | 20 +++++--------------
 1 file changed, 5 insertions(+), 15 deletions(-)

diff --git a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
index 5df1420e60bd4d..453489a2288922 100644
--- a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
+++ b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
@@ -299,32 +299,22 @@ theorem map_smulₛₗ₂ (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (c : R) (x
     f (c • x) y = σ₁₃ c • f x y := by rw [f.map_smulₛₗ, smul_apply]
 
 /-- Send a continuous sesquilinear map to an abstract sesquilinear map (forgetting continuity). -/
-def toLinearMap₁₂ (L : E →SL[σ₁₃] F →SL[σ₂₃] G) : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G :=
-  (coeLMₛₗ σ₂₃).comp L.toLinearMap
+def toLinearMap₁₂ : (E →SL[σ₁₃] F →SL[σ₂₃] G) →ₗ[𝕜₃] (E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) :=
+  { toFun L := (coeLMₛₗ σ₂₃).comp L.toLinearMap
+    map_add' _ _ := by ext; rfl
+    map_smul' _ _ := by ext; rfl}
 
 @[simp] lemma toLinearMap₁₂_apply (L : E →SL[σ₁₃] F →SL[σ₂₃] G) (v : E) (w : F) :
     L.toLinearMap₁₂ v w = L v w := rfl
 
 lemma toLinearMap₁₂_injective :
-    (toLinearMap₁₂ (E := E) (F := F) (G := G) (σ₁₃ := σ₁₃) (σ₂₃ := σ₂₃)).Injective := by
+    Function.Injective (toLinearMap₁₂ (E := E) (F := F) (G := G) (σ₁₃ := σ₁₃) (σ₂₃ := σ₂₃)) := by
   simp [Function.Injective, LinearMap.ext_iff, ← ContinuousLinearMap.ext_iff]
 
 lemma toLinearMap₁₂_inj (L₁ L₂ : E →SL[σ₁₃] F →SL[σ₂₃] G) :
     L₁.toLinearMap₁₂ = L₂.toLinearMap₁₂ ↔ L₁ = L₂ :=
   toLinearMap₁₂_injective.eq_iff
 
-@[simp]
-lemma toLinearMap₁₂_add (L₁ L₂ : E →SL[σ₁₃] F →SL[σ₂₃] G) :
-    (L₁ + L₂).toLinearMap₁₂ = L₁.toLinearMap₁₂ + L₂.toLinearMap₁₂ := by
-  ext x y
-  rfl
-
-@[simp]
-lemma toLinearMap₁₂_smul (c : 𝕜₃) (L : E →SL[σ₁₃] F →SL[σ₂₃] G) :
-    (c • L).toLinearMap₁₂ = c • L.toLinearMap₁₂ := by
-  ext x y
-  rfl
-
 end AddCommMonoid
 
 section Nonsemilinear

From e345bfe8467b57a9157247f85f279a614b12418d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Micha=C5=82=20Pacholski?= <mpacholski@google.com>
Date: Tue, 14 Jul 2026 17:11:38 +0200
Subject: [PATCH 03/30] =?UTF-8?q?feat(ContinuousLinearMap):=20add=20@[simp?=
 =?UTF-8?q?s=20apply]=20annotation=20to=20toLinearMap=E2=82=81=E2=82=82=20?=
 =?UTF-8?q?and=20remove=20the=20now-duplicate=20toLinearMap=E2=82=81?=
 =?UTF-8?q?=E2=82=82=5Fapply=20lemma?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .../Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean   | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
index 453489a2288922..6c2de4a02bd798 100644
--- a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
+++ b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
@@ -299,14 +299,12 @@ theorem map_smulₛₗ₂ (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (c : R) (x
     f (c • x) y = σ₁₃ c • f x y := by rw [f.map_smulₛₗ, smul_apply]
 
 /-- Send a continuous sesquilinear map to an abstract sesquilinear map (forgetting continuity). -/
+@[simps!]
 def toLinearMap₁₂ : (E →SL[σ₁₃] F →SL[σ₂₃] G) →ₗ[𝕜₃] (E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) :=
   { toFun L := (coeLMₛₗ σ₂₃).comp L.toLinearMap
     map_add' _ _ := by ext; rfl
     map_smul' _ _ := by ext; rfl}
 
-@[simp] lemma toLinearMap₁₂_apply (L : E →SL[σ₁₃] F →SL[σ₂₃] G) (v : E) (w : F) :
-    L.toLinearMap₁₂ v w = L v w := rfl
-
 lemma toLinearMap₁₂_injective :
     Function.Injective (toLinearMap₁₂ (E := E) (F := F) (G := G) (σ₁₃ := σ₁₃) (σ₂₃ := σ₂₃)) := by
   simp [Function.Injective, LinearMap.ext_iff, ← ContinuousLinearMap.ext_iff]

From 242e4da0ddcd0c306dd99372ac83160ac0b55044 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Micha=C5=82=20Pacholski?= <mpacholski@google.com>
Date: Tue, 14 Jul 2026 21:44:18 +0200
Subject: [PATCH 04/30] =?UTF-8?q?Reinstate=20toLinearMap=E2=82=81=E2=82=82?=
 =?UTF-8?q?=5Fapply?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .../Algebra/Module/Spaces/ContinuousLinearMap.lean | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
index 6c2de4a02bd798..8a7541852073fc 100644
--- a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
+++ b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
@@ -299,14 +299,16 @@ theorem map_smulₛₗ₂ (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (c : R) (x
     f (c • x) y = σ₁₃ c • f x y := by rw [f.map_smulₛₗ, smul_apply]
 
 /-- Send a continuous sesquilinear map to an abstract sesquilinear map (forgetting continuity). -/
-@[simps!]
-def toLinearMap₁₂ : (E →SL[σ₁₃] F →SL[σ₂₃] G) →ₗ[𝕜₃] (E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) :=
-  { toFun L := (coeLMₛₗ σ₂₃).comp L.toLinearMap
-    map_add' _ _ := by ext; rfl
-    map_smul' _ _ := by ext; rfl}
+def toLinearMap₁₂ : (E →SL[σ₁₃] F →SL[σ₂₃] G) →ₗ[𝕜₃] (E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) where
+  toFun L := (coeLMₛₗ σ₂₃).comp L.toLinearMap
+  map_add' _ _ := by ext; rfl
+  map_smul' _ _ := by ext; rfl
+
+@[simp] lemma toLinearMap₁₂_apply (L : E →SL[σ₁₃] F →SL[σ₂₃] G) (v : E) (w : F) :
+    L.toLinearMap₁₂ v w = L v w := rfl
 
 lemma toLinearMap₁₂_injective :
-    Function.Injective (toLinearMap₁₂ (E := E) (F := F) (G := G) (σ₁₃ := σ₁₃) (σ₂₃ := σ₂₃)) := by
+    (toLinearMap₁₂ (E := E) (F := F) (G := G) (σ₁₃ := σ₁₃) (σ₂₃ := σ₂₃) : _ → _).Injective := by
   simp [Function.Injective, LinearMap.ext_iff, ← ContinuousLinearMap.ext_iff]
 
 lemma toLinearMap₁₂_inj (L₁ L₂ : E →SL[σ₁₃] F →SL[σ₂₃] G) :

From 92ba3d8457d5296caaa7d7fec7c6e3ac6ab0779c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Micha=C5=82=20Pacholski?= <mpacholski@google.com>
Date: Wed, 15 Jul 2026 16:35:49 +0200
Subject: [PATCH 05/30] =?UTF-8?q?fix(CharacteristicFunction/TaylorExpansio?=
 =?UTF-8?q?n):=20change=20rw=20to=20erw=20to=20work=20with=20bundled=20toL?=
 =?UTF-8?q?inearMap=E2=82=81=E2=82=82?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .../Measure/CharacteristicFunction/TaylorExpansion.lean         | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean b/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean
index 2c5f7e64be0c71..16a4391f810bb7 100644
--- a/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean
+++ b/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean
@@ -79,7 +79,7 @@ theorem iteratedFDeriv_charFun {n : ℕ} {t : E} (hint : MemLp id n μ) (x : Fin
   · rw [h]
     exact contDiff_fourierIntegral _ hint'
   simp only [mul_inv_rev, neg_smul]
-  rw [h, iteratedFDeriv_fourierIntegral _ hint' (by fun_prop) le_rfl]
+  erw [h, iteratedFDeriv_fourierIntegral _ hint' (by fun_prop) le_rfl]
   simp only [smul_apply, real_smul, ofReal_pow, ofReal_neg, ofReal_mul, ofReal_inv, ofReal_ofNat,
     ofReal_prod]
   rw [fourierIntegral_continuousMultilinearMap_apply Real.continuous_fourierChar]

From a196ce4a95a37c7e448a8c71ef1aecc2bf2a03d4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Micha=C5=82=20Pacholski?= <mpacholski@google.com>
Date: Wed, 15 Jul 2026 16:35:49 +0200
Subject: [PATCH 06/30] =?UTF-8?q?fix(CharacteristicFunction/TaylorExpansio?=
 =?UTF-8?q?n):=20change=20rw=20to=20erw=20to=20work=20with=20bundled=20toL?=
 =?UTF-8?q?inearMap=E2=82=81=E2=82=82?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .../Measure/CharacteristicFunction/TaylorExpansion.lean          | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean b/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean
index 16a4391f810bb7..9cf391d62f66fc 100644
--- a/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean
+++ b/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean
@@ -66,7 +66,6 @@ lemma continuous_charFun : Continuous (charFun μ) := by
   refine contDiff_zero.1 (contDiff_charFun ?_)
   simpa using by fun_prop
 
-set_option backward.isDefEq.respectTransparency false in
 theorem iteratedFDeriv_charFun {n : ℕ} {t : E} (hint : MemLp id n μ) (x : Fin n → E) :
     iteratedFDeriv ℝ n (charFun μ) t x = I ^ n * ∫ y, (∏ i, ⟪y, x i⟫) * exp (⟪y, t⟫ * I) ∂μ := by
   have h : innerₗ E = (innerSL ℝ).toLinearMap₁₂ := rfl

From 458d12b6360ef640e5bcc8c0e123633ca302efa4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Micha=C5=82=20Pacholski?= <mpacholski@google.com>
Date: Wed, 15 Jul 2026 17:06:49 +0200
Subject: [PATCH 07/30] 
 fix(Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion) go
 back to rw

---
 .../Measure/CharacteristicFunction/TaylorExpansion.lean         | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean b/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean
index 9cf391d62f66fc..e31137a02c5bea 100644
--- a/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean
+++ b/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean
@@ -78,7 +78,7 @@ theorem iteratedFDeriv_charFun {n : ℕ} {t : E} (hint : MemLp id n μ) (x : Fin
   · rw [h]
     exact contDiff_fourierIntegral _ hint'
   simp only [mul_inv_rev, neg_smul]
-  erw [h, iteratedFDeriv_fourierIntegral _ hint' (by fun_prop) le_rfl]
+  rw [h, iteratedFDeriv_fourierIntegral _ hint' (by fun_prop) le_rfl]
   simp only [smul_apply, real_smul, ofReal_pow, ofReal_neg, ofReal_mul, ofReal_inv, ofReal_ofNat,
     ofReal_prod]
   rw [fourierIntegral_continuousMultilinearMap_apply Real.continuous_fourierChar]

From dfaf63b14b05fe44f5d948165c237cfad4a0cb97 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Micha=C5=82=20Pacholski?= <mpacholski@google.com>
Date: Thu, 16 Jul 2026 19:05:37 +0200
Subject: [PATCH 08/30] =?UTF-8?q?fix(Topology/Algebra/Module/Spaces/Contin?=
 =?UTF-8?q?uousLinearMap)=20change=20toLinearMap=E2=82=81=E2=82=82=5Fapply?=
 =?UTF-8?q?=20to=20toLinearMap=E2=82=81=E2=82=82=5Fapply=5Fapply=5Fapply?=
 =?UTF-8?q?=20and=20add=20@[simps=20apply]=20to=20definition?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .../Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean    | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
index 8a7541852073fc..2e03b74285338c 100644
--- a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
+++ b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
@@ -299,12 +299,13 @@ theorem map_smulₛₗ₂ (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (c : R) (x
     f (c • x) y = σ₁₃ c • f x y := by rw [f.map_smulₛₗ, smul_apply]
 
 /-- Send a continuous sesquilinear map to an abstract sesquilinear map (forgetting continuity). -/
+@[simps apply]
 def toLinearMap₁₂ : (E →SL[σ₁₃] F →SL[σ₂₃] G) →ₗ[𝕜₃] (E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) where
   toFun L := (coeLMₛₗ σ₂₃).comp L.toLinearMap
   map_add' _ _ := by ext; rfl
   map_smul' _ _ := by ext; rfl
 
-@[simp] lemma toLinearMap₁₂_apply (L : E →SL[σ₁₃] F →SL[σ₂₃] G) (v : E) (w : F) :
+lemma toLinearMap₁₂_apply_apply_apply (L : E →SL[σ₁₃] F →SL[σ₂₃] G) (v : E) (w : F) :
     L.toLinearMap₁₂ v w = L v w := rfl
 
 lemma toLinearMap₁₂_injective :

From 9ef9116ccf3d9e70ed645c9451977bfbff468ea4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Micha=C5=82=20Pacholski?= <mpacholski@google.com>
Date: Thu, 16 Jul 2026 20:07:11 +0200
Subject: [PATCH 09/30] feat(LinearAlgebra/TensorProduct): port lifts API from
 PiTensorProduct

Port the `lifts` API from `PiTensorProduct` to the binary `TensorProduct` in `Mathlib/LinearAlgebra/TensorProduct/Basic.lean`.

This API provides the necessary machinery to represent any tensor element as a formal sum of pure generators in the free monoid, which is a key prerequisite for defining and proving properties of the binary projective seminorm.

Specifically, add:
- `FreeAddMonoid.toTensorProduct`: proves that the image of a free monoid element is the sum of its pure tensor components.
- `lifts`: defines the set of all valid monoid representations of a given tensor.
- `nonempty_lifts`: proves that every tensor has at least one representation.
- `lifts_zero`, `lifts_add`, `lifts_smul_left` and `lifts_smul_right`: establish the algebraic behavior of lifts under addition, zero, and scalar multiplication.
---
 .../LinearAlgebra/TensorProduct/Basic.lean    | 70 +++++++++++++++++++
 1 file changed, 70 insertions(+)

diff --git a/Mathlib/LinearAlgebra/TensorProduct/Basic.lean b/Mathlib/LinearAlgebra/TensorProduct/Basic.lean
index 4784cba63d32aa..fcbf62c226a0ce 100644
--- a/Mathlib/LinearAlgebra/TensorProduct/Basic.lean
+++ b/Mathlib/LinearAlgebra/TensorProduct/Basic.lean
@@ -82,6 +82,76 @@ theorem liftAddHom_tmul (f : M →+ N →+ P)
     liftAddHom f hf (m ⊗ₜ n) = f m n :=
   rfl
 
+/-- The image of an element `p` of `FreeAddMonoid (M × N)` in the `TensorProduct` is
+equal to the sum of `x ⊗ₜ y` over all the entries `(x, y)` of `p`.
+-/
+lemma _root_.FreeAddMonoid.toTensorProduct (p : FreeAddMonoid (M × N)) :
+    AddCon.toQuotient (c := addConGen (TensorProduct.Eqv R M N)) p =
+    (p.toList.map (fun x ↦ x.1 ⊗ₜ[R] x.2)).sum := by
+  induction p using FreeAddMonoid.inductionOn' with
+  | zero => rfl
+  | add_of b a ih =>
+    rw [FreeAddMonoid.toList_of_add, List.map_cons, List.sum_cons, ← ih]
+    rfl
+
+/-- The set of lifts of an element `x` of `M ⊗[R] N` in `FreeAddMonoid (M × N)`. -/
+def lifts (x : M ⊗[R] N) : Set (FreeAddMonoid (M × N)) :=
+  {p | AddCon.toQuotient (c := addConGen (TensorProduct.Eqv R M N)) p = x}
+
+lemma mem_lifts_iff (x : M ⊗[R] N) (p : FreeAddMonoid (M × N)) :
+    p ∈ lifts x ↔ List.sum (List.map (fun x ↦ x.1 ⊗ₜ[R] x.2) p.toList) = x := by
+  simp only [lifts, Set.mem_setOf_eq, FreeAddMonoid.toTensorProduct]
+  rfl
+
+/-- Every element of `M ⊗[R] N` has a lift in `FreeAddMonoid (M × N)`.
+-/
+lemma nonempty_lifts (x : M ⊗[R] N) : Set.Nonempty (lifts x) := by
+  existsi Quot.out x
+  simp [lifts, ← AddCon.quot_mk_eq_coe]
+
+instance (x : M ⊗[R] N) : Nonempty ↑x.lifts := nonempty_subtype.mpr (nonempty_lifts x)
+
+/-- The empty list lifts the element `0` of `M ⊗[R] N`.
+-/
+lemma lifts_zero : 0 ∈ lifts (0 : M ⊗[R] N) := by
+  rw [mem_lifts_iff, FreeAddMonoid.toList_zero, List.map_nil, List.sum_nil]
+
+set_option backward.isDefEq.respectTransparency false in
+/-- If elements `p, q` of `FreeAddMonoid (M × N)` lift elements `x, y` of `M ⊗[R] N`
+respectively, then `p + q` lifts `x + y`.
+-/
+lemma lifts_add {x y : M ⊗[R] N} {p q : FreeAddMonoid (M × N)}
+    (hp : p ∈ lifts x) (hq : q ∈ lifts y) : p + q ∈ lifts (x + y) := by
+  simp only [lifts, Set.mem_setOf_eq, AddCon.coe_add]
+  rw [hp, hq]
+
+/-- If an element `p` of `FreeAddMonoid (M × N)` lifts an element `x` of `M ⊗[R] N`,
+and if `a` is an element of `R`, then the list obtained by multiplying the first entry of each
+element of `p` by `a` lifts `a • x`.
+-/
+lemma lifts_smul_left {x : M ⊗[R] N} {p : FreeAddMonoid (M × N)} (h : p ∈ lifts x) (a : R) :
+    p.map (fun (y : M × N) ↦ (a • y.1, y.2)) ∈ lifts (a • x) := by
+  rw [mem_lifts_iff] at h ⊢
+  rw [← h]
+  simp only [FreeAddMonoid.toList_map, List.map_map]
+  induction p.toList with
+  | nil => simp
+  | cons hd tl ih => simp [ih, smul_add, smul_tmul]
+
+
+/-- If an element `p` of `FreeAddMonoid (M × N)` lifts an element `x` of `M ⊗[R] N`,
+and if `a` is an element of `R`, then the list obtained by multiplying the second entry of each
+element of `p` by `a` lifts `a • x`.
+-/
+lemma lifts_smul_right {x : M ⊗[R] N} {p : FreeAddMonoid (M × N)} (h : p ∈ lifts x) (a : R) :
+    p.map (fun (y : M × N) ↦ (y.1, a • y.2)) ∈ lifts (a • x) := by
+  rw [mem_lifts_iff] at h ⊢
+  rw [← h]
+  simp only [FreeAddMonoid.toList_map, List.map_map]
+  induction p.toList with
+  | nil => simp
+  | cons hd tl ih => simp [ih, smul_add]
+
 end Module
 
 variable [Module R P] [Module R Q]

From a695f72f27df8616c51d9a96f7356fae90c2a5f1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Micha=C5=82=20Pacholski?= <mpacholski@google.com>
Date: Thu, 16 Jul 2026 20:15:06 +0200
Subject: [PATCH 10/30] =?UTF-8?q?reinstate=20@[simp]=20at=20toLinearMap?=
 =?UTF-8?q?=E2=82=81=E2=82=82=5Fapply=5Fapply=5Fapply?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
index 2e03b74285338c..91ea305a91d401 100644
--- a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
+++ b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
@@ -305,7 +305,7 @@ def toLinearMap₁₂ : (E →SL[σ₁₃] F →SL[σ₂₃] G) →ₗ[𝕜₃]
   map_add' _ _ := by ext; rfl
   map_smul' _ _ := by ext; rfl
 
-lemma toLinearMap₁₂_apply_apply_apply (L : E →SL[σ₁₃] F →SL[σ₂₃] G) (v : E) (w : F) :
+@[simp] lemma toLinearMap₁₂_apply_apply_apply (L : E →SL[σ₁₃] F →SL[σ₂₃] G) (v : E) (w : F) :
     L.toLinearMap₁₂ v w = L v w := rfl
 
 lemma toLinearMap₁₂_injective :

From 95f22fedc2d53305207de3fe5d525790f0b3fdf0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Micha=C5=82=20Pacholski?= <mpacholski@google.com>
Date: Thu, 16 Jul 2026 20:31:49 +0200
Subject: [PATCH 11/30] 
 feat(Mathlib/Analysis/Normed/Module/TensorProduct/ProjectiveSeminorm) Create
 empty file

---
 .../Analysis/Normed/Module/TensorProduct/ProjectiveSeminorm.lean  | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 create mode 100644 Mathlib/Analysis/Normed/Module/TensorProduct/ProjectiveSeminorm.lean

diff --git a/Mathlib/Analysis/Normed/Module/TensorProduct/ProjectiveSeminorm.lean b/Mathlib/Analysis/Normed/Module/TensorProduct/ProjectiveSeminorm.lean
new file mode 100644
index 00000000000000..e69de29bb2d1d6

From 10a8a2878fb28e8f40401014ddbdcf5b44809614 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Micha=C5=82=20Pacholski?= <mpacholski@google.com>
Date: Thu, 16 Jul 2026 20:15:06 +0200
Subject: [PATCH 12/30] =?UTF-8?q?remove=20@[simps=20apply]=20from=20toLine?=
 =?UTF-8?q?arMap=E2=82=81=E2=82=82?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
index 91ea305a91d401..1b167c32a99cd6 100644
--- a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
+++ b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
@@ -299,7 +299,6 @@ theorem map_smulₛₗ₂ (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (c : R) (x
     f (c • x) y = σ₁₃ c • f x y := by rw [f.map_smulₛₗ, smul_apply]
 
 /-- Send a continuous sesquilinear map to an abstract sesquilinear map (forgetting continuity). -/
-@[simps apply]
 def toLinearMap₁₂ : (E →SL[σ₁₃] F →SL[σ₂₃] G) →ₗ[𝕜₃] (E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) where
   toFun L := (coeLMₛₗ σ₂₃).comp L.toLinearMap
   map_add' _ _ := by ext; rfl

From 036006b2eb35c85316e2cdea2f8316b005ea9023 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Micha=C5=82=20Pacholski?= <mpacholski@google.com>
Date: Fri, 17 Jul 2026 08:17:30 +0200
Subject: [PATCH 13/30] =?UTF-8?q?update=20occurences=20of=20toLinearMap?=
 =?UTF-8?q?=E2=82=81=E2=82=82=5Fapply=20to=20toLinearMap=E2=82=81=E2=82=82?=
 =?UTF-8?q?=5Fapply=5Fapply=5Fapply?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Mathlib/Analysis/Fourier/FourierTransformDeriv.lean           | 4 ++--
 .../Measure/CharacteristicFunction/TaylorExpansion.lean       | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean b/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
index 15d25a14e6e7a9..142e17bcae8748 100644
--- a/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
+++ b/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
@@ -263,8 +263,8 @@ theorem fourierIntegral_fderiv [MeasurableSpace V] [BorelSpace V] [FiniteDimensi
   /- First rewrite things in a simplified form, without any real change. -/
   suffices ∫ x, g x • fderiv ℝ f x y ∂μ = ∫ x, (2 * ↑π * I * L y w * g x) • f x ∂μ by
     rw [fourierIntegral_continuousLinearMap_apply' hf']
-    simpa only [fourierIntegral, ContinuousLinearMap.toLinearMap₁₂_apply, fourierSMulRight_apply,
-      neg_apply, ContinuousLinearMap.flip_apply, ← integral_smul, neg_smul,
+    simpa only [fourierIntegral, ContinuousLinearMap.toLinearMap₁₂_apply_apply_apply,
+      fourierSMulRight_apply, neg_apply, ContinuousLinearMap.flip_apply, ← integral_smul, neg_smul,
       smul_neg, ← smul_smul, coe_smul, neg_neg]
   -- Key step: integrate by parts with respect to `y` to switch the derivative from `f` to `g`.
   have A x : fderiv ℝ g x y = - 2 * ↑π * I * L y w * g x :=
diff --git a/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean b/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean
index e31137a02c5bea..208c9f20f2888d 100644
--- a/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean
+++ b/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean
@@ -85,7 +85,7 @@ theorem iteratedFDeriv_charFun {n : ℕ} {t : E} (hint : MemLp id n μ) (x : Fin
   swap;
   · exact integrable_fourierPowSMulRight _ (by simpa using hint.integrable_norm_pow') (by fun_prop)
   simp only [fourierIntegral, Real.fourierChar, Circle.exp, ContinuousMap.coe_mk, ofReal_mul,
-    ofReal_ofNat, innerSL, map_neg, map_smul, ContinuousLinearMap.toLinearMap₁₂_apply,
+    ofReal_ofNat, innerSL, map_neg, map_smul, ContinuousLinearMap.toLinearMap₁₂_apply_apply_apply,
     LinearMap.mkContinuous₂_apply, innerₛₗ_apply_apply, smul_eq_mul, neg_neg, AddChar.coe_mk,
     ofReal_inv, fourierPowSMulRight_apply, Pi.ofNat_apply, real_smul, ofReal_prod, mul_one,
     Circle.smul_def]

From 75616e25a5794a36a47d5747247d9a332ee3293e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Micha=C5=82=20Pacholski?= <mpacholski@google.com>
Date: Fri, 17 Jul 2026 10:34:22 +0200
Subject: [PATCH 14/30] chore: rerun CI


From 4e999a4ff0d1d622f0202c185216024ac283520f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Micha=C5=82=20Pacholski?= <mpacholski@google.com>
Date: Fri, 17 Jul 2026 15:54:48 +0200
Subject: [PATCH 15/30] =?UTF-8?q?Revert=20"update=20occurences=20of=20toLi?=
 =?UTF-8?q?nearMap=E2=82=81=E2=82=82=5Fapply=20to=20toLinearMap=E2=82=81?=
 =?UTF-8?q?=E2=82=82=5Fapply=5Fapply=5Fapply"?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This reverts commit 036006b2eb35c85316e2cdea2f8316b005ea9023.
---
 Mathlib/Analysis/Fourier/FourierTransformDeriv.lean           | 4 ++--
 .../Measure/CharacteristicFunction/TaylorExpansion.lean       | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean b/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
index 142e17bcae8748..15d25a14e6e7a9 100644
--- a/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
+++ b/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
@@ -263,8 +263,8 @@ theorem fourierIntegral_fderiv [MeasurableSpace V] [BorelSpace V] [FiniteDimensi
   /- First rewrite things in a simplified form, without any real change. -/
   suffices ∫ x, g x • fderiv ℝ f x y ∂μ = ∫ x, (2 * ↑π * I * L y w * g x) • f x ∂μ by
     rw [fourierIntegral_continuousLinearMap_apply' hf']
-    simpa only [fourierIntegral, ContinuousLinearMap.toLinearMap₁₂_apply_apply_apply,
-      fourierSMulRight_apply, neg_apply, ContinuousLinearMap.flip_apply, ← integral_smul, neg_smul,
+    simpa only [fourierIntegral, ContinuousLinearMap.toLinearMap₁₂_apply, fourierSMulRight_apply,
+      neg_apply, ContinuousLinearMap.flip_apply, ← integral_smul, neg_smul,
       smul_neg, ← smul_smul, coe_smul, neg_neg]
   -- Key step: integrate by parts with respect to `y` to switch the derivative from `f` to `g`.
   have A x : fderiv ℝ g x y = - 2 * ↑π * I * L y w * g x :=
diff --git a/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean b/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean
index 208c9f20f2888d..e31137a02c5bea 100644
--- a/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean
+++ b/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean
@@ -85,7 +85,7 @@ theorem iteratedFDeriv_charFun {n : ℕ} {t : E} (hint : MemLp id n μ) (x : Fin
   swap;
   · exact integrable_fourierPowSMulRight _ (by simpa using hint.integrable_norm_pow') (by fun_prop)
   simp only [fourierIntegral, Real.fourierChar, Circle.exp, ContinuousMap.coe_mk, ofReal_mul,
-    ofReal_ofNat, innerSL, map_neg, map_smul, ContinuousLinearMap.toLinearMap₁₂_apply_apply_apply,
+    ofReal_ofNat, innerSL, map_neg, map_smul, ContinuousLinearMap.toLinearMap₁₂_apply,
     LinearMap.mkContinuous₂_apply, innerₛₗ_apply_apply, smul_eq_mul, neg_neg, AddChar.coe_mk,
     ofReal_inv, fourierPowSMulRight_apply, Pi.ofNat_apply, real_smul, ofReal_prod, mul_one,
     Circle.smul_def]

From 99c6a83d0b2b403cb9b2569c89e8cddd51b757c8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Micha=C5=82=20Pacholski?= <mpacholski@google.com>
Date: Fri, 17 Jul 2026 15:54:56 +0200
Subject: [PATCH 16/30] =?UTF-8?q?Revert=20"remove=20@[simps=20apply]=20fro?=
 =?UTF-8?q?m=20toLinearMap=E2=82=81=E2=82=82"?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This reverts commit 10a8a2878fb28e8f40401014ddbdcf5b44809614.
---
 Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
index 1b167c32a99cd6..91ea305a91d401 100644
--- a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
+++ b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
@@ -299,6 +299,7 @@ theorem map_smulₛₗ₂ (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (c : R) (x
     f (c • x) y = σ₁₃ c • f x y := by rw [f.map_smulₛₗ, smul_apply]
 
 /-- Send a continuous sesquilinear map to an abstract sesquilinear map (forgetting continuity). -/
+@[simps apply]
 def toLinearMap₁₂ : (E →SL[σ₁₃] F →SL[σ₂₃] G) →ₗ[𝕜₃] (E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) where
   toFun L := (coeLMₛₗ σ₂₃).comp L.toLinearMap
   map_add' _ _ := by ext; rfl

From cc6007aa6bb480e6e7bc86b3688c71439b9c444f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Micha=C5=82=20Pacholski?= <mpacholski@google.com>
Date: Fri, 17 Jul 2026 15:55:22 +0200
Subject: [PATCH 17/30] =?UTF-8?q?Revert=20"reinstate=20@[simp]=20at=20toLi?=
 =?UTF-8?q?nearMap=E2=82=81=E2=82=82=5Fapply=5Fapply=5Fapply"?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This reverts commit a695f72f27df8616c51d9a96f7356fae90c2a5f1.
---
 Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
index 91ea305a91d401..2e03b74285338c 100644
--- a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
+++ b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
@@ -305,7 +305,7 @@ def toLinearMap₁₂ : (E →SL[σ₁₃] F →SL[σ₂₃] G) →ₗ[𝕜₃]
   map_add' _ _ := by ext; rfl
   map_smul' _ _ := by ext; rfl
 
-@[simp] lemma toLinearMap₁₂_apply_apply_apply (L : E →SL[σ₁₃] F →SL[σ₂₃] G) (v : E) (w : F) :
+lemma toLinearMap₁₂_apply_apply_apply (L : E →SL[σ₁₃] F →SL[σ₂₃] G) (v : E) (w : F) :
     L.toLinearMap₁₂ v w = L v w := rfl
 
 lemma toLinearMap₁₂_injective :

From bfab88f1e69001dc6c45738dba485adad2d33f7f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Micha=C5=82=20Pacholski?= <mpacholski@google.com>
Date: Fri, 17 Jul 2026 15:55:30 +0200
Subject: [PATCH 18/30] =?UTF-8?q?Revert=20"fix(Topology/Algebra/Module/Spa?=
 =?UTF-8?q?ces/ContinuousLinearMap)=20change=20toLinearMap=E2=82=81?=
 =?UTF-8?q?=E2=82=82=5Fapply=20to=20toLinearMap=E2=82=81=E2=82=82=5Fapply?=
 =?UTF-8?q?=5Fapply=5Fapply=20and=20add=20@[simps=20apply]=20to=20definiti?=
 =?UTF-8?q?on"?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This reverts commit dfaf63b14b05fe44f5d948165c237cfad4a0cb97.
---
 .../Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean    | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
index 2e03b74285338c..8a7541852073fc 100644
--- a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
+++ b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
@@ -299,13 +299,12 @@ theorem map_smulₛₗ₂ (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (c : R) (x
     f (c • x) y = σ₁₃ c • f x y := by rw [f.map_smulₛₗ, smul_apply]
 
 /-- Send a continuous sesquilinear map to an abstract sesquilinear map (forgetting continuity). -/
-@[simps apply]
 def toLinearMap₁₂ : (E →SL[σ₁₃] F →SL[σ₂₃] G) →ₗ[𝕜₃] (E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) where
   toFun L := (coeLMₛₗ σ₂₃).comp L.toLinearMap
   map_add' _ _ := by ext; rfl
   map_smul' _ _ := by ext; rfl
 
-lemma toLinearMap₁₂_apply_apply_apply (L : E →SL[σ₁₃] F →SL[σ₂₃] G) (v : E) (w : F) :
+@[simp] lemma toLinearMap₁₂_apply (L : E →SL[σ₁₃] F →SL[σ₂₃] G) (v : E) (w : F) :
     L.toLinearMap₁₂ v w = L v w := rfl
 
 lemma toLinearMap₁₂_injective :

From b47f04df5fd11cb81ea71f6fa080171557ffd464 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Micha=C5=82=20Pacholski?= <mpacholski@google.com>
Date: Fri, 17 Jul 2026 16:21:16 +0200
Subject: [PATCH 19/30] feat(Analysis/Normed/Module/TensorProduct): define
 projective seminorm on binary tensor products
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Introduce the projective seminorm on the tensor product of two normed spaces,
mirroring the n-ary construction in `PiTensorProduct.ProjectiveSeminorm`.

- Create `Mathlib/Analysis/Normed/Module/TensorProduct/ProjectiveSeminorm.lean`.
- Define `TensorProduct.projectiveSeminormAux` on `FreeAddMonoid (X × Y)`.
- Define the `Norm` instance on `X ⊗[𝕜] Y` as the infimum of the auxiliary
  seminorm over all representations (lifts) of a tensor.
- Prove basic properties including `projectiveSeminormAux_nonneg`,
  `projectiveSeminormAux_add_le`, `projectiveSeminormAux_smul`, and
  `projectiveSeminorm_zero`.
---
 .../TensorProduct/ProjectiveSeminorm.lean     | 164 ++++++++++++++++++
 1 file changed, 164 insertions(+)

diff --git a/Mathlib/Analysis/Normed/Module/TensorProduct/ProjectiveSeminorm.lean b/Mathlib/Analysis/Normed/Module/TensorProduct/ProjectiveSeminorm.lean
index e69de29bb2d1d6..b787585e11412c 100644
--- a/Mathlib/Analysis/Normed/Module/TensorProduct/ProjectiveSeminorm.lean
+++ b/Mathlib/Analysis/Normed/Module/TensorProduct/ProjectiveSeminorm.lean
@@ -0,0 +1,164 @@
+module
+
+public import Mathlib.Analysis.Normed.Operator.Bilinear
+
+/-!
+# Projective seminorm on the tensor of two normed spaces.
+
+Let `𝕜` be a normed field and `X` and `Y` be normed `𝕜`-vector spaces.
+We define a seminorm on `X ⊗[𝕜] Y`, which we call the "projective seminorm".
+For `t` an element of `X ⊗[𝕜] Y`, its projective seminorm is the
+infimum over all expressions of `t` as `∑ j, xⱼ ⊗ₜ[𝕜] yⱼ` (with the `(xⱼ,yⱼ)` ∈ `X × Y`)
+of `∑ j, ‖xⱼ‖ * ‖yⱼ‖ `.
+
+In particular, every norm `‖.‖` on `X ⨂[𝕜] Y` satisfying `‖x ⊗ₜ[𝕜] y‖ ≤ ‖x‖ * ‖y‖`
+for every `(x,y)` in `X × Y` is bounded above by the projective seminorm.
+
+## Main definitions
+
+* `TensorProduct.projectiveSeminorm`: The projective seminorm on `X ⨂[𝕜] Y`.
+
+## Main results
+
+* `TensorProduct.norm_eval_le_projectiveSeminorm`: If `f` is a continuous bilinear map on
+  `X × Y` and `x` is in `X ⊗[𝕜] Y`, then `‖lift (toLinearMap₁₂ f) x‖ ≤ ‖f‖ * ‖x‖`.
+
+## TODO
+* Port definitions and theorems connected to:
+  *  `PiTensorProduct.liftEquiv`: The bijection between `X →L[𝕜] Y →L[𝕜] F` and
+     `(X ⊗[𝕜] Y) →L[𝕜] F`, as a continuous linear equivalence.
+  *  Port definitions and theorems connected to `PiTensorProduct.liftIsometry`: The bijection
+     between X →L[𝕜] Y →L[𝕜] F` and `(X ⊗[𝕜] Y) →L[𝕜] F`,, as an isometric linear equivalence.
+  *  `PiTensorProduct.tprodL`: The canonical continuous bilinear map from `X × Y`
+     to `X ⊗[𝕜] Y`.
+* Adapt the remaining functoriality constructions/properties from `PiTensorProduct`.
+* If the base field is `ℝ` or `ℂ` (or more generally if the injection of `X` and `Y` into its bidual
+  is an isometry), then we have `projectiveSeminorm x ⊗ₜ[𝕜] y = ‖x‖*‖y‖`.
+* If all `Eᵢ` are separated and satisfy `SeparatingDual`, then the seminorm on
+  `⨂[𝕜] i, Eᵢ` is a norm.
+
+-/
+
+@[expose] public section
+
+variable {𝕜 X Y : Type*}
+variable [SeminormedAddCommGroup X]
+variable [SeminormedAddCommGroup Y]
+
+open scoped TensorProduct
+
+namespace TensorProduct
+
+section NormedField
+
+variable [NormedField 𝕜]
+
+/-- A lift of the projective seminorm to `FreeAddMonoid (X × Y)`, useful to prove the
+properties of `projectiveSeminorm`. -/
+def projectiveSeminormAux : FreeAddMonoid (X × Y) → ℝ :=
+  fun p ↦ (p.toList.map (fun p ↦ ‖p.1‖ * ‖p.2‖)).sum
+
+theorem projectiveSeminormAux_nonneg (p : FreeAddMonoid (X × Y)) :
+    0 ≤ projectiveSeminormAux p := by
+  refine List.sum_nonneg fun a ↦ ?_
+  simp only [List.mem_map, Prod.exists, forall_exists_index, and_imp]
+  intro x y _ rfl
+  positivity
+
+theorem projectiveSeminormAux_add_le (p q : FreeAddMonoid (X × Y)) :
+    projectiveSeminormAux (p + q) ≤ projectiveSeminormAux p + projectiveSeminormAux q := by
+  simp only [projectiveSeminormAux, FreeAddMonoid.toList_add, List.map_append, List.sum_append,
+    Std.le_refl]
+
+variable [NormedSpace 𝕜 X]
+
+theorem projectiveSeminormAux_smul (p : FreeAddMonoid (X × Y)) (a : 𝕜) :
+    projectiveSeminormAux (p.map (fun (y : X × Y) ↦ (a • y.1, y.2))) =
+    ‖a‖ * projectiveSeminormAux p := by
+  simp only [projectiveSeminormAux, FreeAddMonoid.toList_map, List.map_map, Function.comp_def]
+  simp_rw [norm_smul, mul_assoc]
+  rw [List.sum_map_mul_left]
+
+variable [NormedSpace 𝕜 Y]
+
+theorem bddBelow_projectiveSemiNormAux (x : X ⊗[𝕜] Y) :
+    BddBelow (Set.range (fun (p : lifts x) ↦ projectiveSeminormAux p.1)) :=
+  ⟨0, by simp [mem_lowerBounds, projectiveSeminormAux_nonneg]⟩
+
+noncomputable instance : Norm (X ⊗[𝕜] Y) :=
+  ⟨fun x ↦ iInf (fun (p : lifts x) ↦ projectiveSeminormAux p.val)⟩
+
+theorem norm_def (x : X ⊗[𝕜] Y) :
+    ‖x‖ = iInf (fun (p : lifts x) ↦ projectiveSeminormAux p.val) := rfl
+
+theorem projectiveSeminorm_zero : ‖(0 : X ⊗[𝕜] Y)‖ = 0 :=
+  le_antisymm (ciInf_le (bddBelow_projectiveSemiNormAux _) ⟨0, lifts_zero⟩)
+    (le_ciInf (fun p ↦ projectiveSeminormAux_nonneg p.val))
+
+theorem projectiveSeminorm_add_le (x y : X ⊗[𝕜] Y) : ‖x + y‖ ≤ ‖x‖ + ‖y‖ :=
+  le_ciInf_add_ciInf (fun p q ↦ ciInf_le_of_le (bddBelow_projectiveSemiNormAux _)
+    ⟨p.1 + q.1, lifts_add p.2 q.2⟩ (projectiveSeminormAux_add_le p.1 q.1))
+
+theorem projectiveSeminorm_smul_le (a : 𝕜) (x : X ⊗[𝕜] Y) : ‖a • x‖ ≤ ‖a‖ * ‖x‖ := by
+  simp only [norm_def, Real.mul_iInf_of_nonneg (norm_nonneg _)]
+  refine le_ciInf fun p ↦ ?_
+  simpa [projectiveSeminormAux_smul] using
+    ciInf_le_of_le (bddBelow_projectiveSemiNormAux _) ⟨_, lifts_smul_left p.2 a⟩ (le_refl _)
+
+/-- The projective seminorm on `X ⊗[𝕜] Y`. It sends an element `x` of `X ⊗[𝕜] Y` to the
+infimum over all expressions of `x` as `∑ j, xⱼ ⊗ₜ[𝕜] yⱼ` (with the `(xⱼ,yⱼ)` ∈ `X × Y`)
+of `∑ j, ‖xⱼ‖ * ‖yⱼ‖ `. -/
+noncomputable def projectiveSeminorm : Seminorm 𝕜 (X ⊗[𝕜] Y) := .ofSMulLE
+    _ projectiveSeminorm_zero projectiveSeminorm_add_le projectiveSeminorm_smul_le
+
+noncomputable instance : SeminormedAddCommGroup (X ⊗[𝕜] Y) :=
+  fast_instance% AddGroupSeminorm.toSeminormedAddCommGroup projectiveSeminorm.toAddGroupSeminorm
+
+noncomputable instance : NormedSpace 𝕜 (X ⊗[𝕜] Y) := ⟨projectiveSeminorm_smul_le⟩
+
+theorem projectiveSeminorm_tprod_le (x : X) (y : Y) :
+    projectiveSeminorm (x ⊗ₜ[𝕜] y) ≤ ‖x‖*‖y‖ := by
+  convert! ciInf_le (bddBelow_projectiveSemiNormAux _) ⟨FreeAddMonoid.of (x, y), ?_⟩
+  · simp [projectiveSeminormAux]
+  · simp [mem_lifts_iff]
+
+end NormedField
+
+section NontriviallyNormedField
+
+variable [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 X] [NormedSpace 𝕜 Y]
+
+open ContinuousLinearMap
+
+example {G : Type*} [SeminormedAddCommGroup G]
+    [NormedSpace 𝕜 G] (f : X →L[𝕜] Y →L[𝕜] G) : X →ₗ[𝕜] Y →ₗ[𝕜] G :=
+  (coeLM 𝕜 ∘ₗ f.toLinearMap)
+
+theorem norm_eval_le_projectiveSeminorm {G : Type*} [SeminormedAddCommGroup G]
+    [NormedSpace 𝕜 G] (f : X →L[𝕜] Y →L[𝕜] G) (x : X ⊗[𝕜] Y) :
+    ‖lift (toLinearMap₁₂ f) x‖ ≤ ‖f‖ * ‖x‖ := by
+  rw [norm_def, mul_comm, Real.iInf_mul_of_nonneg (norm_nonneg _)]
+  refine le_ciInf fun ⟨p, hp⟩ ↦ ?_
+  rw! [← ((mem_lifts_iff x p).mp hp), ← List.sum_map_hom, ← Multiset.sum_coe]
+  grw [norm_multiset_sum_le]
+  simp only [mul_comm, ← smul_eq_mul, List.smul_sum, projectiveSeminormAux]
+  refine List.Forall₂.sum_le_sum ?_
+  simpa [←mul_assoc, mul_comm] using fun x y _ ↦
+    ((f x).le_opNorm y).trans (mul_le_mul_of_nonneg_right (f.le_opNorm x) (norm_nonneg y))
+
+lemma _root_.ContinuousLinearMap.le_opNorm_tprod {𝕜 X Y F : Type*}
+    [NontriviallyNormedField 𝕜]
+    [SeminormedAddCommGroup X] [NormedSpace 𝕜 X]
+    [SeminormedAddCommGroup Y] [NormedSpace 𝕜 Y]
+    [SeminormedAddCommGroup F] [NormedSpace 𝕜 F]
+    (l : X ⊗[𝕜] Y →L[𝕜] F) (x : X) (y : Y) :
+    ‖l (x ⊗ₜ[𝕜] y)‖ ≤ ‖l‖ * ‖x‖ * ‖y‖ := by
+    calc
+      ‖l (x ⊗ₜ[𝕜] y)‖ ≤ ‖l‖ * projectiveSeminorm (x ⊗ₜ[𝕜] y) := l.le_opNorm (x ⊗ₜ[𝕜] y)
+      _ ≤ ‖l‖ * (‖x‖ * ‖y‖) := mul_le_mul_of_nonneg_left (projectiveSeminorm_tprod_le x y)
+        (norm_nonneg l)
+      _ = ‖l‖ * ‖x‖ * ‖y‖ := by rw [mul_assoc]
+
+end NontriviallyNormedField
+
+end TensorProduct

From 04ec6855dfadced5b7f708ec30bbca59fc3d56fe Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Micha=C5=82=20Pacholski?= <mpacholski@google.com>
Date: Fri, 17 Jul 2026 16:23:39 +0200
Subject: [PATCH 20/30] Add public import
 Mathlib.Analysis.Normed.Module.TensorProduct.ProjectiveSeminorm to Mathlib
 file

---
 Mathlib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index f152a16c49fc9c..c0424ce1791419 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2231,6 +2231,7 @@ public import Mathlib.Analysis.Normed.Module.RieszLemma
 public import Mathlib.Analysis.Normed.Module.Shrink
 public import Mathlib.Analysis.Normed.Module.Span
 public import Mathlib.Analysis.Normed.Module.TransferInstance
+public import Mathlib.Analysis.Normed.Module.TensorProduct.ProjectiveSeminorm
 public import Mathlib.Analysis.Normed.Module.WeakDual
 public import Mathlib.Analysis.Normed.MulAction
 public import Mathlib.Analysis.Normed.Operator.Asymptotics

From 04e71b24729ab0b4399278259688bcaa57b50e98 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Micha=C5=82=20Pacholski?= <mpacholski@google.com>
Date: Sat, 18 Jul 2026 18:53:46 +0200
Subject: [PATCH 21/30] simplify proof and parentheses

---
 .../Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
index 8a7541852073fc..23d5d4e3795335 100644
--- a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
+++ b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
@@ -299,10 +299,10 @@ theorem map_smulₛₗ₂ (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (c : R) (x
     f (c • x) y = σ₁₃ c • f x y := by rw [f.map_smulₛₗ, smul_apply]
 
 /-- Send a continuous sesquilinear map to an abstract sesquilinear map (forgetting continuity). -/
-def toLinearMap₁₂ : (E →SL[σ₁₃] F →SL[σ₂₃] G) →ₗ[𝕜₃] (E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) where
+def toLinearMap₁₂ : (E →SL[σ₁₃] F →SL[σ₂₃] G) →ₗ[𝕜₃] E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G where
   toFun L := (coeLMₛₗ σ₂₃).comp L.toLinearMap
-  map_add' _ _ := by ext; rfl
-  map_smul' _ _ := by ext; rfl
+  map_add' _ _ := by rfl
+  map_smul' _ _ := by rfl
 
 @[simp] lemma toLinearMap₁₂_apply (L : E →SL[σ₁₃] F →SL[σ₂₃] G) (v : E) (w : F) :
     L.toLinearMap₁₂ v w = L v w := rfl

From 78c0b49ed3bd81f904b3d0795dbc4ca45f66e6d1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Micha=C5=82=20Pacholski?= <mpacholski@google.com>
Date: Sat, 18 Jul 2026 09:37:30 +0200
Subject: [PATCH 22/30] =?UTF-8?q?Add=20@[simps=20apply]=20to=20toLinearMap?=
 =?UTF-8?q?=E2=82=81=E2=82=82,=20rename=20old=20apply=20lemma=20toLinearMa?=
 =?UTF-8?q?p=E2=82=81=E2=82=82=5Fapply=5Fapply=5Fapply,=20and=20assign=20i?=
 =?UTF-8?q?t=20a=20hight=20priority?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .../Measure/CharacteristicFunction/TaylorExpansion.lean         | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean b/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean
index e31137a02c5bea..9005eeb0e7a4ea 100644
--- a/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean
+++ b/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean
@@ -84,7 +84,7 @@ theorem iteratedFDeriv_charFun {n : ℕ} {t : E} (hint : MemLp id n μ) (x : Fin
   rw [fourierIntegral_continuousMultilinearMap_apply Real.continuous_fourierChar]
   swap;
   · exact integrable_fourierPowSMulRight _ (by simpa using hint.integrable_norm_pow') (by fun_prop)
-  simp only [fourierIntegral, Real.fourierChar, Circle.exp, ContinuousMap.coe_mk, ofReal_mul,
+  simp only [fourierIntegral, Real.fourierChar, Circle.coe_exp, ofReal_mul,
     ofReal_ofNat, innerSL, map_neg, map_smul, ContinuousLinearMap.toLinearMap₁₂_apply,
     LinearMap.mkContinuous₂_apply, innerₛₗ_apply_apply, smul_eq_mul, neg_neg, AddChar.coe_mk,
     ofReal_inv, fourierPowSMulRight_apply, Pi.ofNat_apply, real_smul, ofReal_prod, mul_one,

From 80be38630b569d403ec196a1c9ec0d4d30ae9adb Mon Sep 17 00:00:00 2001
From: mpacholski <michal.pacholski@gmail.com>
Date: Sat, 18 Jul 2026 21:04:51 +0200
Subject: [PATCH 23/30] Apply suggestion from @themathqueen

Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>
---
 .../Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean   | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
index 23d5d4e3795335..18df0bfb478d49 100644
--- a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
+++ b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
@@ -301,8 +301,8 @@ theorem map_smulₛₗ₂ (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (c : R) (x
 /-- Send a continuous sesquilinear map to an abstract sesquilinear map (forgetting continuity). -/
 def toLinearMap₁₂ : (E →SL[σ₁₃] F →SL[σ₂₃] G) →ₗ[𝕜₃] E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G where
   toFun L := (coeLMₛₗ σ₂₃).comp L.toLinearMap
-  map_add' _ _ := by rfl
-  map_smul' _ _ := by rfl
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
 
 @[simp] lemma toLinearMap₁₂_apply (L : E →SL[σ₁₃] F →SL[σ₂₃] G) (v : E) (w : F) :
     L.toLinearMap₁₂ v w = L v w := rfl

From a99a05881722c10e8a86abd8fa3db9699870530c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Micha=C5=82=20Pacholski?= <mpacholski@google.com>
Date: Sat, 18 Jul 2026 21:13:37 +0200
Subject: [PATCH 24/30] =?UTF-8?q?Rename=20to=20toLinearMap=E2=82=81?=
 =?UTF-8?q?=E2=82=82=5Fapply=5Fapply=5Fapply=20and=20add=20@[simps=20-isSi?=
 =?UTF-8?q?mp=20apply]?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Mathlib/Analysis/Fourier/FourierTransformDeriv.lean           | 4 ++--
 .../Measure/CharacteristicFunction/TaylorExpansion.lean       | 2 +-
 .../Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean   | 3 ++-
 3 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean b/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
index 01d43a1b8b62e8..0a07d00935193c 100644
--- a/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
+++ b/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
@@ -263,8 +263,8 @@ theorem fourierIntegral_fderiv [MeasurableSpace V] [BorelSpace V] [FiniteDimensi
   /- First rewrite things in a simplified form, without any real change. -/
   suffices ∫ x, g x • fderiv ℝ f x y ∂μ = ∫ x, (2 * ↑π * I * L y w * g x) • f x ∂μ by
     rw [fourierIntegral_continuousLinearMap_apply' hf']
-    simpa only [fourierIntegral, ContinuousLinearMap.toLinearMap₁₂_apply, fourierSMulRight_apply,
-      neg_apply, ContinuousLinearMap.flip_apply, ← integral_smul, neg_smul,
+    simpa only [fourierIntegral, ContinuousLinearMap.toLinearMap₁₂_apply_apply_apply,
+      fourierSMulRight_apply, neg_apply, ContinuousLinearMap.flip_apply, ← integral_smul, neg_smul,
       smul_neg, ← smul_smul, coe_smul, neg_neg]
   -- Key step: integrate by parts with respect to `y` to switch the derivative from `f` to `g`.
   have A x : fderiv ℝ g x y = - 2 * ↑π * I * L y w * g x :=
diff --git a/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean b/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean
index 9005eeb0e7a4ea..e11fe18fba5c33 100644
--- a/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean
+++ b/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean
@@ -85,7 +85,7 @@ theorem iteratedFDeriv_charFun {n : ℕ} {t : E} (hint : MemLp id n μ) (x : Fin
   swap;
   · exact integrable_fourierPowSMulRight _ (by simpa using hint.integrable_norm_pow') (by fun_prop)
   simp only [fourierIntegral, Real.fourierChar, Circle.coe_exp, ofReal_mul,
-    ofReal_ofNat, innerSL, map_neg, map_smul, ContinuousLinearMap.toLinearMap₁₂_apply,
+    ofReal_ofNat, innerSL, map_neg, map_smul, ContinuousLinearMap.toLinearMap₁₂_apply_apply_apply,
     LinearMap.mkContinuous₂_apply, innerₛₗ_apply_apply, smul_eq_mul, neg_neg, AddChar.coe_mk,
     ofReal_inv, fourierPowSMulRight_apply, Pi.ofNat_apply, real_smul, ofReal_prod, mul_one,
     Circle.smul_def]
diff --git a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
index 18df0bfb478d49..a59c26385477df 100644
--- a/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
+++ b/Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean
@@ -299,12 +299,13 @@ theorem map_smulₛₗ₂ (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (c : R) (x
     f (c • x) y = σ₁₃ c • f x y := by rw [f.map_smulₛₗ, smul_apply]
 
 /-- Send a continuous sesquilinear map to an abstract sesquilinear map (forgetting continuity). -/
+@[simps -isSimp apply]
 def toLinearMap₁₂ : (E →SL[σ₁₃] F →SL[σ₂₃] G) →ₗ[𝕜₃] E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G where
   toFun L := (coeLMₛₗ σ₂₃).comp L.toLinearMap
   map_add' _ _ := rfl
   map_smul' _ _ := rfl
 
-@[simp] lemma toLinearMap₁₂_apply (L : E →SL[σ₁₃] F →SL[σ₂₃] G) (v : E) (w : F) :
+@[simp] lemma toLinearMap₁₂_apply_apply_apply (L : E →SL[σ₁₃] F →SL[σ₂₃] G) (v : E) (w : F) :
     L.toLinearMap₁₂ v w = L v w := rfl
 
 lemma toLinearMap₁₂_injective :

From 899b37074aefc52ebb9d179776b77e1e8a87a7f3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Micha=C5=82=20Pacholski?= <mpacholski@google.com>
Date: Sat, 18 Jul 2026 22:01:38 +0200
Subject: [PATCH 25/30] remove lifts_smul_right and rename lifts_smul_left

---
 Mathlib/LinearAlgebra/TensorProduct/Basic.lean | 16 +---------------
 1 file changed, 1 insertion(+), 15 deletions(-)

diff --git a/Mathlib/LinearAlgebra/TensorProduct/Basic.lean b/Mathlib/LinearAlgebra/TensorProduct/Basic.lean
index 3b1c9227e3d103..1f8111a6cadc0a 100644
--- a/Mathlib/LinearAlgebra/TensorProduct/Basic.lean
+++ b/Mathlib/LinearAlgebra/TensorProduct/Basic.lean
@@ -129,7 +129,7 @@ lemma lifts_add {x y : M ⊗[R] N} {p q : FreeAddMonoid (M × N)}
 and if `a` is an element of `R`, then the list obtained by multiplying the first entry of each
 element of `p` by `a` lifts `a • x`.
 -/
-lemma lifts_smul_left {x : M ⊗[R] N} {p : FreeAddMonoid (M × N)} (h : p ∈ lifts x) (a : R) :
+lemma lifts_smul {x : M ⊗[R] N} {p : FreeAddMonoid (M × N)} (h : p ∈ lifts x) (a : R) :
     p.map (fun (y : M × N) ↦ (a • y.1, y.2)) ∈ lifts (a • x) := by
   rw [mem_lifts_iff] at h ⊢
   rw [← h]
@@ -138,20 +138,6 @@ lemma lifts_smul_left {x : M ⊗[R] N} {p : FreeAddMonoid (M × N)} (h : p ∈ l
   | nil => simp
   | cons hd tl ih => simp [ih, smul_add, smul_tmul]
 
-
-/-- If an element `p` of `FreeAddMonoid (M × N)` lifts an element `x` of `M ⊗[R] N`,
-and if `a` is an element of `R`, then the list obtained by multiplying the second entry of each
-element of `p` by `a` lifts `a • x`.
--/
-lemma lifts_smul_right {x : M ⊗[R] N} {p : FreeAddMonoid (M × N)} (h : p ∈ lifts x) (a : R) :
-    p.map (fun (y : M × N) ↦ (y.1, a • y.2)) ∈ lifts (a • x) := by
-  rw [mem_lifts_iff] at h ⊢
-  rw [← h]
-  simp only [FreeAddMonoid.toList_map, List.map_map]
-  induction p.toList with
-  | nil => simp
-  | cons hd tl ih => simp [ih, smul_add]
-
 end Module
 
 variable [Module R P] [Module R Q]

From d01a04435c4612226281b87349c6eeee79903d1f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Micha=C5=82=20Pacholski?= <mpacholski@google.com>
Date: Sat, 18 Jul 2026 22:05:57 +0200
Subject: [PATCH 26/30] fix proof of nonempty_lifts

---
 Mathlib/LinearAlgebra/TensorProduct/Basic.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/LinearAlgebra/TensorProduct/Basic.lean b/Mathlib/LinearAlgebra/TensorProduct/Basic.lean
index 1f8111a6cadc0a..acef0aa25b0663 100644
--- a/Mathlib/LinearAlgebra/TensorProduct/Basic.lean
+++ b/Mathlib/LinearAlgebra/TensorProduct/Basic.lean
@@ -100,14 +100,14 @@ def lifts (x : M ⊗[R] N) : Set (FreeAddMonoid (M × N)) :=
 
 lemma mem_lifts_iff (x : M ⊗[R] N) (p : FreeAddMonoid (M × N)) :
     p ∈ lifts x ↔ List.sum (List.map (fun x ↦ x.1 ⊗ₜ[R] x.2) p.toList) = x := by
-  simp only [lifts, Set.mem_setOf_eq, FreeAddMonoid.toTensorProduct]
+  simp only [lifts, Set.mem_ofPred_eq, FreeAddMonoid.toTensorProduct]
   rfl
 
 /-- Every element of `M ⊗[R] N` has a lift in `FreeAddMonoid (M × N)`.
 -/
 lemma nonempty_lifts (x : M ⊗[R] N) : Set.Nonempty (lifts x) := by
   existsi Quot.out x
-  simp [lifts, ← AddCon.quot_mk_eq_coe]
+  exact Function.surjInv_eq Quot.exists_rep x
 
 instance (x : M ⊗[R] N) : Nonempty ↑x.lifts := nonempty_subtype.mpr (nonempty_lifts x)
 
@@ -122,7 +122,7 @@ respectively, then `p + q` lifts `x + y`.
 -/
 lemma lifts_add {x y : M ⊗[R] N} {p q : FreeAddMonoid (M × N)}
     (hp : p ∈ lifts x) (hq : q ∈ lifts y) : p + q ∈ lifts (x + y) := by
-  simp only [lifts, Set.mem_setOf_eq, AddCon.coe_add]
+  simp only [lifts, Set.mem_ofPred_eq, AddCon.coe_add]
   rw [hp, hq]
 
 /-- If an element `p` of `FreeAddMonoid (M × N)` lifts an element `x` of `M ⊗[R] N`,

From 768cc70adce210d18ee268375f1e0992c1fbd18b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Micha=C5=82=20Pacholski?= <mpacholski@google.com>
Date: Sun, 19 Jul 2026 05:57:23 +0200
Subject: [PATCH 27/30] chore: rerun CI


From 5991e29957bd540249e68782407c1225067ca9b4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Micha=C5=82=20Pacholski?= <mpacholski@google.com>
Date: Sun, 19 Jul 2026 06:00:21 +0200
Subject: [PATCH 28/30] update name of lifts_smul

---
 .../Normed/Module/TensorProduct/ProjectiveSeminorm.lean         | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Analysis/Normed/Module/TensorProduct/ProjectiveSeminorm.lean b/Mathlib/Analysis/Normed/Module/TensorProduct/ProjectiveSeminorm.lean
index b787585e11412c..e1638781c1c4a4 100644
--- a/Mathlib/Analysis/Normed/Module/TensorProduct/ProjectiveSeminorm.lean
+++ b/Mathlib/Analysis/Normed/Module/TensorProduct/ProjectiveSeminorm.lean
@@ -103,7 +103,7 @@ theorem projectiveSeminorm_smul_le (a : 𝕜) (x : X ⊗[𝕜] Y) : ‖a • x
   simp only [norm_def, Real.mul_iInf_of_nonneg (norm_nonneg _)]
   refine le_ciInf fun p ↦ ?_
   simpa [projectiveSeminormAux_smul] using
-    ciInf_le_of_le (bddBelow_projectiveSemiNormAux _) ⟨_, lifts_smul_left p.2 a⟩ (le_refl _)
+    ciInf_le_of_le (bddBelow_projectiveSemiNormAux _) ⟨_, lifts_smul p.2 a⟩ (le_refl _)
 
 /-- The projective seminorm on `X ⊗[𝕜] Y`. It sends an element `x` of `X ⊗[𝕜] Y` to the
 infimum over all expressions of `x` as `∑ j, xⱼ ⊗ₜ[𝕜] yⱼ` (with the `(xⱼ,yⱼ)` ∈ `X × Y`)

From f21ad55b21074ee31c7585c744a17a6b2ffc924e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Micha=C5=82=20Pacholski?= <mpacholski@google.com>
Date: Sun, 19 Jul 2026 06:52:05 +0200
Subject: [PATCH 29/30] add copyright

---
 .../Normed/Module/TensorProduct/ProjectiveSeminorm.lean     | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/Mathlib/Analysis/Normed/Module/TensorProduct/ProjectiveSeminorm.lean b/Mathlib/Analysis/Normed/Module/TensorProduct/ProjectiveSeminorm.lean
index e1638781c1c4a4..38b5377bc6a8a3 100644
--- a/Mathlib/Analysis/Normed/Module/TensorProduct/ProjectiveSeminorm.lean
+++ b/Mathlib/Analysis/Normed/Module/TensorProduct/ProjectiveSeminorm.lean
@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2026 Michał Pacholski. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michał Pacholski
+-/
+
 module
 
 public import Mathlib.Analysis.Normed.Operator.Bilinear

From ce4169d83a7d4863a1ec95c2eb4e39ffdf084449 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Micha=C5=82=20Pacholski?= <mpacholski@google.com>
Date: Sun, 19 Jul 2026 13:48:41 +0200
Subject: [PATCH 30/30] feat(Analysis/LocallyConvex/TensorProduct): define the
 projective seminorm family
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Introduce `ProjectiveSeminormFamily` on the binary tensor product `X ⊗[𝕜] Y` of two polynormable spaces.

For each pair of indices `(i, j) : ιX × ιY`, the corresponding seminorm is constructed by:
- Temporarily equipping `X` and `Y` with the `SeminormedAddCommGroup` structures induced by `p i` and `q j`.
- Upgrading these locally to `NormedSpace` structures.
- Instantiating the binary `projectiveSeminorm` on the tensor product under these local structures.

feat(Topology/Algebra/Module): define projective tensor product of topological modules

Introduce the topological foundations for the projective tensor product of
topological modules, following the geometric formulation in Schaefer's
"Topological Vector Spaces".

- Define the type synonym `ProjectiveTensorProduct 𝕜 X Y` with scoped notation `X ⊗[𝕜]π Y`.
- Define the `TopologicalSpace` instance on `X ⊗[𝕜]π Y` as the supremum (`sSup`) of all topologies making the tensor product a locally convex topological module for which the canonical bilinear map `tmul` is continuous.

Specifically:
- Prove that the topology generated by `ProjectiveSeminormFamily p q` makes the canonical map `tmul` continuous.
- Establish the compatibility class `WithSeminorms (ProjectiveSeminormFamily p q)` on the topological space `M ⊗[R]π N` by showing the equivalence between the supremum topology and the seminorm-induced topology.

feat(Analysis/LocallyConvex/TensorProduct): show projective topology is induced by the projective seminorm family

Prove that the projective tensor topology on `X ⊗[𝕜]π Y` (defined via the `sSup` of compatible topologies making the canonical bilinear map `tmul` continuous) is strictly induced by the projective seminorm family `ProjectiveSeminormFamily p q`.

Specifically:
- Prove that the topology generated by `ProjectiveSeminormFamily p q` makes the canonical map `tmul` continuous.
- Establish the compatibility class `WithSeminorms (ProjectiveSeminormFamily p q)` on the topological space `M ⊗[R]π N` by showing the equivalence between the supremum topology and the seminorm-induced topology.

feat(Analysis/LocallyConvex/TensorProduct): show projective topology is induced by the projective seminorm family

Prove that the projective tensor topology on `X ⊗[𝕜]π Y` (defined via the `sSup` of compatible topologies making the canonical bilinear map `tmul` continuous) is strictly induced by the projective seminorm family `ProjectiveSeminormFamily p q`.

Specifically:
- Prove that the topology generated by `ProjectiveSeminormFamily p q` makes the canonical map `tmul` continuous.
- Establish the compatibility class `WithSeminorms (ProjectiveSeminormFamily p q)` on the topological space `M ⊗[R]π N` by showing the equivalence between the supremum topology and the seminorm-induced topology.
---
 .../TensorProduct/Projective.lean             |  35 +++
 .../Module/TensorProduct/Projective.lean      | 219 ++++++++++++++++++
 2 files changed, 254 insertions(+)
 create mode 100644 Mathlib/Analysis/LocallyConvex/TensorProduct/Projective.lean
 create mode 100644 Mathlib/Topology/Algebra/Module/TensorProduct/Projective.lean

diff --git a/Mathlib/Analysis/LocallyConvex/TensorProduct/Projective.lean b/Mathlib/Analysis/LocallyConvex/TensorProduct/Projective.lean
new file mode 100644
index 00000000000000..2db559ea1cd257
--- /dev/null
+++ b/Mathlib/Analysis/LocallyConvex/TensorProduct/Projective.lean
@@ -0,0 +1,35 @@
+module
+
+public import Mathlib.Analysis.Normed.Module.TensorProduct.ProjectiveSeminorm
+public import Mathlib.Topology.Algebra.Module.TensorProduct.Projective
+
+import Mathlib.Analysis.Seminorm
+
+@[expose] public section
+
+open TensorProduct Seminorm NNReal WithSeminorms
+
+variable {𝕜 X Y : Type*}
+
+variable [NormedField 𝕜] [PartialOrder 𝕜]
+variable [AddCommGroup X] [Module 𝕜 X] [TopologicalSpace X] [PolynormableSpace 𝕜 X]
+variable [AddCommGroup Y] [Module 𝕜 Y] [TopologicalSpace Y] [PolynormableSpace 𝕜 Y]
+
+variable {ιX ιY : Type*}
+
+variable (p : SeminormFamily 𝕜 X ιX) (q : SeminormFamily 𝕜 Y ιY)
+
+noncomputable def ProjectiveSeminormFamily : SeminormFamily 𝕜 (X ⊗[𝕜]π Y) (ιX × ιY) := fun ⟨i, j⟩ ↦
+  letI := AddGroupSeminorm.toSeminormedAddCommGroup (p i).toAddGroupSeminorm
+  letI := AddGroupSeminorm.toSeminormedAddCommGroup (q j).toAddGroupSeminorm
+  letI : NormedSpace 𝕜 X := ⟨fun a b ↦ ((p i).smul' a b).le⟩
+  letI : NormedSpace 𝕜 Y := ⟨fun a b ↦ ((q j).smul' a b).le⟩
+  projectiveSeminorm
+
+
+
+
+-- /-- The projective tensor topology is strictly induced by the projective seminorm family. -/
+-- theorem withSeminorms_projectiveTensorProduct :
+--     WithSeminorms (ProjectiveSeminormFamily p q) (topology := instTopologicalSpaceProjectiveTensorProduct) := by
+--   sorry
diff --git a/Mathlib/Topology/Algebra/Module/TensorProduct/Projective.lean b/Mathlib/Topology/Algebra/Module/TensorProduct/Projective.lean
new file mode 100644
index 00000000000000..03d0893e001ef0
--- /dev/null
+++ b/Mathlib/Topology/Algebra/Module/TensorProduct/Projective.lean
@@ -0,0 +1,219 @@
+/-
+Copyright (c) 2026 . All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michał Pacholski
+-/
+module
+
+public import Mathlib.Analysis.LocallyConvex.AbsConvex
+public import Mathlib.LinearAlgebra.TensorProduct.Basic
+public import Mathlib.Topology.Algebra.FilterBasis
+
+import Mathlib.Analysis.LocallyConvex.AbsConvex
+@[expose] public section
+
+open scoped TensorProduct Topology Pointwise
+open Filter Function Bornology
+
+section Semiring
+
+variable {R M N : Type*}
+variable [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N]
+
+variable (M N)
+
+variable (R) in
+/-- Type synonym for the projective tensor product of topological modules. -/
+public def ProjectiveTensorProduct := M ⊗[R] N
+
+@[inherit_doc] scoped[TensorProduct] notation:100 M:100 " ⊗[" R "]π " N:101 =>
+  ProjectiveTensorProduct R M N
+
+end Semiring
+
+namespace TensorProduct
+
+section TopologicalSpace
+
+section CommSemiring
+
+variable {R M N : Type*}
+variable [CommSemiring R] [PartialOrder R] [TopologicalSpace R]
+variable [AddCommGroup M] [Module R M] [TopologicalSpace M] [LocallyConvexSpace R M]
+variable [AddCommGroup N] [Module R N] [TopologicalSpace N] [LocallyConvexSpace R N]
+
+instance : AddCommGroup (M ⊗[R]π N) := addCommGroup
+instance : Module R (M ⊗[R]π  N) := instModule
+
+variable (R) in
+def tensorProductTopologies := { t : TopologicalSpace (M ⊗[R] N) |
+    letI := t
+    IsTopologicalAddGroup (M ⊗[R] N) ∧
+    LocallyConvexSpace R (M ⊗[R] N) ∧
+    Continuous (fun (p : M × N) ↦ TensorProduct.mk R M N p.1 p.2)
+}
+
+/-- The projective topology on `X ⊗[𝕜]π Y` is defined as the supremum of all topologies
+making the space a locally convex topological module such that `tmul` is continuous. -/
+instance instTopologicalSpaceProjectiveTensorProduct : TopologicalSpace (M ⊗[R]π N) :=
+  sInf (tensorProductTopologies R)
+
+instance : LocallyConvexSpace R (M ⊗[R]π N) := LocallyConvexSpace.sInf fun _ ⟨_, h, _⟩ ↦ h
+
+example {t : TopologicalSpace (M ⊗[R] N)} (ht : t ∈ tensorProductTopologies R) :
+  instTopologicalSpaceProjectiveTensorProduct ≤ t := sInf_le ht
+
+example {t : TopologicalSpace (M ⊗[R] N)} (ht : t ∈ tensorProductTopologies R) :
+    𝓝 (0 : (M ⊗[R]π N)) ≤ 𝓝 (0 : (M ⊗[R] N)) := nhds_mono (sInf_le ht)
+
+end CommSemiring
+section NontriviallyNormedField
+
+variable {R M N : Type*}
+variable [NontriviallyNormedField R] [PartialOrder R]
+variable [AddCommGroup M] [Module R M] [TopologicalSpace M] [LocallyConvexSpace R M]
+  [IsTopologicalAddGroup M] [ContinuousSMul R M]
+variable [AddCommGroup N] [Module R N] [TopologicalSpace N] [LocallyConvexSpace R N]
+  [IsTopologicalAddGroup N] [ContinuousSMul R N]
+
+-- (𝕜 : Type u_1) (E : Type u_2) [Semiring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E]
+-- [TopologicalSpace E] [IsTopologicalAddGroup E]
+
+abbrev absConvexHulls (B : Set (Set M)) (B' : Set (Set N)) :=
+  { s | ∃ b ∈ B, ∃ b' ∈ B', s = absConvexHull R (Set.image2 (tmul R) b b') }
+
+def moduleFilterBasis {B : Set (Set M)} {B' : Set (Set N)}
+    (hB : (𝓝 (0 : M)).HasBasis (fun s => s ∈ B) id)
+    (hB' : (𝓝 (0 : N)).HasBasis (fun s => s ∈ B') id) : ModuleFilterBasis R (M ⊗[R] N) where
+  sets := absConvexHulls B B'
+  nonempty := sorry
+  inter_sets := sorry
+  zero' := sorry
+  add' := sorry
+  neg' := sorry
+  conj' := sorry
+  smul' := sorry
+  smul_left' := sorry
+  smul_right' := sorry
+
+/-- Every element in a topological vector space over a nontrivially normed field
+can be represented as a scaled version of an element in any given neighborhood of zero. -/
+lemma exists_smul_of_mem_nhds_zero {𝕜 E : Type*} [NontriviallyNormedField 𝕜]
+    [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E]
+    {V : Set E} (hV : V ∈ 𝓝 0) (x : E) :
+    ∃ (r : 𝕜) (hr : r ≠ 0), ∃ x' ∈ V, x = r • x' := by
+  have h_abs := absorbent_nhds_zero (𝕜 := 𝕜) hV x
+  have h_abs' : ∀ᶠ (r : 𝕜) in cobounded 𝕜, ∃ x' ∈ V, x = r • x' := by
+    filter_upwards [h_abs] with r hr
+    have hx : x ∈ r • V := Set.singleton_subset_iff.mp hr
+    rcases Set.mem_smul_set.mp hx with ⟨x', hx', rfl⟩
+    exact ⟨x', hx', rfl⟩
+  have h_abs_ne := h_abs'.and (eventually_ne_cobounded 0)
+  rcases h_abs_ne.exists with ⟨r, ⟨x', hx', rfl⟩, hr_ne⟩
+  exact ⟨r, hr_ne, x', hx', rfl⟩
+
+lemma locallyConvexSpace_of_basis {B : Set (Set M)} {B' : Set (Set N)}
+    (hB : (𝓝 (0 : M)).HasBasis (fun s => s ∈ B) id)
+    (hB' : (𝓝 (0 : N)).HasBasis (fun s => s ∈ B') id) :
+    @LocallyConvexSpace R (M ⊗[R] N) _ _ _ _ (moduleFilterBasis hB hB').topology := by
+  letI topology := (moduleFilterBasis hB hB').topology (R:=R)
+  apply LocallyConvexSpace.ofBasisZero R (M ⊗[R] N) id _
+    (moduleFilterBasis hB hB').nhds_zero_hasBasis
+  rintro s ⟨b, hb, b', hb', rfl⟩
+  exact convex_absConvexHull
+
+lemma tendsto_tmul_nhds_zero_of_basis {B : Set (Set M)} {B' : Set (Set N)}
+    (hB : (𝓝 (0 : M)).HasBasis (fun s => s ∈ B) id)
+    (hB' : (𝓝 (0 : N)).HasBasis (fun s => s ∈ B') id) :
+    Tendsto (fun p : M × N ↦ p.1 ⊗ₜ[R] p.2) (𝓝 0 ×ˢ 𝓝 0) (moduleFilterBasis hB hB').toAddGroupFilterBasis.filter := by
+  rw [(moduleFilterBasis hB hB').toAddGroupFilterBasis.toFilterBasis.hasBasis.tendsto_right_iff]
+  rintro s ⟨b, hb, b', hb', rfl⟩
+  have hb_nhds : b ∈ 𝓝 (0 : M) := hB.mem_of_mem hb
+  have hb'_nhds : b' ∈ 𝓝 (0 : N) := hB'.mem_of_mem hb'
+  have h_prod : b ×ˢ b' ∈ 𝓝 (0 : M) ×ˢ 𝓝 (0 : N) := prod_mem_prod hb_nhds hb'_nhds
+  filter_upwards [h_prod]
+  rintro ⟨x, y⟩ ⟨hx : x ∈ b, hy : y ∈ b'⟩
+  exact subset_absConvexHull (Set.mem_image2_of_mem hx hy)
+
+lemma continuousAt_mk_apply_of_basis {B : Set (Set M)} {B' : Set (Set N)}
+    (hB : (𝓝 (0 : M)).HasBasis (fun s => s ∈ B) id)
+    (hB' : (𝓝 (0 : N)).HasBasis (fun s => s ∈ B') id) (x : M) :
+    @ContinuousAt N (M ⊗[R] N) _ (moduleFilterBasis hB hB').topology ((mk R M N) x) 0 := by
+  letI topology := (moduleFilterBasis hB hB').topology (R:=R)
+  rw [ContinuousAt, map_zero]
+  rw [(moduleFilterBasis hB hB').nhds_zero_hasBasis.tendsto_right_iff]
+  rintro s ⟨b, hb, b', hb', rfl⟩
+  have hb_nhds : b ∈ 𝓝 (0 : M) := hB.mem_of_mem hb
+  rcases exists_smul_of_mem_nhds_zero (𝕜 := R) hb_nhds x with ⟨r, hr_ne, x', hx', rfl⟩
+  have hb'_nhds : b' ∈ 𝓝 (0 : N) := hB'.mem_of_mem hb'
+  have h_smul : ∀ᶠ y : N in 𝓝 0, r • y ∈ b' :=
+    (continuous_const_smul r).continuousAt (by simpa using hb'_nhds)
+  filter_upwards [h_smul] with y hy
+  rw [mk_apply, smul_tmul]
+  exact subset_absConvexHull (Set.mem_image2_of_mem hx' hy)
+
+lemma continuousAt_tmul_right_of_basis {B : Set (Set M)} {B' : Set (Set N)}
+    (hB : (𝓝 (0 : M)).HasBasis (fun s => s ∈ B) id)
+    (hB' : (𝓝 (0 : N)).HasBasis (fun s => s ∈ B') id) (y : N) :
+    @ContinuousAt M (M ⊗[R] N) _ (moduleFilterBasis hB hB').topology (fun x ↦ x ⊗ₜ[R] y) 0 := by
+  letI topology := (moduleFilterBasis hB hB').topology (R:=R)
+  rw [ContinuousAt, zero_tmul]
+  rw [(moduleFilterBasis hB hB').toAddGroupFilterBasis.nhds_zero_hasBasis.tendsto_right_iff]
+  rintro s ⟨b, hb, b', hb', rfl⟩
+  have hb'_nhds : b' ∈ 𝓝 (0 : N) := hB'.mem_of_mem hb'
+  rcases exists_smul_of_mem_nhds_zero (𝕜 := R) hb'_nhds y with ⟨r, hr_ne, y', hy', rfl⟩
+  have hb_nhds : b ∈ 𝓝 (0 : M) := hB.mem_of_mem hb
+  have h_smul : ∀ᶠ x : M in 𝓝 0, r • x ∈ b :=
+    (continuous_const_smul r).continuousAt (by simpa using hb_nhds)
+  filter_upwards [h_smul] with x hx
+  rw [← TensorProduct.smul_tmul]
+  exact subset_absConvexHull (Set.mem_image2_of_mem hx hy')
+
+example {B : Set (Set M)} {B' : Set (Set N)}
+    (hB : (𝓝 (0 : M)).HasBasis (fun s => s ∈ B) id)
+    (hB' : (𝓝 (0 : N)).HasBasis (fun s => s ∈ B') id) :
+    (moduleFilterBasis hB hB').topology ∈ tensorProductTopologies R := by
+  letI topology := (moduleFilterBasis hB hB').topology (R:=R)
+  unfold tensorProductTopologies
+  simp only [Set.mem_ofPred_eq]
+  refine ⟨(moduleFilterBasis hB hB').isTopologicalAddGroup,
+    locallyConvexSpace_of_basis hB hB', ?_⟩
+  apply continuous_of_continuousAt_zero₂
+    (LinearMap.toAddMonoidHom'.comp (TensorProduct.mk R M N).toAddMonoidHom)
+  · rw [ContinuousAt, Prod.mk_zero_zero]
+    simp only [AddMonoidHom.coe_comp, LinearMap.toAddMonoidHom_coe, comp_apply,
+      LinearMap.toAddMonoidHom'_apply, mk_apply, Prod.fst_zero, map_zero, Prod.snd_zero]
+    rw [nhds_prod_eq, (moduleFilterBasis hB hB').toAddGroupFilterBasis.nhds_zero_eq]
+    exact tendsto_tmul_nhds_zero_of_basis (R := R) hB hB'
+  · simp only [AddMonoidHom.coe_comp, LinearMap.toAddMonoidHom_coe, comp_apply,
+      LinearMap.toAddMonoidHom'_apply]
+    exact continuousAt_mk_apply_of_basis hB hB'
+  · simp only [AddMonoidHom.coe_comp, LinearMap.toAddMonoidHom_coe, comp_apply,
+      LinearMap.toAddMonoidHom'_apply, mk_apply]
+    exact continuousAt_tmul_right_of_basis hB hB'
+
+
+def filterBasis (B : Set (Set M)) (B' : Set (Set N))
+    (hB : (𝓝 (0 : M)).HasBasis (fun s => s ∈ B) id)
+    (hB' : (𝓝 (0 : N)).HasBasis (fun s => s ∈ B') id) : FilterBasis (M ⊗[R] N) where
+  sets :=
+  nonempty := by sorry
+  inter_sets := by sorry
+
+#check (filterBasis _ _ _ _).filter
+
+theorem nhdsZero_hasBasis_absConvexHull_tmul (B : Set (Set M)) (B' : Set (Set N))
+    (hB : (𝓝 (0 : M)).HasBasis (fun s => s ∈ B) id)
+    (hB' : (𝓝 (0 : N)).HasBasis (fun s => s ∈ B') id) :
+    (𝓝 (0 : N ⊗[R]π M)).HasBasis (fun s => s ∈ { s | ∃ b ∈ B, ∃ b' ∈ B', s = absConvexHull R
+      (Set.image2 (tmul R) b' b) }) id := by
+
+  sorry
+
+
+
+end NontriviallyNormedField
+
+end TopologicalSpace
+
+end TensorProduct