From 5a25d459cb107fab61e7650c44df92e22167b5bf Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Mon, 13 Apr 2026 10:18:17 +0800 Subject: [PATCH 1/3] 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/3] 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 ab0cb64496cbded6c9bec3f422946d27b7fdd1a0 Mon Sep 17 00:00:00 2001 From: yuanyi-350 Date: Tue, 14 Apr 2026 22:25:55 +0800 Subject: [PATCH 3/3] chore(Analysis): golf Order, Asymptotic, and Between --- .../ContinuousFunctionalCalculus/Order.lean | 27 ++++-------- .../LogCounting/Asymptotic.lean | 42 ++++--------------- Mathlib/Analysis/Convex/Between.lean | 39 ++--------------- 3 files changed, 20 insertions(+), 88 deletions(-) diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean index d2c1d46f0f2fcd..5cc34ccc55b266 100644 --- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean +++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean @@ -292,15 +292,12 @@ 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 + rw [← spectrum.zero_notMem_iff ℝ] + obtain ⟨r, hr, hr_le⟩ : ∃ r > 0, (algebraMap ℝ A) r ≤ a := + (exists_pos_algebraMap_le_iff h.isSelfAdjoint).2 fun x hx ↦ h.spectrum_pos hx + exact fun h0 ↦ not_le_of_gt hr <| (algebraMap_le_iff_le_spectrum <| .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) : @@ -446,18 +443,8 @@ lemma norm_le_norm_of_nonneg_of_le {a b : A} (ha : 0 ≤ a := by cfc_tac) (hab : 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 - -- 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 (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/Complex/ValueDistribution/LogCounting/Asymptotic.lean b/Mathlib/Analysis/Complex/ValueDistribution/LogCounting/Asymptotic.lean index 2323bd2ca1b3a5..26d186a187df70 100644 --- a/Mathlib/Analysis/Complex/ValueDistribution/LogCounting/Asymptotic.lean +++ b/Mathlib/Analysis/Complex/ValueDistribution/LogCounting/Asymptotic.lean @@ -46,28 +46,13 @@ is little o of the logarithmic counting function attached to `single e`. -/ lemma one_isLittleO_logCounting_single [DecidableEq E] [ProperSpace E] {e : E} : (1 : ℝ → ℝ) =o[atTop] logCounting (single e 1) := by - rw [isLittleO_iff] - intro c hc - simp only [Pi.one_apply, norm_eq_abs, eventually_atTop, abs_one] - use exp (|log ‖e‖| + c⁻¹) - intro b hb - have h₁b : 1 ≤ b := by - calc 1 - _ ≤ exp (|log ‖e‖| + c⁻¹) := one_le_exp (by positivity) - _ ≤ b := hb - have h₁c : ‖e‖ ≤ exp (|log ‖e‖| + c⁻¹) := by - calc ‖e‖ - _ ≤ exp (log ‖e‖) := le_exp_log ‖e‖ - _ ≤ exp (|log ‖e‖| + c⁻¹) := - exp_monotone (le_add_of_le_of_nonneg (le_abs_self _) (inv_pos.2 hc).le) - rw [← inv_mul_le_iff₀ hc, mul_one, abs_of_nonneg (logCounting_nonneg - (single_pos.2 Int.one_pos).le h₁b)] - calc c⁻¹ - _ ≤ logCounting (single e 1) (exp (|log ‖e‖| + c⁻¹)) := by - simp [logCounting_single_eq_log_sub_const h₁c, le_sub_iff_add_le', le_abs_self (log ‖e‖)] - _ ≤ logCounting (single e 1) b := by - apply logCounting_mono (single_pos.2 Int.one_pos).le (mem_Ioi.2 (exp_pos _)) _ hb - simpa [mem_Ioi] using one_pos.trans_le h₁b + have hΘ : (fun r : ℝ ↦ log r - log ‖e‖) =Θ[atTop] log := + (IsEquivalent.refl.sub_isLittleO (Real.isLittleO_const_log_atTop (c := log ‖e‖))).isTheta + have h₁ : (1 : ℝ → ℝ) =o[atTop] fun r : ℝ ↦ log r - log ‖e‖ := + (hΘ.isLittleO_congr_right).2 Real.isLittleO_const_log_atTop + refine h₁.congr' EventuallyEq.rfl ?_ + filter_upwards [eventually_ge_atTop ‖e‖] with r hr + simp [logCounting_single_eq_log_sub_const hr] /-- A non-negative function with locally finite support is zero if and only if its logarithmic counting @@ -124,16 +109,7 @@ theorem logCounting_isBigO_one_iff_analyticOnNhd {f : 𝕜 → E} (h : Meromorph logCounting f ⊤ =O[atTop] (1 : ℝ → ℝ) ↔ AnalyticOnNhd 𝕜 (toMeromorphicNFOn f univ) univ := by simp only [logCounting, reduceDIte] rw [← Function.locallyFinsuppWithin.zero_iff_logCounting_bounded (negPart_nonneg _)] - constructor - · intro h₁f z hz - apply (meromorphicNFOn_toMeromorphicNFOn f univ - trivial).meromorphicOrderAt_nonneg_iff_analyticAt.1 - rw [meromorphicOrderAt_toMeromorphicNFOn h.meromorphicOn (by trivial), ← WithTop.untop₀_nonneg, - ← h.meromorphicOn.divisor_apply (by trivial), ← negPart_eq_zero, - ← locallyFinsuppWithin.negPart_apply] - aesop - · intro h₁f - rwa [negPart_eq_zero, ← h.meromorphicOn.divisor_of_toMeromorphicNFOn, - (meromorphicNFOn_toMeromorphicNFOn _ _).divisor_nonneg_iff_analyticOnNhd] + rw [negPart_eq_zero, ← h.meromorphicOn.divisor_of_toMeromorphicNFOn, + (meromorphicNFOn_toMeromorphicNFOn _ _).divisor_nonneg_iff_analyticOnNhd] end ValueDistribution diff --git a/Mathlib/Analysis/Convex/Between.lean b/Mathlib/Analysis/Convex/Between.lean index 957e9d0ca4125b..d681b1f8f235af 100644 --- a/Mathlib/Analysis/Convex/Between.lean +++ b/Mathlib/Analysis/Convex/Between.lean @@ -732,13 +732,8 @@ variable [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] variable {R} theorem Wbtw.sameRay_vsub {x y z : P} (h : Wbtw R x y z) : SameRay R (y -ᵥ x) (z -ᵥ y) := by - rcases h with ⟨t, ⟨ht0, ht1⟩, rfl⟩ - simp_rw [lineMap_apply] - rcases ht0.lt_or_eq with (ht0' | rfl); swap; · simp - rcases ht1.lt_or_eq with (ht1' | rfl); swap; · simp - refine Or.inr (Or.inr ⟨1 - t, t, sub_pos.2 ht1', ht0', ?_⟩) - simp only [vadd_vsub, smul_smul, vsub_vadd_eq_vsub_sub, smul_sub, ← sub_smul] - ring_nf + have h' := sameRay_of_mem_segment ((mem_segment_iff_wbtw).2 (by simpa using h.vsub_const x)) + simpa [sub_zero, vsub_sub_vsub_cancel_right] using h' theorem Wbtw.sameRay_vsub_left {x y z : P} (h : Wbtw R x y z) : SameRay R (y -ᵥ x) (z -ᵥ x) := by rcases h with ⟨t, ⟨ht0, _⟩, rfl⟩ @@ -1041,17 +1036,7 @@ theorem Sbtw.trans_expand_right {w x y z : P} (h₁ : Sbtw R w x y) (h₂ : Sbtw omit [IsStrictOrderedRing R] in theorem Wbtw.collinear {x y z : P} (h : Wbtw R x y z) : Collinear R ({x, y, z} : Set P) := by - rw [collinear_iff_exists_forall_eq_smul_vadd] - refine ⟨x, z -ᵥ x, ?_⟩ - intro p hp - simp_rw [Set.mem_insert_iff, Set.mem_singleton_iff] at hp - rcases hp with (rfl | rfl | rfl) - · refine ⟨0, ?_⟩ - simp - · rcases h with ⟨t, -, rfl⟩ - exact ⟨t, rfl⟩ - · refine ⟨1, ?_⟩ - simp + simpa [Set.insert_comm] using collinear_insert_of_mem_affineSpan_pair h.mem_affineSpan theorem Collinear.wbtw_or_wbtw_or_wbtw {x y z : P} (h : Collinear R ({x, y, z} : Set P)) : Wbtw R x y z ∨ Wbtw R y z x ∨ Wbtw R z x y := by @@ -1078,23 +1063,7 @@ theorem Collinear.wbtw_or_wbtw_or_wbtw {x y z : P} (h : Collinear R ({x, y, z} : exact Or.inl (wbtw_or_wbtw_smul_vadd_of_nonneg _ _ hy0.le hz0.le) theorem wbtw_iff_sameRay_vsub {x y z : P} : Wbtw R x y z ↔ SameRay R (y -ᵥ x) (z -ᵥ y) := by - refine ⟨Wbtw.sameRay_vsub, fun h => ?_⟩ - rcases h with (h | h | ⟨r₁, r₂, hr₁, hr₂, h⟩) - · rw [vsub_eq_zero_iff_eq] at h - simp [h] - · rw [vsub_eq_zero_iff_eq] at h - simp [h] - · refine - ⟨r₂ / (r₁ + r₂), - ⟨div_nonneg hr₂.le (add_nonneg hr₁.le hr₂.le), - div_le_one_of_le₀ (le_add_of_nonneg_left hr₁.le) (add_nonneg hr₁.le hr₂.le)⟩, - ?_⟩ - have h' : z = r₂⁻¹ • r₁ • (y -ᵥ x) +ᵥ y := by simp [h, hr₂.ne'] - rw [eq_comm] - simp only [lineMap_apply, h', vadd_vsub_assoc, smul_smul, ← add_smul, eq_vadd_iff_vsub_eq, - smul_add] - convert (one_smul R (y -ᵥ x)).symm - field + simp [← wbtw_vsub_const_iff x, ← mem_segment_iff_wbtw, mem_segment_iff_sameRay] lemma wbtw_total_of_sameRay_vsub_left {x y z : P} (h : SameRay R (y -ᵥ x) (z -ᵥ x)) : Wbtw R x y z ∨ Wbtw R x z y := by