From 5a25d459cb107fab61e7650c44df92e22167b5bf Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Mon, 13 Apr 2026 10:18:17 +0800 Subject: [PATCH 1/5] Merge branch 'golf_27' --- .../Analysis/BoxIntegral/Partition/Split.lean | 8 ++--- .../Isometric.lean | 12 ++----- .../ContinuousFunctionalCalculus/Order.lean | 32 ++++++------------- .../ContinuousFunctionalCalculus/Range.lean | 22 ++++--------- .../Analysis/CStarAlgebra/Exponential.lean | 15 +++------ .../Analysis/CStarAlgebra/Module/Synonym.lean | 12 +++---- Mathlib/Analysis/CStarAlgebra/Spectrum.lean | 8 ++--- 7 files changed, 30 insertions(+), 79 deletions(-) diff --git a/Mathlib/Analysis/BoxIntegral/Partition/Split.lean b/Mathlib/Analysis/BoxIntegral/Partition/Split.lean index 64048745bab0a2..dee1534aca942e 100644 --- a/Mathlib/Analysis/BoxIntegral/Partition/Split.lean +++ b/Mathlib/Analysis/BoxIntegral/Partition/Split.lean @@ -187,12 +187,8 @@ theorem sum_split_boxes {M : Type*} [AddCommMonoid M] (I : Box ι) (i : ι) (x : /-- If `x ∉ (I.lower i, I.upper i)`, then the hyperplane `{y | y i = x}` does not split `I`. -/ theorem split_of_notMem_Ioo (h : x ∉ Ioo (I.lower i) (I.upper i)) : split I i x = ⊤ := by refine ((isPartitionTop I).eq_of_boxes_subset fun J hJ => ?_).symm - rcases mem_top.1 hJ with rfl; clear hJ - rw [mem_boxes, mem_split_iff] - rw [mem_Ioo, not_and_or, not_lt, not_lt] at h - cases h <;> [right; left] - · rwa [eq_comm, Box.splitUpper_eq_self] - · rwa [eq_comm, Box.splitLower_eq_self] + rcases mem_top.1 hJ with rfl + grind [Box.splitUpper_eq_self, Box.splitLower_eq_self, mem_boxes, mem_split_iff, not_lt] theorem coe_eq_of_mem_split_of_mem_le {y : ι → ℝ} (h₁ : J ∈ split I i x) (h₂ : y ∈ J) (h₃ : y i ≤ x) : (J : Set (ι → ℝ)) = ↑I ∩ { y | y i ≤ x } := by diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean index f95ff5e2884ecd..5fc929c0bfb683 100644 --- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean +++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean @@ -458,11 +458,7 @@ lemma IsGreatest.nnnorm_cfc_nnreal [Nontrivial A] (f : ℝ≥0 → ℝ≥0) (a : convert IsGreatest.nnnorm_cfc (fun x : ℝ ↦ (f x.toNNReal : ℝ)) a ?hf_cont case hf_cont => exact continuous_subtype_val.comp_continuousOn <| ContinuousOn.comp ‹_› continuous_real_toNNReal.continuousOn <| ha'.image ▸ Set.mapsTo_image .. - ext x - constructor - all_goals rintro ⟨x, hx, rfl⟩ - · exact ⟨x, spectrum.algebraMap_mem ℝ hx, by simp⟩ - · exact ⟨x.toNNReal, ha'.apply_mem hx, by simp⟩ + simp [Set.image_image, ← ha'.image] lemma apply_le_nnnorm_cfc_nnreal (f : ℝ≥0 → ℝ≥0) (a : A) ⦃x : ℝ≥0⦄ (hx : x ∈ σ ℝ≥0 a) (hf : ContinuousOn f (σ ℝ≥0 a) := by cfc_cont_tac) (ha : 0 ≤ a := by cfc_tac) : @@ -536,11 +532,7 @@ lemma IsGreatest.nnnorm_cfcₙ_nnreal (f : ℝ≥0 → ℝ≥0) (a : A) convert IsGreatest.nnnorm_cfcₙ (fun x : ℝ ↦ (f x.toNNReal : ℝ)) a ?hf_cont (by simpa) case hf_cont => exact continuous_subtype_val.comp_continuousOn <| ContinuousOn.comp ‹_› continuous_real_toNNReal.continuousOn <| ha'.image ▸ Set.mapsTo_image .. - ext x - constructor - all_goals rintro ⟨x, hx, rfl⟩ - · exact ⟨x, quasispectrum.algebraMap_mem ℝ hx, by simp⟩ - · exact ⟨x.toNNReal, ha'.apply_mem hx, by simp⟩ + simp [Set.image_image, ← ha'.image] lemma apply_le_nnnorm_cfcₙ_nnreal (f : ℝ≥0 → ℝ≥0) (a : A) ⦃x : ℝ≥0⦄ (hx : x ∈ σₙ ℝ≥0 a) (hf : ContinuousOn f (σₙ ℝ≥0 a) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean index d2c1d46f0f2fcd..aa2ab470e02e56 100644 --- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean +++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean @@ -292,15 +292,11 @@ lemma CFC.conjugate_rpow_neg_one_half (a : A) (ha : IsStrictlyPositive a := by c invertible. -/ lemma CStarAlgebra.isUnit_of_le (a : A) {b : A} (hab : a ≤ b) (h : IsStrictlyPositive a := by cfc_tac) : IsUnit b := by - have h₀ := h.isUnit - have ha := h.nonneg - rw [← spectrum.zero_notMem_iff ℝ≥0] at h₀ ⊢ - nontriviality A - have hb := (show 0 ≤ a from ha).trans hab - rw [zero_notMem_iff, SpectrumRestricts.nnreal_lt_iff (.nnreal_of_nonneg ‹_›), - NNReal.coe_zero, ← CFC.exists_pos_algebraMap_le_iff (.of_nonneg ‹_›)] at h₀ ⊢ - peel h₀ with r hr _ - exact this.trans hab + nontriviality A; rw [← spectrum.zero_notMem_iff ℝ]; intro h0 + obtain ⟨r, hr, hr_le⟩ := (CFC.exists_pos_algebraMap_le_iff h.isSelfAdjoint).2 fun x hx ↦ + h.spectrum_pos hx + exact not_le_of_gt hr ((algebraMap_le_iff_le_spectrum (a := b) (ha := .of_nonneg + (h.nonneg.trans hab))).1 (hr_le.trans hab) 0 h0) lemma le_iff_norm_sqrt_mul_rpow (a b : A) (ha : 0 ≤ a := by cfc_tac) (hb : IsStrictlyPositive b := by cfc_tac) : @@ -441,23 +437,13 @@ instance instNonnegSpectrumClassComplexNonUnital : NonnegSpectrumClass ℂ A whe lemma norm_le_norm_of_nonneg_of_le {a b : A} (ha : 0 ≤ a := by cfc_tac) (hab : a ≤ b) : ‖a‖ ≤ ‖b‖ := by suffices ∀ a b : A⁺¹, 0 ≤ a → a ≤ b → ‖a‖ ≤ ‖b‖ by - have hb := ha.trans hab + have hb : 0 ≤ b := ha.trans hab simpa only [ge_iff_le, Unitization.norm_inr] using - this a b (by simpa) (by rwa [Unitization.inr_le_iff a b]) + this a b (by simpa) (by rwa [Unitization.inr_le_iff a b (.of_nonneg ha) (.of_nonneg hb)]) intro a b ha hab have hb : 0 ≤ b := ha.trans hab - -- these two `have`s are just for performance - have := IsSelfAdjoint.of_nonneg ha; have := IsSelfAdjoint.of_nonneg hb - have h₂ : cfc (id : ℝ → ℝ) a ≤ cfc (fun _ => ‖b‖) a := by - calc _ = a := by rw [cfc_id ℝ a] - _ ≤ cfc id b := (cfc_id ℝ b) ▸ hab - _ ≤ cfc (fun _ => ‖b‖) b := by - refine cfc_mono fun x hx => ?_ - calc x = ‖x‖ := (Real.norm_of_nonneg (spectrum_nonneg_of_nonneg hb hx)).symm - _ ≤ ‖b‖ := spectrum.norm_le_norm_of_mem hx - _ = _ := by rw [cfc_const _ _, cfc_const _ _] - rw [cfc_le_iff id (fun _ => ‖b‖) a] at h₂ - exact h₂ ‖a‖ <| norm_mem_spectrum_of_nonneg ha + exact (CStarAlgebra.norm_le_iff_le_algebraMap a (norm_nonneg _) ha).2 <| + hab.trans <| IsSelfAdjoint.le_algebraMap_norm_self (.of_nonneg hb) theorem nnnorm_le_nnnorm_of_nonneg_of_le {a : A} {b : A} (ha : 0 ≤ a := by cfc_tac) (hab : a ≤ b) : ‖a‖₊ ≤ ‖b‖₊ := diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Range.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Range.lean index d402b443a6ad3f..ecc3522cb35215 100644 --- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Range.lean +++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Range.lean @@ -136,13 +136,9 @@ lemma range_cfc_nnreal rw [range_cfc_nnreal_eq_image_cfc_real a ha, Set.setOf_and, SetLike.setOf_mem_eq, ← range_cfc _ ha.isSelfAdjoint, Set.inter_comm, ← Set.image_preimage_eq_inter_range] rintro _ ⟨f, hf, rfl⟩ - simp only [Set.preimage_setOf_eq, Set.mem_setOf_eq, Set.mem_image] at hf ⊢ - obtain (⟨h₁, h₂⟩ | h | h) := by - simpa only [not_and_or] using em (ContinuousOn f (spectrum ℝ a) ∧ IsSelfAdjoint a) - · refine ⟨f, ?_, rfl⟩ - rwa [cfc_nonneg_iff f a] at hf - · exact ⟨0, by simp, by simp [cfc_apply_of_not_continuousOn a h]⟩ - · exact ⟨0, by simp, by simp [cfc_apply_of_not_predicate a h]⟩ + exact cfc_cases (p := IsSelfAdjoint) _ a f ⟨0, by simp, by simp⟩ fun hf' ha' ↦ + ⟨f, (cfc_nonneg_iff f a hf' ha').mp (by simpa [Set.mem_preimage, Set.mem_setOf_eq] using hf), + by simp [cfc_apply f a ha' hf']⟩ end Unital @@ -253,14 +249,8 @@ lemma range_cfcₙ_nnreal [NonUnitalClosedEmbeddingContinuousFunctionalCalculus ← range_cfcₙ _ ha.isSelfAdjoint, Set.inter_comm, ← Set.image_preimage_eq_inter_range] refine Set.Subset.antisymm (Set.image_mono (fun _ ↦ cfcₙ_nonneg)) ?_ rintro _ ⟨f, hf, rfl⟩ - simp only [Set.preimage_setOf_eq, Set.mem_setOf_eq, Set.mem_image] at hf ⊢ - obtain (⟨h₁, h₂, h₃⟩ | h | h | h) := by - simpa only [not_and_or] using - em (ContinuousOn f (quasispectrum ℝ a) ∧ f 0 = 0 ∧ IsSelfAdjoint a) - · refine ⟨f, ?_, rfl⟩ - rwa [cfcₙ_nonneg_iff f a] at hf - · exact ⟨0, by simp, by simp [cfcₙ_apply_of_not_continuousOn a h]⟩ - · exact ⟨0, by simp, by simp [cfcₙ_apply_of_not_map_zero a h]⟩ - · exact ⟨0, by simp, by simp [cfcₙ_apply_of_not_predicate a h]⟩ + exact cfcₙ_cases (p := IsSelfAdjoint) _ a f ⟨0, by simp, by simp⟩ fun hf' h0 ha' ↦ + ⟨f, (cfcₙ_nonneg_iff f a hf' h0 ha').mp + (by simpa [Set.mem_preimage, Set.mem_setOf_eq] using hf), by simp [cfcₙ_apply f a hf' h0 ha']⟩ end NonUnital diff --git a/Mathlib/Analysis/CStarAlgebra/Exponential.lean b/Mathlib/Analysis/CStarAlgebra/Exponential.lean index 2bef6805c902c6..f5f709d3b023ff 100644 --- a/Mathlib/Analysis/CStarAlgebra/Exponential.lean +++ b/Mathlib/Analysis/CStarAlgebra/Exponential.lean @@ -55,17 +55,12 @@ lemma selfAdjoint.continuous_expUnitary : Continuous (expUnitary : selfAdjoint A theorem Commute.expUnitary_add {a b : selfAdjoint A} (h : Commute (a : A) (b : A)) : expUnitary (a + b) = expUnitary a * expUnitary b := by let +nondep : NormedAlgebra ℚ A := .restrictScalars ℚ ℂ A - ext - have hcomm : Commute (I • (a : A)) (I • (b : A)) := by - unfold Commute SemiconjBy - simp only [h.eq, Algebra.smul_mul_assoc, Algebra.mul_smul_comm] - simpa only [expUnitary_coe, AddSubgroup.coe_add, smul_add] using exp_add_of_commute hcomm + simpa only [Subtype.ext_iff, expUnitary_coe, AddSubgroup.coe_add, smul_add] using + exp_add_of_commute ((h.smul_left I).smul_right I) theorem Commute.expUnitary {a b : selfAdjoint A} (h : Commute (a : A) (b : A)) : - Commute (expUnitary a) (expUnitary b) := - calc - selfAdjoint.expUnitary a * selfAdjoint.expUnitary b = - selfAdjoint.expUnitary b * selfAdjoint.expUnitary a := by - rw [← h.expUnitary_add, ← h.symm.expUnitary_add, add_comm] + Commute (expUnitary a) (expUnitary b) := by + simpa only [Commute, SemiconjBy, Subtype.ext_iff, expUnitary_coe] using + ((h.smul_left I).smul_right I).exp end Star diff --git a/Mathlib/Analysis/CStarAlgebra/Module/Synonym.lean b/Mathlib/Analysis/CStarAlgebra/Module/Synonym.lean index dd10e630df16d7..910af77d7b6fa7 100644 --- a/Mathlib/Analysis/CStarAlgebra/Module/Synonym.lean +++ b/Mathlib/Analysis/CStarAlgebra/Module/Synonym.lean @@ -8,7 +8,7 @@ module public import Mathlib.RingTheory.Finiteness.Defs public import Mathlib.Topology.Bornology.Constructions public import Mathlib.Topology.UniformSpace.Equiv -public import Mathlib.Topology.Algebra.Module.Equiv +public import Mathlib.Topology.Algebra.Module.TransferInstance public import Mathlib.Topology.Algebra.IsUniformGroup.Constructions /-! # Type synonym for types with a `CStarModule` structure @@ -162,16 +162,12 @@ end Equiv /-- `WithCStarModule.equiv` as an additive equivalence. -/ def addEquiv [AddCommGroup E] : C⋆ᵐᵒᵈ(A, E) ≃+ E := - { AddEquiv.refl _ with - toFun := equiv _ _ - invFun := (equiv _ _).symm } + Equiv.addEquiv (equiv A E) /-- `WithCStarModule.equiv` as a linear equivalence. -/ -@[simps -fullyApplied] +@[simps! -fullyApplied] def linearEquiv [Semiring R] [AddCommGroup E] [Module R E] : C⋆ᵐᵒᵈ(A, E) ≃ₗ[R] E := - { LinearEquiv.refl _ _ with - toFun := equiv _ _ - invFun := (equiv _ _).symm } + (addEquiv A E).toLinearEquiv fun _ _ ↦ rfl lemma map_top_submodule {R : Type*} [Semiring R] [AddCommGroup E] [Module R E] : (⊤ : Submodule R E).map (linearEquiv R A E).symm.toLinearMap = ⊤ := diff --git a/Mathlib/Analysis/CStarAlgebra/Spectrum.lean b/Mathlib/Analysis/CStarAlgebra/Spectrum.lean index d716c1e4af8af6..4c143a3ca4ca7a 100644 --- a/Mathlib/Analysis/CStarAlgebra/Spectrum.lean +++ b/Mathlib/Analysis/CStarAlgebra/Spectrum.lean @@ -313,12 +313,8 @@ noncomputable instance (priority := 100) Complex.instStarHomClass : StarHomClass rw [← realPart_add_I_smul_imaginaryPart a] simp only [map_add, map_smul, star_add, star_smul, hsa, selfAdjoint.star_val_eq] intro s - have := AlgHom.apply_mem_spectrum φ (s : A) - rw [selfAdjoint.val_re_map_spectrum s] at this - rcases this with ⟨⟨_, _⟩, _, heq⟩ - simp only [Function.comp_apply] at heq - rw [← heq, RCLike.star_def] - exact RCLike.conj_ofReal _ + rw [selfAdjoint.mem_spectrum_eq_re s (AlgHom.apply_mem_spectrum φ (s : A))] + simp /-- This is not an instance to avoid type class inference loops. See `WeakDual.Complex.instStarHomClass`. -/ From 0915ed3b1c13fe5f2220be6acab06f57a9ba69df Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Mon, 13 Apr 2026 10:19:19 +0800 Subject: [PATCH 2/5] Revert "Merge branch 'golf_27'" This reverts commit 5a25d459cb107fab61e7650c44df92e22167b5bf. --- .../Analysis/BoxIntegral/Partition/Split.lean | 8 +++-- .../Isometric.lean | 12 +++++-- .../ContinuousFunctionalCalculus/Order.lean | 32 +++++++++++++------ .../ContinuousFunctionalCalculus/Range.lean | 22 +++++++++---- .../Analysis/CStarAlgebra/Exponential.lean | 15 ++++++--- .../Analysis/CStarAlgebra/Module/Synonym.lean | 12 ++++--- Mathlib/Analysis/CStarAlgebra/Spectrum.lean | 8 +++-- 7 files changed, 79 insertions(+), 30 deletions(-) diff --git a/Mathlib/Analysis/BoxIntegral/Partition/Split.lean b/Mathlib/Analysis/BoxIntegral/Partition/Split.lean index dee1534aca942e..64048745bab0a2 100644 --- a/Mathlib/Analysis/BoxIntegral/Partition/Split.lean +++ b/Mathlib/Analysis/BoxIntegral/Partition/Split.lean @@ -187,8 +187,12 @@ theorem sum_split_boxes {M : Type*} [AddCommMonoid M] (I : Box ι) (i : ι) (x : /-- If `x ∉ (I.lower i, I.upper i)`, then the hyperplane `{y | y i = x}` does not split `I`. -/ theorem split_of_notMem_Ioo (h : x ∉ Ioo (I.lower i) (I.upper i)) : split I i x = ⊤ := by refine ((isPartitionTop I).eq_of_boxes_subset fun J hJ => ?_).symm - rcases mem_top.1 hJ with rfl - grind [Box.splitUpper_eq_self, Box.splitLower_eq_self, mem_boxes, mem_split_iff, not_lt] + rcases mem_top.1 hJ with rfl; clear hJ + rw [mem_boxes, mem_split_iff] + rw [mem_Ioo, not_and_or, not_lt, not_lt] at h + cases h <;> [right; left] + · rwa [eq_comm, Box.splitUpper_eq_self] + · rwa [eq_comm, Box.splitLower_eq_self] theorem coe_eq_of_mem_split_of_mem_le {y : ι → ℝ} (h₁ : J ∈ split I i x) (h₂ : y ∈ J) (h₃ : y i ≤ x) : (J : Set (ι → ℝ)) = ↑I ∩ { y | y i ≤ x } := by diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean index 5fc929c0bfb683..f95ff5e2884ecd 100644 --- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean +++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean @@ -458,7 +458,11 @@ lemma IsGreatest.nnnorm_cfc_nnreal [Nontrivial A] (f : ℝ≥0 → ℝ≥0) (a : convert IsGreatest.nnnorm_cfc (fun x : ℝ ↦ (f x.toNNReal : ℝ)) a ?hf_cont case hf_cont => exact continuous_subtype_val.comp_continuousOn <| ContinuousOn.comp ‹_› continuous_real_toNNReal.continuousOn <| ha'.image ▸ Set.mapsTo_image .. - simp [Set.image_image, ← ha'.image] + ext x + constructor + all_goals rintro ⟨x, hx, rfl⟩ + · exact ⟨x, spectrum.algebraMap_mem ℝ hx, by simp⟩ + · exact ⟨x.toNNReal, ha'.apply_mem hx, by simp⟩ lemma apply_le_nnnorm_cfc_nnreal (f : ℝ≥0 → ℝ≥0) (a : A) ⦃x : ℝ≥0⦄ (hx : x ∈ σ ℝ≥0 a) (hf : ContinuousOn f (σ ℝ≥0 a) := by cfc_cont_tac) (ha : 0 ≤ a := by cfc_tac) : @@ -532,7 +536,11 @@ lemma IsGreatest.nnnorm_cfcₙ_nnreal (f : ℝ≥0 → ℝ≥0) (a : A) convert IsGreatest.nnnorm_cfcₙ (fun x : ℝ ↦ (f x.toNNReal : ℝ)) a ?hf_cont (by simpa) case hf_cont => exact continuous_subtype_val.comp_continuousOn <| ContinuousOn.comp ‹_› continuous_real_toNNReal.continuousOn <| ha'.image ▸ Set.mapsTo_image .. - simp [Set.image_image, ← ha'.image] + ext x + constructor + all_goals rintro ⟨x, hx, rfl⟩ + · exact ⟨x, quasispectrum.algebraMap_mem ℝ hx, by simp⟩ + · exact ⟨x.toNNReal, ha'.apply_mem hx, by simp⟩ lemma apply_le_nnnorm_cfcₙ_nnreal (f : ℝ≥0 → ℝ≥0) (a : A) ⦃x : ℝ≥0⦄ (hx : x ∈ σₙ ℝ≥0 a) (hf : ContinuousOn f (σₙ ℝ≥0 a) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean index aa2ab470e02e56..d2c1d46f0f2fcd 100644 --- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean +++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean @@ -292,11 +292,15 @@ lemma CFC.conjugate_rpow_neg_one_half (a : A) (ha : IsStrictlyPositive a := by c invertible. -/ lemma CStarAlgebra.isUnit_of_le (a : A) {b : A} (hab : a ≤ b) (h : IsStrictlyPositive a := by cfc_tac) : IsUnit b := by - nontriviality A; rw [← spectrum.zero_notMem_iff ℝ]; intro h0 - obtain ⟨r, hr, hr_le⟩ := (CFC.exists_pos_algebraMap_le_iff h.isSelfAdjoint).2 fun x hx ↦ - h.spectrum_pos hx - exact not_le_of_gt hr ((algebraMap_le_iff_le_spectrum (a := b) (ha := .of_nonneg - (h.nonneg.trans hab))).1 (hr_le.trans hab) 0 h0) + have h₀ := h.isUnit + have ha := h.nonneg + rw [← spectrum.zero_notMem_iff ℝ≥0] at h₀ ⊢ + nontriviality A + have hb := (show 0 ≤ a from ha).trans hab + rw [zero_notMem_iff, SpectrumRestricts.nnreal_lt_iff (.nnreal_of_nonneg ‹_›), + NNReal.coe_zero, ← CFC.exists_pos_algebraMap_le_iff (.of_nonneg ‹_›)] at h₀ ⊢ + peel h₀ with r hr _ + exact this.trans hab lemma le_iff_norm_sqrt_mul_rpow (a b : A) (ha : 0 ≤ a := by cfc_tac) (hb : IsStrictlyPositive b := by cfc_tac) : @@ -437,13 +441,23 @@ instance instNonnegSpectrumClassComplexNonUnital : NonnegSpectrumClass ℂ A whe lemma norm_le_norm_of_nonneg_of_le {a b : A} (ha : 0 ≤ a := by cfc_tac) (hab : a ≤ b) : ‖a‖ ≤ ‖b‖ := by suffices ∀ a b : A⁺¹, 0 ≤ a → a ≤ b → ‖a‖ ≤ ‖b‖ by - have hb : 0 ≤ b := ha.trans hab + have hb := ha.trans hab simpa only [ge_iff_le, Unitization.norm_inr] using - this a b (by simpa) (by rwa [Unitization.inr_le_iff a b (.of_nonneg ha) (.of_nonneg hb)]) + this a b (by simpa) (by rwa [Unitization.inr_le_iff a b]) intro a b ha hab have hb : 0 ≤ b := ha.trans hab - exact (CStarAlgebra.norm_le_iff_le_algebraMap a (norm_nonneg _) ha).2 <| - hab.trans <| IsSelfAdjoint.le_algebraMap_norm_self (.of_nonneg hb) + -- these two `have`s are just for performance + have := IsSelfAdjoint.of_nonneg ha; have := IsSelfAdjoint.of_nonneg hb + have h₂ : cfc (id : ℝ → ℝ) a ≤ cfc (fun _ => ‖b‖) a := by + calc _ = a := by rw [cfc_id ℝ a] + _ ≤ cfc id b := (cfc_id ℝ b) ▸ hab + _ ≤ cfc (fun _ => ‖b‖) b := by + refine cfc_mono fun x hx => ?_ + calc x = ‖x‖ := (Real.norm_of_nonneg (spectrum_nonneg_of_nonneg hb hx)).symm + _ ≤ ‖b‖ := spectrum.norm_le_norm_of_mem hx + _ = _ := by rw [cfc_const _ _, cfc_const _ _] + rw [cfc_le_iff id (fun _ => ‖b‖) a] at h₂ + exact h₂ ‖a‖ <| norm_mem_spectrum_of_nonneg ha theorem nnnorm_le_nnnorm_of_nonneg_of_le {a : A} {b : A} (ha : 0 ≤ a := by cfc_tac) (hab : a ≤ b) : ‖a‖₊ ≤ ‖b‖₊ := diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Range.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Range.lean index ecc3522cb35215..d402b443a6ad3f 100644 --- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Range.lean +++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Range.lean @@ -136,9 +136,13 @@ lemma range_cfc_nnreal rw [range_cfc_nnreal_eq_image_cfc_real a ha, Set.setOf_and, SetLike.setOf_mem_eq, ← range_cfc _ ha.isSelfAdjoint, Set.inter_comm, ← Set.image_preimage_eq_inter_range] rintro _ ⟨f, hf, rfl⟩ - exact cfc_cases (p := IsSelfAdjoint) _ a f ⟨0, by simp, by simp⟩ fun hf' ha' ↦ - ⟨f, (cfc_nonneg_iff f a hf' ha').mp (by simpa [Set.mem_preimage, Set.mem_setOf_eq] using hf), - by simp [cfc_apply f a ha' hf']⟩ + simp only [Set.preimage_setOf_eq, Set.mem_setOf_eq, Set.mem_image] at hf ⊢ + obtain (⟨h₁, h₂⟩ | h | h) := by + simpa only [not_and_or] using em (ContinuousOn f (spectrum ℝ a) ∧ IsSelfAdjoint a) + · refine ⟨f, ?_, rfl⟩ + rwa [cfc_nonneg_iff f a] at hf + · exact ⟨0, by simp, by simp [cfc_apply_of_not_continuousOn a h]⟩ + · exact ⟨0, by simp, by simp [cfc_apply_of_not_predicate a h]⟩ end Unital @@ -249,8 +253,14 @@ lemma range_cfcₙ_nnreal [NonUnitalClosedEmbeddingContinuousFunctionalCalculus ← range_cfcₙ _ ha.isSelfAdjoint, Set.inter_comm, ← Set.image_preimage_eq_inter_range] refine Set.Subset.antisymm (Set.image_mono (fun _ ↦ cfcₙ_nonneg)) ?_ rintro _ ⟨f, hf, rfl⟩ - exact cfcₙ_cases (p := IsSelfAdjoint) _ a f ⟨0, by simp, by simp⟩ fun hf' h0 ha' ↦ - ⟨f, (cfcₙ_nonneg_iff f a hf' h0 ha').mp - (by simpa [Set.mem_preimage, Set.mem_setOf_eq] using hf), by simp [cfcₙ_apply f a hf' h0 ha']⟩ + simp only [Set.preimage_setOf_eq, Set.mem_setOf_eq, Set.mem_image] at hf ⊢ + obtain (⟨h₁, h₂, h₃⟩ | h | h | h) := by + simpa only [not_and_or] using + em (ContinuousOn f (quasispectrum ℝ a) ∧ f 0 = 0 ∧ IsSelfAdjoint a) + · refine ⟨f, ?_, rfl⟩ + rwa [cfcₙ_nonneg_iff f a] at hf + · exact ⟨0, by simp, by simp [cfcₙ_apply_of_not_continuousOn a h]⟩ + · exact ⟨0, by simp, by simp [cfcₙ_apply_of_not_map_zero a h]⟩ + · exact ⟨0, by simp, by simp [cfcₙ_apply_of_not_predicate a h]⟩ end NonUnital diff --git a/Mathlib/Analysis/CStarAlgebra/Exponential.lean b/Mathlib/Analysis/CStarAlgebra/Exponential.lean index f5f709d3b023ff..2bef6805c902c6 100644 --- a/Mathlib/Analysis/CStarAlgebra/Exponential.lean +++ b/Mathlib/Analysis/CStarAlgebra/Exponential.lean @@ -55,12 +55,17 @@ lemma selfAdjoint.continuous_expUnitary : Continuous (expUnitary : selfAdjoint A theorem Commute.expUnitary_add {a b : selfAdjoint A} (h : Commute (a : A) (b : A)) : expUnitary (a + b) = expUnitary a * expUnitary b := by let +nondep : NormedAlgebra ℚ A := .restrictScalars ℚ ℂ A - simpa only [Subtype.ext_iff, expUnitary_coe, AddSubgroup.coe_add, smul_add] using - exp_add_of_commute ((h.smul_left I).smul_right I) + ext + have hcomm : Commute (I • (a : A)) (I • (b : A)) := by + unfold Commute SemiconjBy + simp only [h.eq, Algebra.smul_mul_assoc, Algebra.mul_smul_comm] + simpa only [expUnitary_coe, AddSubgroup.coe_add, smul_add] using exp_add_of_commute hcomm theorem Commute.expUnitary {a b : selfAdjoint A} (h : Commute (a : A) (b : A)) : - Commute (expUnitary a) (expUnitary b) := by - simpa only [Commute, SemiconjBy, Subtype.ext_iff, expUnitary_coe] using - ((h.smul_left I).smul_right I).exp + Commute (expUnitary a) (expUnitary b) := + calc + selfAdjoint.expUnitary a * selfAdjoint.expUnitary b = + selfAdjoint.expUnitary b * selfAdjoint.expUnitary a := by + rw [← h.expUnitary_add, ← h.symm.expUnitary_add, add_comm] end Star diff --git a/Mathlib/Analysis/CStarAlgebra/Module/Synonym.lean b/Mathlib/Analysis/CStarAlgebra/Module/Synonym.lean index 910af77d7b6fa7..dd10e630df16d7 100644 --- a/Mathlib/Analysis/CStarAlgebra/Module/Synonym.lean +++ b/Mathlib/Analysis/CStarAlgebra/Module/Synonym.lean @@ -8,7 +8,7 @@ module public import Mathlib.RingTheory.Finiteness.Defs public import Mathlib.Topology.Bornology.Constructions public import Mathlib.Topology.UniformSpace.Equiv -public import Mathlib.Topology.Algebra.Module.TransferInstance +public import Mathlib.Topology.Algebra.Module.Equiv public import Mathlib.Topology.Algebra.IsUniformGroup.Constructions /-! # Type synonym for types with a `CStarModule` structure @@ -162,12 +162,16 @@ end Equiv /-- `WithCStarModule.equiv` as an additive equivalence. -/ def addEquiv [AddCommGroup E] : C⋆ᵐᵒᵈ(A, E) ≃+ E := - Equiv.addEquiv (equiv A E) + { AddEquiv.refl _ with + toFun := equiv _ _ + invFun := (equiv _ _).symm } /-- `WithCStarModule.equiv` as a linear equivalence. -/ -@[simps! -fullyApplied] +@[simps -fullyApplied] def linearEquiv [Semiring R] [AddCommGroup E] [Module R E] : C⋆ᵐᵒᵈ(A, E) ≃ₗ[R] E := - (addEquiv A E).toLinearEquiv fun _ _ ↦ rfl + { LinearEquiv.refl _ _ with + toFun := equiv _ _ + invFun := (equiv _ _).symm } lemma map_top_submodule {R : Type*} [Semiring R] [AddCommGroup E] [Module R E] : (⊤ : Submodule R E).map (linearEquiv R A E).symm.toLinearMap = ⊤ := diff --git a/Mathlib/Analysis/CStarAlgebra/Spectrum.lean b/Mathlib/Analysis/CStarAlgebra/Spectrum.lean index 4c143a3ca4ca7a..d716c1e4af8af6 100644 --- a/Mathlib/Analysis/CStarAlgebra/Spectrum.lean +++ b/Mathlib/Analysis/CStarAlgebra/Spectrum.lean @@ -313,8 +313,12 @@ noncomputable instance (priority := 100) Complex.instStarHomClass : StarHomClass rw [← realPart_add_I_smul_imaginaryPart a] simp only [map_add, map_smul, star_add, star_smul, hsa, selfAdjoint.star_val_eq] intro s - rw [selfAdjoint.mem_spectrum_eq_re s (AlgHom.apply_mem_spectrum φ (s : A))] - simp + have := AlgHom.apply_mem_spectrum φ (s : A) + rw [selfAdjoint.val_re_map_spectrum s] at this + rcases this with ⟨⟨_, _⟩, _, heq⟩ + simp only [Function.comp_apply] at heq + rw [← heq, RCLike.star_def] + exact RCLike.conj_ofReal _ /-- This is not an instance to avoid type class inference loops. See `WeakDual.Complex.instStarHomClass`. -/ From 9b892e5b5a13dc81f2b16e645805240db9f8383c Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Mon, 13 Apr 2026 17:43:23 +0800 Subject: [PATCH 3/5] golf Mathlib/Analysis/Convex/Approximation.lean --- Mathlib/Analysis/Convex/Approximation.lean | 20 +++++++------------- 1 file changed, 7 insertions(+), 13 deletions(-) diff --git a/Mathlib/Analysis/Convex/Approximation.lean b/Mathlib/Analysis/Convex/Approximation.lean index cfc8bd5556a13f..4c7fca57290943 100644 --- a/Mathlib/Analysis/Convex/Approximation.lean +++ b/Mathlib/Analysis/Convex/Approximation.lean @@ -220,19 +220,13 @@ theorem univ_sSup_of_nat_affine_eq [HereditarilyLindelofSpace E] (hφc : LowerSemicontinuous φ) (hφcv : ConvexOn ℝ univ φ) : ∃ (l : ℕ → E →L[𝕜] 𝕜) (c : ℕ → ℝ), (∀ i, re ∘ (l i) + const E (c i) ≤ φ) ∧ ⨆ i, re ∘ (l i) + const E (c i) = φ := by - obtain ⟨𝓕', h𝓕'⟩ := hφcv.univ_sSup_of_countable_affine_eq (𝕜 := 𝕜) hφc - by_cases! he : 𝓕'.Nonempty - · obtain ⟨f, hf⟩ := h𝓕'.1.exists_eq_range he - have (i : ℕ) : ∃ (l : E →L[𝕜] 𝕜) (c : ℝ), f i = re ∘ l + const E c := by simp_all - choose l c hlc using this - refine ⟨l, c, fun i => (hlc i) ▸ (h𝓕'.2.2 (f i) (hf ▸ mem_range_self i)).1, ?_⟩ - calc - _ = ⨆ i, f i := by congr with i x; exact congrFun (hlc i).symm x - _ = _ := by rw [← sSup_range, ← hf, h𝓕'.2.1] - · refine ⟨fun _ => 0, fun _ => 0, fun i x => ?_, ?_⟩ - · simp_all [← congrFun h𝓕'.2.1 x] - · ext x - simp_all [← congrFun h𝓕'.2.1 x] + obtain ⟨l, c, hle, hsup⟩ := hφcv.sSup_of_nat_affine_eq (𝕜 := 𝕜) (s := univ) isClosed_univ + (lowerSemicontinuousOn_univ_iff.2 hφc) + refine ⟨l, c, ?_, ?_⟩ + · intro i x + simpa using hle i ⟨x, trivial⟩ + · ext x + simpa using congrFun hsup ⟨x, trivial⟩ end RCLike From be09512c7539914e006c7f9eac2a1a2a6c276e47 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Mon, 13 Apr 2026 18:00:19 +0800 Subject: [PATCH 4/5] apply suggestions --- Mathlib/Analysis/Convex/Approximation.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Mathlib/Analysis/Convex/Approximation.lean b/Mathlib/Analysis/Convex/Approximation.lean index 4c7fca57290943..dd5fa60e8fc6e0 100644 --- a/Mathlib/Analysis/Convex/Approximation.lean +++ b/Mathlib/Analysis/Convex/Approximation.lean @@ -222,9 +222,8 @@ theorem univ_sSup_of_nat_affine_eq [HereditarilyLindelofSpace E] ∧ ⨆ i, re ∘ (l i) + const E (c i) = φ := by obtain ⟨l, c, hle, hsup⟩ := hφcv.sSup_of_nat_affine_eq (𝕜 := 𝕜) (s := univ) isClosed_univ (lowerSemicontinuousOn_univ_iff.2 hφc) - refine ⟨l, c, ?_, ?_⟩ - · intro i x - simpa using hle i ⟨x, trivial⟩ + refine ⟨l, c, fun i x ↦ ?_, ?_⟩ + · exact hle i ⟨x, trivial⟩ · ext x simpa using congrFun hsup ⟨x, trivial⟩ From c33ff46acd903a00ba0d58bef74ecca2f56ba86c Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Mon, 13 Apr 2026 18:22:20 +0800 Subject: [PATCH 5/5] Apply suggestion from @themathqueen Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com> --- Mathlib/Analysis/Convex/Approximation.lean | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/Mathlib/Analysis/Convex/Approximation.lean b/Mathlib/Analysis/Convex/Approximation.lean index dd5fa60e8fc6e0..330f08e2b85ed9 100644 --- a/Mathlib/Analysis/Convex/Approximation.lean +++ b/Mathlib/Analysis/Convex/Approximation.lean @@ -222,10 +222,9 @@ theorem univ_sSup_of_nat_affine_eq [HereditarilyLindelofSpace E] ∧ ⨆ i, re ∘ (l i) + const E (c i) = φ := by obtain ⟨l, c, hle, hsup⟩ := hφcv.sSup_of_nat_affine_eq (𝕜 := 𝕜) (s := univ) isClosed_univ (lowerSemicontinuousOn_univ_iff.2 hφc) - refine ⟨l, c, fun i x ↦ ?_, ?_⟩ - · exact hle i ⟨x, trivial⟩ - · ext x - simpa using congrFun hsup ⟨x, trivial⟩ + refine ⟨l, c, fun i x ↦ hle i ⟨x, trivial⟩, ?_⟩ + ext x + simpa using congrFun hsup ⟨x, trivial⟩ end RCLike