From ad319e0aacfa9c0d10e9f7f0f70f11a208e44cab Mon Sep 17 00:00:00 2001 From: TJHeeringa Date: Thu, 30 Apr 2026 10:45:07 +0200 Subject: [PATCH 01/39] Add Gram.posSemidef_of_mapL --- .../Analysis/InnerProductSpace/GramMatrix.lean | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/Mathlib/Analysis/InnerProductSpace/GramMatrix.lean b/Mathlib/Analysis/InnerProductSpace/GramMatrix.lean index 0272b40459cb10..bc5328c1fe6cc7 100644 --- a/Mathlib/Analysis/InnerProductSpace/GramMatrix.lean +++ b/Mathlib/Analysis/InnerProductSpace/GramMatrix.lean @@ -134,6 +134,23 @@ theorem gram_eq_conjTranspose_mul {ι : Type*} [Fintype ι] (b : OrthonormalBasi ext i j simp [mul_apply, b.repr_apply_apply, b.sum_inner_mul_inner] +open scoped MatrixOrder in +omit [Finite n] in +/-- Inequality `‖f x‖ ≤ ‖f‖ * ‖x‖` lifted to Gram matrices. -/ +theorem posSemidef_of_mapL {F} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (v : n → E) + (f : E →L[𝕜] F) : (‖f‖^2 • gram 𝕜 v - gram 𝕜 (f ∘ v)).PosSemidef := by + refine ⟨(isHermitian_gram 𝕜 v).smul + (IsSelfAdjoint.pow (IsSelfAdjoint.apply (Pi.isSelfAdjoint.mpr (congrFun rfl)) f) 2) + |>.sub (isHermitian_gram 𝕜 (f ∘ v)), ?_⟩ + intro c + simp_rw [Finsupp.sum, Matrix.sub_apply, Matrix.smul_apply, mul_sub, sub_mul, + Finset.sum_sub_distrib, sub_nonneg, Algebra.mul_smul_comm, gram_apply, ← starRingEnd_apply, + ← inner_smul_left, mul_comm _ (c _), Algebra.mul_smul_comm, ← Finset.smul_sum, + ← inner_smul_right, ← inner_sum, ← sum_inner, inner_self_eq_norm_sq_to_K, Function.comp_apply, + ← map_smul, ← map_sum] + norm_cast + grw [f.le_opNorm _, smul_eq_mul, ← mul_pow] + end NormedInnerProductSpace end Matrix From b950d062b7ac0c357f0b7f115663c99c5c048a62 Mon Sep 17 00:00:00 2001 From: TJHeeringa Date: Fri, 1 May 2026 11:00:24 +0200 Subject: [PATCH 02/39] Updates according to review --- Mathlib/Analysis/InnerProductSpace/GramMatrix.lean | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/GramMatrix.lean b/Mathlib/Analysis/InnerProductSpace/GramMatrix.lean index bc5328c1fe6cc7..8965f52c20ad5b 100644 --- a/Mathlib/Analysis/InnerProductSpace/GramMatrix.lean +++ b/Mathlib/Analysis/InnerProductSpace/GramMatrix.lean @@ -134,15 +134,12 @@ theorem gram_eq_conjTranspose_mul {ι : Type*} [Fintype ι] (b : OrthonormalBasi ext i j simp [mul_apply, b.repr_apply_apply, b.sum_inner_mul_inner] -open scoped MatrixOrder in omit [Finite n] in /-- Inequality `‖f x‖ ≤ ‖f‖ * ‖x‖` lifted to Gram matrices. -/ -theorem posSemidef_of_mapL {F} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (v : n → E) - (f : E →L[𝕜] F) : (‖f‖^2 • gram 𝕜 v - gram 𝕜 (f ∘ v)).PosSemidef := by - refine ⟨(isHermitian_gram 𝕜 v).smul - (IsSelfAdjoint.pow (IsSelfAdjoint.apply (Pi.isSelfAdjoint.mpr (congrFun rfl)) f) 2) - |>.sub (isHermitian_gram 𝕜 (f ∘ v)), ?_⟩ - intro c +theorem posSemidef_opNorm_smul_gram_sub_gram {F} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] + (v : n → E)(f : E →L[𝕜] F) : (‖f‖ ^ 2 • gram 𝕜 v - gram 𝕜 (f ∘ v)).PosSemidef := by + refine ⟨(isHermitian_gram 𝕜 v).smul (((Pi.isSelfAdjoint.mpr (congrFun rfl)).apply f).pow 2) + |>.sub (isHermitian_gram 𝕜 (f ∘ v)), fun c ↦ ?_⟩ simp_rw [Finsupp.sum, Matrix.sub_apply, Matrix.smul_apply, mul_sub, sub_mul, Finset.sum_sub_distrib, sub_nonneg, Algebra.mul_smul_comm, gram_apply, ← starRingEnd_apply, ← inner_smul_left, mul_comm _ (c _), Algebra.mul_smul_comm, ← Finset.smul_sum, From 8fc955b6b9b301f8d74714a6e202516543a8d7bc Mon Sep 17 00:00:00 2001 From: TJHeeringa Date: Fri, 1 May 2026 11:11:27 +0200 Subject: [PATCH 03/39] Fixed missing space --- Mathlib/Analysis/InnerProductSpace/GramMatrix.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/InnerProductSpace/GramMatrix.lean b/Mathlib/Analysis/InnerProductSpace/GramMatrix.lean index 8965f52c20ad5b..83fbe29db5d256 100644 --- a/Mathlib/Analysis/InnerProductSpace/GramMatrix.lean +++ b/Mathlib/Analysis/InnerProductSpace/GramMatrix.lean @@ -137,7 +137,7 @@ theorem gram_eq_conjTranspose_mul {ι : Type*} [Fintype ι] (b : OrthonormalBasi omit [Finite n] in /-- Inequality `‖f x‖ ≤ ‖f‖ * ‖x‖` lifted to Gram matrices. -/ theorem posSemidef_opNorm_smul_gram_sub_gram {F} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] - (v : n → E)(f : E →L[𝕜] F) : (‖f‖ ^ 2 • gram 𝕜 v - gram 𝕜 (f ∘ v)).PosSemidef := by + (v : n → E) (f : E →L[𝕜] F) : (‖f‖ ^ 2 • gram 𝕜 v - gram 𝕜 (f ∘ v)).PosSemidef := by refine ⟨(isHermitian_gram 𝕜 v).smul (((Pi.isSelfAdjoint.mpr (congrFun rfl)).apply f).pow 2) |>.sub (isHermitian_gram 𝕜 (f ∘ v)), fun c ↦ ?_⟩ simp_rw [Finsupp.sum, Matrix.sub_apply, Matrix.smul_apply, mul_sub, sub_mul, From b66bd1c8b8a9ef91f9b8705f89eb0605b3983fda Mon Sep 17 00:00:00 2001 From: TJHeeringa Date: Tue, 5 May 2026 12:33:00 +0200 Subject: [PATCH 04/39] Added TensorProduct.mapL --- .../InnerProductSpace/TensorProduct.lean | 49 +++++++++++++++++++ 1 file changed, 49 insertions(+) diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean index 00acc51790a69b..948fdaccb0b180 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -8,6 +8,8 @@ module public import Mathlib.Analysis.InnerProductSpace.Adjoint public import Mathlib.LinearAlgebra.TensorProduct.Finiteness public import Mathlib.RingTheory.TensorProduct.Finite +import Mathlib.Analysis.InnerProductSpace.GramMatrix +import Mathlib.Analysis.InnerProductSpace.Positive /-! @@ -414,6 +416,53 @@ noncomputable def assocIsometry : E ⊗[𝕜] F ⊗[𝕜] G ≃ₗᵢ[𝕜] E end isometry +lemma exists_repr (x : E ⊗[𝕜] F) : + ∃ (n : ℕ) (e : Fin n → E) (g : Fin n → F), + x = ∑ i, e i ⊗ₜ[𝕜] g i := by + induction x using TensorProduct.induction_on with + | zero => + exact ⟨0, Fin.elim0, Fin.elim0, by simp⟩ + | tmul m n => + exact ⟨1, fun _ => m, fun _ => n, by simp⟩ + | add x y hx hy => + obtain ⟨nx, ex, gx, hx ⟩ := hx + obtain ⟨ny, ey, gy, hy ⟩ := hy + refine ⟨nx + ny, Fin.append ex ey, Fin.append gx gy, ?_⟩ + rw [hx, hy, Fin.sum_univ_add] + simp [Fin.append] + +noncomputable def mapL_id (f : E →L[𝕜] F) : (E ⊗[𝕜] G) →L[𝕜] (F ⊗[𝕜] G) := + (TensorProduct.map f.toLinearMap LinearMap.id).mkContinuous ‖f‖ (fun x => by + obtain ⟨n, e, g, hx ⟩ := exists_repr x + obtain ⟨m, A, hA⟩ := Matrix.posSemidef_iff_eq_sum_vecMulVec.mp (Matrix.posSemidef_of_mapL e f) + apply (sq_le_sq₀ (norm_nonneg _) (by positivity)).mp + simp_rw [sub_eq_iff_eq_add', ← sub_eq_iff_eq_add, ← Matrix.ext_iff, Matrix.sub_apply, + Matrix.smul_apply, Matrix.gram_apply, Function.comp_apply] at hA + simp_rw [mul_pow, hx, map_sum, map_tmul, ContinuousLinearMap.coe_coe, LinearMap.id_coe, + id_eq, ← inner_self_eq_norm_sq (𝕜:=𝕜), inner_sum, sum_inner, inner_tmul, ← hA, + sub_mul, Finset.sum_sub_distrib, map_sub, ← RCLike.smul_re, Finset.smul_sum, + smul_mul_assoc, sub_le_self_iff, Matrix.sum_apply, mul_comm, Finset.mul_sum] + rw [Finset.sum_comm_cycle] + simp_rw [Matrix.vecMulVec, Matrix.of_apply, Pi.star_apply, ← mul_left_comm, ← mul_assoc] + simp_rw (config := { singlePass := true }) [← starRingEnd_self_apply (A _ _)] + simp_rw [← inner_smul_left, mul_comm (inner 𝕜 _ _) _, ← starRingEnd_apply, ← inner_smul_right, + starRingEnd_self_apply, ← sum_inner, ← inner_sum, map_sum, + ← InnerProductSpace.norm_sq_eq_re_inner] + exact Finset.sum_nonneg (fun x _ => by simp) + ) + +noncomputable def map_idL (g : G →L[𝕜] H) : (E ⊗[𝕜] G) →L[𝕜] (E ⊗[𝕜] H) := + (commIsometry 𝕜 H E) ∘L (mapL_id g) ∘L + (commIsometry 𝕜 E G).toContinuousLinearEquiv.toContinuousLinearMap + +noncomputable def mapL (f : E →L[𝕜] F) (g : G →L[𝕜] H) : (E ⊗[𝕜] G) →L[𝕜] (F ⊗[𝕜] H) := + mapL_id f ∘L map_idL g + +@[simp] +theorem mapL_tmul (f : E →L[𝕜] F) (g : G →L[𝕜] H) (m : E) (n : G) : + mapL f g (m ⊗ₜ n) = f m ⊗ₜ g n := + rfl + -- TODO: upgrade `map` to a `ContinuousLinearMap` @[simp] theorem adjoint_map [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] [FiniteDimensional 𝕜 G] [FiniteDimensional 𝕜 H] (f : E →ₗ[𝕜] F) (g : G →ₗ[𝕜] H) : From 7b49096b6e7c420093a3add7289595c9392b212d Mon Sep 17 00:00:00 2001 From: TJHeeringa Date: Tue, 5 May 2026 15:55:03 +0200 Subject: [PATCH 05/39] Fixed theorem name --- Mathlib/Analysis/InnerProductSpace/TensorProduct.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean index 948fdaccb0b180..c2eae0f3f0ed69 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -434,7 +434,8 @@ lemma exists_repr (x : E ⊗[𝕜] F) : noncomputable def mapL_id (f : E →L[𝕜] F) : (E ⊗[𝕜] G) →L[𝕜] (F ⊗[𝕜] G) := (TensorProduct.map f.toLinearMap LinearMap.id).mkContinuous ‖f‖ (fun x => by obtain ⟨n, e, g, hx ⟩ := exists_repr x - obtain ⟨m, A, hA⟩ := Matrix.posSemidef_iff_eq_sum_vecMulVec.mp (Matrix.posSemidef_of_mapL e f) + obtain ⟨m, A, hA⟩ := Matrix.posSemidef_iff_eq_sum_vecMulVec.mp + (Matrix.posSemidef_opNorm_smul_gram_sub_gram e f) apply (sq_le_sq₀ (norm_nonneg _) (by positivity)).mp simp_rw [sub_eq_iff_eq_add', ← sub_eq_iff_eq_add, ← Matrix.ext_iff, Matrix.sub_apply, Matrix.smul_apply, Matrix.gram_apply, Function.comp_apply] at hA From a409578acf2be20f03dc4f1977ee90945ea7088e Mon Sep 17 00:00:00 2001 From: TJHeeringa Date: Wed, 6 May 2026 11:51:51 +0200 Subject: [PATCH 06/39] Added adjoint_mapL --- .../Analysis/InnerProductSpace/TensorProduct.lean | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean index c2eae0f3f0ed69..22e9779505adb3 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -464,6 +464,19 @@ theorem mapL_tmul (f : E →L[𝕜] F) (g : G →L[𝕜] H) (m : E) (n : G) : mapL f g (m ⊗ₜ n) = f m ⊗ₜ g n := rfl +theorem adjoint_mapL [CompleteSpace E] [CompleteSpace G] [CompleteSpace (E ⊗[𝕜] G)] + [CompleteSpace F] [CompleteSpace H] [CompleteSpace (F ⊗[𝕜] H)] + (f : E →L[𝕜] F) (g : G →L[𝕜] H) : (mapL f g).adjoint = mapL f.adjoint g.adjoint := by + ext v + induction v using TensorProduct.induction_on with + | zero => simp + | tmul => + rw [TensorProduct.ext_iff_inner_right] + intro e₁ e₂ + simp_rw [ContinuousLinearMap.adjoint_inner_left, mapL_tmul, inner_tmul, + ContinuousLinearMap.adjoint_inner_left] + | add x y hx hy => simp_rw [ContinuousLinearMap.map_add, hx, hy] + -- TODO: upgrade `map` to a `ContinuousLinearMap` @[simp] theorem adjoint_map [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] [FiniteDimensional 𝕜 G] [FiniteDimensional 𝕜 H] (f : E →ₗ[𝕜] F) (g : G →ₗ[𝕜] H) : From a9f5aa8004d4a91572696563a81fcca12af9d4e8 Mon Sep 17 00:00:00 2001 From: TJHeeringa Date: Mon, 11 May 2026 17:26:26 +0200 Subject: [PATCH 07/39] Add norms of maps --- .../InnerProductSpace/TensorProduct.lean | 30 ++++++++++++++----- 1 file changed, 23 insertions(+), 7 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean index 22e9779505adb3..cf0330437f6ba4 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -417,8 +417,7 @@ noncomputable def assocIsometry : E ⊗[𝕜] F ⊗[𝕜] G ≃ₗᵢ[𝕜] E end isometry lemma exists_repr (x : E ⊗[𝕜] F) : - ∃ (n : ℕ) (e : Fin n → E) (g : Fin n → F), - x = ∑ i, e i ⊗ₜ[𝕜] g i := by + ∃ (n : ℕ) (e : Fin n → E) (g : Fin n → F), x = ∑ i, e i ⊗ₜ[𝕜] g i := by induction x using TensorProduct.induction_on with | zero => exact ⟨0, Fin.elim0, Fin.elim0, by simp⟩ @@ -431,9 +430,11 @@ lemma exists_repr (x : E ⊗[𝕜] F) : rw [hx, hy, Fin.sum_univ_add] simp [Fin.append] -noncomputable def mapL_id (f : E →L[𝕜] F) : (E ⊗[𝕜] G) →L[𝕜] (F ⊗[𝕜] G) := - (TensorProduct.map f.toLinearMap LinearMap.id).mkContinuous ‖f‖ (fun x => by +noncomputable def mapLId (f : E →L[𝕜] F) : (E ⊗[𝕜] G) →L[𝕜] (F ⊗[𝕜] G) := + (map f.toLinearMap LinearMap.id).mkContinuous ‖f‖ (fun x => by obtain ⟨n, e, g, hx ⟩ := exists_repr x + obtain ⟨c, hc_supp, hc⟩ := Submodule.mem_span_set.mp + ((span_tmul_eq_top 𝕜 E G) ▸ Submodule.mem_top (x := x)) obtain ⟨m, A, hA⟩ := Matrix.posSemidef_iff_eq_sum_vecMulVec.mp (Matrix.posSemidef_opNorm_smul_gram_sub_gram e f) apply (sq_le_sq₀ (norm_nonneg _) (by positivity)).mp @@ -452,12 +453,27 @@ noncomputable def mapL_id (f : E →L[𝕜] F) : (E ⊗[𝕜] G) →L[𝕜] (F exact Finset.sum_nonneg (fun x _ => by simp) ) -noncomputable def map_idL (g : G →L[𝕜] H) : (E ⊗[𝕜] G) →L[𝕜] (E ⊗[𝕜] H) := - (commIsometry 𝕜 H E) ∘L (mapL_id g) ∘L +theorem norm_mapLId (f : E →L[𝕜] F) : ‖mapLId (G:=G) f‖ ≤ ‖f‖ := by + apply LinearMap.mkContinuous_norm_le _ (norm_nonneg _) _ + +noncomputable def mapIdL (g : G →L[𝕜] H) : (E ⊗[𝕜] G) →L[𝕜] (E ⊗[𝕜] H) := + (commIsometry 𝕜 H E) ∘L (mapLId g) ∘L (commIsometry 𝕜 E G).toContinuousLinearEquiv.toContinuousLinearMap +theorem norm_mapIdL (g : G →L[𝕜] H) : ‖mapIdL (E:=E) g‖ ≤ ‖g‖ := by + unfold mapIdL + simp_rw [← LinearIsometryEquiv.toContinuousLinearMap_toLinearIsometry] + grw [ContinuousLinearMap.opNorm_comp_le, ContinuousLinearMap.opNorm_comp_le, norm_mapLId, + (commIsometry 𝕜 E G).toLinearIsometry.norm_toContinuousLinearMap_le, + (commIsometry 𝕜 H E).toLinearIsometry.norm_toContinuousLinearMap_le] + simp + noncomputable def mapL (f : E →L[𝕜] F) (g : G →L[𝕜] H) : (E ⊗[𝕜] G) →L[𝕜] (F ⊗[𝕜] H) := - mapL_id f ∘L map_idL g + mapLId f ∘L mapIdL g + +theorem norm_mapL (f : E →L[𝕜] F) (g : G →L[𝕜] H) : ‖mapL f g‖ ≤ ‖f‖*‖g‖ := by + unfold mapL + grw [ContinuousLinearMap.opNorm_comp_le, norm_mapLId, norm_mapIdL] @[simp] theorem mapL_tmul (f : E →L[𝕜] F) (g : G →L[𝕜] H) (m : E) (n : G) : From edf5018ba931f4e12b7a99a4e0b17a68bb540922 Mon Sep 17 00:00:00 2001 From: TJHeeringa Date: Sun, 31 May 2026 09:46:16 +0200 Subject: [PATCH 08/39] Fixed some spacing --- Mathlib/Analysis/InnerProductSpace/TensorProduct.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean index e04633660577e6..e5641f5117bf1e 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -424,8 +424,8 @@ lemma exists_repr (x : E ⊗[𝕜] F) : | tmul m n => exact ⟨1, fun _ => m, fun _ => n, by simp⟩ | add x y hx hy => - obtain ⟨nx, ex, gx, hx ⟩ := hx - obtain ⟨ny, ey, gy, hy ⟩ := hy + obtain ⟨nx, ex, gx, hx⟩ := hx + obtain ⟨ny, ey, gy, hy⟩ := hy refine ⟨nx + ny, Fin.append ex ey, Fin.append gx gy, ?_⟩ rw [hx, hy, Fin.sum_univ_add] simp [Fin.append] From 0b8bf3008bb23d3352a0e58a46977e123c67c3d8 Mon Sep 17 00:00:00 2001 From: TJHeeringa Date: Sun, 31 May 2026 10:19:03 +0200 Subject: [PATCH 09/39] Added docstrings --- Mathlib/Analysis/InnerProductSpace/TensorProduct.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean index e5641f5117bf1e..f66ac9209fc23b 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -430,6 +430,7 @@ lemma exists_repr (x : E ⊗[𝕜] F) : rw [hx, hy, Fin.sum_univ_add] simp [Fin.append] +/-- Extention of a continuous linear map `f` to the map `x ⊗ₜ[𝕜] y ↦ f(x) ⊗ₜ[𝕜] y`. -/ noncomputable def mapLId (f : E →L[𝕜] F) : (E ⊗[𝕜] G) →L[𝕜] (F ⊗[𝕜] G) := (map f.toLinearMap LinearMap.id).mkContinuous ‖f‖ (fun x => by obtain ⟨n, e, g, hx ⟩ := exists_repr x @@ -456,6 +457,7 @@ noncomputable def mapLId (f : E →L[𝕜] F) : (E ⊗[𝕜] G) →L[𝕜] (F theorem norm_mapLId (f : E →L[𝕜] F) : ‖mapLId (G:=G) f‖ ≤ ‖f‖ := by apply LinearMap.mkContinuous_norm_le _ (norm_nonneg _) _ +/-- Extention of a continuous linear map `g` to the map `x ⊗ₜ[𝕜] y ↦ x ⊗ₜ[𝕜] g(y)`. -/ noncomputable def mapIdL (g : G →L[𝕜] H) : (E ⊗[𝕜] G) →L[𝕜] (E ⊗[𝕜] H) := (commIsometry 𝕜 H E) ∘L (mapLId g) ∘L (commIsometry 𝕜 E G).toContinuousLinearEquiv.toContinuousLinearMap @@ -468,6 +470,7 @@ theorem norm_mapIdL (g : G →L[𝕜] H) : ‖mapIdL (E:=E) g‖ ≤ ‖g‖ := (commIsometry 𝕜 H E).toLinearIsometry.norm_toContinuousLinearMap_le] simp +/-- Extention of a continuous linear maps `f` and `g` to the map `x ⊗ₜ[𝕜] y ↦ f(x) ⊗ₜ[𝕜] g(y)`. -/ noncomputable def mapL (f : E →L[𝕜] F) (g : G →L[𝕜] H) : (E ⊗[𝕜] G) →L[𝕜] (F ⊗[𝕜] H) := mapLId f ∘L mapIdL g From d75db259d5a822b5e5bf7542a6a396c8c9f1e83f Mon Sep 17 00:00:00 2001 From: TJHeeringa Date: Tue, 2 Jun 2026 16:12:52 +0200 Subject: [PATCH 10/39] Add basic lemma's, simplify proofs, adapt naming --- .../InnerProductSpace/TensorProduct.lean | 95 ++++++++++++++----- 1 file changed, 73 insertions(+), 22 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean index f66ac9209fc23b..f4ff250f9846c2 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -430,8 +430,10 @@ lemma exists_repr (x : E ⊗[𝕜] F) : rw [hx, hy, Fin.sum_univ_add] simp [Fin.append] +variable (G) in /-- Extention of a continuous linear map `f` to the map `x ⊗ₜ[𝕜] y ↦ f(x) ⊗ₜ[𝕜] y`. -/ -noncomputable def mapLId (f : E →L[𝕜] F) : (E ⊗[𝕜] G) →L[𝕜] (F ⊗[𝕜] G) := +noncomputable def _root_.ContinuousLinearMap.rTensor (f : E →L[𝕜] F) : + (E ⊗[𝕜] G) →L[𝕜] (F ⊗[𝕜] G) := (map f.toLinearMap LinearMap.id).mkContinuous ‖f‖ (fun x => by obtain ⟨n, e, g, hx ⟩ := exists_repr x obtain ⟨c, hc_supp, hc⟩ := Submodule.mem_span_set.mp @@ -454,49 +456,98 @@ noncomputable def mapLId (f : E →L[𝕜] F) : (E ⊗[𝕜] G) →L[𝕜] (F exact Finset.sum_nonneg (fun x _ => by simp) ) -theorem norm_mapLId (f : E →L[𝕜] F) : ‖mapLId (G:=G) f‖ ≤ ‖f‖ := by +@[simp] +lemma _root_.ContinuousLinearMap.rTensor_apply (f : E →L[𝕜] F) (x : E ⊗ G) : + f.rTensor G x = (map f.toLinearMap LinearMap.id) x := rfl + +@[simp] +lemma _root_.ContinuousLinearMap.rTensor_tmul (f : E →L[𝕜] F) (m : E) (n : G) : + f.rTensor G (m ⊗ₜ n) = f m ⊗ₜ n := rfl + +variable (G) in +@[simp] +lemma _root_.ContinuousLinearMap.toLinearMap_rTensor (f : E →L[𝕜] F) : + (f.rTensor G).toLinearMap = f.toLinearMap.rTensor G := rfl + +variable (G) in +theorem _root_.ContinuousLinearMap.rTensor_norm_le (f : E →L[𝕜] F) : + ‖ContinuousLinearMap.rTensor G f‖ ≤ ‖f‖ := by apply LinearMap.mkContinuous_norm_le _ (norm_nonneg _) _ +variable (G) in +omit [InnerProductSpace 𝕜 H] in +theorem _root_.ContinuousLinearMap.adjoint_rTensor [CompleteSpace E] [CompleteSpace G] + [CompleteSpace (E ⊗[𝕜] G)] [CompleteSpace (F ⊗[𝕜] G)] [CompleteSpace F] [CompleteSpace H] + (f : E →L[𝕜] F) : + (f.rTensor G).adjoint = f.adjoint.rTensor G := by + apply ContinuousLinearMap.coe_inj.mp <| ext' ?_ + simp [TensorProduct.ext_iff_inner_right, ContinuousLinearMap.adjoint_inner_left] + +variable (E) in /-- Extention of a continuous linear map `g` to the map `x ⊗ₜ[𝕜] y ↦ x ⊗ₜ[𝕜] g(y)`. -/ -noncomputable def mapIdL (g : G →L[𝕜] H) : (E ⊗[𝕜] G) →L[𝕜] (E ⊗[𝕜] H) := - (commIsometry 𝕜 H E) ∘L (mapLId g) ∘L +noncomputable def _root_.ContinuousLinearMap.lTensor (g : G →L[𝕜] H) : + (E ⊗[𝕜] G) →L[𝕜] (E ⊗[𝕜] H) := + (commIsometry 𝕜 H E) ∘L (ContinuousLinearMap.rTensor E g) ∘L (commIsometry 𝕜 E G).toContinuousLinearEquiv.toContinuousLinearMap -theorem norm_mapIdL (g : G →L[𝕜] H) : ‖mapIdL (E:=E) g‖ ≤ ‖g‖ := by - unfold mapIdL +variable (E) in +@[simp] +lemma _root_.ContinuousLinearMap.lTensor_def (g : G →L[𝕜] H) : + g.lTensor E = (commIsometry 𝕜 H E) ∘L (ContinuousLinearMap.rTensor E g) ∘L + (commIsometry 𝕜 E G).toContinuousLinearEquiv.toContinuousLinearMap := rfl + +variable (E) in +@[simp] +lemma _root_.ContinuousLinearMap.lTensor_tmul (g : G →L[𝕜] H) (m : E) (n : G) : + g.lTensor E (m ⊗ₜ n) = m ⊗ₜ g n := rfl + +variable (E) in +lemma _root_.ContinuousLinearMap.toLinearMap_lTensor (g : G →L[𝕜] H) : + (g.lTensor E).toLinearMap = g.toLinearMap.lTensor E := by + ext; simp + +variable (E) in +theorem _root_.ContinuousLinearMap.lTensor_norm_le (g : G →L[𝕜] H) : ‖ContinuousLinearMap.lTensor E g‖ ≤ ‖g‖ := by + unfold ContinuousLinearMap.lTensor simp_rw [← LinearIsometryEquiv.toContinuousLinearMap_toLinearIsometry] - grw [ContinuousLinearMap.opNorm_comp_le, ContinuousLinearMap.opNorm_comp_le, norm_mapLId, + grw [ContinuousLinearMap.opNorm_comp_le, ContinuousLinearMap.opNorm_comp_le, + ContinuousLinearMap.rTensor_norm_le, (commIsometry 𝕜 E G).toLinearIsometry.norm_toContinuousLinearMap_le, (commIsometry 𝕜 H E).toLinearIsometry.norm_toContinuousLinearMap_le] simp +variable (E) in +omit [InnerProductSpace 𝕜 F] in +theorem _root_.ContinuousLinearMap.adjoint_lTensor [CompleteSpace E] [CompleteSpace G] + [CompleteSpace (H ⊗[𝕜] E)] [CompleteSpace (G ⊗[𝕜] E)] [CompleteSpace F] [CompleteSpace H] + (g : G →L[𝕜] H) : + (g.rTensor E).adjoint = g.adjoint.rTensor E := by + apply ContinuousLinearMap.coe_inj.mp <| ext' ?_ + simp [TensorProduct.ext_iff_inner_right, ContinuousLinearMap.adjoint_inner_left] + /-- Extention of a continuous linear maps `f` and `g` to the map `x ⊗ₜ[𝕜] y ↦ f(x) ⊗ₜ[𝕜] g(y)`. -/ noncomputable def mapL (f : E →L[𝕜] F) (g : G →L[𝕜] H) : (E ⊗[𝕜] G) →L[𝕜] (F ⊗[𝕜] H) := - mapLId f ∘L mapIdL g + ContinuousLinearMap.rTensor H f ∘L ContinuousLinearMap.lTensor E g -theorem norm_mapL (f : E →L[𝕜] F) (g : G →L[𝕜] H) : ‖mapL f g‖ ≤ ‖f‖*‖g‖ := by +theorem norm_mapL_le (f : E →L[𝕜] F) (g : G →L[𝕜] H) : ‖mapL f g‖ ≤ ‖f‖ * ‖g‖ := by unfold mapL - grw [ContinuousLinearMap.opNorm_comp_le, norm_mapLId, norm_mapIdL] + grw [ContinuousLinearMap.opNorm_comp_le, ContinuousLinearMap.rTensor_norm_le, + ContinuousLinearMap.lTensor_norm_le] @[simp] -theorem mapL_tmul (f : E →L[𝕜] F) (g : G →L[𝕜] H) (m : E) (n : G) : +lemma mapL_tmul (f : E →L[𝕜] F) (g : G →L[𝕜] H) (m : E) (n : G) : mapL f g (m ⊗ₜ n) = f m ⊗ₜ g n := rfl +lemma toLinearMap_mapL (f : E →L[𝕜] F) (g : G →L[𝕜] H) : (mapL f g).toLinearMap = map f g := by + ext; simp + theorem adjoint_mapL [CompleteSpace E] [CompleteSpace G] [CompleteSpace (E ⊗[𝕜] G)] [CompleteSpace F] [CompleteSpace H] [CompleteSpace (F ⊗[𝕜] H)] (f : E →L[𝕜] F) (g : G →L[𝕜] H) : (mapL f g).adjoint = mapL f.adjoint g.adjoint := by - ext v - induction v using TensorProduct.induction_on with - | zero => simp - | tmul => - rw [TensorProduct.ext_iff_inner_right] - intro e₁ e₂ - simp_rw [ContinuousLinearMap.adjoint_inner_left, mapL_tmul, inner_tmul, - ContinuousLinearMap.adjoint_inner_left] - | add x y hx hy => simp_rw [ContinuousLinearMap.map_add, hx, hy] - --- TODO: upgrade `map` to a `ContinuousLinearMap` + apply ContinuousLinearMap.coe_inj.mp <| ext' ?_ + simp [TensorProduct.ext_iff_inner_right, ContinuousLinearMap.adjoint_inner_left] + @[simp] theorem adjoint_map [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] [FiniteDimensional 𝕜 G] [FiniteDimensional 𝕜 H] (f : E →ₗ[𝕜] F) (g : G →ₗ[𝕜] H) : LinearMap.adjoint (map f g) = map (LinearMap.adjoint f) (LinearMap.adjoint g) := From c0405ea167685fc57f107e7646395bb99c6d0019 Mon Sep 17 00:00:00 2001 From: TJHeeringa Date: Tue, 2 Jun 2026 16:26:27 +0200 Subject: [PATCH 11/39] Add lTensor_apply --- Mathlib/Analysis/InnerProductSpace/TensorProduct.lean | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean index f4ff250f9846c2..5b641221826929 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -501,6 +501,16 @@ variable (E) in lemma _root_.ContinuousLinearMap.lTensor_tmul (g : G →L[𝕜] H) (m : E) (n : G) : g.lTensor E (m ⊗ₜ n) = m ⊗ₜ g n := rfl +lemma _root_.ContinuousLinearMap.lTensor_apply (g : G →L[𝕜] H) (x : E ⊗ G) : + g.lTensor E x = (map LinearMap.id g.toLinearMap) x := by + simp only [ContinuousLinearMap.lTensor_def, ContinuousLinearMap.coe_comp', + ContinuousLinearEquiv.coe_coe, LinearIsometryEquiv.coe_toContinuousLinearEquiv, + Function.comp_apply, commIsometry_apply, ContinuousLinearMap.rTensor_apply] + induction x using TensorProduct.induction_on with + | zero => simp + | tmul => simp + | add _ _ h1 h2 => simp [h1, h2] + variable (E) in lemma _root_.ContinuousLinearMap.toLinearMap_lTensor (g : G →L[𝕜] H) : (g.lTensor E).toLinearMap = g.toLinearMap.lTensor E := by From 42ec1d242291a0c7a6753f4695c4326f12096d70 Mon Sep 17 00:00:00 2001 From: TJHeeringa Date: Tue, 2 Jun 2026 22:30:07 +0200 Subject: [PATCH 12/39] Add comm_comp_Tensor_comp_comm_eq and Tensor_comp_comm theorems --- .../InnerProductSpace/TensorProduct.lean | 41 ++++++++++++++----- 1 file changed, 30 insertions(+), 11 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean index ca859bd6135185..de9df01200bb14 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -39,8 +39,6 @@ inner product spaces. ## TODO: -* Define the continuous linear map version of `TensorProduct.map`. -* Complete space of tensor products. * Define the normed space without needing inner products, this should be analogous to `Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean`. @@ -431,7 +429,8 @@ lemma exists_repr (x : E ⊗[𝕜] F) : simp [Fin.append] variable (G) in -/-- Extention of a continuous linear map `f` to the map `x ⊗ₜ[𝕜] y ↦ f(x) ⊗ₜ[𝕜] y`. -/ +/-- `LinearMap.rTensor` as a continuous linear map, i.e. the continuous linear map `f` extended to +the map `x ⊗ₜ[𝕜] y ↦ f(x) ⊗ₜ[𝕜] y`. -/ noncomputable def _root_.ContinuousLinearMap.rTensor (f : E →L[𝕜] F) : (E ⊗[𝕜] G) →L[𝕜] (F ⊗[𝕜] G) := (map f.toLinearMap LinearMap.id).mkContinuous ‖f‖ (fun x => by @@ -460,7 +459,6 @@ noncomputable def _root_.ContinuousLinearMap.rTensor (f : E →L[𝕜] F) : lemma _root_.ContinuousLinearMap.rTensor_apply (f : E →L[𝕜] F) (x : E ⊗ G) : f.rTensor G x = (map f.toLinearMap LinearMap.id) x := rfl -@[simp] lemma _root_.ContinuousLinearMap.rTensor_tmul (f : E →L[𝕜] F) (m : E) (n : G) : f.rTensor G (m ⊗ₜ n) = f m ⊗ₜ n := rfl @@ -484,7 +482,8 @@ theorem _root_.ContinuousLinearMap.adjoint_rTensor [CompleteSpace E] [CompleteSp simp [TensorProduct.ext_iff_inner_right, ContinuousLinearMap.adjoint_inner_left] variable (E) in -/-- Extention of a continuous linear map `g` to the map `x ⊗ₜ[𝕜] y ↦ x ⊗ₜ[𝕜] g(y)`. -/ +/-- `LinearMap.lTensor` as a continuous linear map, i.e. the continuous linear map `g` extended to +the map `x ⊗ₜ[𝕜] y ↦ x ⊗ₜ[𝕜] g(y)`. -/ noncomputable def _root_.ContinuousLinearMap.lTensor (g : G →L[𝕜] H) : (E ⊗[𝕜] G) →L[𝕜] (E ⊗[𝕜] H) := (commIsometry 𝕜 H E) ∘L (ContinuousLinearMap.rTensor E g) ∘L @@ -501,15 +500,33 @@ variable (E) in lemma _root_.ContinuousLinearMap.lTensor_tmul (g : G →L[𝕜] H) (m : E) (n : G) : g.lTensor E (m ⊗ₜ n) = m ⊗ₜ g n := rfl +variable (E) in +theorem _root_.ContinuousLinearMap.comm_comp_lTensor_comp_comm_eq (g : G →L[𝕜] H) : + commIsometry 𝕜 H E ∘L g.rTensor E ∘L commIsometry 𝕜 E G = g.lTensor E := + rfl + +variable (G) in +theorem _root_.ContinuousLinearMap.comm_comp_rTensor_comp_comm_eq (f : E →L[𝕜] F) : + commIsometry 𝕜 G F ∘L f.lTensor G ∘L commIsometry 𝕜 E G = f.rTensor G := + by ext; simp + +variable (G) in +theorem _root_.ContinuousLinearMap.lTensor_comp_comm (f : E →L[𝕜] F) : + f.lTensor G ∘L commIsometry 𝕜 E G = commIsometry 𝕜 F G ∘L f.rTensor G := + by ext; simp + +variable (E) in +theorem _root_.ContinuousLinearMap.rTensor_comp_comm (g : G →L[𝕜] H) : + g.rTensor E ∘L commIsometry 𝕜 E G = commIsometry 𝕜 E H ∘L g.lTensor E := + by ext; simp + lemma _root_.ContinuousLinearMap.lTensor_apply (g : G →L[𝕜] H) (x : E ⊗ G) : g.lTensor E x = (map LinearMap.id g.toLinearMap) x := by simp only [ContinuousLinearMap.lTensor_def, ContinuousLinearMap.coe_comp', ContinuousLinearEquiv.coe_coe, LinearIsometryEquiv.coe_toContinuousLinearEquiv, Function.comp_apply, commIsometry_apply, ContinuousLinearMap.rTensor_apply] - induction x using TensorProduct.induction_on with - | zero => simp - | tmul => simp - | add _ _ h1 h2 => simp [h1, h2] + simp_rw [← LinearMap.lTensor_def, ← LinearMap.rTensor_def] + exact LinearMap.congr_fun (LinearMap.comm_comp_rTensor_comp_comm_eq g.toLinearMap (Q:=E)) x variable (E) in lemma _root_.ContinuousLinearMap.toLinearMap_lTensor (g : G →L[𝕜] H) : @@ -517,7 +534,8 @@ lemma _root_.ContinuousLinearMap.toLinearMap_lTensor (g : G →L[𝕜] H) : ext; simp variable (E) in -theorem _root_.ContinuousLinearMap.lTensor_norm_le (g : G →L[𝕜] H) : ‖ContinuousLinearMap.lTensor E g‖ ≤ ‖g‖ := by +theorem _root_.ContinuousLinearMap.lTensor_norm_le (g : G →L[𝕜] H) : + ‖ContinuousLinearMap.lTensor E g‖ ≤ ‖g‖ := by unfold ContinuousLinearMap.lTensor simp_rw [← LinearIsometryEquiv.toContinuousLinearMap_toLinearIsometry] grw [ContinuousLinearMap.opNorm_comp_le, ContinuousLinearMap.opNorm_comp_le, @@ -535,7 +553,8 @@ theorem _root_.ContinuousLinearMap.adjoint_lTensor [CompleteSpace E] [CompleteSp apply ContinuousLinearMap.coe_inj.mp <| ext' ?_ simp [TensorProduct.ext_iff_inner_right, ContinuousLinearMap.adjoint_inner_left] -/-- Extention of a continuous linear maps `f` and `g` to the map `x ⊗ₜ[𝕜] y ↦ f(x) ⊗ₜ[𝕜] g(y)`. -/ +/-- `TensorProduct.map` as a continuous linear map, i.e. the continuous linear map +`x ⊗ₜ[𝕜] y ↦ f(x) ⊗ₜ[𝕜] g(y)` formed from the continuous linear maps `f` and `g`. -/ noncomputable def mapL (f : E →L[𝕜] F) (g : G →L[𝕜] H) : (E ⊗[𝕜] G) →L[𝕜] (F ⊗[𝕜] H) := ContinuousLinearMap.rTensor H f ∘L ContinuousLinearMap.lTensor E g From 46b5ec85e586ab51666888d7ed179028e5b962b2 Mon Sep 17 00:00:00 2001 From: TJHeeringa Date: Wed, 3 Jun 2026 10:23:34 +0200 Subject: [PATCH 13/39] Remove exists_repr --- .../InnerProductSpace/TensorProduct.lean | 16 +--------------- 1 file changed, 1 insertion(+), 15 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean index de9df01200bb14..9107f460f01c0e 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -414,27 +414,13 @@ noncomputable def assocIsometry : E ⊗[𝕜] F ⊗[𝕜] G ≃ₗᵢ[𝕜] E end isometry -lemma exists_repr (x : E ⊗[𝕜] F) : - ∃ (n : ℕ) (e : Fin n → E) (g : Fin n → F), x = ∑ i, e i ⊗ₜ[𝕜] g i := by - induction x using TensorProduct.induction_on with - | zero => - exact ⟨0, Fin.elim0, Fin.elim0, by simp⟩ - | tmul m n => - exact ⟨1, fun _ => m, fun _ => n, by simp⟩ - | add x y hx hy => - obtain ⟨nx, ex, gx, hx⟩ := hx - obtain ⟨ny, ey, gy, hy⟩ := hy - refine ⟨nx + ny, Fin.append ex ey, Fin.append gx gy, ?_⟩ - rw [hx, hy, Fin.sum_univ_add] - simp [Fin.append] - variable (G) in /-- `LinearMap.rTensor` as a continuous linear map, i.e. the continuous linear map `f` extended to the map `x ⊗ₜ[𝕜] y ↦ f(x) ⊗ₜ[𝕜] y`. -/ noncomputable def _root_.ContinuousLinearMap.rTensor (f : E →L[𝕜] F) : (E ⊗[𝕜] G) →L[𝕜] (F ⊗[𝕜] G) := (map f.toLinearMap LinearMap.id).mkContinuous ‖f‖ (fun x => by - obtain ⟨n, e, g, hx ⟩ := exists_repr x + obtain ⟨n, e, g, hx ⟩ := exists_sum_tmul_eq x obtain ⟨c, hc_supp, hc⟩ := Submodule.mem_span_set.mp ((span_tmul_eq_top 𝕜 E G) ▸ Submodule.mem_top (x := x)) obtain ⟨m, A, hA⟩ := Matrix.posSemidef_iff_eq_sum_vecMulVec.mp From c72a81b2646606be54b662689fb946d47f57928e Mon Sep 17 00:00:00 2001 From: TJHeeringa Date: Wed, 3 Jun 2026 11:48:24 +0200 Subject: [PATCH 14/39] Change CLM.rTensor from map to LM.rTensor --- Mathlib/Analysis/InnerProductSpace/TensorProduct.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean index 9107f460f01c0e..3cc0f981d4db23 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -419,7 +419,7 @@ variable (G) in the map `x ⊗ₜ[𝕜] y ↦ f(x) ⊗ₜ[𝕜] y`. -/ noncomputable def _root_.ContinuousLinearMap.rTensor (f : E →L[𝕜] F) : (E ⊗[𝕜] G) →L[𝕜] (F ⊗[𝕜] G) := - (map f.toLinearMap LinearMap.id).mkContinuous ‖f‖ (fun x => by + (f.toLinearMap.rTensor G).mkContinuous ‖f‖ (fun x => by obtain ⟨n, e, g, hx ⟩ := exists_sum_tmul_eq x obtain ⟨c, hc_supp, hc⟩ := Submodule.mem_span_set.mp ((span_tmul_eq_top 𝕜 E G) ▸ Submodule.mem_top (x := x)) @@ -428,10 +428,10 @@ noncomputable def _root_.ContinuousLinearMap.rTensor (f : E →L[𝕜] F) : apply (sq_le_sq₀ (norm_nonneg _) (by positivity)).mp simp_rw [sub_eq_iff_eq_add', ← sub_eq_iff_eq_add, ← Matrix.ext_iff, Matrix.sub_apply, Matrix.smul_apply, Matrix.gram_apply, Function.comp_apply] at hA - simp_rw [mul_pow, hx, map_sum, map_tmul, ContinuousLinearMap.coe_coe, LinearMap.id_coe, - id_eq, ← inner_self_eq_norm_sq (𝕜:=𝕜), inner_sum, sum_inner, inner_tmul, ← hA, - sub_mul, Finset.sum_sub_distrib, map_sub, ← RCLike.smul_re, Finset.smul_sum, - smul_mul_assoc, sub_le_self_iff, Matrix.sum_apply, mul_comm, Finset.mul_sum] + simp_rw [mul_pow, hx, map_sum, LinearMap.rTensor_tmul, ContinuousLinearMap.coe_coe, + ← inner_self_eq_norm_sq (𝕜:=𝕜), inner_sum, sum_inner, inner_tmul, ← hA, sub_mul, + Finset.sum_sub_distrib, map_sub, ← RCLike.smul_re, Finset.smul_sum, smul_mul_assoc, + sub_le_self_iff, Matrix.sum_apply, mul_comm, Finset.mul_sum] rw [Finset.sum_comm_cycle] simp_rw [Matrix.vecMulVec, Matrix.of_apply, Pi.star_apply, ← mul_left_comm, ← mul_assoc] simp_rw (config := { singlePass := true }) [← starRingEnd_self_apply (A _ _)] From 48ee90710e0b5b65167b4cfde055f6d0882accb4 Mon Sep 17 00:00:00 2001 From: TJHeeringa Date: Wed, 3 Jun 2026 12:19:09 +0200 Subject: [PATCH 15/39] Update namespace TensorProduct to CLM --- .../InnerProductSpace/TensorProduct.lean | 93 ++++++++++--------- 1 file changed, 51 insertions(+), 42 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean index 3cc0f981d4db23..e2ae2c1d58da11 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -414,10 +414,16 @@ noncomputable def assocIsometry : E ⊗[𝕜] F ⊗[𝕜] G ≃ₗᵢ[𝕜] E end isometry +end TensorProduct + +namespace ContinuousLinearMap + +open TensorProduct + variable (G) in /-- `LinearMap.rTensor` as a continuous linear map, i.e. the continuous linear map `f` extended to the map `x ⊗ₜ[𝕜] y ↦ f(x) ⊗ₜ[𝕜] y`. -/ -noncomputable def _root_.ContinuousLinearMap.rTensor (f : E →L[𝕜] F) : +noncomputable def rTensor (f : E →L[𝕜] F) : (E ⊗[𝕜] G) →L[𝕜] (F ⊗[𝕜] G) := (f.toLinearMap.rTensor G).mkContinuous ‖f‖ (fun x => by obtain ⟨n, e, g, hx ⟩ := exists_sum_tmul_eq x @@ -428,10 +434,10 @@ noncomputable def _root_.ContinuousLinearMap.rTensor (f : E →L[𝕜] F) : apply (sq_le_sq₀ (norm_nonneg _) (by positivity)).mp simp_rw [sub_eq_iff_eq_add', ← sub_eq_iff_eq_add, ← Matrix.ext_iff, Matrix.sub_apply, Matrix.smul_apply, Matrix.gram_apply, Function.comp_apply] at hA - simp_rw [mul_pow, hx, map_sum, LinearMap.rTensor_tmul, ContinuousLinearMap.coe_coe, - ← inner_self_eq_norm_sq (𝕜:=𝕜), inner_sum, sum_inner, inner_tmul, ← hA, sub_mul, - Finset.sum_sub_distrib, map_sub, ← RCLike.smul_re, Finset.smul_sum, smul_mul_assoc, - sub_le_self_iff, Matrix.sum_apply, mul_comm, Finset.mul_sum] + simp_rw [mul_pow, hx, map_sum, LinearMap.rTensor_tmul, coe_coe, ← inner_self_eq_norm_sq (𝕜:=𝕜), + inner_sum, sum_inner, inner_tmul, ← hA, sub_mul, Finset.sum_sub_distrib, map_sub, + ← RCLike.smul_re, Finset.smul_sum, smul_mul_assoc, sub_le_self_iff, Matrix.sum_apply, + mul_comm, Finset.mul_sum] rw [Finset.sum_comm_cycle] simp_rw [Matrix.vecMulVec, Matrix.of_apply, Pi.star_apply, ← mul_left_comm, ← mul_assoc] simp_rw (config := { singlePass := true }) [← starRingEnd_self_apply (A _ _)] @@ -442,107 +448,110 @@ noncomputable def _root_.ContinuousLinearMap.rTensor (f : E →L[𝕜] F) : ) @[simp] -lemma _root_.ContinuousLinearMap.rTensor_apply (f : E →L[𝕜] F) (x : E ⊗ G) : +lemma rTensor_apply (f : E →L[𝕜] F) (x : E ⊗ G) : f.rTensor G x = (map f.toLinearMap LinearMap.id) x := rfl -lemma _root_.ContinuousLinearMap.rTensor_tmul (f : E →L[𝕜] F) (m : E) (n : G) : +lemma rTensor_tmul (f : E →L[𝕜] F) (m : E) (n : G) : f.rTensor G (m ⊗ₜ n) = f m ⊗ₜ n := rfl variable (G) in @[simp] -lemma _root_.ContinuousLinearMap.toLinearMap_rTensor (f : E →L[𝕜] F) : +lemma toLinearMap_rTensor (f : E →L[𝕜] F) : (f.rTensor G).toLinearMap = f.toLinearMap.rTensor G := rfl variable (G) in -theorem _root_.ContinuousLinearMap.rTensor_norm_le (f : E →L[𝕜] F) : - ‖ContinuousLinearMap.rTensor G f‖ ≤ ‖f‖ := by +theorem rTensor_norm_le (f : E →L[𝕜] F) : + ‖f.rTensor G‖ ≤ ‖f‖ := by apply LinearMap.mkContinuous_norm_le _ (norm_nonneg _) _ variable (G) in omit [InnerProductSpace 𝕜 H] in -theorem _root_.ContinuousLinearMap.adjoint_rTensor [CompleteSpace E] [CompleteSpace G] +theorem adjoint_rTensor [CompleteSpace E] [CompleteSpace G] [CompleteSpace (E ⊗[𝕜] G)] [CompleteSpace (F ⊗[𝕜] G)] [CompleteSpace F] [CompleteSpace H] (f : E →L[𝕜] F) : (f.rTensor G).adjoint = f.adjoint.rTensor G := by - apply ContinuousLinearMap.coe_inj.mp <| ext' ?_ - simp [TensorProduct.ext_iff_inner_right, ContinuousLinearMap.adjoint_inner_left] + apply coe_inj.mp <| ext' ?_ + simp [TensorProduct.ext_iff_inner_right, adjoint_inner_left] variable (E) in /-- `LinearMap.lTensor` as a continuous linear map, i.e. the continuous linear map `g` extended to the map `x ⊗ₜ[𝕜] y ↦ x ⊗ₜ[𝕜] g(y)`. -/ -noncomputable def _root_.ContinuousLinearMap.lTensor (g : G →L[𝕜] H) : +noncomputable def lTensor (g : G →L[𝕜] H) : (E ⊗[𝕜] G) →L[𝕜] (E ⊗[𝕜] H) := - (commIsometry 𝕜 H E) ∘L (ContinuousLinearMap.rTensor E g) ∘L + (commIsometry 𝕜 H E) ∘L (g.rTensor E) ∘L (commIsometry 𝕜 E G).toContinuousLinearEquiv.toContinuousLinearMap variable (E) in @[simp] -lemma _root_.ContinuousLinearMap.lTensor_def (g : G →L[𝕜] H) : - g.lTensor E = (commIsometry 𝕜 H E) ∘L (ContinuousLinearMap.rTensor E g) ∘L +lemma lTensor_def (g : G →L[𝕜] H) : + g.lTensor E = (commIsometry 𝕜 H E) ∘L (g.rTensor E) ∘L (commIsometry 𝕜 E G).toContinuousLinearEquiv.toContinuousLinearMap := rfl variable (E) in @[simp] -lemma _root_.ContinuousLinearMap.lTensor_tmul (g : G →L[𝕜] H) (m : E) (n : G) : +lemma lTensor_tmul (g : G →L[𝕜] H) (m : E) (n : G) : g.lTensor E (m ⊗ₜ n) = m ⊗ₜ g n := rfl variable (E) in -theorem _root_.ContinuousLinearMap.comm_comp_lTensor_comp_comm_eq (g : G →L[𝕜] H) : +theorem comm_comp_lTensor_comp_comm_eq (g : G →L[𝕜] H) : commIsometry 𝕜 H E ∘L g.rTensor E ∘L commIsometry 𝕜 E G = g.lTensor E := rfl variable (G) in -theorem _root_.ContinuousLinearMap.comm_comp_rTensor_comp_comm_eq (f : E →L[𝕜] F) : +theorem comm_comp_rTensor_comp_comm_eq (f : E →L[𝕜] F) : commIsometry 𝕜 G F ∘L f.lTensor G ∘L commIsometry 𝕜 E G = f.rTensor G := by ext; simp variable (G) in -theorem _root_.ContinuousLinearMap.lTensor_comp_comm (f : E →L[𝕜] F) : +theorem lTensor_comp_comm (f : E →L[𝕜] F) : f.lTensor G ∘L commIsometry 𝕜 E G = commIsometry 𝕜 F G ∘L f.rTensor G := by ext; simp variable (E) in -theorem _root_.ContinuousLinearMap.rTensor_comp_comm (g : G →L[𝕜] H) : +theorem rTensor_comp_comm (g : G →L[𝕜] H) : g.rTensor E ∘L commIsometry 𝕜 E G = commIsometry 𝕜 E H ∘L g.lTensor E := by ext; simp -lemma _root_.ContinuousLinearMap.lTensor_apply (g : G →L[𝕜] H) (x : E ⊗ G) : +lemma lTensor_apply (g : G →L[𝕜] H) (x : E ⊗ G) : g.lTensor E x = (map LinearMap.id g.toLinearMap) x := by - simp only [ContinuousLinearMap.lTensor_def, ContinuousLinearMap.coe_comp', - ContinuousLinearEquiv.coe_coe, LinearIsometryEquiv.coe_toContinuousLinearEquiv, - Function.comp_apply, commIsometry_apply, ContinuousLinearMap.rTensor_apply] + simp only [lTensor_def, coe_comp', ContinuousLinearEquiv.coe_coe, + LinearIsometryEquiv.coe_toContinuousLinearEquiv, Function.comp_apply, commIsometry_apply, + rTensor_apply] simp_rw [← LinearMap.lTensor_def, ← LinearMap.rTensor_def] exact LinearMap.congr_fun (LinearMap.comm_comp_rTensor_comp_comm_eq g.toLinearMap (Q:=E)) x variable (E) in -lemma _root_.ContinuousLinearMap.toLinearMap_lTensor (g : G →L[𝕜] H) : +lemma toLinearMap_lTensor (g : G →L[𝕜] H) : (g.lTensor E).toLinearMap = g.toLinearMap.lTensor E := by ext; simp variable (E) in -theorem _root_.ContinuousLinearMap.lTensor_norm_le (g : G →L[𝕜] H) : - ‖ContinuousLinearMap.lTensor E g‖ ≤ ‖g‖ := by - unfold ContinuousLinearMap.lTensor +theorem lTensor_norm_le (g : G →L[𝕜] H) : + ‖g.lTensor E‖ ≤ ‖g‖ := by + unfold lTensor simp_rw [← LinearIsometryEquiv.toContinuousLinearMap_toLinearIsometry] - grw [ContinuousLinearMap.opNorm_comp_le, ContinuousLinearMap.opNorm_comp_le, - ContinuousLinearMap.rTensor_norm_le, + grw [opNorm_comp_le, opNorm_comp_le, rTensor_norm_le, (commIsometry 𝕜 E G).toLinearIsometry.norm_toContinuousLinearMap_le, (commIsometry 𝕜 H E).toLinearIsometry.norm_toContinuousLinearMap_le] simp variable (E) in omit [InnerProductSpace 𝕜 F] in -theorem _root_.ContinuousLinearMap.adjoint_lTensor [CompleteSpace E] [CompleteSpace G] +theorem adjoint_lTensor [CompleteSpace E] [CompleteSpace G] [CompleteSpace (H ⊗[𝕜] E)] [CompleteSpace (G ⊗[𝕜] E)] [CompleteSpace F] [CompleteSpace H] (g : G →L[𝕜] H) : (g.rTensor E).adjoint = g.adjoint.rTensor E := by - apply ContinuousLinearMap.coe_inj.mp <| ext' ?_ - simp [TensorProduct.ext_iff_inner_right, ContinuousLinearMap.adjoint_inner_left] + apply coe_inj.mp <| ext' ?_ + simp [TensorProduct.ext_iff_inner_right, adjoint_inner_left] + +end ContinuousLinearMap + +namespace TensorProduct /-- `TensorProduct.map` as a continuous linear map, i.e. the continuous linear map `x ⊗ₜ[𝕜] y ↦ f(x) ⊗ₜ[𝕜] g(y)` formed from the continuous linear maps `f` and `g`. -/ noncomputable def mapL (f : E →L[𝕜] F) (g : G →L[𝕜] H) : (E ⊗[𝕜] G) →L[𝕜] (F ⊗[𝕜] H) := - ContinuousLinearMap.rTensor H f ∘L ContinuousLinearMap.lTensor E g + f.rTensor H ∘L g.lTensor E theorem norm_mapL_le (f : E →L[𝕜] F) (g : G →L[𝕜] H) : ‖mapL f g‖ ≤ ‖f‖ * ‖g‖ := by unfold mapL @@ -563,20 +572,20 @@ theorem adjoint_mapL [CompleteSpace E] [CompleteSpace G] [CompleteSpace (E ⊗[ apply ContinuousLinearMap.coe_inj.mp <| ext' ?_ simp [TensorProduct.ext_iff_inner_right, ContinuousLinearMap.adjoint_inner_left] +open LinearMap + @[simp] theorem adjoint_map [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] [FiniteDimensional 𝕜 G] [FiniteDimensional 𝕜 H] (f : E →ₗ[𝕜] F) (g : G →ₗ[𝕜] H) : - LinearMap.adjoint (map f g) = map (LinearMap.adjoint f) (LinearMap.adjoint g) := - ext' fun _ _ => by simp [TensorProduct.ext_iff_inner_right, LinearMap.adjoint_inner_left] - -open LinearMap + adjoint (map f g) = map (adjoint f) (adjoint g) := + ext' fun _ _ => by simp [TensorProduct.ext_iff_inner_right, adjoint_inner_left] @[simp] theorem _root_.LinearMap.adjoint_rTensor [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] [FiniteDimensional 𝕜 G] (f : E →ₗ[𝕜] F) : - adjoint (rTensor G f) = rTensor G f.adjoint := by simp [rTensor] + adjoint (f.rTensor G) = f.adjoint.rTensor G := by simp [rTensor] @[simp] theorem _root_.LinearMap.adjoint_lTensor [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] [FiniteDimensional 𝕜 G] (f : E →ₗ[𝕜] F) : - adjoint (lTensor G f) = lTensor G f.adjoint := by simp [lTensor] + adjoint (f.lTensor G) = f.adjoint.lTensor G := by simp [lTensor] /-- Given `x, y : E ⊗ (F ⊗ G)`, `x = y` iff `⟪x, a ⊗ₜ (b ⊗ₜ c)⟫ = ⟪y, a ⊗ₜ (b ⊗ₜ c)⟫` for all `a, b, c`. From 1c799e163caa4912d0211f4dd8d76d356a72f367 Mon Sep 17 00:00:00 2001 From: Heeringa Date: Thu, 4 Jun 2026 14:29:56 +0200 Subject: [PATCH 16/39] Revise simp decorations --- Mathlib/Analysis/InnerProductSpace/TensorProduct.lean | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean index e2ae2c1d58da11..faafa6e341ad1a 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -482,7 +482,6 @@ noncomputable def lTensor (g : G →L[𝕜] H) : (commIsometry 𝕜 E G).toContinuousLinearEquiv.toContinuousLinearMap variable (E) in -@[simp] lemma lTensor_def (g : G →L[𝕜] H) : g.lTensor E = (commIsometry 𝕜 H E) ∘L (g.rTensor E) ∘L (commIsometry 𝕜 E G).toContinuousLinearEquiv.toContinuousLinearMap := rfl @@ -500,17 +499,17 @@ theorem comm_comp_lTensor_comp_comm_eq (g : G →L[𝕜] H) : variable (G) in theorem comm_comp_rTensor_comp_comm_eq (f : E →L[𝕜] F) : commIsometry 𝕜 G F ∘L f.lTensor G ∘L commIsometry 𝕜 E G = f.rTensor G := - by ext; simp + by ext; simp [lTensor_def] variable (G) in theorem lTensor_comp_comm (f : E →L[𝕜] F) : f.lTensor G ∘L commIsometry 𝕜 E G = commIsometry 𝕜 F G ∘L f.rTensor G := - by ext; simp + by ext; simp [lTensor_def] variable (E) in theorem rTensor_comp_comm (g : G →L[𝕜] H) : g.rTensor E ∘L commIsometry 𝕜 E G = commIsometry 𝕜 E H ∘L g.lTensor E := - by ext; simp + by ext; simp [lTensor_def] lemma lTensor_apply (g : G →L[𝕜] H) (x : E ⊗ G) : g.lTensor E x = (map LinearMap.id g.toLinearMap) x := by @@ -521,6 +520,7 @@ lemma lTensor_apply (g : G →L[𝕜] H) (x : E ⊗ G) : exact LinearMap.congr_fun (LinearMap.comm_comp_rTensor_comp_comm_eq g.toLinearMap (Q:=E)) x variable (E) in +@[simp] lemma toLinearMap_lTensor (g : G →L[𝕜] H) : (g.lTensor E).toLinearMap = g.toLinearMap.lTensor E := by ext; simp @@ -566,6 +566,7 @@ lemma mapL_tmul (f : E →L[𝕜] F) (g : G →L[𝕜] H) (m : E) (n : G) : lemma toLinearMap_mapL (f : E →L[𝕜] F) (g : G →L[𝕜] H) : (mapL f g).toLinearMap = map f g := by ext; simp +@[simp] theorem adjoint_mapL [CompleteSpace E] [CompleteSpace G] [CompleteSpace (E ⊗[𝕜] G)] [CompleteSpace F] [CompleteSpace H] [CompleteSpace (F ⊗[𝕜] H)] (f : E →L[𝕜] F) (g : G →L[𝕜] H) : (mapL f g).adjoint = mapL f.adjoint g.adjoint := by From 54582f2a58582c452f1206384c087600b1da5ca3 Mon Sep 17 00:00:00 2001 From: Heeringa Date: Thu, 4 Jun 2026 14:57:39 +0200 Subject: [PATCH 17/39] Add Tensor_eq_mapL, shorten adjoint_tensor --- .../InnerProductSpace/TensorProduct.lean | 45 +++++++++++-------- 1 file changed, 27 insertions(+), 18 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean index faafa6e341ad1a..ced7192ad49144 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -464,15 +464,6 @@ theorem rTensor_norm_le (f : E →L[𝕜] F) : ‖f.rTensor G‖ ≤ ‖f‖ := by apply LinearMap.mkContinuous_norm_le _ (norm_nonneg _) _ -variable (G) in -omit [InnerProductSpace 𝕜 H] in -theorem adjoint_rTensor [CompleteSpace E] [CompleteSpace G] - [CompleteSpace (E ⊗[𝕜] G)] [CompleteSpace (F ⊗[𝕜] G)] [CompleteSpace F] [CompleteSpace H] - (f : E →L[𝕜] F) : - (f.rTensor G).adjoint = f.adjoint.rTensor G := by - apply coe_inj.mp <| ext' ?_ - simp [TensorProduct.ext_iff_inner_right, adjoint_inner_left] - variable (E) in /-- `LinearMap.lTensor` as a continuous linear map, i.e. the continuous linear map `g` extended to the map `x ⊗ₜ[𝕜] y ↦ x ⊗ₜ[𝕜] g(y)`. -/ @@ -535,15 +526,6 @@ theorem lTensor_norm_le (g : G →L[𝕜] H) : (commIsometry 𝕜 H E).toLinearIsometry.norm_toContinuousLinearMap_le] simp -variable (E) in -omit [InnerProductSpace 𝕜 F] in -theorem adjoint_lTensor [CompleteSpace E] [CompleteSpace G] - [CompleteSpace (H ⊗[𝕜] E)] [CompleteSpace (G ⊗[𝕜] E)] [CompleteSpace F] [CompleteSpace H] - (g : G →L[𝕜] H) : - (g.rTensor E).adjoint = g.adjoint.rTensor E := by - apply coe_inj.mp <| ext' ?_ - simp [TensorProduct.ext_iff_inner_right, adjoint_inner_left] - end ContinuousLinearMap namespace TensorProduct @@ -558,14 +540,25 @@ theorem norm_mapL_le (f : E →L[𝕜] F) (g : G →L[𝕜] H) : ‖mapL f g‖ grw [ContinuousLinearMap.opNorm_comp_le, ContinuousLinearMap.rTensor_norm_le, ContinuousLinearMap.lTensor_norm_le] +lemma mapL_def (f : E →L[𝕜] F) (g : G →L[𝕜] H) : mapL f g = f.rTensor H ∘L g.lTensor E := rfl + @[simp] lemma mapL_tmul (f : E →L[𝕜] F) (g : G →L[𝕜] H) (m : E) (n : G) : mapL f g (m ⊗ₜ n) = f m ⊗ₜ g n := rfl +@[simp] lemma toLinearMap_mapL (f : E →L[𝕜] F) (g : G →L[𝕜] H) : (mapL f g).toLinearMap = map f g := by ext; simp +variable (G) in +theorem rTensor_eq_mapL (f : E →L[𝕜] F) : f.rTensor G = mapL f (ContinuousLinearMap.id 𝕜 G) := by + ext; simp [mapL_def, ContinuousLinearMap.lTensor_def] + +variable (E) in +theorem lTensor_eq_mapL (g : G →L[𝕜] H) : g.lTensor E = mapL (ContinuousLinearMap.id 𝕜 E) g := by + ext; simp [mapL_def, ContinuousLinearMap.lTensor_def] + @[simp] theorem adjoint_mapL [CompleteSpace E] [CompleteSpace G] [CompleteSpace (E ⊗[𝕜] G)] [CompleteSpace F] [CompleteSpace H] [CompleteSpace (F ⊗[𝕜] H)] @@ -573,6 +566,22 @@ theorem adjoint_mapL [CompleteSpace E] [CompleteSpace G] [CompleteSpace (E ⊗[ apply ContinuousLinearMap.coe_inj.mp <| ext' ?_ simp [TensorProduct.ext_iff_inner_right, ContinuousLinearMap.adjoint_inner_left] +variable (G) in +omit [InnerProductSpace 𝕜 H] in +theorem adjoint_rTensor [CompleteSpace E] [CompleteSpace G] + [CompleteSpace (E ⊗[𝕜] G)] [CompleteSpace (F ⊗[𝕜] G)] [CompleteSpace F] [CompleteSpace H] + (f : E →L[𝕜] F) : + (f.rTensor G).adjoint = f.adjoint.rTensor G := by + simp [rTensor_eq_mapL] + +variable (E) in +omit [InnerProductSpace 𝕜 F] in +theorem adjoint_lTensor [CompleteSpace E] [CompleteSpace G] + [CompleteSpace (E ⊗[𝕜] H)] [CompleteSpace (E ⊗[𝕜] G)] [CompleteSpace F] [CompleteSpace H] + (g : G →L[𝕜] H) : + (g.lTensor E).adjoint = g.adjoint.lTensor E := by + simp [lTensor_eq_mapL] + open LinearMap @[simp] theorem adjoint_map [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] [FiniteDimensional 𝕜 G] From c03238c87651cdae6bed7ed75e8671ecd5da71b6 Mon Sep 17 00:00:00 2001 From: TJHeeringa Date: Sun, 7 Jun 2026 16:41:28 +0200 Subject: [PATCH 18/39] Remove redundant types --- .../Analysis/InnerProductSpace/TensorProduct.lean | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean index ced7192ad49144..311faf3dade1b2 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -567,18 +567,14 @@ theorem adjoint_mapL [CompleteSpace E] [CompleteSpace G] [CompleteSpace (E ⊗[ simp [TensorProduct.ext_iff_inner_right, ContinuousLinearMap.adjoint_inner_left] variable (G) in -omit [InnerProductSpace 𝕜 H] in -theorem adjoint_rTensor [CompleteSpace E] [CompleteSpace G] - [CompleteSpace (E ⊗[𝕜] G)] [CompleteSpace (F ⊗[𝕜] G)] [CompleteSpace F] [CompleteSpace H] - (f : E →L[𝕜] F) : +theorem adjoint_rTensor [CompleteSpace E] [CompleteSpace G] [CompleteSpace (E ⊗[𝕜] G)] + [CompleteSpace (F ⊗[𝕜] G)] [CompleteSpace F] (f : E →L[𝕜] F) : (f.rTensor G).adjoint = f.adjoint.rTensor G := by simp [rTensor_eq_mapL] variable (E) in -omit [InnerProductSpace 𝕜 F] in -theorem adjoint_lTensor [CompleteSpace E] [CompleteSpace G] - [CompleteSpace (E ⊗[𝕜] H)] [CompleteSpace (E ⊗[𝕜] G)] [CompleteSpace F] [CompleteSpace H] - (g : G →L[𝕜] H) : +theorem adjoint_lTensor [CompleteSpace E] [CompleteSpace G] [CompleteSpace (E ⊗[𝕜] H)] + [CompleteSpace (E ⊗[𝕜] G)] [CompleteSpace H] (g : G →L[𝕜] H) : (g.lTensor E).adjoint = g.adjoint.lTensor E := by simp [lTensor_eq_mapL] From a33fa56e8ce77d357649559c49d04bcdee05fe50 Mon Sep 17 00:00:00 2001 From: TJHeeringa Date: Sun, 7 Jun 2026 16:47:03 +0200 Subject: [PATCH 19/39] Update rTensor_apply --- Mathlib/Analysis/InnerProductSpace/TensorProduct.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean index 311faf3dade1b2..f20b5ee948e2a1 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -449,7 +449,7 @@ noncomputable def rTensor (f : E →L[𝕜] F) : @[simp] lemma rTensor_apply (f : E →L[𝕜] F) (x : E ⊗ G) : - f.rTensor G x = (map f.toLinearMap LinearMap.id) x := rfl + f.rTensor G x = f.toLinearMap.rTensor G x := rfl lemma rTensor_tmul (f : E →L[𝕜] F) (m : E) (n : G) : f.rTensor G (m ⊗ₜ n) = f m ⊗ₜ n := rfl @@ -507,7 +507,7 @@ lemma lTensor_apply (g : G →L[𝕜] H) (x : E ⊗ G) : simp only [lTensor_def, coe_comp', ContinuousLinearEquiv.coe_coe, LinearIsometryEquiv.coe_toContinuousLinearEquiv, Function.comp_apply, commIsometry_apply, rTensor_apply] - simp_rw [← LinearMap.lTensor_def, ← LinearMap.rTensor_def] + simp_rw [← LinearMap.lTensor_def] exact LinearMap.congr_fun (LinearMap.comm_comp_rTensor_comp_comm_eq g.toLinearMap (Q:=E)) x variable (E) in From 3d744d1651159909d6267699f7fa986029235036 Mon Sep 17 00:00:00 2001 From: TJHeeringa Date: Sun, 7 Jun 2026 17:02:50 +0200 Subject: [PATCH 20/39] Resolve CoAlgebra ambiquities --- .../Analysis/InnerProductSpace/Coalgebra.lean | 45 ++++++++++--------- 1 file changed, 24 insertions(+), 21 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Coalgebra.lean b/Mathlib/Analysis/InnerProductSpace/Coalgebra.lean index a4e67bc0f020af..248600985c38fb 100644 --- a/Mathlib/Analysis/InnerProductSpace/Coalgebra.lean +++ b/Mathlib/Analysis/InnerProductSpace/Coalgebra.lean @@ -73,18 +73,20 @@ noncomputable abbrev coalgebraOfAlgebra (e : E ≃ₗ[𝕜] A) : Coalgebra 𝕜 comul := adjoint (e.symm.toLinearMap ∘ₗ mul' 𝕜 A ∘ₗ map e.toLinearMap e.toLinearMap) counit := innerₛₗ 𝕜 (e.symm 1) coassoc := by - rw [← adjoint_lTensor, ← adjoint_rTensor, ← toLinearEquiv_assocIsometry, + rw [← LinearMap.adjoint_lTensor, ← LinearMap.adjoint_rTensor, ← toLinearEquiv_assocIsometry, ← (assocIsometry 𝕜 _ _ _).symm_symm, ← adjoint_toLinearMap_eq_symm] simp_rw [← adjoint_comp] congr 1; ext; simp [mul_assoc] rTensor_counit_comp_comul := by - rw [← adjoint_toSpanSingleton, ← adjoint_rTensor, ← adjoint_comp, ← toLinearMap_symm_lid, - ← toLinearEquiv_lidIsometry, ← toLinearEquiv_symm, ← adjoint_toLinearMap_eq_symm] + rw [← adjoint_toSpanSingleton, ← LinearMap.adjoint_rTensor, ← adjoint_comp, + ← toLinearMap_symm_lid, ← toLinearEquiv_lidIsometry, ← toLinearEquiv_symm, + ← adjoint_toLinearMap_eq_symm] congr 1; ext; simp lTensor_counit_comp_comul := by - rw [← adjoint_toSpanSingleton, ← adjoint_lTensor, ← adjoint_comp, ← toLinearMap_symm_rid, - ← comm_trans_lid, ← toLinearEquiv_commIsometry, ← toLinearEquiv_lidIsometry, - ← toLinearEquiv_trans, ← toLinearEquiv_symm, ← adjoint_toLinearMap_eq_symm] + rw [← adjoint_toSpanSingleton, ← LinearMap.adjoint_lTensor, ← adjoint_comp, + ← toLinearMap_symm_rid, ← comm_trans_lid, ← toLinearEquiv_commIsometry, + ← toLinearEquiv_lidIsometry, ← toLinearEquiv_trans, ← toLinearEquiv_symm, + ← adjoint_toLinearMap_eq_symm] congr 1; ext; simp end coalgebraOfAlgebra @@ -118,24 +120,24 @@ noncomputable abbrev ringOfCoalgebra : zero_mul x := by simp mul_zero x := by simp mul_assoc x y z := by - simp_rw [AlgebraOfCoalgebra.mul_def, ← rTensor_tmul, ← comp_apply, ← adjoint_rTensor, - ← adjoint_comp, ← coassoc_symm, adjoint_comp, adjoint_lTensor, comp_apply, + simp_rw [AlgebraOfCoalgebra.mul_def, ← rTensor_tmul, ← comp_apply, ← LinearMap.adjoint_rTensor, + ← adjoint_comp, ← coassoc_symm, adjoint_comp, LinearMap.adjoint_lTensor, comp_apply, ← toLinearEquiv_assocIsometry, ← toLinearEquiv_symm, adjoint_toLinearMap_eq_symm] simp only [symm_symm, toLinearEquiv_assocIsometry, LinearEquiv.coe_coe, assoc_tmul, lTensor_tmul] one := adjoint (counit (R := 𝕜) (A := E)) 1 one_mul x := by dsimp [OfNat.ofNat] - rw [← rTensor_tmul, ← comp_apply, ← adjoint_rTensor, ← adjoint_comp, rTensor_counit_comp_comul, - ← toLinearMap_symm_lid, ← toLinearEquiv_lidIsometry, ← toLinearEquiv_symm, - adjoint_toLinearMap_eq_symm] + rw [← rTensor_tmul, ← comp_apply, ← LinearMap.adjoint_rTensor, ← adjoint_comp, + rTensor_counit_comp_comul, ← toLinearMap_symm_lid, ← toLinearEquiv_lidIsometry, + ← toLinearEquiv_symm, adjoint_toLinearMap_eq_symm] exact one_smul _ _ mul_one x := by dsimp [OfNat.ofNat] - rw [← lTensor_tmul, ← comp_apply, ← adjoint_lTensor, ← adjoint_comp, lTensor_counit_comp_comul, - ← toLinearMap_symm_rid, ← comm_trans_lid, ← toLinearEquiv_commIsometry, - ← toLinearEquiv_lidIsometry, ← toLinearEquiv_trans, ← toLinearEquiv_symm, - adjoint_toLinearMap_eq_symm] + rw [← lTensor_tmul, ← comp_apply, ← LinearMap.adjoint_lTensor, ← adjoint_comp, + lTensor_counit_comp_comul, ← toLinearMap_symm_rid, ← comm_trans_lid, + ← toLinearEquiv_commIsometry, ← toLinearEquiv_lidIsometry, ← toLinearEquiv_trans, + ← toLinearEquiv_symm, adjoint_toLinearMap_eq_symm] exact one_smul _ _ attribute [local instance] InnerProductSpace.ringOfCoalgebra in @@ -153,22 +155,23 @@ noncomputable abbrev algebraOfCoalgebra : Algebra 𝕜 E where ← adjoint_comp, ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, adjoint_comp, ← toLinearMap_symm_lid, ← toLinearEquiv_lidIsometry, ← toLinearEquiv_symm, adjoint_toLinearMap_eq_symm] - simp only [LinearIsometryEquiv.symm_symm, toLinearEquiv_lidIsometry, adjoint_lTensor, - coe_comp, LinearEquiv.coe_coe, Function.comp_apply, lTensor_tmul, lid_tmul] + simp only [LinearIsometryEquiv.symm_symm, toLinearEquiv_lidIsometry, + LinearMap.adjoint_lTensor, coe_comp, LinearEquiv.coe_coe, Function.comp_apply, + lTensor_tmul, lid_tmul] rw [← smul_eq_mul, ← _root_.map_smul] map_zero' := map_zero _ map_add' := map_add _ } commutes' r x := by dsimp - simp_rw [← rTensor_tmul, ← lTensor_tmul, ← adjoint_lTensor, ← adjoint_rTensor, - ← comp_apply, ← adjoint_comp, rTensor_counit_comp_comul, lTensor_counit_comp_comul, - ← toLinearMap_symm_rid, ← toLinearMap_symm_lid, ← comm_trans_lid, + simp_rw [← rTensor_tmul, ← lTensor_tmul, ← LinearMap.adjoint_lTensor, + ← LinearMap.adjoint_rTensor, ← comp_apply, ← adjoint_comp, rTensor_counit_comp_comul, + lTensor_counit_comp_comul, ← toLinearMap_symm_rid, ← toLinearMap_symm_lid, ← comm_trans_lid, ← toLinearEquiv_commIsometry, ← toLinearEquiv_lidIsometry, ← toLinearEquiv_trans, ← toLinearEquiv_symm, adjoint_toLinearMap_eq_symm] simp smul_def' r x := by dsimp - simp_rw [← rTensor_tmul, ← adjoint_rTensor, ← comp_apply, ← adjoint_comp, + simp_rw [← rTensor_tmul, ← LinearMap.adjoint_rTensor, ← comp_apply, ← adjoint_comp, rTensor_counit_comp_comul, ← toLinearMap_symm_lid, ← toLinearEquiv_lidIsometry, ← toLinearEquiv_symm, adjoint_toLinearMap_eq_symm] simp From 2b2a03afd09eb044ec1ee8cbf084c5267077ed4e Mon Sep 17 00:00:00 2001 From: Monica Omar <23701951+themathqueen@users.noreply.github.com> Date: Sun, 7 Jun 2026 16:30:02 +0100 Subject: [PATCH 21/39] some cleanup and easy lemmas, feel free to revert anything you don't like --- .../InnerProductSpace/TensorProduct.lean | 139 ++++++++---------- 1 file changed, 63 insertions(+), 76 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean index f20b5ee948e2a1..7f8984a93d76b7 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -423,9 +423,8 @@ open TensorProduct variable (G) in /-- `LinearMap.rTensor` as a continuous linear map, i.e. the continuous linear map `f` extended to the map `x ⊗ₜ[𝕜] y ↦ f(x) ⊗ₜ[𝕜] y`. -/ -noncomputable def rTensor (f : E →L[𝕜] F) : - (E ⊗[𝕜] G) →L[𝕜] (F ⊗[𝕜] G) := - (f.toLinearMap.rTensor G).mkContinuous ‖f‖ (fun x => by +noncomputable def rTensor (f : E →L[𝕜] F) : (E ⊗[𝕜] G) →L[𝕜] (F ⊗[𝕜] G) := + (f.toLinearMap.rTensor G).mkContinuous ‖f‖ fun x ↦ by obtain ⟨n, e, g, hx ⟩ := exists_sum_tmul_eq x obtain ⟨c, hc_supp, hc⟩ := Submodule.mem_span_set.mp ((span_tmul_eq_top 𝕜 E G) ▸ Submodule.mem_top (x := x)) @@ -438,49 +437,42 @@ noncomputable def rTensor (f : E →L[𝕜] F) : inner_sum, sum_inner, inner_tmul, ← hA, sub_mul, Finset.sum_sub_distrib, map_sub, ← RCLike.smul_re, Finset.smul_sum, smul_mul_assoc, sub_le_self_iff, Matrix.sum_apply, mul_comm, Finset.mul_sum] - rw [Finset.sum_comm_cycle] - simp_rw [Matrix.vecMulVec, Matrix.of_apply, Pi.star_apply, ← mul_left_comm, ← mul_assoc] - simp_rw (config := { singlePass := true }) [← starRingEnd_self_apply (A _ _)] - simp_rw [← inner_smul_left, mul_comm (inner 𝕜 _ _) _, ← starRingEnd_apply, ← inner_smul_right, - starRingEnd_self_apply, ← sum_inner, ← inner_sum, map_sum, - ← InnerProductSpace.norm_sq_eq_re_inner] - exact Finset.sum_nonneg (fun x _ => by simp) - ) + simp_rw +singlePass [Finset.sum_comm_cycle, Matrix.vecMulVec, Matrix.of_apply, Pi.star_apply, + ← mul_left_comm, ← mul_assoc, ← starRingEnd_self_apply (A _ _), ← inner_smul_left] + simp [mul_comm, ← inner_smul_right, ← sum_inner, ← inner_sum, Finset.sum_nonneg] -@[simp] -lemma rTensor_apply (f : E →L[𝕜] F) (x : E ⊗ G) : +@[simp] lemma rTensor_apply (f : E →L[𝕜] F) (x : E ⊗ G) : f.rTensor G x = f.toLinearMap.rTensor G x := rfl -lemma rTensor_tmul (f : E →L[𝕜] F) (m : E) (n : G) : - f.rTensor G (m ⊗ₜ n) = f m ⊗ₜ n := rfl +lemma rTensor_tmul (f : E →L[𝕜] F) (m : E) (n : G) : f.rTensor G (m ⊗ₜ n) = f m ⊗ₜ n := rfl variable (G) in -@[simp] -lemma toLinearMap_rTensor (f : E →L[𝕜] F) : +@[simp] lemma toLinearMap_rTensor (f : E →L[𝕜] F) : (f.rTensor G).toLinearMap = f.toLinearMap.rTensor G := rfl variable (G) in -theorem rTensor_norm_le (f : E →L[𝕜] F) : - ‖f.rTensor G‖ ≤ ‖f‖ := by - apply LinearMap.mkContinuous_norm_le _ (norm_nonneg _) _ +theorem rTensor_norm_le (f : E →L[𝕜] F) : ‖f.rTensor G‖ ≤ ‖f‖ := + LinearMap.mkContinuous_norm_le _ (norm_nonneg _) _ + +@[simp] lemma rTensor_id : (.id 𝕜 E : E →L[𝕜] E).rTensor G = .id 𝕜 _ := by ext; simp +@[simp] lemma rTensor_zero : (0 : E →L[𝕜] G).rTensor H = 0 := by ext; simp variable (E) in /-- `LinearMap.lTensor` as a continuous linear map, i.e. the continuous linear map `g` extended to the map `x ⊗ₜ[𝕜] y ↦ x ⊗ₜ[𝕜] g(y)`. -/ -noncomputable def lTensor (g : G →L[𝕜] H) : - (E ⊗[𝕜] G) →L[𝕜] (E ⊗[𝕜] H) := - (commIsometry 𝕜 H E) ∘L (g.rTensor E) ∘L - (commIsometry 𝕜 E G).toContinuousLinearEquiv.toContinuousLinearMap +noncomputable def lTensor (g : G →L[𝕜] H) : (E ⊗[𝕜] G) →L[𝕜] (E ⊗[𝕜] H) := + commIsometry 𝕜 H E ∘L g.rTensor E ∘L commIsometry 𝕜 E G variable (E) in lemma lTensor_def (g : G →L[𝕜] H) : - g.lTensor E = (commIsometry 𝕜 H E) ∘L (g.rTensor E) ∘L - (commIsometry 𝕜 E G).toContinuousLinearEquiv.toContinuousLinearMap := rfl + g.lTensor E = commIsometry 𝕜 H E ∘L g.rTensor E ∘L commIsometry 𝕜 E G := rfl + +@[simp] lemma lTensor_apply (g : G →L[𝕜] H) (x : E ⊗ G) : + g.lTensor E x = g.toLinearMap.lTensor E x := by + simp [lTensor_def, ← LinearMap.comm_comp_rTensor_comp_comm_eq] variable (E) in -@[simp] -lemma lTensor_tmul (g : G →L[𝕜] H) (m : E) (n : G) : - g.lTensor E (m ⊗ₜ n) = m ⊗ₜ g n := rfl +lemma lTensor_tmul (g : G →L[𝕜] H) (m : E) (n : G) : g.lTensor E (m ⊗ₜ n) = m ⊗ₜ g n := rfl variable (E) in theorem comm_comp_lTensor_comp_comm_eq (g : G →L[𝕜] H) : @@ -489,42 +481,32 @@ theorem comm_comp_lTensor_comp_comm_eq (g : G →L[𝕜] H) : variable (G) in theorem comm_comp_rTensor_comp_comm_eq (f : E →L[𝕜] F) : - commIsometry 𝕜 G F ∘L f.lTensor G ∘L commIsometry 𝕜 E G = f.rTensor G := - by ext; simp [lTensor_def] + commIsometry 𝕜 G F ∘L f.lTensor G ∘L commIsometry 𝕜 E G = f.rTensor G := by + ext; simp [lTensor_def] variable (G) in theorem lTensor_comp_comm (f : E →L[𝕜] F) : - f.lTensor G ∘L commIsometry 𝕜 E G = commIsometry 𝕜 F G ∘L f.rTensor G := - by ext; simp [lTensor_def] + f.lTensor G ∘L commIsometry 𝕜 E G = commIsometry 𝕜 F G ∘L f.rTensor G := by + ext; simp [lTensor_def] variable (E) in theorem rTensor_comp_comm (g : G →L[𝕜] H) : - g.rTensor E ∘L commIsometry 𝕜 E G = commIsometry 𝕜 E H ∘L g.lTensor E := - by ext; simp [lTensor_def] - -lemma lTensor_apply (g : G →L[𝕜] H) (x : E ⊗ G) : - g.lTensor E x = (map LinearMap.id g.toLinearMap) x := by - simp only [lTensor_def, coe_comp', ContinuousLinearEquiv.coe_coe, - LinearIsometryEquiv.coe_toContinuousLinearEquiv, Function.comp_apply, commIsometry_apply, - rTensor_apply] - simp_rw [← LinearMap.lTensor_def] - exact LinearMap.congr_fun (LinearMap.comm_comp_rTensor_comp_comm_eq g.toLinearMap (Q:=E)) x + g.rTensor E ∘L commIsometry 𝕜 E G = commIsometry 𝕜 E H ∘L g.lTensor E := by + ext; simp [lTensor_def] variable (E) in -@[simp] -lemma toLinearMap_lTensor (g : G →L[𝕜] H) : - (g.lTensor E).toLinearMap = g.toLinearMap.lTensor E := by - ext; simp +@[simp] lemma toLinearMap_lTensor (g : G →L[𝕜] H) : + (g.lTensor E).toLinearMap = g.toLinearMap.lTensor E := by ext; simp variable (E) in -theorem lTensor_norm_le (g : G →L[𝕜] H) : - ‖g.lTensor E‖ ≤ ‖g‖ := by - unfold lTensor - simp_rw [← LinearIsometryEquiv.toContinuousLinearMap_toLinearIsometry] +theorem lTensor_norm_le (g : G →L[𝕜] H) : ‖g.lTensor E‖ ≤ ‖g‖ := by + simp_rw [lTensor_def, ← LinearIsometryEquiv.toContinuousLinearMap_toLinearIsometry] grw [opNorm_comp_le, opNorm_comp_le, rTensor_norm_le, (commIsometry 𝕜 E G).toLinearIsometry.norm_toContinuousLinearMap_le, - (commIsometry 𝕜 H E).toLinearIsometry.norm_toContinuousLinearMap_le] - simp + (commIsometry 𝕜 H E).toLinearIsometry.norm_toContinuousLinearMap_le, mul_one, one_mul] + +@[simp] lemma lTensor_id : (.id 𝕜 E : E →L[𝕜] E).lTensor G = .id 𝕜 _ := by ext; simp +@[simp] lemma lTensor_zero : (0 : E →L[𝕜] G).lTensor H = 0 := by ext; simp end ContinuousLinearMap @@ -535,48 +517,53 @@ namespace TensorProduct noncomputable def mapL (f : E →L[𝕜] F) (g : G →L[𝕜] H) : (E ⊗[𝕜] G) →L[𝕜] (F ⊗[𝕜] H) := f.rTensor H ∘L g.lTensor E +lemma mapL_def (f : E →L[𝕜] F) (g : G →L[𝕜] H) : mapL f g = f.rTensor H ∘L g.lTensor E := rfl + theorem norm_mapL_le (f : E →L[𝕜] F) (g : G →L[𝕜] H) : ‖mapL f g‖ ≤ ‖f‖ * ‖g‖ := by - unfold mapL - grw [ContinuousLinearMap.opNorm_comp_le, ContinuousLinearMap.rTensor_norm_le, + grw [mapL_def, ContinuousLinearMap.opNorm_comp_le, ContinuousLinearMap.rTensor_norm_le, ContinuousLinearMap.lTensor_norm_le] -lemma mapL_def (f : E →L[𝕜] F) (g : G →L[𝕜] H) : mapL f g = f.rTensor H ∘L g.lTensor E := rfl +@[simp] lemma mapL_apply (f : E →L[𝕜] F) (g : G →L[𝕜] H) (x) : + mapL f g x = map f.toLinearMap g.toLinearMap x := by + simp [mapL_def, ← LinearMap.rTensor_comp_lTensor] -@[simp] lemma mapL_tmul (f : E →L[𝕜] F) (g : G →L[𝕜] H) (m : E) (n : G) : - mapL f g (m ⊗ₜ n) = f m ⊗ₜ g n := - rfl + mapL f g (m ⊗ₜ n) = f m ⊗ₜ g n := rfl -@[simp] -lemma toLinearMap_mapL (f : E →L[𝕜] F) (g : G →L[𝕜] H) : (mapL f g).toLinearMap = map f g := by - ext; simp +@[simp] lemma mapL_zero_left (f : E →L[𝕜] F) : mapL (0 : G →L[𝕜] H) f = 0 := by simp [mapL_def] +@[simp] lemma mapL_zero_right (f : E →L[𝕜] F) : mapL f (0 : G →L[𝕜] H) = 0 := by simp [mapL_def] +@[simp] lemma mapL_id_id : mapL (.id 𝕜 E) (.id 𝕜 G) = .id 𝕜 _ := by simp [mapL_def] + +@[simp] lemma toLinearMap_mapL (f : E →L[𝕜] F) (g : G →L[𝕜] H) : + (mapL f g).toLinearMap = map f g := by ext; simp variable (G) in -theorem rTensor_eq_mapL (f : E →L[𝕜] F) : f.rTensor G = mapL f (ContinuousLinearMap.id 𝕜 G) := by - ext; simp [mapL_def, ContinuousLinearMap.lTensor_def] +theorem rTensor_eq_mapL (f : E →L[𝕜] F) : f.rTensor G = mapL f (.id 𝕜 G) := by simp [mapL_def] variable (E) in -theorem lTensor_eq_mapL (g : G →L[𝕜] H) : g.lTensor E = mapL (ContinuousLinearMap.id 𝕜 E) g := by - ext; simp [mapL_def, ContinuousLinearMap.lTensor_def] +theorem lTensor_eq_mapL (g : G →L[𝕜] H) : g.lTensor E = mapL (.id 𝕜 E) g := by simp [mapL_def] -@[simp] -theorem adjoint_mapL [CompleteSpace E] [CompleteSpace G] [CompleteSpace (E ⊗[𝕜] G)] +lemma lTensor_comp_rTensor (f : E →L[𝕜] F) (g : G →L[𝕜] H) : + f.lTensor H ∘L g.rTensor E = mapL g f := by ext; simp [← LinearMap.lTensor_comp_rTensor] + +lemma rTensor_comp_lTensor (f : E →L[𝕜] F) (g : G →L[𝕜] H) : + f.rTensor H ∘L g.lTensor E = mapL f g := mapL_def _ _ |>.symm + +@[simp] theorem adjoint_mapL [CompleteSpace E] [CompleteSpace G] [CompleteSpace (E ⊗[𝕜] G)] [CompleteSpace F] [CompleteSpace H] [CompleteSpace (F ⊗[𝕜] H)] (f : E →L[𝕜] F) (g : G →L[𝕜] H) : (mapL f g).adjoint = mapL f.adjoint g.adjoint := by apply ContinuousLinearMap.coe_inj.mp <| ext' ?_ simp [TensorProduct.ext_iff_inner_right, ContinuousLinearMap.adjoint_inner_left] variable (G) in -theorem adjoint_rTensor [CompleteSpace E] [CompleteSpace G] [CompleteSpace (E ⊗[𝕜] G)] +@[simp] theorem adjoint_rTensor [CompleteSpace E] [CompleteSpace G] [CompleteSpace (E ⊗[𝕜] G)] [CompleteSpace (F ⊗[𝕜] G)] [CompleteSpace F] (f : E →L[𝕜] F) : - (f.rTensor G).adjoint = f.adjoint.rTensor G := by - simp [rTensor_eq_mapL] + (f.rTensor G).adjoint = f.adjoint.rTensor G := by simp [rTensor_eq_mapL] variable (E) in -theorem adjoint_lTensor [CompleteSpace E] [CompleteSpace G] [CompleteSpace (E ⊗[𝕜] H)] +@[simp] theorem adjoint_lTensor [CompleteSpace E] [CompleteSpace G] [CompleteSpace (E ⊗[𝕜] H)] [CompleteSpace (E ⊗[𝕜] G)] [CompleteSpace H] (g : G →L[𝕜] H) : - (g.lTensor E).adjoint = g.adjoint.lTensor E := by - simp [lTensor_eq_mapL] + (g.lTensor E).adjoint = g.adjoint.lTensor E := by simp [lTensor_eq_mapL] open LinearMap @@ -587,11 +574,11 @@ open LinearMap @[simp] theorem _root_.LinearMap.adjoint_rTensor [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] [FiniteDimensional 𝕜 G] (f : E →ₗ[𝕜] F) : - adjoint (f.rTensor G) = f.adjoint.rTensor G := by simp [rTensor] + adjoint (f.rTensor G) = f.adjoint.rTensor G := by simp [rTensor] @[simp] theorem _root_.LinearMap.adjoint_lTensor [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] [FiniteDimensional 𝕜 G] (f : E →ₗ[𝕜] F) : - adjoint (f.lTensor G) = f.adjoint.lTensor G := by simp [lTensor] + adjoint (f.lTensor G) = f.adjoint.lTensor G := by simp [lTensor] /-- Given `x, y : E ⊗ (F ⊗ G)`, `x = y` iff `⟪x, a ⊗ₜ (b ⊗ₜ c)⟫ = ⟪y, a ⊗ₜ (b ⊗ₜ c)⟫` for all `a, b, c`. From dc9cb1644306626f3d660756bd1343c7b5c3b45a Mon Sep 17 00:00:00 2001 From: Monica Omar <23701951+themathqueen@users.noreply.github.com> Date: Sun, 7 Jun 2026 16:35:48 +0100 Subject: [PATCH 22/39] fix names and revert coalgebra file --- .../Analysis/InnerProductSpace/Coalgebra.lean | 45 +++++++++---------- .../InnerProductSpace/TensorProduct.lean | 22 ++++----- 2 files changed, 33 insertions(+), 34 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Coalgebra.lean b/Mathlib/Analysis/InnerProductSpace/Coalgebra.lean index 248600985c38fb..a4e67bc0f020af 100644 --- a/Mathlib/Analysis/InnerProductSpace/Coalgebra.lean +++ b/Mathlib/Analysis/InnerProductSpace/Coalgebra.lean @@ -73,20 +73,18 @@ noncomputable abbrev coalgebraOfAlgebra (e : E ≃ₗ[𝕜] A) : Coalgebra 𝕜 comul := adjoint (e.symm.toLinearMap ∘ₗ mul' 𝕜 A ∘ₗ map e.toLinearMap e.toLinearMap) counit := innerₛₗ 𝕜 (e.symm 1) coassoc := by - rw [← LinearMap.adjoint_lTensor, ← LinearMap.adjoint_rTensor, ← toLinearEquiv_assocIsometry, + rw [← adjoint_lTensor, ← adjoint_rTensor, ← toLinearEquiv_assocIsometry, ← (assocIsometry 𝕜 _ _ _).symm_symm, ← adjoint_toLinearMap_eq_symm] simp_rw [← adjoint_comp] congr 1; ext; simp [mul_assoc] rTensor_counit_comp_comul := by - rw [← adjoint_toSpanSingleton, ← LinearMap.adjoint_rTensor, ← adjoint_comp, - ← toLinearMap_symm_lid, ← toLinearEquiv_lidIsometry, ← toLinearEquiv_symm, - ← adjoint_toLinearMap_eq_symm] + rw [← adjoint_toSpanSingleton, ← adjoint_rTensor, ← adjoint_comp, ← toLinearMap_symm_lid, + ← toLinearEquiv_lidIsometry, ← toLinearEquiv_symm, ← adjoint_toLinearMap_eq_symm] congr 1; ext; simp lTensor_counit_comp_comul := by - rw [← adjoint_toSpanSingleton, ← LinearMap.adjoint_lTensor, ← adjoint_comp, - ← toLinearMap_symm_rid, ← comm_trans_lid, ← toLinearEquiv_commIsometry, - ← toLinearEquiv_lidIsometry, ← toLinearEquiv_trans, ← toLinearEquiv_symm, - ← adjoint_toLinearMap_eq_symm] + rw [← adjoint_toSpanSingleton, ← adjoint_lTensor, ← adjoint_comp, ← toLinearMap_symm_rid, + ← comm_trans_lid, ← toLinearEquiv_commIsometry, ← toLinearEquiv_lidIsometry, + ← toLinearEquiv_trans, ← toLinearEquiv_symm, ← adjoint_toLinearMap_eq_symm] congr 1; ext; simp end coalgebraOfAlgebra @@ -120,24 +118,24 @@ noncomputable abbrev ringOfCoalgebra : zero_mul x := by simp mul_zero x := by simp mul_assoc x y z := by - simp_rw [AlgebraOfCoalgebra.mul_def, ← rTensor_tmul, ← comp_apply, ← LinearMap.adjoint_rTensor, - ← adjoint_comp, ← coassoc_symm, adjoint_comp, LinearMap.adjoint_lTensor, comp_apply, + simp_rw [AlgebraOfCoalgebra.mul_def, ← rTensor_tmul, ← comp_apply, ← adjoint_rTensor, + ← adjoint_comp, ← coassoc_symm, adjoint_comp, adjoint_lTensor, comp_apply, ← toLinearEquiv_assocIsometry, ← toLinearEquiv_symm, adjoint_toLinearMap_eq_symm] simp only [symm_symm, toLinearEquiv_assocIsometry, LinearEquiv.coe_coe, assoc_tmul, lTensor_tmul] one := adjoint (counit (R := 𝕜) (A := E)) 1 one_mul x := by dsimp [OfNat.ofNat] - rw [← rTensor_tmul, ← comp_apply, ← LinearMap.adjoint_rTensor, ← adjoint_comp, - rTensor_counit_comp_comul, ← toLinearMap_symm_lid, ← toLinearEquiv_lidIsometry, - ← toLinearEquiv_symm, adjoint_toLinearMap_eq_symm] + rw [← rTensor_tmul, ← comp_apply, ← adjoint_rTensor, ← adjoint_comp, rTensor_counit_comp_comul, + ← toLinearMap_symm_lid, ← toLinearEquiv_lidIsometry, ← toLinearEquiv_symm, + adjoint_toLinearMap_eq_symm] exact one_smul _ _ mul_one x := by dsimp [OfNat.ofNat] - rw [← lTensor_tmul, ← comp_apply, ← LinearMap.adjoint_lTensor, ← adjoint_comp, - lTensor_counit_comp_comul, ← toLinearMap_symm_rid, ← comm_trans_lid, - ← toLinearEquiv_commIsometry, ← toLinearEquiv_lidIsometry, ← toLinearEquiv_trans, - ← toLinearEquiv_symm, adjoint_toLinearMap_eq_symm] + rw [← lTensor_tmul, ← comp_apply, ← adjoint_lTensor, ← adjoint_comp, lTensor_counit_comp_comul, + ← toLinearMap_symm_rid, ← comm_trans_lid, ← toLinearEquiv_commIsometry, + ← toLinearEquiv_lidIsometry, ← toLinearEquiv_trans, ← toLinearEquiv_symm, + adjoint_toLinearMap_eq_symm] exact one_smul _ _ attribute [local instance] InnerProductSpace.ringOfCoalgebra in @@ -155,23 +153,22 @@ noncomputable abbrev algebraOfCoalgebra : Algebra 𝕜 E where ← adjoint_comp, ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, adjoint_comp, ← toLinearMap_symm_lid, ← toLinearEquiv_lidIsometry, ← toLinearEquiv_symm, adjoint_toLinearMap_eq_symm] - simp only [LinearIsometryEquiv.symm_symm, toLinearEquiv_lidIsometry, - LinearMap.adjoint_lTensor, coe_comp, LinearEquiv.coe_coe, Function.comp_apply, - lTensor_tmul, lid_tmul] + simp only [LinearIsometryEquiv.symm_symm, toLinearEquiv_lidIsometry, adjoint_lTensor, + coe_comp, LinearEquiv.coe_coe, Function.comp_apply, lTensor_tmul, lid_tmul] rw [← smul_eq_mul, ← _root_.map_smul] map_zero' := map_zero _ map_add' := map_add _ } commutes' r x := by dsimp - simp_rw [← rTensor_tmul, ← lTensor_tmul, ← LinearMap.adjoint_lTensor, - ← LinearMap.adjoint_rTensor, ← comp_apply, ← adjoint_comp, rTensor_counit_comp_comul, - lTensor_counit_comp_comul, ← toLinearMap_symm_rid, ← toLinearMap_symm_lid, ← comm_trans_lid, + simp_rw [← rTensor_tmul, ← lTensor_tmul, ← adjoint_lTensor, ← adjoint_rTensor, + ← comp_apply, ← adjoint_comp, rTensor_counit_comp_comul, lTensor_counit_comp_comul, + ← toLinearMap_symm_rid, ← toLinearMap_symm_lid, ← comm_trans_lid, ← toLinearEquiv_commIsometry, ← toLinearEquiv_lidIsometry, ← toLinearEquiv_trans, ← toLinearEquiv_symm, adjoint_toLinearMap_eq_symm] simp smul_def' r x := by dsimp - simp_rw [← rTensor_tmul, ← LinearMap.adjoint_rTensor, ← comp_apply, ← adjoint_comp, + simp_rw [← rTensor_tmul, ← adjoint_rTensor, ← comp_apply, ← adjoint_comp, rTensor_counit_comp_comul, ← toLinearMap_symm_lid, ← toLinearEquiv_lidIsometry, ← toLinearEquiv_symm, adjoint_toLinearMap_eq_symm] simp diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean index 7f8984a93d76b7..37e554b878217c 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -538,15 +538,17 @@ lemma mapL_tmul (f : E →L[𝕜] F) (g : G →L[𝕜] H) (m : E) (n : G) : (mapL f g).toLinearMap = map f g := by ext; simp variable (G) in -theorem rTensor_eq_mapL (f : E →L[𝕜] F) : f.rTensor G = mapL f (.id 𝕜 G) := by simp [mapL_def] +theorem _root_.ContinuousLinearMap.rTensor_eq_mapL (f : E →L[𝕜] F) : + f.rTensor G = mapL f (.id 𝕜 G) := by simp [mapL_def] variable (E) in -theorem lTensor_eq_mapL (g : G →L[𝕜] H) : g.lTensor E = mapL (.id 𝕜 E) g := by simp [mapL_def] +theorem _root_.ContinuousLinearMap.lTensor_eq_mapL (g : G →L[𝕜] H) : + g.lTensor E = mapL (.id 𝕜 E) g := by simp [mapL_def] -lemma lTensor_comp_rTensor (f : E →L[𝕜] F) (g : G →L[𝕜] H) : +lemma _root_.ContinuousLinearMap.lTensor_comp_rTensor (f : E →L[𝕜] F) (g : G →L[𝕜] H) : f.lTensor H ∘L g.rTensor E = mapL g f := by ext; simp [← LinearMap.lTensor_comp_rTensor] -lemma rTensor_comp_lTensor (f : E →L[𝕜] F) (g : G →L[𝕜] H) : +lemma _root_.ContinuousLinearMap.rTensor_comp_lTensor (f : E →L[𝕜] F) (g : G →L[𝕜] H) : f.rTensor H ∘L g.lTensor E = mapL f g := mapL_def _ _ |>.symm @[simp] theorem adjoint_mapL [CompleteSpace E] [CompleteSpace G] [CompleteSpace (E ⊗[𝕜] G)] @@ -556,14 +558,14 @@ lemma rTensor_comp_lTensor (f : E →L[𝕜] F) (g : G →L[𝕜] H) : simp [TensorProduct.ext_iff_inner_right, ContinuousLinearMap.adjoint_inner_left] variable (G) in -@[simp] theorem adjoint_rTensor [CompleteSpace E] [CompleteSpace G] [CompleteSpace (E ⊗[𝕜] G)] - [CompleteSpace (F ⊗[𝕜] G)] [CompleteSpace F] (f : E →L[𝕜] F) : - (f.rTensor G).adjoint = f.adjoint.rTensor G := by simp [rTensor_eq_mapL] +@[simp] theorem _root_.ContinuousLinearMap.adjoint_rTensor [CompleteSpace E] [CompleteSpace G] + [CompleteSpace (E ⊗[𝕜] G)] [CompleteSpace (F ⊗[𝕜] G)] [CompleteSpace F] (f : E →L[𝕜] F) : + (f.rTensor G).adjoint = f.adjoint.rTensor G := by simp [ContinuousLinearMap.rTensor_eq_mapL] variable (E) in -@[simp] theorem adjoint_lTensor [CompleteSpace E] [CompleteSpace G] [CompleteSpace (E ⊗[𝕜] H)] - [CompleteSpace (E ⊗[𝕜] G)] [CompleteSpace H] (g : G →L[𝕜] H) : - (g.lTensor E).adjoint = g.adjoint.lTensor E := by simp [lTensor_eq_mapL] +@[simp] theorem _root_.ContinuousLinearMap.adjoint_lTensor [CompleteSpace E] [CompleteSpace G] + [CompleteSpace (E ⊗[𝕜] H)] [CompleteSpace (E ⊗[𝕜] G)] [CompleteSpace H] (g : G →L[𝕜] H) : + (g.lTensor E).adjoint = g.adjoint.lTensor E := by simp [ContinuousLinearMap.lTensor_eq_mapL] open LinearMap From 985abd99242ecadd248f8fb7c766c9d8808c75e3 Mon Sep 17 00:00:00 2001 From: TJHeeringa Date: Sun, 7 Jun 2026 17:57:54 +0200 Subject: [PATCH 23/39] Remove redundant spacing, postfix adjoint, rename _comm to _commIsometry --- .../InnerProductSpace/TensorProduct.lean | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean index 37e554b878217c..85d6a87817e2ef 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -425,10 +425,10 @@ variable (G) in the map `x ⊗ₜ[𝕜] y ↦ f(x) ⊗ₜ[𝕜] y`. -/ noncomputable def rTensor (f : E →L[𝕜] F) : (E ⊗[𝕜] G) →L[𝕜] (F ⊗[𝕜] G) := (f.toLinearMap.rTensor G).mkContinuous ‖f‖ fun x ↦ by - obtain ⟨n, e, g, hx ⟩ := exists_sum_tmul_eq x + obtain ⟨n, e, g, hx⟩ := exists_sum_tmul_eq x obtain ⟨c, hc_supp, hc⟩ := Submodule.mem_span_set.mp ((span_tmul_eq_top 𝕜 E G) ▸ Submodule.mem_top (x := x)) - obtain ⟨m, A, hA⟩ := Matrix.posSemidef_iff_eq_sum_vecMulVec.mp + obtain ⟨m, A, hA⟩ := Matrix.posSemidef_iff_eq_sum_vecMulVec.mp (Matrix.posSemidef_opNorm_smul_gram_sub_gram e f) apply (sq_le_sq₀ (norm_nonneg _) (by positivity)).mp simp_rw [sub_eq_iff_eq_add', ← sub_eq_iff_eq_add, ← Matrix.ext_iff, Matrix.sub_apply, @@ -475,22 +475,22 @@ variable (E) in lemma lTensor_tmul (g : G →L[𝕜] H) (m : E) (n : G) : g.lTensor E (m ⊗ₜ n) = m ⊗ₜ g n := rfl variable (E) in -theorem comm_comp_lTensor_comp_comm_eq (g : G →L[𝕜] H) : +theorem commIsometry_comp_lTensor_comp_commIsometry_eq (g : G →L[𝕜] H) : commIsometry 𝕜 H E ∘L g.rTensor E ∘L commIsometry 𝕜 E G = g.lTensor E := rfl variable (G) in -theorem comm_comp_rTensor_comp_comm_eq (f : E →L[𝕜] F) : +theorem commIsometry_comp_rTensor_comp_commIsometry_eq (f : E →L[𝕜] F) : commIsometry 𝕜 G F ∘L f.lTensor G ∘L commIsometry 𝕜 E G = f.rTensor G := by ext; simp [lTensor_def] variable (G) in -theorem lTensor_comp_comm (f : E →L[𝕜] F) : +theorem lTensor_comp_commIsometry (f : E →L[𝕜] F) : f.lTensor G ∘L commIsometry 𝕜 E G = commIsometry 𝕜 F G ∘L f.rTensor G := by ext; simp [lTensor_def] variable (E) in -theorem rTensor_comp_comm (g : G →L[𝕜] H) : +theorem rTensor_comp_commIsometry (g : G →L[𝕜] H) : g.rTensor E ∘L commIsometry 𝕜 E G = commIsometry 𝕜 E H ∘L g.lTensor E := by ext; simp [lTensor_def] @@ -571,16 +571,16 @@ open LinearMap @[simp] theorem adjoint_map [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] [FiniteDimensional 𝕜 G] [FiniteDimensional 𝕜 H] (f : E →ₗ[𝕜] F) (g : G →ₗ[𝕜] H) : - adjoint (map f g) = map (adjoint f) (adjoint g) := + (map f g).adjoint = map f.adjoint g.adjoint := ext' fun _ _ => by simp [TensorProduct.ext_iff_inner_right, adjoint_inner_left] @[simp] theorem _root_.LinearMap.adjoint_rTensor [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] [FiniteDimensional 𝕜 G] (f : E →ₗ[𝕜] F) : - adjoint (f.rTensor G) = f.adjoint.rTensor G := by simp [rTensor] + (f.rTensor G).adjoint = f.adjoint.rTensor G := by simp [rTensor] @[simp] theorem _root_.LinearMap.adjoint_lTensor [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] [FiniteDimensional 𝕜 G] (f : E →ₗ[𝕜] F) : - adjoint (f.lTensor G) = f.adjoint.lTensor G := by simp [lTensor] + (f.lTensor G).adjoint = f.adjoint.lTensor G := by simp [lTensor] /-- Given `x, y : E ⊗ (F ⊗ G)`, `x = y` iff `⟪x, a ⊗ₜ (b ⊗ₜ c)⟫ = ⟪y, a ⊗ₜ (b ⊗ₜ c)⟫` for all `a, b, c`. From b54f70b5aa18f91bb5418be79ea2bb107f552ead Mon Sep 17 00:00:00 2001 From: TJHeeringa Date: Sun, 7 Jun 2026 18:08:03 +0200 Subject: [PATCH 24/39] Remove redundant spacing --- Mathlib/Analysis/InnerProductSpace/TensorProduct.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean index 85d6a87817e2ef..e7e088a708f1b1 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -485,12 +485,12 @@ theorem commIsometry_comp_rTensor_comp_commIsometry_eq (f : E →L[𝕜] F) : ext; simp [lTensor_def] variable (G) in -theorem lTensor_comp_commIsometry (f : E →L[𝕜] F) : +theorem lTensor_comp_commIsometry (f : E →L[𝕜] F) : f.lTensor G ∘L commIsometry 𝕜 E G = commIsometry 𝕜 F G ∘L f.rTensor G := by ext; simp [lTensor_def] variable (E) in -theorem rTensor_comp_commIsometry (g : G →L[𝕜] H) : +theorem rTensor_comp_commIsometry (g : G →L[𝕜] H) : g.rTensor E ∘L commIsometry 𝕜 E G = commIsometry 𝕜 E H ∘L g.lTensor E := by ext; simp [lTensor_def] From 692ad12b51f1aac5062ec3a8b00e55ebfb816516 Mon Sep 17 00:00:00 2001 From: TJHeeringa Date: Sun, 7 Jun 2026 18:22:44 +0200 Subject: [PATCH 25/39] Apply suggestions from code review Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com> --- Mathlib/Analysis/InnerProductSpace/TensorProduct.lean | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean index e7e088a708f1b1..42f29c65233b0f 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -451,7 +451,7 @@ variable (G) in (f.rTensor G).toLinearMap = f.toLinearMap.rTensor G := rfl variable (G) in -theorem rTensor_norm_le (f : E →L[𝕜] F) : ‖f.rTensor G‖ ≤ ‖f‖ := +theorem norm_rTensor_le (f : E →L[𝕜] F) : ‖f.rTensor G‖ ≤ ‖f‖ := LinearMap.mkContinuous_norm_le _ (norm_nonneg _) _ @[simp] lemma rTensor_id : (.id 𝕜 E : E →L[𝕜] E).rTensor G = .id 𝕜 _ := by ext; simp @@ -499,11 +499,10 @@ variable (E) in (g.lTensor E).toLinearMap = g.toLinearMap.lTensor E := by ext; simp variable (E) in -theorem lTensor_norm_le (g : G →L[𝕜] H) : ‖g.lTensor E‖ ≤ ‖g‖ := by +theorem norm_lTensor_le (g : G →L[𝕜] H) : ‖g.lTensor E‖ ≤ ‖g‖ := by simp_rw [lTensor_def, ← LinearIsometryEquiv.toContinuousLinearMap_toLinearIsometry] - grw [opNorm_comp_le, opNorm_comp_le, rTensor_norm_le, - (commIsometry 𝕜 E G).toLinearIsometry.norm_toContinuousLinearMap_le, - (commIsometry 𝕜 H E).toLinearIsometry.norm_toContinuousLinearMap_le, mul_one, one_mul] + grw [opNorm_comp_le, opNorm_comp_le, LinearIsometry.norm_toContinuousLinearMap_le, + LinearIsometry.norm_toContinuousLinearMap_le, mul_one, one_mul, norm_rTensor_le] @[simp] lemma lTensor_id : (.id 𝕜 E : E →L[𝕜] E).lTensor G = .id 𝕜 _ := by ext; simp @[simp] lemma lTensor_zero : (0 : E →L[𝕜] G).lTensor H = 0 := by ext; simp From 5943bd1182f03755e1c5222dcd468737918bc028 Mon Sep 17 00:00:00 2001 From: TJHeeringa Date: Sun, 7 Jun 2026 18:31:40 +0200 Subject: [PATCH 26/39] Fix missed rename, missing spacing --- .../Analysis/InnerProductSpace/TensorProduct.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean index 42f29c65233b0f..aa51d4e26a516b 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -433,10 +433,10 @@ noncomputable def rTensor (f : E →L[𝕜] F) : (E ⊗[𝕜] G) →L[𝕜] (F apply (sq_le_sq₀ (norm_nonneg _) (by positivity)).mp simp_rw [sub_eq_iff_eq_add', ← sub_eq_iff_eq_add, ← Matrix.ext_iff, Matrix.sub_apply, Matrix.smul_apply, Matrix.gram_apply, Function.comp_apply] at hA - simp_rw [mul_pow, hx, map_sum, LinearMap.rTensor_tmul, coe_coe, ← inner_self_eq_norm_sq (𝕜:=𝕜), - inner_sum, sum_inner, inner_tmul, ← hA, sub_mul, Finset.sum_sub_distrib, map_sub, - ← RCLike.smul_re, Finset.smul_sum, smul_mul_assoc, sub_le_self_iff, Matrix.sum_apply, - mul_comm, Finset.mul_sum] + simp_rw [mul_pow, hx, map_sum, LinearMap.rTensor_tmul, coe_coe, + ← inner_self_eq_norm_sq (𝕜 := 𝕜), inner_sum, sum_inner, inner_tmul, ← hA, sub_mul, + Finset.sum_sub_distrib, map_sub, ← RCLike.smul_re, Finset.smul_sum, smul_mul_assoc, + sub_le_self_iff, Matrix.sum_apply, mul_comm, Finset.mul_sum] simp_rw +singlePass [Finset.sum_comm_cycle, Matrix.vecMulVec, Matrix.of_apply, Pi.star_apply, ← mul_left_comm, ← mul_assoc, ← starRingEnd_self_apply (A _ _), ← inner_smul_left] simp [mul_comm, ← inner_smul_right, ← sum_inner, ← inner_sum, Finset.sum_nonneg] @@ -519,8 +519,8 @@ noncomputable def mapL (f : E →L[𝕜] F) (g : G →L[𝕜] H) : (E ⊗[𝕜] lemma mapL_def (f : E →L[𝕜] F) (g : G →L[𝕜] H) : mapL f g = f.rTensor H ∘L g.lTensor E := rfl theorem norm_mapL_le (f : E →L[𝕜] F) (g : G →L[𝕜] H) : ‖mapL f g‖ ≤ ‖f‖ * ‖g‖ := by - grw [mapL_def, ContinuousLinearMap.opNorm_comp_le, ContinuousLinearMap.rTensor_norm_le, - ContinuousLinearMap.lTensor_norm_le] + grw [mapL_def, ContinuousLinearMap.opNorm_comp_le, ContinuousLinearMap.norm_rTensor_le, + ContinuousLinearMap.norm_lTensor_le] @[simp] lemma mapL_apply (f : E →L[𝕜] F) (g : G →L[𝕜] H) (x) : mapL f g x = map f.toLinearMap g.toLinearMap x := by From b2765d0b926ece33fb8f5933db94ae4e6be7ae1b Mon Sep 17 00:00:00 2001 From: Monica Omar <23701951+themathqueen@users.noreply.github.com> Date: Sun, 7 Jun 2026 18:02:05 +0100 Subject: [PATCH 27/39] tiny more cleanup --- .../InnerProductSpace/TensorProduct.lean | 59 +++++++++++-------- 1 file changed, 33 insertions(+), 26 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean index aa51d4e26a516b..7e630b1b5f96ec 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -420,7 +420,8 @@ namespace ContinuousLinearMap open TensorProduct -variable (G) in +variable (G) + /-- `LinearMap.rTensor` as a continuous linear map, i.e. the continuous linear map `f` extended to the map `x ⊗ₜ[𝕜] y ↦ f(x) ⊗ₜ[𝕜] y`. -/ noncomputable def rTensor (f : E →L[𝕜] F) : (E ⊗[𝕜] G) →L[𝕜] (F ⊗[𝕜] G) := @@ -441,71 +442,77 @@ noncomputable def rTensor (f : E →L[𝕜] F) : (E ⊗[𝕜] G) →L[𝕜] (F ← mul_left_comm, ← mul_assoc, ← starRingEnd_self_apply (A _ _), ← inner_smul_left] simp [mul_comm, ← inner_smul_right, ← sum_inner, ← inner_sum, Finset.sum_nonneg] +variable {G} in @[simp] lemma rTensor_apply (f : E →L[𝕜] F) (x : E ⊗ G) : f.rTensor G x = f.toLinearMap.rTensor G x := rfl +variable {G} in lemma rTensor_tmul (f : E →L[𝕜] F) (m : E) (n : G) : f.rTensor G (m ⊗ₜ n) = f m ⊗ₜ n := rfl -variable (G) in @[simp] lemma toLinearMap_rTensor (f : E →L[𝕜] F) : (f.rTensor G).toLinearMap = f.toLinearMap.rTensor G := rfl -variable (G) in theorem norm_rTensor_le (f : E →L[𝕜] F) : ‖f.rTensor G‖ ≤ ‖f‖ := LinearMap.mkContinuous_norm_le _ (norm_nonneg _) _ +@[simp] lemma rTensor_add (f₁ f₂ : E →L[𝕜] F) : + (f₁ + f₂).rTensor G = f₁.rTensor G + f₂.rTensor G := by ext; simp + +@[simp] lemma rTensor_smul (r : 𝕜) (f : E →L[𝕜] F) : + (r • f).rTensor G = r • f.rTensor G := by ext; simp + @[simp] lemma rTensor_id : (.id 𝕜 E : E →L[𝕜] E).rTensor G = .id 𝕜 _ := by ext; simp -@[simp] lemma rTensor_zero : (0 : E →L[𝕜] G).rTensor H = 0 := by ext; simp +@[simp] lemma rTensor_one : (1 : E →L[𝕜] E).rTensor G = 1 := rTensor_id _ +@[simp] lemma rTensor_zero : (0 : E →L[𝕜] F).rTensor G = 0 := by ext; simp -variable (E) in /-- `LinearMap.lTensor` as a continuous linear map, i.e. the continuous linear map `g` extended to the map `x ⊗ₜ[𝕜] y ↦ x ⊗ₜ[𝕜] g(y)`. -/ -noncomputable def lTensor (g : G →L[𝕜] H) : (E ⊗[𝕜] G) →L[𝕜] (E ⊗[𝕜] H) := - commIsometry 𝕜 H E ∘L g.rTensor E ∘L commIsometry 𝕜 E G +noncomputable def lTensor (g : E →L[𝕜] F) : (G ⊗[𝕜] E) →L[𝕜] (G ⊗[𝕜] F) := + commIsometry 𝕜 F G ∘L g.rTensor G ∘L commIsometry 𝕜 G E -variable (E) in -lemma lTensor_def (g : G →L[𝕜] H) : - g.lTensor E = commIsometry 𝕜 H E ∘L g.rTensor E ∘L commIsometry 𝕜 E G := rfl +lemma lTensor_def (g : E →L[𝕜] F) : + g.lTensor G = commIsometry 𝕜 F G ∘L g.rTensor G ∘L commIsometry 𝕜 G E := rfl +variable {G} in @[simp] lemma lTensor_apply (g : G →L[𝕜] H) (x : E ⊗ G) : g.lTensor E x = g.toLinearMap.lTensor E x := by simp [lTensor_def, ← LinearMap.comm_comp_rTensor_comp_comm_eq] -variable (E) in -lemma lTensor_tmul (g : G →L[𝕜] H) (m : E) (n : G) : g.lTensor E (m ⊗ₜ n) = m ⊗ₜ g n := rfl +lemma lTensor_tmul (g : E →L[𝕜] F) (m : G) (n : E) : g.lTensor G (m ⊗ₜ n) = m ⊗ₜ g n := rfl -variable (E) in -theorem commIsometry_comp_lTensor_comp_commIsometry_eq (g : G →L[𝕜] H) : - commIsometry 𝕜 H E ∘L g.rTensor E ∘L commIsometry 𝕜 E G = g.lTensor E := +theorem commIsometry_comp_lTensor_comp_commIsometry_eq (g : E →L[𝕜] F) : + commIsometry 𝕜 F G ∘L g.rTensor G ∘L commIsometry 𝕜 G E = g.lTensor G := rfl -variable (G) in theorem commIsometry_comp_rTensor_comp_commIsometry_eq (f : E →L[𝕜] F) : commIsometry 𝕜 G F ∘L f.lTensor G ∘L commIsometry 𝕜 E G = f.rTensor G := by ext; simp [lTensor_def] -variable (G) in theorem lTensor_comp_commIsometry (f : E →L[𝕜] F) : f.lTensor G ∘L commIsometry 𝕜 E G = commIsometry 𝕜 F G ∘L f.rTensor G := by ext; simp [lTensor_def] -variable (E) in -theorem rTensor_comp_commIsometry (g : G →L[𝕜] H) : - g.rTensor E ∘L commIsometry 𝕜 E G = commIsometry 𝕜 E H ∘L g.lTensor E := by +theorem rTensor_comp_commIsometry (g : E →L[𝕜] F) : + g.rTensor G ∘L commIsometry 𝕜 G E = commIsometry 𝕜 G F ∘L g.lTensor G := by ext; simp [lTensor_def] -variable (E) in -@[simp] lemma toLinearMap_lTensor (g : G →L[𝕜] H) : - (g.lTensor E).toLinearMap = g.toLinearMap.lTensor E := by ext; simp +@[simp] lemma toLinearMap_lTensor (g : E →L[𝕜] F) : + (g.lTensor G).toLinearMap = g.toLinearMap.lTensor G := by ext; simp -variable (E) in -theorem norm_lTensor_le (g : G →L[𝕜] H) : ‖g.lTensor E‖ ≤ ‖g‖ := by +theorem norm_lTensor_le (g : E →L[𝕜] F) : ‖g.lTensor G‖ ≤ ‖g‖ := by simp_rw [lTensor_def, ← LinearIsometryEquiv.toContinuousLinearMap_toLinearIsometry] grw [opNorm_comp_le, opNorm_comp_le, LinearIsometry.norm_toContinuousLinearMap_le, LinearIsometry.norm_toContinuousLinearMap_le, mul_one, one_mul, norm_rTensor_le] +@[simp] lemma lTensor_add (f₁ f₂ : E →L[𝕜] F) : + (f₁ + f₂).lTensor G = f₁.lTensor G + f₂.lTensor G := by ext; simp + +@[simp] lemma lTensor_smul (r : 𝕜) (f : E →L[𝕜] F) : (r • f).lTensor G = r • f.lTensor G := by + ext; simp + @[simp] lemma lTensor_id : (.id 𝕜 E : E →L[𝕜] E).lTensor G = .id 𝕜 _ := by ext; simp -@[simp] lemma lTensor_zero : (0 : E →L[𝕜] G).lTensor H = 0 := by ext; simp +@[simp] lemma lTensor_one : (1 : E →L[𝕜] E).lTensor G = 1 := lTensor_id _ +@[simp] lemma lTensor_zero : (0 : E →L[𝕜] F).lTensor G = 0 := by ext; simp end ContinuousLinearMap From cb4b67a06301860305c669a314ea534bf7637f08 Mon Sep 17 00:00:00 2001 From: TJHeeringa Date: Mon, 8 Jun 2026 09:18:14 +0200 Subject: [PATCH 28/39] Add proof description --- Mathlib/Analysis/InnerProductSpace/TensorProduct.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean index 7e630b1b5f96ec..97f9acbeed8493 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -426,6 +426,13 @@ variable (G) the map `x ⊗ₜ[𝕜] y ↦ f(x) ⊗ₜ[𝕜] y`. -/ noncomputable def rTensor (f : E →L[𝕜] F) : (E ⊗[𝕜] G) →L[𝕜] (F ⊗[𝕜] G) := (f.toLinearMap.rTensor G).mkContinuous ‖f‖ fun x ↦ by + /- + Any tensor `x` can be written as a linear combination of pure tensors, `x= ∑ e n ⊗ₜ g n`. This + induces three Gram matrices, one based on `e`, one on `f ∘ e` and one on `g`. Up to a constant, + the `e`-based Gram matrix is larger than the `f ∘ e`-based one. This implies the existence of + a matrix, whose form is used to show that `‖f‖^2 * ‖x‖^2 - ‖f x‖^2` is a sum of nonnegative + terms. + -/ obtain ⟨n, e, g, hx⟩ := exists_sum_tmul_eq x obtain ⟨c, hc_supp, hc⟩ := Submodule.mem_span_set.mp ((span_tmul_eq_top 𝕜 E G) ▸ Submodule.mem_top (x := x)) From 1463c2df2fa3a6cef4fa6f83d439532060a4a505 Mon Sep 17 00:00:00 2001 From: TJHeeringa Date: Mon, 8 Jun 2026 10:05:12 +0200 Subject: [PATCH 29/39] Expand API for l/rTensor and mapL --- .../InnerProductSpace/TensorProduct.lean | 82 ++++++++++++++++++- 1 file changed, 80 insertions(+), 2 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean index 97f9acbeed8493..d5df31ebf96252 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -459,6 +459,9 @@ lemma rTensor_tmul (f : E →L[𝕜] F) (m : E) (n : G) : f.rTensor G (m ⊗ₜ @[simp] lemma toLinearMap_rTensor (f : E →L[𝕜] F) : (f.rTensor G).toLinearMap = f.toLinearMap.rTensor G := rfl +@[simp] lemma _root_.LinearIsometry.toContinuousLinearMap_rTensor (f : E →ₗᵢ[𝕜] F) : + (f.rTensor G).toContinuousLinearMap = f.toContinuousLinearMap.rTensor G := rfl + theorem norm_rTensor_le (f : E →L[𝕜] F) : ‖f.rTensor G‖ ≤ ‖f‖ := LinearMap.mkContinuous_norm_le _ (norm_nonneg _) _ @@ -471,6 +474,18 @@ theorem norm_rTensor_le (f : E →L[𝕜] F) : ‖f.rTensor G‖ ≤ ‖f‖ := @[simp] lemma rTensor_id : (.id 𝕜 E : E →L[𝕜] E).rTensor G = .id 𝕜 _ := by ext; simp @[simp] lemma rTensor_one : (1 : E →L[𝕜] E).rTensor G = 1 := rTensor_id _ @[simp] lemma rTensor_zero : (0 : E →L[𝕜] F).rTensor G = 0 := by ext; simp +@[simp] lemma rTensor_neg (f : E →L[𝕜] F) : (-f).rTensor G = -f.rTensor G := by ext; simp +@[simp] lemma rTensor_sub (f₁ f₂ : E →L[𝕜] F) : + (f₁ - f₂).rTensor G = f₁.rTensor G - f₂.rTensor G := by ext; simp + +lemma rTensor_comp (f₁ : E →L[𝕜] F) (f₂ : H →L[𝕜] E) : + (f₁ ∘L f₂).rTensor G = f₁.rTensor G ∘L f₂.rTensor G := by ext; simp [LinearMap.rTensor_comp] + +lemma rTensor_mul (f₁ f₂ : E →L[𝕜] E) : (f₁ * f₂).rTensor G = f₁.rTensor G * f₂.rTensor G := + rTensor_comp _ _ _ + +@[simp] lemma rTensor_pow (f : E →L[𝕜] E) (n : ℕ) : (f ^ n).rTensor G = (f.rTensor G) ^ n := by + simp [← coe_inj] /-- `LinearMap.lTensor` as a continuous linear map, i.e. the continuous linear map `g` extended to the map `x ⊗ₜ[𝕜] y ↦ x ⊗ₜ[𝕜] g(y)`. -/ @@ -506,6 +521,9 @@ theorem rTensor_comp_commIsometry (g : E →L[𝕜] F) : @[simp] lemma toLinearMap_lTensor (g : E →L[𝕜] F) : (g.lTensor G).toLinearMap = g.toLinearMap.lTensor G := by ext; simp +@[simp] lemma _root_.LinearIsometry.toContinuousLinearMap_lTensor (g : E →ₗᵢ[𝕜] F) : + (g.lTensor G).toContinuousLinearMap = g.toContinuousLinearMap.lTensor G := by ext; simp; rfl + theorem norm_lTensor_le (g : E →L[𝕜] F) : ‖g.lTensor G‖ ≤ ‖g‖ := by simp_rw [lTensor_def, ← LinearIsometryEquiv.toContinuousLinearMap_toLinearIsometry] grw [opNorm_comp_le, opNorm_comp_le, LinearIsometry.norm_toContinuousLinearMap_le, @@ -520,6 +538,18 @@ theorem norm_lTensor_le (g : E →L[𝕜] F) : ‖g.lTensor G‖ ≤ ‖g‖ := @[simp] lemma lTensor_id : (.id 𝕜 E : E →L[𝕜] E).lTensor G = .id 𝕜 _ := by ext; simp @[simp] lemma lTensor_one : (1 : E →L[𝕜] E).lTensor G = 1 := lTensor_id _ @[simp] lemma lTensor_zero : (0 : E →L[𝕜] F).lTensor G = 0 := by ext; simp +@[simp] lemma lTensor_neg (f : E →L[𝕜] F) : (-f).lTensor G = -f.lTensor G := by ext; simp +@[simp] lemma lTensor_sub (f₁ f₂ : E →L[𝕜] F) : + (f₁ - f₂).lTensor G = f₁.lTensor G - f₂.lTensor G := by ext; simp + +lemma lTensor_comp (f₁ : E →L[𝕜] F) (f₂ : H →L[𝕜] E) : + (f₁ ∘L f₂).lTensor G = f₁.lTensor G ∘L f₂.lTensor G := by ext; simp [LinearMap.lTensor_comp] + +lemma lTensor_mul (f₁ f₂ : E →L[𝕜] E) : (f₁ * f₂).lTensor G = f₁.lTensor G * f₂.lTensor G := + lTensor_comp _ _ _ + +@[simp] lemma lTensor_pow (f : E →L[𝕜] E) (n : ℕ) : (f ^ n).lTensor G = (f.lTensor G) ^ n := by + simp [← coe_inj] end ContinuousLinearMap @@ -547,9 +577,57 @@ lemma mapL_tmul (f : E →L[𝕜] F) (g : G →L[𝕜] H) (m : E) (n : G) : @[simp] lemma mapL_zero_right (f : E →L[𝕜] F) : mapL f (0 : G →L[𝕜] H) = 0 := by simp [mapL_def] @[simp] lemma mapL_id_id : mapL (.id 𝕜 E) (.id 𝕜 G) = .id 𝕜 _ := by simp [mapL_def] +lemma mapL_comp_commIsometry (f : E →L[𝕜] F) (g : G →L[𝕜] H) : + mapL f g ∘L commIsometry 𝕜 G E = commIsometry 𝕜 H F ∘L mapL g f := by ext; simp [map_comm] + +lemma mapL_add_left (f₁ f₂ : E →L[𝕜] F) (g : G →L[𝕜] H) : + mapL (f₁ + f₂) g = mapL f₁ g + mapL f₂ g := by ext; simp [map_add_left] + +lemma mapL_add_right (f : E →L[𝕜] F) (g₁ g₂ : G →L[𝕜] H) : + mapL f (g₁ + g₂) = mapL f g₁ + mapL f g₂ := by ext; simp [map_add_right] + +lemma mapL_smul_left (r : 𝕜) (f : E →L[𝕜] F) (g : G →L[𝕜] H) : + mapL (r • f) g = r • mapL f g := by ext; simp [map_smul_left] + +lemma mapL_smul_right (r : 𝕜) (f : E →L[𝕜] F) (g : G →L[𝕜] H) : + mapL f (r • g) = r • mapL f g := by ext; simp [map_smul_right] + @[simp] lemma toLinearMap_mapL (f : E →L[𝕜] F) (g : G →L[𝕜] H) : (mapL f g).toLinearMap = map f g := by ext; simp +@[simp] lemma toContinuousLinearMap_mapIsometry (f : E →ₗᵢ[𝕜] F) (g : G →ₗᵢ[𝕜] H) : + (mapIsometry f g).toContinuousLinearMap = + mapL f.toContinuousLinearMap g.toContinuousLinearMap := by + ext; simp; rfl + +section comp + +variable {A B : Type*} [NormedAddCommGroup A] [InnerProductSpace 𝕜 A] [NormedAddCommGroup B] + [InnerProductSpace 𝕜 B] + +lemma mapL_comp (f₁ : E →L[𝕜] F) (f₂ : A →L[𝕜] E) (g₁ : G →L[𝕜] H) (g₂ : B →L[𝕜] G) : + mapL (f₁ ∘L f₂) (g₁ ∘L g₂) = mapL f₁ g₁ ∘L mapL f₂ g₂ := by ext; simp [map_map] + +lemma mapL_mul (f₁ f₂ : E →L[𝕜] E) (g₁ g₂ : F →L[𝕜] F) : + mapL (f₁ * f₂) (g₁ * g₂) = mapL f₁ g₁ * mapL f₂ g₂ := mapL_comp _ _ _ _ + +@[simp] lemma mapL_pow (f : E →L[𝕜] E) (g : F →L[𝕜] F) (n : ℕ) : + (mapL f g) ^ n = mapL (f ^ n) (g ^ n) := by simp [← ContinuousLinearMap.coe_inj] + +@[simp] lemma _root_.ContinuousLinearMap.mapL_comp_rTensor (f₁ : E →L[𝕜] F) (f₂ : A →L[𝕜] E) + (g : G →L[𝕜] H) : mapL f₁ g ∘L f₂.rTensor G = mapL (f₁ ∘L f₂) g := by ext; simp + +@[simp] lemma _root_.ContinuousLinearMap.mapL_comp_lTensor (f : E →L[𝕜] F) (g₁ : G →L[𝕜] H) + (g₂ : A →L[𝕜] G) : mapL f g₁ ∘L g₂.lTensor E = mapL f (g₁ ∘L g₂) := by ext; simp + +@[simp] lemma _root_.ContinuousLinearMap.rTensor_comp_mapL (f₁ : E →L[𝕜] F) (f₂ : A →L[𝕜] E) + (g : G →L[𝕜] H) : f₁.rTensor H ∘L mapL f₂ g = mapL (f₁ ∘L f₂) g := by ext; simp + +@[simp] lemma _root_.ContinuousLinearMap.lTensor_comp_mapL (f : E →L[𝕜] F) (g₁ : G →L[𝕜] H) + (g₂ : A →L[𝕜] G) : g₁.lTensor F ∘L mapL f g₂ = mapL f (g₁ ∘L g₂) := by ext; simp + +end comp + variable (G) in theorem _root_.ContinuousLinearMap.rTensor_eq_mapL (f : E →L[𝕜] F) : f.rTensor G = mapL f (.id 𝕜 G) := by simp [mapL_def] @@ -558,10 +636,10 @@ variable (E) in theorem _root_.ContinuousLinearMap.lTensor_eq_mapL (g : G →L[𝕜] H) : g.lTensor E = mapL (.id 𝕜 E) g := by simp [mapL_def] -lemma _root_.ContinuousLinearMap.lTensor_comp_rTensor (f : E →L[𝕜] F) (g : G →L[𝕜] H) : +@[simp] lemma _root_.ContinuousLinearMap.lTensor_comp_rTensor (f : E →L[𝕜] F) (g : G →L[𝕜] H) : f.lTensor H ∘L g.rTensor E = mapL g f := by ext; simp [← LinearMap.lTensor_comp_rTensor] -lemma _root_.ContinuousLinearMap.rTensor_comp_lTensor (f : E →L[𝕜] F) (g : G →L[𝕜] H) : +@[simp] lemma _root_.ContinuousLinearMap.rTensor_comp_lTensor (f : E →L[𝕜] F) (g : G →L[𝕜] H) : f.rTensor H ∘L g.lTensor E = mapL f g := mapL_def _ _ |>.symm @[simp] theorem adjoint_mapL [CompleteSpace E] [CompleteSpace G] [CompleteSpace (E ⊗[𝕜] G)] From a1ce3d8037813abdf5b93fef144599238aae4c8b Mon Sep 17 00:00:00 2001 From: TJHeeringa Date: Mon, 8 Jun 2026 10:07:53 +0200 Subject: [PATCH 30/39] Update file description --- Mathlib/Analysis/InnerProductSpace/TensorProduct.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean index d5df31ebf96252..bd1e48806aa59c 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -34,6 +34,8 @@ inner product spaces. * `TensorProduct.commIsometry`: the linear isometry version of `TensorProduct.comm`. * `TensorProduct.lidIsometry`: the linear isometry version of `TensorProduct.lid`. * `TensorProduct.assocIsometry`: the linear isometry version of `TensorProduct.assoc`. +* `TensorProduct.mapL`: the continuous version of `TensorProduct.map f g` when + `f` and `g` are continuous linear maps. * `OrthonormalBasis.tensorProduct`: the orthonormal basis of the tensor product of two orthonormal bases. From 988c4d3479adbabbcedb2f2d87a4ba2a0a370c60 Mon Sep 17 00:00:00 2001 From: TJHeeringa Date: Mon, 8 Jun 2026 11:06:23 +0200 Subject: [PATCH 31/39] Apply suggestions from code review Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com> --- Mathlib/Analysis/InnerProductSpace/TensorProduct.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean index bd1e48806aa59c..3fa69379f77f90 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -477,6 +477,7 @@ theorem norm_rTensor_le (f : E →L[𝕜] F) : ‖f.rTensor G‖ ≤ ‖f‖ := @[simp] lemma rTensor_one : (1 : E →L[𝕜] E).rTensor G = 1 := rTensor_id _ @[simp] lemma rTensor_zero : (0 : E →L[𝕜] F).rTensor G = 0 := by ext; simp @[simp] lemma rTensor_neg (f : E →L[𝕜] F) : (-f).rTensor G = -f.rTensor G := by ext; simp + @[simp] lemma rTensor_sub (f₁ f₂ : E →L[𝕜] F) : (f₁ - f₂).rTensor G = f₁.rTensor G - f₂.rTensor G := by ext; simp @@ -541,6 +542,7 @@ theorem norm_lTensor_le (g : E →L[𝕜] F) : ‖g.lTensor G‖ ≤ ‖g‖ := @[simp] lemma lTensor_one : (1 : E →L[𝕜] E).lTensor G = 1 := lTensor_id _ @[simp] lemma lTensor_zero : (0 : E →L[𝕜] F).lTensor G = 0 := by ext; simp @[simp] lemma lTensor_neg (f : E →L[𝕜] F) : (-f).lTensor G = -f.lTensor G := by ext; simp + @[simp] lemma lTensor_sub (f₁ f₂ : E →L[𝕜] F) : (f₁ - f₂).lTensor G = f₁.lTensor G - f₂.lTensor G := by ext; simp From 97b5b1bbf892ad8488b9952506fec9cbccc9447c Mon Sep 17 00:00:00 2001 From: TJHeeringa Date: Mon, 8 Jun 2026 11:11:56 +0200 Subject: [PATCH 32/39] Update comment spacing Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com> --- Mathlib/Analysis/InnerProductSpace/TensorProduct.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean index 3fa69379f77f90..eefe6fbe96f25a 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -429,10 +429,10 @@ the map `x ⊗ₜ[𝕜] y ↦ f(x) ⊗ₜ[𝕜] y`. -/ noncomputable def rTensor (f : E →L[𝕜] F) : (E ⊗[𝕜] G) →L[𝕜] (F ⊗[𝕜] G) := (f.toLinearMap.rTensor G).mkContinuous ‖f‖ fun x ↦ by /- - Any tensor `x` can be written as a linear combination of pure tensors, `x= ∑ e n ⊗ₜ g n`. This + Any tensor `x` can be written as a linear combination of pure tensors, `x = ∑ e n ⊗ₜ g n`. This induces three Gram matrices, one based on `e`, one on `f ∘ e` and one on `g`. Up to a constant, the `e`-based Gram matrix is larger than the `f ∘ e`-based one. This implies the existence of - a matrix, whose form is used to show that `‖f‖^2 * ‖x‖^2 - ‖f x‖^2` is a sum of nonnegative + a matrix, whose form is used to show that `‖f‖ ^ 2 * ‖x‖ ^ 2 - ‖f x‖ ^ 2` is a sum of nonnegative terms. -/ obtain ⟨n, e, g, hx⟩ := exists_sum_tmul_eq x From 7b71db9e9a138b489d90695ca9d82e0df567e81e Mon Sep 17 00:00:00 2001 From: TJHeeringa Date: Mon, 8 Jun 2026 17:14:13 +0200 Subject: [PATCH 33/39] Add LinearIsometry.toLinearMap_toContinuousLinearMap --- Mathlib/Analysis/InnerProductSpace/TensorProduct.lean | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean index eefe6fbe96f25a..8e91770dd5f5a0 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -524,8 +524,13 @@ theorem rTensor_comp_commIsometry (g : E →L[𝕜] F) : @[simp] lemma toLinearMap_lTensor (g : E →L[𝕜] F) : (g.lTensor G).toLinearMap = g.toLinearMap.lTensor G := by ext; simp +@[simp] lemma _root_.LinearIsometry.toLinearMap_toContinuousLinearMap {R R₂ E E₂ : Type*} + [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] + [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) : + f.toContinuousLinearMap.toLinearMap = f.toLinearMap := rfl + @[simp] lemma _root_.LinearIsometry.toContinuousLinearMap_lTensor (g : E →ₗᵢ[𝕜] F) : - (g.lTensor G).toContinuousLinearMap = g.toContinuousLinearMap.lTensor G := by ext; simp; rfl + (g.lTensor G).toContinuousLinearMap = g.toContinuousLinearMap.lTensor G := by ext; simp theorem norm_lTensor_le (g : E →L[𝕜] F) : ‖g.lTensor G‖ ≤ ‖g‖ := by simp_rw [lTensor_def, ← LinearIsometryEquiv.toContinuousLinearMap_toLinearIsometry] @@ -602,8 +607,7 @@ lemma mapL_smul_right (r : 𝕜) (f : E →L[𝕜] F) (g : G →L[𝕜] H) : @[simp] lemma toContinuousLinearMap_mapIsometry (f : E →ₗᵢ[𝕜] F) (g : G →ₗᵢ[𝕜] H) : (mapIsometry f g).toContinuousLinearMap = mapL f.toContinuousLinearMap g.toContinuousLinearMap := by - ext; simp; rfl - + ext; simp section comp variable {A B : Type*} [NormedAddCommGroup A] [InnerProductSpace 𝕜 A] [NormedAddCommGroup B] From 682c8d6fe35dafe64dceb2ec6d5ba27113768aac Mon Sep 17 00:00:00 2001 From: TJHeeringa Date: Mon, 8 Jun 2026 18:42:06 +0200 Subject: [PATCH 34/39] Move LinearIsometry.toLinearMap_toContinuousLinearMap earlier, fix space in comment --- Mathlib/Analysis/InnerProductSpace/TensorProduct.lean | 9 ++------- Mathlib/Analysis/Normed/Operator/LinearIsometry.lean | 3 +++ 2 files changed, 5 insertions(+), 7 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean index 8e91770dd5f5a0..888cdc4fb8116f 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -432,8 +432,8 @@ noncomputable def rTensor (f : E →L[𝕜] F) : (E ⊗[𝕜] G) →L[𝕜] (F Any tensor `x` can be written as a linear combination of pure tensors, `x = ∑ e n ⊗ₜ g n`. This induces three Gram matrices, one based on `e`, one on `f ∘ e` and one on `g`. Up to a constant, the `e`-based Gram matrix is larger than the `f ∘ e`-based one. This implies the existence of - a matrix, whose form is used to show that `‖f‖ ^ 2 * ‖x‖ ^ 2 - ‖f x‖ ^ 2` is a sum of nonnegative - terms. + a matrix, whose form is used to show that `‖f‖ ^ 2 * ‖x‖ ^ 2 - ‖f x‖ ^ 2` is a sum of + nonnegative terms. -/ obtain ⟨n, e, g, hx⟩ := exists_sum_tmul_eq x obtain ⟨c, hc_supp, hc⟩ := Submodule.mem_span_set.mp @@ -524,11 +524,6 @@ theorem rTensor_comp_commIsometry (g : E →L[𝕜] F) : @[simp] lemma toLinearMap_lTensor (g : E →L[𝕜] F) : (g.lTensor G).toLinearMap = g.toLinearMap.lTensor G := by ext; simp -@[simp] lemma _root_.LinearIsometry.toLinearMap_toContinuousLinearMap {R R₂ E E₂ : Type*} - [Semiring R] [Semiring R₂] {σ₁₂ : R →+* R₂} [SeminormedAddCommGroup E] - [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) : - f.toContinuousLinearMap.toLinearMap = f.toLinearMap := rfl - @[simp] lemma _root_.LinearIsometry.toContinuousLinearMap_lTensor (g : E →ₗᵢ[𝕜] F) : (g.lTensor G).toContinuousLinearMap = g.toContinuousLinearMap.lTensor G := by ext; simp diff --git a/Mathlib/Analysis/Normed/Operator/LinearIsometry.lean b/Mathlib/Analysis/Normed/Operator/LinearIsometry.lean index 3144e2967bff2b..79f9d9b3cf0c89 100644 --- a/Mathlib/Analysis/Normed/Operator/LinearIsometry.lean +++ b/Mathlib/Analysis/Normed/Operator/LinearIsometry.lean @@ -284,6 +284,9 @@ theorem diam_range : Metric.diam (range f) = Metric.diam (univ : Set E) := def toContinuousLinearMap : E →SL[σ₁₂] E₂ := ⟨f.toLinearMap, f.continuous⟩ +@[simp] lemma toLinearMap_toContinuousLinearMap (f : E →ₛₗᵢ[σ₁₂] E₂) : + f.toContinuousLinearMap.toLinearMap = f.toLinearMap := rfl + theorem toContinuousLinearMap_injective : Function.Injective (toContinuousLinearMap : _ → E →SL[σ₁₂] E₂) := fun x _ h => coe_injective (congr_arg _ h : ⇑x.toContinuousLinearMap = _) From 277de34dc4269f0239cde5308eb6175bc46038c4 Mon Sep 17 00:00:00 2001 From: TJHeeringa Date: Tue, 9 Jun 2026 09:15:46 +0200 Subject: [PATCH 35/39] Remove _def lemma's --- .../InnerProductSpace/TensorProduct.lean | 32 ++++++++----------- 1 file changed, 14 insertions(+), 18 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean index 888cdc4fb8116f..14ab7bd00c413f 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -495,13 +495,10 @@ the map `x ⊗ₜ[𝕜] y ↦ x ⊗ₜ[𝕜] g(y)`. -/ noncomputable def lTensor (g : E →L[𝕜] F) : (G ⊗[𝕜] E) →L[𝕜] (G ⊗[𝕜] F) := commIsometry 𝕜 F G ∘L g.rTensor G ∘L commIsometry 𝕜 G E -lemma lTensor_def (g : E →L[𝕜] F) : - g.lTensor G = commIsometry 𝕜 F G ∘L g.rTensor G ∘L commIsometry 𝕜 G E := rfl - variable {G} in @[simp] lemma lTensor_apply (g : G →L[𝕜] H) (x : E ⊗ G) : g.lTensor E x = g.toLinearMap.lTensor E x := by - simp [lTensor_def, ← LinearMap.comm_comp_rTensor_comp_comm_eq] + simp [lTensor, ← LinearMap.comm_comp_rTensor_comp_comm_eq] lemma lTensor_tmul (g : E →L[𝕜] F) (m : G) (n : E) : g.lTensor G (m ⊗ₜ n) = m ⊗ₜ g n := rfl @@ -511,15 +508,15 @@ theorem commIsometry_comp_lTensor_comp_commIsometry_eq (g : E →L[𝕜] F) : theorem commIsometry_comp_rTensor_comp_commIsometry_eq (f : E →L[𝕜] F) : commIsometry 𝕜 G F ∘L f.lTensor G ∘L commIsometry 𝕜 E G = f.rTensor G := by - ext; simp [lTensor_def] + ext; simp [lTensor] theorem lTensor_comp_commIsometry (f : E →L[𝕜] F) : f.lTensor G ∘L commIsometry 𝕜 E G = commIsometry 𝕜 F G ∘L f.rTensor G := by - ext; simp [lTensor_def] + ext; simp [lTensor] theorem rTensor_comp_commIsometry (g : E →L[𝕜] F) : g.rTensor G ∘L commIsometry 𝕜 G E = commIsometry 𝕜 G F ∘L g.lTensor G := by - ext; simp [lTensor_def] + ext; simp [lTensor] @[simp] lemma toLinearMap_lTensor (g : E →L[𝕜] F) : (g.lTensor G).toLinearMap = g.toLinearMap.lTensor G := by ext; simp @@ -528,7 +525,7 @@ theorem rTensor_comp_commIsometry (g : E →L[𝕜] F) : (g.lTensor G).toContinuousLinearMap = g.toContinuousLinearMap.lTensor G := by ext; simp theorem norm_lTensor_le (g : E →L[𝕜] F) : ‖g.lTensor G‖ ≤ ‖g‖ := by - simp_rw [lTensor_def, ← LinearIsometryEquiv.toContinuousLinearMap_toLinearIsometry] + simp_rw [lTensor, ← LinearIsometryEquiv.toContinuousLinearMap_toLinearIsometry] grw [opNorm_comp_le, opNorm_comp_le, LinearIsometry.norm_toContinuousLinearMap_le, LinearIsometry.norm_toContinuousLinearMap_le, mul_one, one_mul, norm_rTensor_le] @@ -564,22 +561,20 @@ namespace TensorProduct noncomputable def mapL (f : E →L[𝕜] F) (g : G →L[𝕜] H) : (E ⊗[𝕜] G) →L[𝕜] (F ⊗[𝕜] H) := f.rTensor H ∘L g.lTensor E -lemma mapL_def (f : E →L[𝕜] F) (g : G →L[𝕜] H) : mapL f g = f.rTensor H ∘L g.lTensor E := rfl - theorem norm_mapL_le (f : E →L[𝕜] F) (g : G →L[𝕜] H) : ‖mapL f g‖ ≤ ‖f‖ * ‖g‖ := by - grw [mapL_def, ContinuousLinearMap.opNorm_comp_le, ContinuousLinearMap.norm_rTensor_le, + grw [mapL, ContinuousLinearMap.opNorm_comp_le, ContinuousLinearMap.norm_rTensor_le, ContinuousLinearMap.norm_lTensor_le] @[simp] lemma mapL_apply (f : E →L[𝕜] F) (g : G →L[𝕜] H) (x) : mapL f g x = map f.toLinearMap g.toLinearMap x := by - simp [mapL_def, ← LinearMap.rTensor_comp_lTensor] + simp [mapL, ← LinearMap.rTensor_comp_lTensor] lemma mapL_tmul (f : E →L[𝕜] F) (g : G →L[𝕜] H) (m : E) (n : G) : mapL f g (m ⊗ₜ n) = f m ⊗ₜ g n := rfl -@[simp] lemma mapL_zero_left (f : E →L[𝕜] F) : mapL (0 : G →L[𝕜] H) f = 0 := by simp [mapL_def] -@[simp] lemma mapL_zero_right (f : E →L[𝕜] F) : mapL f (0 : G →L[𝕜] H) = 0 := by simp [mapL_def] -@[simp] lemma mapL_id_id : mapL (.id 𝕜 E) (.id 𝕜 G) = .id 𝕜 _ := by simp [mapL_def] +@[simp] lemma mapL_zero_left (f : E →L[𝕜] F) : mapL (0 : G →L[𝕜] H) f = 0 := by simp [mapL] +@[simp] lemma mapL_zero_right (f : E →L[𝕜] F) : mapL f (0 : G →L[𝕜] H) = 0 := by simp [mapL] +@[simp] lemma mapL_id_id : mapL (.id 𝕜 E) (.id 𝕜 G) = .id 𝕜 _ := by simp [mapL] lemma mapL_comp_commIsometry (f : E →L[𝕜] F) (g : G →L[𝕜] H) : mapL f g ∘L commIsometry 𝕜 G E = commIsometry 𝕜 H F ∘L mapL g f := by ext; simp [map_comm] @@ -603,6 +598,7 @@ lemma mapL_smul_right (r : 𝕜) (f : E →L[𝕜] F) (g : G →L[𝕜] H) : (mapIsometry f g).toContinuousLinearMap = mapL f.toContinuousLinearMap g.toContinuousLinearMap := by ext; simp + section comp variable {A B : Type*} [NormedAddCommGroup A] [InnerProductSpace 𝕜 A] [NormedAddCommGroup B] @@ -633,17 +629,17 @@ end comp variable (G) in theorem _root_.ContinuousLinearMap.rTensor_eq_mapL (f : E →L[𝕜] F) : - f.rTensor G = mapL f (.id 𝕜 G) := by simp [mapL_def] + f.rTensor G = mapL f (.id 𝕜 G) := by simp [mapL] variable (E) in theorem _root_.ContinuousLinearMap.lTensor_eq_mapL (g : G →L[𝕜] H) : - g.lTensor E = mapL (.id 𝕜 E) g := by simp [mapL_def] + g.lTensor E = mapL (.id 𝕜 E) g := by simp [mapL] @[simp] lemma _root_.ContinuousLinearMap.lTensor_comp_rTensor (f : E →L[𝕜] F) (g : G →L[𝕜] H) : f.lTensor H ∘L g.rTensor E = mapL g f := by ext; simp [← LinearMap.lTensor_comp_rTensor] @[simp] lemma _root_.ContinuousLinearMap.rTensor_comp_lTensor (f : E →L[𝕜] F) (g : G →L[𝕜] H) : - f.rTensor H ∘L g.lTensor E = mapL f g := mapL_def _ _ |>.symm + f.rTensor H ∘L g.lTensor E = mapL f g := by ext; simp [← LinearMap.rTensor_comp_lTensor] @[simp] theorem adjoint_mapL [CompleteSpace E] [CompleteSpace G] [CompleteSpace (E ⊗[𝕜] G)] [CompleteSpace F] [CompleteSpace H] [CompleteSpace (F ⊗[𝕜] H)] From c1b07a9c0d803d6b869b59f0e61cf46a5368f79b Mon Sep 17 00:00:00 2001 From: TJHeeringa Date: Tue, 9 Jun 2026 14:21:39 +0200 Subject: [PATCH 36/39] Fix space, simplified proof --- Mathlib/Analysis/InnerProductSpace/TensorProduct.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean index 14ab7bd00c413f..d2308458331455 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -430,7 +430,7 @@ noncomputable def rTensor (f : E →L[𝕜] F) : (E ⊗[𝕜] G) →L[𝕜] (F (f.toLinearMap.rTensor G).mkContinuous ‖f‖ fun x ↦ by /- Any tensor `x` can be written as a linear combination of pure tensors, `x = ∑ e n ⊗ₜ g n`. This - induces three Gram matrices, one based on `e`, one on `f ∘ e` and one on `g`. Up to a constant, + induces three Gram matrices, one based on `e`, one on `f ∘ e` and one on `g`. Up to a constant, the `e`-based Gram matrix is larger than the `f ∘ e`-based one. This implies the existence of a matrix, whose form is used to show that `‖f‖ ^ 2 * ‖x‖ ^ 2 - ‖f x‖ ^ 2` is a sum of nonnegative terms. @@ -639,7 +639,7 @@ theorem _root_.ContinuousLinearMap.lTensor_eq_mapL (g : G →L[𝕜] H) : f.lTensor H ∘L g.rTensor E = mapL g f := by ext; simp [← LinearMap.lTensor_comp_rTensor] @[simp] lemma _root_.ContinuousLinearMap.rTensor_comp_lTensor (f : E →L[𝕜] F) (g : G →L[𝕜] H) : - f.rTensor H ∘L g.lTensor E = mapL f g := by ext; simp [← LinearMap.rTensor_comp_lTensor] + f.rTensor H ∘L g.lTensor E = mapL f g := rfl @[simp] theorem adjoint_mapL [CompleteSpace E] [CompleteSpace G] [CompleteSpace (E ⊗[𝕜] G)] [CompleteSpace F] [CompleteSpace H] [CompleteSpace (F ⊗[𝕜] H)] From 2b7d5f7668135e673900bafe25e377174845da63 Mon Sep 17 00:00:00 2001 From: TJHeeringa Date: Sat, 20 Jun 2026 15:22:32 +0200 Subject: [PATCH 37/39] Add ContinuousLinearEquiv.ofContinuousLinearMap --- Mathlib/Topology/Algebra/Module/Equiv.lean | 34 ++++++++++++++++++++++ 1 file changed, 34 insertions(+) diff --git a/Mathlib/Topology/Algebra/Module/Equiv.lean b/Mathlib/Topology/Algebra/Module/Equiv.lean index afc135bda2246b..6047fb955e2932 100644 --- a/Mathlib/Topology/Algebra/Module/Equiv.lean +++ b/Mathlib/Topology/Algebra/Module/Equiv.lean @@ -342,6 +342,40 @@ initialize_simps_projections ContinuousLinearEquiv (toFun → apply, invFun → theorem symm_map_nhds_eq (e : M₁ ≃SL[σ₁₂] M₂) (x : M₁) : map e.symm (𝓝 (e x)) = 𝓝 x := e.toHomeomorph.symm_map_nhds_eq x +section + +variable (f : M₁ →SL[σ₁₂] M₂) (g : M₂ →SL[σ₂₁] M₁) + +/-- If a continuous linear map has a continuous inverse, it is a continuous linear equivalence. -/ +def ofContinuousLinear (h₁ : f.comp g = ContinuousLinearMap.id R₂ M₂) + (h₂ : g.comp f = ContinuousLinearMap.id R₁ M₁) : M₁ ≃SL[σ₁₂] M₂ := + { f with + invFun := g + left_inv := ContinuousLinearMap.ext_iff.1 h₂ + right_inv := ContinuousLinearMap.ext_iff.1 h₁ } + +@[simp] +theorem ofContinuousLinear_apply {h₁ h₂} (x : M₁) : + (ofContinuousLinear f g h₁ h₂ : M₁ ≃SL[σ₁₂] M₂) x = f x := + rfl + +@[simp] +theorem ofContinuousLinear_symm_apply {h₁ h₂} (x : M₂) : + (ofContinuousLinear f g h₁ h₂ : M₁ ≃SL[σ₁₂] M₂).symm x = g x := + rfl + +@[simp] +theorem ofContinuousLinear_toLinearMap {h₁ h₂} : + (ofContinuousLinear f g h₁ h₂ : M₁ ≃SL[σ₁₂] M₂) = f := + rfl + +@[simp] +theorem ofContinuousLinear_symm_toContinuousLinearMap {h₁ h₂} : + (ofContinuousLinear f g h₁ h₂ : M₁ ≃SL[σ₁₂] M₂).symm = g := + rfl + +end + /-- The composition of two continuous linear equivalences as a continuous linear equivalence. -/ @[trans] protected def trans (e₁ : M₁ ≃SL[σ₁₂] M₂) (e₂ : M₂ ≃SL[σ₂₃] M₃) : M₁ ≃SL[σ₁₃] M₃ where From e8edc76d40857d11a0b800b56d0a521019c06a1c Mon Sep 17 00:00:00 2001 From: TJHeeringa Date: Sat, 20 Jun 2026 17:41:52 +0200 Subject: [PATCH 38/39] Add tensorProduct_congrL --- .../InnerProductSpace/TensorProduct.lean | 64 +++++++++++++++++++ 1 file changed, 64 insertions(+) diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean index e2360e5c1d9801..954d327b97d812 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -10,6 +10,7 @@ public import Mathlib.LinearAlgebra.TensorProduct.Finiteness public import Mathlib.RingTheory.TensorProduct.Finite import Mathlib.Analysis.InnerProductSpace.GramMatrix import Mathlib.Analysis.InnerProductSpace.Positive +import Mathlib.Topology.Algebra.Module.Equiv /-! @@ -36,6 +37,7 @@ inner product spaces. * `TensorProduct.assocIsometry`: the linear isometry version of `TensorProduct.assoc`. * `TensorProduct.mapL`: the continuous version of `TensorProduct.map f g` when `f` and `g` are continuous linear maps. + `TensorProduct.congrL f g` the continuous version of `TensorProduct.congr f g`. * `OrthonormalBasis.tensorProduct`: the orthonormal basis of the tensor product of two orthonormal bases. @@ -667,6 +669,68 @@ open LinearMap [FiniteDimensional 𝕜 G] (f : E →ₗ[𝕜] F) : (f.lTensor G).adjoint = f.adjoint.lTensor G := by simp [lTensor] +/-- If `M` and `P` are semilinearly equivalent and `N` and `Q` are semilinearly equivalent +then `M ⊗ N` and `P ⊗ Q` are semilinearly equivalent. -/ +noncomputable def congrL (f : E ≃L[𝕜] F) (g : G ≃L[𝕜] H) : E ⊗[𝕜] G ≃L[𝕜] F ⊗[𝕜] H := + ContinuousLinearEquiv.ofContinuousLinear (mapL f g) (mapL f.symm g.symm) + (by ext; simp [← mapL_comp]) + (by ext; simp [← mapL_comp]) + +@[simp] +theorem congrL_tmul (f : E ≃L[𝕜] F) (g : G ≃L[𝕜] H) (x : E) (y : G) : + congrL f g (x ⊗ₜ y) = f x ⊗ₜ g y := + rfl + +@[simp] +theorem congrL_symm_tmul (f : E ≃L[𝕜] F) (g : G ≃L[𝕜] H) (x : F) (y : H) : + (congrL f g).symm (x ⊗ₜ y) = f.symm x ⊗ₜ g.symm y := + rfl + +theorem congrL_symm (f : E ≃L[𝕜] F) (g : G ≃L[𝕜] H) : + (congrL f g).symm = congrL f.symm g.symm := + rfl + +@[simp] +lemma toContinuousLinearMap_congrL (f : E ≃L[𝕜] F) (g : G ≃L[𝕜] H) : + (congrL f g).toContinuousLinearMap = mapL f g := + rfl + +@[simp] +lemma toLinearMap_congrL (f : E ≃L[𝕜] F) (g : G ≃L[𝕜] H) : (congrL f g).toLinearMap = map f g := by + ext; simp + +@[simp] +theorem congrL_refl_refl : congrL (.refl 𝕜 E) (.refl 𝕜 G) = .refl 𝕜 _ := + ContinuousLinearEquiv.toLinearEquiv_injective <| (by simp [congrL]; rfl) + +section congr_congr +variable {F₂ H₂ : Type*} [NormedAddCommGroup F₂] [InnerProductSpace 𝕜 F₂] [NormedAddCommGroup H₂] + [InnerProductSpace 𝕜 H₂] (f₂ : F ≃L[𝕜] F₂) (g₂ : H ≃L[𝕜] H₂) (f₁ : E ≃L[𝕜] F) (g₁ : G ≃L[𝕜] H) + +theorem congrL_trans : congrL (f₁.trans f₂) (g₁.trans g₂) = (congrL f₁ g₁).trans (congrL f₂ g₂) := + ContinuousLinearEquiv.toLinearEquiv_injective <| (by ext; simp [congrL, map_map]) + +theorem congrL_congr (x : E ⊗[𝕜] G) : + congrL f₂ g₂ (congrL f₁ g₁ x) = congrL (f₁.trans f₂) (g₁.trans g₂) x := + DFunLike.congr_fun (congrL_trans ..).symm x + +end congr_congr + +theorem congrL_mul (f : E ≃L[𝕜] E) (g : G ≃L[𝕜] G) (f' : E ≃L[𝕜] E) (g' : G ≃L[𝕜] G) : + congrL (f * f') (g * g') = congrL f g * congrL f' g' := congrL_trans .. + +@[simp] theorem congrL_pow (f : E ≃L[𝕜] E) (g : G ≃L[𝕜] G) (n : ℕ) : + congrL f g ^ n = congrL (f ^ n) (g ^ n) := by + induction n with + | zero => exact congrL_refl_refl.symm + | succ n ih => simp_rw [pow_succ, ih, congrL_mul] + +@[simp] theorem congrL_zpow (f : E ≃L[𝕜] E) (g : G ≃L[𝕜] G) (n : ℤ) : + congrL f g ^ n = congrL (f ^ n) (g ^ n) := by + cases n with + | ofNat n => exact congrL_pow _ _ _ + | negSucc n => simp_rw [zpow_negSucc, congrL_pow]; exact congrL_symm _ _ + /-- Given `x, y : E ⊗ (F ⊗ G)`, `x = y` iff `⟪x, a ⊗ₜ (b ⊗ₜ c)⟫ = ⟪y, a ⊗ₜ (b ⊗ₜ c)⟫` for all `a, b, c`. From e2feb2851b93df17920ae1efaed09d0707216b15 Mon Sep 17 00:00:00 2001 From: TJHeeringa Date: Sat, 20 Jun 2026 17:49:12 +0200 Subject: [PATCH 39/39] Update congrL docstring --- Mathlib/Analysis/InnerProductSpace/TensorProduct.lean | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean index 954d327b97d812..8a304a199f0035 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -669,8 +669,8 @@ open LinearMap [FiniteDimensional 𝕜 G] (f : E →ₗ[𝕜] F) : (f.lTensor G).adjoint = f.adjoint.lTensor G := by simp [lTensor] -/-- If `M` and `P` are semilinearly equivalent and `N` and `Q` are semilinearly equivalent -then `M ⊗ N` and `P ⊗ Q` are semilinearly equivalent. -/ +/-- If `E` and `F` are continuously and linearly equivalent and `G` and `H` are continuously and +linearly equivalent, then `E ⊗ G` and `F ⊗ H` are continuously and linearly equivalent. -/ noncomputable def congrL (f : E ≃L[𝕜] F) (g : G ≃L[𝕜] H) : E ⊗[𝕜] G ≃L[𝕜] F ⊗[𝕜] H := ContinuousLinearEquiv.ofContinuousLinear (mapL f g) (mapL f.symm g.symm) (by ext; simp [← mapL_comp]) @@ -719,13 +719,15 @@ end congr_congr theorem congrL_mul (f : E ≃L[𝕜] E) (g : G ≃L[𝕜] G) (f' : E ≃L[𝕜] E) (g' : G ≃L[𝕜] G) : congrL (f * f') (g * g') = congrL f g * congrL f' g' := congrL_trans .. -@[simp] theorem congrL_pow (f : E ≃L[𝕜] E) (g : G ≃L[𝕜] G) (n : ℕ) : +@[simp] +theorem congrL_pow (f : E ≃L[𝕜] E) (g : G ≃L[𝕜] G) (n : ℕ) : congrL f g ^ n = congrL (f ^ n) (g ^ n) := by induction n with | zero => exact congrL_refl_refl.symm | succ n ih => simp_rw [pow_succ, ih, congrL_mul] -@[simp] theorem congrL_zpow (f : E ≃L[𝕜] E) (g : G ≃L[𝕜] G) (n : ℤ) : +@[simp] +theorem congrL_zpow (f : E ≃L[𝕜] E) (g : G ≃L[𝕜] G) (n : ℤ) : congrL f g ^ n = congrL (f ^ n) (g ^ n) := by cases n with | ofNat n => exact congrL_pow _ _ _