From 843b4600aa7f9116f287bda7b8275485e43c271b Mon Sep 17 00:00:00 2001 From: yuanyi-350 Date: Mon, 20 Apr 2026 14:10:45 +0800 Subject: [PATCH 1/6] refactor(Analysis): golf Normed Operator Mul --- Mathlib/Analysis/Normed/Operator/Mul.lean | 17 ++++------------- 1 file changed, 4 insertions(+), 13 deletions(-) diff --git a/Mathlib/Analysis/Normed/Operator/Mul.lean b/Mathlib/Analysis/Normed/Operator/Mul.lean index a7a789021e55a6..4ed36b9561d0f8 100644 --- a/Mathlib/Analysis/Normed/Operator/Mul.lean +++ b/Mathlib/Analysis/Normed/Operator/Mul.lean @@ -158,24 +158,15 @@ variable (𝕜 E) /-- If `M` is a normed space over `𝕜`, then the space of maps `𝕜 →L[𝕜] M` is linearly equivalent to `M`. (See `ring_lmap_equiv_self` for a stronger statement.) -/ -def ring_lmap_equiv_selfₗ : (𝕜 →L[𝕜] E) ≃ₗ[𝕜] E where - toFun := fun f ↦ f 1 - invFun := (ContinuousLinearMap.id 𝕜 𝕜).smulRight - map_smul' := fun a f ↦ by simp only [coe_smul', Pi.smul_apply, RingHom.id_apply] - map_add' := fun f g ↦ by simp only [add_apply] - left_inv := fun f ↦ by ext; simp only [smulRight_apply, coe_id', _root_.id, one_smul] - right_inv := fun m ↦ by simp only [smulRight_apply, id_apply, one_smul] +def ring_lmap_equiv_selfₗ : (𝕜 →L[𝕜] E) ≃ₗ[𝕜] E := + (ContinuousLinearMap.toSpanSingletonLE 𝕜 𝕜 E).symm /-- If `M` is a normed space over `𝕜`, then the space of maps `𝕜 →L[𝕜] M` is linearly isometrically equivalent to `M`. -/ def ring_lmap_equiv_self : (𝕜 →L[𝕜] E) ≃ₗᵢ[𝕜] E where toLinearEquiv := ring_lmap_equiv_selfₗ 𝕜 E - norm_map' := by - refine fun f ↦ le_antisymm ?_ ?_ - · simpa only [norm_one, mul_one] using le_opNorm f 1 - · refine opNorm_le_bound' f (norm_nonneg <| f 1) (fun x _ ↦ ?_) - rw [(by rw [smul_eq_mul, mul_one] : f x = f (x • 1)), map_smul, - norm_smul, mul_comm, (by rfl : ring_lmap_equiv_selfₗ 𝕜 E f = f 1)] + norm_map' f := by + simpa using (ContinuousLinearMap.norm_toSpanSingleton (𝕜 := 𝕜) (x := f 1)).symm end RingEquiv From 5b781adc94b56eeff780a6737d8f5f1bfc1e4674 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Thu, 23 Apr 2026 08:48:44 +0800 Subject: [PATCH 2/6] apply suggestions --- Mathlib/Analysis/Normed/Operator/Mul.lean | 30 +++++++++++++------ .../Topology/Algebra/Module/LinearMap.lean | 3 +- 2 files changed, 23 insertions(+), 10 deletions(-) diff --git a/Mathlib/Analysis/Normed/Operator/Mul.lean b/Mathlib/Analysis/Normed/Operator/Mul.lean index 4ed36b9561d0f8..188a8be2740697 100644 --- a/Mathlib/Analysis/Normed/Operator/Mul.lean +++ b/Mathlib/Analysis/Normed/Operator/Mul.lean @@ -156,17 +156,29 @@ section RingEquiv variable (𝕜 E) -/-- If `M` is a normed space over `𝕜`, then the space of maps `𝕜 →L[𝕜] M` is linearly equivalent -to `M`. (See `ring_lmap_equiv_self` for a stronger statement.) -/ -def ring_lmap_equiv_selfₗ : (𝕜 →L[𝕜] E) ≃ₗ[𝕜] E := - (ContinuousLinearMap.toSpanSingletonLE 𝕜 𝕜 E).symm - /-- If `M` is a normed space over `𝕜`, then the space of maps `𝕜 →L[𝕜] M` is linearly isometrically equivalent to `M`. -/ -def ring_lmap_equiv_self : (𝕜 →L[𝕜] E) ≃ₗᵢ[𝕜] E where - toLinearEquiv := ring_lmap_equiv_selfₗ 𝕜 E - norm_map' f := by - simpa using (ContinuousLinearMap.norm_toSpanSingleton (𝕜 := 𝕜) (x := f 1)).symm +@[simp] +def toSpanSingletonₗᵢ : E ≃ₗᵢ[𝕜] (𝕜 →L[𝕜] E) where + toLinearEquiv := toSpanSingletonLE 𝕜 𝕜 E + norm_map' _ := by simp + +lemma toSpanSingletonₗᵢ_apply (x : E) : toSpanSingletonₗᵢ 𝕜 E x = toSpanSingletonLE 𝕜 𝕜 E x := by + simp + +lemma toSpanSingletonₗᵢ_symm_apply (f : 𝕜 →L[𝕜] E) : + (toSpanSingletonₗᵢ 𝕜 E).symm f = (toSpanSingletonLE 𝕜 𝕜 E).symm f := + Eq.symm (DFunLike.congr_fun rfl f) + +lemma toSpanSingletonₗᵢ_toLinearEquiv : + (toSpanSingletonₗᵢ 𝕜 E).toLinearEquiv = toSpanSingletonLE 𝕜 𝕜 E := by + simp + +@[deprecated (since := "2026-04-23")] +alias ring_lmap_equiv_selfₗ := toSpanSingletonLE + +@[deprecated (since := "2026-04-23")] +alias ring_lmap_equiv_self := toSpanSingletonₗᵢ end RingEquiv diff --git a/Mathlib/Topology/Algebra/Module/LinearMap.lean b/Mathlib/Topology/Algebra/Module/LinearMap.lean index f7860d68752d09..c5e039d7c354ef 100644 --- a/Mathlib/Topology/Algebra/Module/LinearMap.lean +++ b/Mathlib/Topology/Algebra/Module/LinearMap.lean @@ -1096,7 +1096,8 @@ variable (R S M : Type*) [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M [SMulCommClass R S M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousConstSMul S M] [TopologicalSpace R] [ContinuousSMul R M] -/-- `ContinuousLinearMap.toSpanSingleton` as a linear equivalence. -/ +/-- `ContinuousLinearMap.toSpanSingleton` as a linear equivalence. See +`ContinuousLinearMap.toSpanSingletonₗᵢ` for a stronger statement. -/ @[simps -fullyApplied] def toSpanSingletonLE : M ≃ₗ[S] (R →L[R] M) where toFun := toSpanSingleton R From 78d08d0722953df4ec728d5c37829d28af2d6790 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Thu, 23 Apr 2026 09:12:50 +0800 Subject: [PATCH 3/6] fix ci --- Mathlib/Analysis/Fourier/FourierTransformDeriv.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean b/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean index 0a786f27805b91..a7043e8176fb59 100644 --- a/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean +++ b/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean @@ -795,8 +795,8 @@ lemma hasDerivAt_fourier have h_int : Integrable fun v ↦ fourierSMulRight L f v := by suffices Integrable fun v ↦ ContinuousLinearMap.smulRight (L v) (f v) by simpa only [fourierSMulRight, neg_smul, neg_mul, Pi.smul_apply] using this.smul (-2 * π * I) - convert ((ContinuousLinearMap.ring_lmap_equiv_self ℝ - E).symm.toContinuousLinearEquiv.toContinuousLinearMap).integrable_comp hf' using 2 with _ v + convert ((ContinuousLinearMap.toSpanSingletonₗᵢ ℝ + E).toContinuousLinearEquiv.toContinuousLinearMap).integrable_comp hf' using 2 with _ v apply ContinuousLinearMap.ext_ring rw [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.flip_apply, ContinuousLinearMap.mul_apply', one_mul, map_smul] From 01f8ae8dd2a1d636c0552d0ed133ed2bf0705399 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Thu, 23 Apr 2026 18:22:02 +0800 Subject: [PATCH 4/6] Apply suggestions from code review Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com> --- Mathlib/Analysis/Normed/Operator/Mul.lean | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) diff --git a/Mathlib/Analysis/Normed/Operator/Mul.lean b/Mathlib/Analysis/Normed/Operator/Mul.lean index 188a8be2740697..f83ec4ad788c4c 100644 --- a/Mathlib/Analysis/Normed/Operator/Mul.lean +++ b/Mathlib/Analysis/Normed/Operator/Mul.lean @@ -158,21 +158,18 @@ variable (𝕜 E) /-- If `M` is a normed space over `𝕜`, then the space of maps `𝕜 →L[𝕜] M` is linearly isometrically equivalent to `M`. -/ -@[simp] def toSpanSingletonₗᵢ : E ≃ₗᵢ[𝕜] (𝕜 →L[𝕜] E) where toLinearEquiv := toSpanSingletonLE 𝕜 𝕜 E norm_map' _ := by simp -lemma toSpanSingletonₗᵢ_apply (x : E) : toSpanSingletonₗᵢ 𝕜 E x = toSpanSingletonLE 𝕜 𝕜 E x := by - simp +@[simp] +lemma toSpanSingletonₗᵢ_apply (x : E) : toSpanSingletonₗᵢ 𝕜 E x = toSpanSingleton 𝕜 x := rfl -lemma toSpanSingletonₗᵢ_symm_apply (f : 𝕜 →L[𝕜] E) : - (toSpanSingletonₗᵢ 𝕜 E).symm f = (toSpanSingletonLE 𝕜 𝕜 E).symm f := - Eq.symm (DFunLike.congr_fun rfl f) +@[simp] lemma toSpanSingletonₗᵢ_symm_apply (f : 𝕜 →L[𝕜] E) : + (toSpanSingletonₗᵢ 𝕜 E).symm f = f 1 := rfl -lemma toSpanSingletonₗᵢ_toLinearEquiv : - (toSpanSingletonₗᵢ 𝕜 E).toLinearEquiv = toSpanSingletonLE 𝕜 𝕜 E := by - simp +@[simp] lemma toLinearEquiv_toSpanSingletonₗᵢ : + (toSpanSingletonₗᵢ 𝕜 E).toLinearEquiv = toSpanSingletonLE 𝕜 𝕜 E := rfl @[deprecated (since := "2026-04-23")] alias ring_lmap_equiv_selfₗ := toSpanSingletonLE From 1ae1e9ed5b66d0e2fc619f1a115680769764bcde Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Fri, 24 Apr 2026 14:31:23 +0800 Subject: [PATCH 5/6] Apply suggestion from @themathqueen Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com> --- Mathlib/Analysis/Normed/Operator/Mul.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Mathlib/Analysis/Normed/Operator/Mul.lean b/Mathlib/Analysis/Normed/Operator/Mul.lean index f83ec4ad788c4c..72d5581da8a1ce 100644 --- a/Mathlib/Analysis/Normed/Operator/Mul.lean +++ b/Mathlib/Analysis/Normed/Operator/Mul.lean @@ -170,6 +170,9 @@ lemma toSpanSingletonₗᵢ_apply (x : E) : toSpanSingletonₗᵢ 𝕜 E x = toS @[simp] lemma toLinearEquiv_toSpanSingletonₗᵢ : (toSpanSingletonₗᵢ 𝕜 E).toLinearEquiv = toSpanSingletonLE 𝕜 𝕜 E := rfl + +@[simp] lemma toContinuousLinearEquiv_toSpanSingletonₗᵢ : + (toSpanSingletonₗᵢ 𝕜 E).toContinuousLinearEquiv = toSpanSingletonCLE := rfl @[deprecated (since := "2026-04-23")] alias ring_lmap_equiv_selfₗ := toSpanSingletonLE From 27d21aa2590ae1f9f93a5546cedbc54a5b455911 Mon Sep 17 00:00:00 2001 From: "pre-commit-ci-lite[bot]" <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> Date: Fri, 24 Apr 2026 06:32:05 +0000 Subject: [PATCH 6/6] [pre-commit.ci lite] apply automatic fixes --- Mathlib/Analysis/Normed/Operator/Mul.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/Normed/Operator/Mul.lean b/Mathlib/Analysis/Normed/Operator/Mul.lean index 72d5581da8a1ce..108957e121171d 100644 --- a/Mathlib/Analysis/Normed/Operator/Mul.lean +++ b/Mathlib/Analysis/Normed/Operator/Mul.lean @@ -170,7 +170,7 @@ lemma toSpanSingletonₗᵢ_apply (x : E) : toSpanSingletonₗᵢ 𝕜 E x = toS @[simp] lemma toLinearEquiv_toSpanSingletonₗᵢ : (toSpanSingletonₗᵢ 𝕜 E).toLinearEquiv = toSpanSingletonLE 𝕜 𝕜 E := rfl - + @[simp] lemma toContinuousLinearEquiv_toSpanSingletonₗᵢ : (toSpanSingletonₗᵢ 𝕜 E).toContinuousLinearEquiv = toSpanSingletonCLE := rfl