From 98cd08775a3f25d58d6203b548f1fa5faf7cca3a Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Mon, 9 Mar 2026 12:53:31 -0500 Subject: [PATCH 1/8] feat: norm of sums of continuous functions whose product is zero --- .../ContinuousMap/Bounded/Normed.lean | 37 +++++++++++++++++++ Mathlib/Topology/ContinuousMap/Compact.lean | 34 +++++++++++++++++ 2 files changed, 71 insertions(+) diff --git a/Mathlib/Topology/ContinuousMap/Bounded/Normed.lean b/Mathlib/Topology/ContinuousMap/Bounded/Normed.lean index c074a2ddc96f21..5eccffbae62d8c 100644 --- a/Mathlib/Topology/ContinuousMap/Bounded/Normed.lean +++ b/Mathlib/Topology/ContinuousMap/Bounded/Normed.lean @@ -304,6 +304,43 @@ instance instNonUnitalSeminormedRing : NonUnitalSeminormedRing (α →ᵇ R) whe (fun x ↦ (norm_mul_le _ _).trans <| mul_le_mul (norm_coe_le_norm f x) (norm_coe_le_norm g x) (norm_nonneg _) (norm_nonneg _)) +/-- If the product of bounded continuous functions is zero, then the norm of their sum is the +maximum of their norms. -/ +lemma norm_add_eq_max [IsCancelMulZero R] {f g : α →ᵇ R} (h : f * g = 0) : + ‖f + g‖ = max ‖f‖ ‖g‖ := by + have hfg : ∀ x, f x = 0 ∨ g x = 0 := by simpa [DFunLike.ext_iff, mul_eq_zero] using h + have hfg' x : ‖(f + g) x‖ = max ‖f x‖ ‖g x‖ := by obtain (h | h) := hfg x <;> simp [h] + apply le_antisymm + · rw [norm_le (by positivity)] + intro x + rw [hfg'] + apply max_le <;> exact norm_coe_le_norm _ x |>.trans (by simp) + · apply max_le + all_goals + rw [norm_le (by positivity)] + intro x + grw [← (f + g).norm_coe_le_norm x, hfg'] + simp + +/-- If the product of bounded continuous functions is zero, then the norm of their sum is the +maximum of their norms. -/ +lemma nnnorm_add_eq_max [IsCancelMulZero R] {f g : α →ᵇ R} (h : f * g = 0) : + ‖f + g‖₊ = max ‖f‖₊ ‖g‖₊ := + NNReal.eq <| norm_add_eq_max h + +open scoped Function +/-- If the pairwise products of bounded continuous functions are all zero, then the norm of their +sum is the maximum of their norms. -/ +lemma nnnorm_sum_eq_sup [IsCancelMulZero R] {ι : Type*} {f : ι → (α →ᵇ R)} (s : Finset ι) + (h : Pairwise ((· * · = 0) on f)) : + ‖∑ i ∈ s, f i‖₊ = s.sup (‖f ·‖₊) := by + classical + induction s using Finset.induction_on with + | empty => simp + | insert j s hj ih => + suffices f j * ∑ i ∈ s, f i = 0 by simpa [hj, ← ih] using nnnorm_add_eq_max this + simpa [Finset.mul_sum] using Finset.sum_eq_zero fun i hi ↦ h (by grind) + end Seminormed instance instNonUnitalSeminormedCommRing [NonUnitalSeminormedCommRing R] : diff --git a/Mathlib/Topology/ContinuousMap/Compact.lean b/Mathlib/Topology/ContinuousMap/Compact.lean index 18481b23e5a173..437c3995a4fe22 100644 --- a/Mathlib/Topology/ContinuousMap/Compact.lean +++ b/Mathlib/Topology/ContinuousMap/Compact.lean @@ -344,6 +344,40 @@ end ‖f • const α b‖ = ‖f‖ * ‖b‖ := by simp only [← coe_nnnorm, NNReal.coe_mul, nnnorm_smul_const] +section NormSum + +variable {R : Type*} [NonUnitalSeminormedRing R] [IsCancelMulZero R] + +open BoundedContinuousFunction + +/-- If the product of continuous functions is zero, then the norm of their sum is the +maximum of their norms. -/ +lemma norm_add_eq_max {f g : C(α, R)} (h : f * g = 0) : + ‖f + g‖ = max ‖f‖ ‖g‖ := by + replace h : mkOfCompact f * mkOfCompact g = 0 := by ext x; simpa using congr($h x) + simpa using BoundedContinuousFunction.norm_add_eq_max h + +/-- If the product of bounded continuous functions is zero, then the norm of their sum is the +maximum of their norms. -/ +lemma nnnorm_add_eq_max {f g : C(α, R)} (h : f * g = 0) : + ‖f + g‖₊ = max ‖f‖₊ ‖g‖₊ := + NNReal.eq <| norm_add_eq_max h + +open scoped Function +/-- If the pairwise products of bounded continuous functions are all zero, then the norm of their +sum is the maximum of their norms. -/ +lemma nnnorm_sum_eq_sup {ι : Type*} {f : ι → C(α, R)} (s : Finset ι) + (h : Pairwise ((· * · = 0) on f)) : + ‖∑ i ∈ s, f i‖₊ = s.sup (‖f ·‖₊) := by + classical + induction s using Finset.induction_on with + | empty => simp + | insert j s hj ih => + suffices f j * ∑ i ∈ s, f i = 0 by simpa [hj, ← ih] using nnnorm_add_eq_max this + simpa [Finset.mul_sum] using Finset.sum_eq_zero fun i hi ↦ h (by grind) + +end NormSum + section variable {𝕜 : Type*} {γ : Type*} [NormedField 𝕜] [SeminormedRing γ] [NormedAlgebra 𝕜 γ] From 7e9cc94554a0e38358bb08cd6c23560bf5e347a9 Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Mon, 9 Mar 2026 15:18:24 -0500 Subject: [PATCH 2/8] feat(Analysis/CStarAlgebra): norms of sums of orthogonal selfadjoint elements --- .../Analysis/CStarAlgebra/GelfandDuality.lean | 79 +++++++++++++++++++ 1 file changed, 79 insertions(+) diff --git a/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean b/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean index 14950ace52e6ff..a1f738e8eb23e0 100644 --- a/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean +++ b/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean @@ -130,6 +130,8 @@ end ComplexBanachAlgebra section ComplexCStarAlgebra +section Commutative + variable {A : Type*} [CommCStarAlgebra A] theorem gelfandTransform_map_star (a : A) : @@ -194,6 +196,83 @@ noncomputable def gelfandStarTransform : A ≃⋆ₐ[ℂ] C(characterSpace ℂ A { gelfandTransform ℂ A with map_star' := fun x => gelfandTransform_map_star x }) (gelfandTransform_bijective A) +end Commutative + +section NonUnitalComm + +variable {A : Type*} [NonUnitalCommCStarAlgebra A] + +open scoped CStarAlgebra in +open Unitization in +lemma CommCStarAlgebra.norm_add_eq_max {a b : A} (h : a * b = 0) : + ‖a + b‖ = max ‖a‖ ‖b‖ := by + let f := gelfandStarTransform A⁺¹ ∘ inrNonUnitalAlgHom ℂ A + have hf : Isometry f := gelfandTransform_isometry _ |>.comp isometry_inr + simp_rw [← hf.norm_map_of_map_zero (by simp [f]), show f (a + b) = f a + f b by simp [f]] + exact ContinuousMap.norm_add_eq_max <| by simpa [f] using congr(f $h) + +lemma CommCStarAlgebra.nnnorm_add_eq_max {a b : A} (h : a * b = 0) : + ‖a + b‖₊ = max ‖a‖₊ ‖b‖₊ := + NNReal.eq <| CommCStarAlgebra.norm_add_eq_max h + +end NonUnitalComm + +section NonUnital + +variable {A : Type*} [NonUnitalCStarAlgebra A] + +open NonUnitalStarAlgebra in +lemma IsSelfAdjoint.norm_add_eq_max {a b : A} (hab : a * b = 0) + (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) : + ‖a + b‖ = max ‖a‖ ‖b‖ := by + let S : NonUnitalStarSubalgebra ℂ A := (adjoin ℂ {a, b}).topologicalClosure + have hS : IsClosed (S : Set A) := (adjoin ℂ {a, b}).isClosed_topologicalClosure + have hab' : a * b = b * a := by + rw [hab, eq_comm]; simpa [ha.star_eq, hb.star_eq] using congr(star $hab) + let _ : NonUnitalCommRing (adjoin ℂ {a, b}) := + adjoinNonUnitalCommRingOfComm ℂ (by grind) (by grind [IsSelfAdjoint.star_eq]) + let _ : NonUnitalCommRing S := (adjoin ℂ {a, b}).nonUnitalCommRingTopologicalClosure mul_comm + let _ : NonUnitalCommCStarAlgebra S := { } + let c : S := ⟨a, subset_closure <| subset_adjoin _ _ <| by grind⟩ + let d : S := ⟨b, subset_closure <| subset_adjoin _ _ <| by grind⟩ + exact CommCStarAlgebra.norm_add_eq_max (a := c) (b := d) (by ext; simpa) + +lemma IsSelfAdjoint.nnnorm_add_eq_max {a b : A} (hab : a * b = 0) + (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) : + ‖a + b‖₊ = max ‖a‖₊ ‖b‖₊ := + NNReal.eq <| IsSelfAdjoint.norm_add_eq_max hab ha hb + +lemma IsSelfAdjoint.norm_sub_eq_max {a b : A} (hab : a * b = 0) + (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) : + ‖a - b‖ = max ‖a‖ ‖b‖ := by + rw [← sq_eq_sq₀ (by positivity) (by positivity)] + simp only [sq, ← ha.norm_add_eq_max hab hb, ← CStarRing.norm_star_mul_self] + have : b * a = 0 := by simpa [ha.star_eq, hb.star_eq] using congr(star $hab) + simp [sub_mul, mul_sub, hb.star_eq, ha.star_eq, hab, this, add_mul, mul_add] + +lemma IsSelfAdjoint.nnnorm_sub_eq_max {a b : A} (hab : a * b = 0) + (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) : + ‖a - b‖₊ = max ‖a‖₊ ‖b‖₊ := + NNReal.eq <| IsSelfAdjoint.norm_sub_eq_max hab ha hb + +attribute [aesop safe apply (rule_sets := [CStarAlgebra])] isSelfAdjoint_sum + +open scoped Function in +lemma IsSelfAdjoint.nnnorm_sum_eq_sup {ι : Type*} {f : ι → A} (s : Finset ι) + (h0 : Pairwise ((· * · = 0) on f)) (h : ∀ i ∈ s, IsSelfAdjoint (f i)) : + ‖∑ i ∈ s, f i‖₊ = s.sup (‖f ·‖₊) := by + classical + induction s using Finset.induction with + | empty => simp + | insert j s hj ih => + suffices f j * ∑ i ∈ s, f i = 0 by + simp_all only [Finset.mem_insert, or_true, implies_true, forall_const, forall_eq_or_imp, + not_false_eq_true, Finset.sum_insert, Finset.sup_insert] + simpa [← ih] using h.1.nnnorm_add_eq_max this (by cfc_tac) + simpa [Finset.mul_sum] using Finset.sum_eq_zero fun i hi ↦ h0 (by grind) + +end NonUnital + end ComplexCStarAlgebra section Functoriality From a45bfe23628f6a16aa8ae2d581916d9a080a88a5 Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Wed, 25 Mar 2026 13:18:12 -0500 Subject: [PATCH 3/8] Apply suggestions from code review Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com> --- Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean b/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean index f421beabb69795..6f8064130dcbd2 100644 --- a/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean +++ b/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean @@ -213,6 +213,14 @@ lemma CommCStarAlgebra.norm_add_eq_max {a b : A} (h : a * b = 0) : lemma CommCStarAlgebra.nnnorm_add_eq_max {a b : A} (h : a * b = 0) : ‖a + b‖₊ = max ‖a‖₊ ‖b‖₊ := NNReal.eq <| CommCStarAlgebra.norm_add_eq_max h + +lemma CommCStarAlgebra.norm_sub_eq_max {a b : A} (h : a * b = 0) : + ‖a - b‖ = max ‖a‖ ‖b‖ := by + simpa [sub_eq_add_neg] using norm_add_eq_max (a := a) (b := -b) (by simpa) + +lemma CommCStarAlgebra.nnnorm_sub_eq_max {a b : A} (h : a * b = 0) : + ‖a - b‖₊ = max ‖a‖₊ ‖b‖₊ := + NNReal.eq <| norm_sub_eq_max h end NonUnitalComm @@ -244,10 +252,7 @@ lemma IsSelfAdjoint.nnnorm_add_eq_max {a b : A} (hab : a * b = 0) lemma IsSelfAdjoint.norm_sub_eq_max {a b : A} (hab : a * b = 0) (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) : ‖a - b‖ = max ‖a‖ ‖b‖ := by - rw [← sq_eq_sq₀ (by positivity) (by positivity)] - simp only [sq, ← ha.norm_add_eq_max hab hb, ← CStarRing.norm_star_mul_self] - have : b * a = 0 := by simpa [ha.star_eq, hb.star_eq] using congr(star $hab) - simp [sub_mul, mul_sub, hb.star_eq, ha.star_eq, hab, this, add_mul, mul_add] + simpa [sub_eq_add_neg] using ha.norm_add_eq_max (by simpa) hb.neg lemma IsSelfAdjoint.nnnorm_sub_eq_max {a b : A} (hab : a * b = 0) (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) : From 16f32ea993de9082e319a0925ad2df676f246c84 Mon Sep 17 00:00:00 2001 From: "pre-commit-ci-lite[bot]" <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> Date: Wed, 25 Mar 2026 18:18:53 +0000 Subject: [PATCH 4/8] [pre-commit.ci lite] apply automatic fixes --- Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean b/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean index 6f8064130dcbd2..b3087a2077f387 100644 --- a/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean +++ b/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean @@ -213,7 +213,7 @@ lemma CommCStarAlgebra.norm_add_eq_max {a b : A} (h : a * b = 0) : lemma CommCStarAlgebra.nnnorm_add_eq_max {a b : A} (h : a * b = 0) : ‖a + b‖₊ = max ‖a‖₊ ‖b‖₊ := NNReal.eq <| CommCStarAlgebra.norm_add_eq_max h - + lemma CommCStarAlgebra.norm_sub_eq_max {a b : A} (h : a * b = 0) : ‖a - b‖ = max ‖a‖ ‖b‖ := by simpa [sub_eq_add_neg] using norm_add_eq_max (a := a) (b := -b) (by simpa) From 84f642ac4cce615ee61ed99c6a29a169dd6ce91b Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Wed, 25 Mar 2026 13:36:57 -0500 Subject: [PATCH 5/8] move `aesop` attribute --- Mathlib/Algebra/Star/BigOperators.lean | 2 ++ Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean | 4 +--- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Algebra/Star/BigOperators.lean b/Mathlib/Algebra/Star/BigOperators.lean index 2887fdf49930f7..eb273c10b5b329 100644 --- a/Mathlib/Algebra/Star/BigOperators.lean +++ b/Mathlib/Algebra/Star/BigOperators.lean @@ -7,6 +7,7 @@ module public import Mathlib.Algebra.BigOperators.Finsupp.Basic public import Mathlib.Algebra.Star.SelfAdjoint +public import Mathlib.Tactic.ContinuousFunctionalCalculus /-! # Big-operators lemmas about `star` algebraic operations @@ -26,6 +27,7 @@ theorem star_prod [CommMonoid R] [StarMul R] {α : Type*} (s : Finset α) (f : theorem star_sum [AddCommMonoid R] [StarAddMonoid R] {α : Type*} (s : Finset α) (f : α → R) : star (∑ x ∈ s, f x) = ∑ x ∈ s, star (f x) := map_sum (starAddEquiv : R ≃+ R) _ _ +@[aesop safe apply (rule_sets := [CStarAlgebra])] theorem isSelfAdjoint_sum {ι : Type*} [AddCommMonoid R] [StarAddMonoid R] (s : Finset ι) {x : ι → R} (h : ∀ i ∈ s, IsSelfAdjoint (x i)) : IsSelfAdjoint (∑ i ∈ s, x i) := by simpa [IsSelfAdjoint, star_sum] using Finset.sum_congr rfl fun _ hi => h _ hi diff --git a/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean b/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean index 6f8064130dcbd2..592ff8bd69c3a0 100644 --- a/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean +++ b/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean @@ -213,7 +213,7 @@ lemma CommCStarAlgebra.norm_add_eq_max {a b : A} (h : a * b = 0) : lemma CommCStarAlgebra.nnnorm_add_eq_max {a b : A} (h : a * b = 0) : ‖a + b‖₊ = max ‖a‖₊ ‖b‖₊ := NNReal.eq <| CommCStarAlgebra.norm_add_eq_max h - + lemma CommCStarAlgebra.norm_sub_eq_max {a b : A} (h : a * b = 0) : ‖a - b‖ = max ‖a‖ ‖b‖ := by simpa [sub_eq_add_neg] using norm_add_eq_max (a := a) (b := -b) (by simpa) @@ -259,8 +259,6 @@ lemma IsSelfAdjoint.nnnorm_sub_eq_max {a b : A} (hab : a * b = 0) ‖a - b‖₊ = max ‖a‖₊ ‖b‖₊ := NNReal.eq <| IsSelfAdjoint.norm_sub_eq_max hab ha hb -attribute [aesop safe apply (rule_sets := [CStarAlgebra])] isSelfAdjoint_sum - open scoped Function in lemma IsSelfAdjoint.nnnorm_sum_eq_sup {ι : Type*} {f : ι → A} (s : Finset ι) (h0 : Pairwise ((· * · = 0) on f)) (h : ∀ i ∈ s, IsSelfAdjoint (f i)) : From 2a972f7206aaf2aec535b342bee10080055d0794 Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Wed, 1 Apr 2026 13:45:28 -0500 Subject: [PATCH 6/8] code review --- Mathlib/Algebra/Star/SelfAdjoint.lean | 6 ++ .../Analysis/CStarAlgebra/GelfandDuality.lean | 71 ++++++++++++++----- 2 files changed, 61 insertions(+), 16 deletions(-) diff --git a/Mathlib/Algebra/Star/SelfAdjoint.lean b/Mathlib/Algebra/Star/SelfAdjoint.lean index 728f636b55dc8b..d9edbca078db83 100644 --- a/Mathlib/Algebra/Star/SelfAdjoint.lean +++ b/Mathlib/Algebra/Star/SelfAdjoint.lean @@ -654,6 +654,12 @@ instance IsStarNormal.one_sub [NonAssocRing R] [StarRing R] {a : R} [ha : IsStarNormal a] : IsStarNormal (1 - a) := Commute.one_left (star a) |>.isStarNormal_sub +lemma IsSelfAdjoint.commute_of_mul_eq_zero [NonUnitalNonAssocRing R] [StarRing R] + {a b : R} (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) (hab : a * b = 0) : + Commute a b := by + have : b * a = 0 := by simpa [ha.star_eq, hb.star_eq] using congr(star $hab) + grind [commute_iff_eq] + namespace Pi variable {ι : Type*} {α : ι → Type*} [∀ i, Star (α i)] {f : ∀ i, α i} diff --git a/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean b/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean index 592ff8bd69c3a0..b240b792f5be4e 100644 --- a/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean +++ b/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean @@ -222,6 +222,19 @@ lemma CommCStarAlgebra.nnnorm_sub_eq_max {a b : A} (h : a * b = 0) : ‖a - b‖₊ = max ‖a‖₊ ‖b‖₊ := NNReal.eq <| norm_sub_eq_max h +open scoped Function in +lemma CommCStarAlgebra.nnnorm_sum_eq_sup {ι : Type*} {f : ι → A} (s : Finset ι) + (h0 : Pairwise ((· * · = 0) on f)) : + ‖∑ i ∈ s, f i‖₊ = s.sup (‖f ·‖₊) := by + classical + induction s using Finset.induction with + | empty => simp + | insert j s hj ih => + suffices f j * ∑ i ∈ s, f i = 0 by + simp_all only [not_false_eq_true, Finset.sum_insert, Finset.sup_insert] + simpa [← ih] using nnnorm_add_eq_max this + simpa [Finset.mul_sum] using Finset.sum_eq_zero fun i hi ↦ h0 (by grind) + end NonUnitalComm section NonUnital @@ -229,39 +242,65 @@ section NonUnital variable {A : Type*} [NonUnitalCStarAlgebra A] open NonUnitalStarAlgebra in -lemma IsSelfAdjoint.norm_add_eq_max {a b : A} (hab : a * b = 0) - (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) : +lemma IsStarNormal.norm_add_eq_max {a b : A} (ha : IsStarNormal a) (hb : IsStarNormal b) + (hab₁ : Commute a b) (hab₂ : Commute a (star b)) (hab : a * b = 0) : ‖a + b‖ = max ‖a‖ ‖b‖ := by + /- Since `a` and `b` are normal and commute and commute with the `star` of the other, + the C⋆-subalgebra generated by `a` and `b` is commutative, and the result follows from the + correpsonding result for commutative C⋆-algebras. -/ + -- TODO: once #36418 is merged, simplify the following using `IsMulCommutative`. let S : NonUnitalStarSubalgebra ℂ A := (adjoin ℂ {a, b}).topologicalClosure have hS : IsClosed (S : Set A) := (adjoin ℂ {a, b}).isClosed_topologicalClosure - have hab' : a * b = b * a := by - rw [hab, eq_comm]; simpa [ha.star_eq, hb.star_eq] using congr(star $hab) + have hab₃ : Commute (star a) b := by simpa [commute_star_comm] let _ : NonUnitalCommRing (adjoin ℂ {a, b}) := - adjoinNonUnitalCommRingOfComm ℂ (by grind) (by grind [IsSelfAdjoint.star_eq]) + adjoinNonUnitalCommRingOfComm ℂ (by grind) (by grind [commute_star_comm]) let _ : NonUnitalCommRing S := (adjoin ℂ {a, b}).nonUnitalCommRingTopologicalClosure mul_comm let _ : NonUnitalCommCStarAlgebra S := { } let c : S := ⟨a, subset_closure <| subset_adjoin _ _ <| by grind⟩ let d : S := ⟨b, subset_closure <| subset_adjoin _ _ <| by grind⟩ exact CommCStarAlgebra.norm_add_eq_max (a := c) (b := d) (by ext; simpa) -lemma IsSelfAdjoint.nnnorm_add_eq_max {a b : A} (hab : a * b = 0) - (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) : +lemma IsStarNormal.nnnorm_add_eq_max {a b : A} (ha : IsStarNormal a) (hb : IsStarNormal b) + (hab₁ : Commute a b) (hab₂ : Commute a (star b)) (hab : a * b = 0) : + ‖a + b‖₊ = max ‖a‖₊ ‖b‖₊ := + NNReal.eq <| ha.norm_add_eq_max hb hab₁ hab₂ hab + +lemma IsStarNormal.norm_sub_eq_max {a b : A} (ha : IsStarNormal a) (hb : IsStarNormal b) + (hab₁ : Commute a b) (hab₂ : Commute a (star b)) (hab : a * b = 0) : + ‖a - b‖ = max ‖a‖ ‖b‖ := by + simpa [sub_eq_add_neg] using + ha.norm_add_eq_max hb.neg hab₁.neg_right (by simpa using hab₂) (by simpa) + +lemma IsStarNormal.nnnorm_sub_eq_max {a b : A} (ha : IsStarNormal a) (hb : IsStarNormal b) + (hab₁ : Commute a b) (hab₂ : Commute a (star b)) (hab : a * b = 0) : + ‖a - b‖₊ = max ‖a‖₊ ‖b‖₊ := + NNReal.eq <| ha.norm_sub_eq_max hb hab₁ hab₂ hab + +open NonUnitalStarAlgebra in +lemma IsSelfAdjoint.norm_add_eq_max {a b : A} + (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) (hab : a * b = 0) : + ‖a + b‖ = max ‖a‖ ‖b‖ := + ha.isStarNormal.norm_add_eq_max hb.isStarNormal (by grind [commute_of_mul_eq_zero]) + (by grind [commute_of_mul_eq_zero, hb.star_eq]) hab + +lemma IsSelfAdjoint.nnnorm_add_eq_max {a b : A} + (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) (hab : a * b = 0) : ‖a + b‖₊ = max ‖a‖₊ ‖b‖₊ := - NNReal.eq <| IsSelfAdjoint.norm_add_eq_max hab ha hb + NNReal.eq <| ha.norm_add_eq_max hb hab -lemma IsSelfAdjoint.norm_sub_eq_max {a b : A} (hab : a * b = 0) - (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) : +lemma IsSelfAdjoint.norm_sub_eq_max {a b : A} + (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) (hab : a * b = 0) : ‖a - b‖ = max ‖a‖ ‖b‖ := by - simpa [sub_eq_add_neg] using ha.norm_add_eq_max (by simpa) hb.neg + simpa [sub_eq_add_neg] using ha.norm_add_eq_max hb.neg (by simpa) -lemma IsSelfAdjoint.nnnorm_sub_eq_max {a b : A} (hab : a * b = 0) - (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) : +lemma IsSelfAdjoint.nnnorm_sub_eq_max {a b : A} + (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) (hab : a * b = 0) : ‖a - b‖₊ = max ‖a‖₊ ‖b‖₊ := - NNReal.eq <| IsSelfAdjoint.norm_sub_eq_max hab ha hb + NNReal.eq <| ha.norm_sub_eq_max hb hab open scoped Function in lemma IsSelfAdjoint.nnnorm_sum_eq_sup {ι : Type*} {f : ι → A} (s : Finset ι) - (h0 : Pairwise ((· * · = 0) on f)) (h : ∀ i ∈ s, IsSelfAdjoint (f i)) : + (h : ∀ i ∈ s, IsSelfAdjoint (f i)) (h0 : Pairwise ((· * · = 0) on f)) : ‖∑ i ∈ s, f i‖₊ = s.sup (‖f ·‖₊) := by classical induction s using Finset.induction with @@ -270,7 +309,7 @@ lemma IsSelfAdjoint.nnnorm_sum_eq_sup {ι : Type*} {f : ι → A} (s : Finset ι suffices f j * ∑ i ∈ s, f i = 0 by simp_all only [Finset.mem_insert, or_true, implies_true, forall_const, forall_eq_or_imp, not_false_eq_true, Finset.sum_insert, Finset.sup_insert] - simpa [← ih] using h.1.nnnorm_add_eq_max this (by cfc_tac) + simpa [← ih] using h.1.nnnorm_add_eq_max (by cfc_tac) this simpa [Finset.mul_sum] using Finset.sum_eq_zero fun i hi ↦ h0 (by grind) end NonUnital From eb2b87339c75412f0c1fd1d01e9bee1eb35e3710 Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Wed, 1 Apr 2026 15:54:55 -0500 Subject: [PATCH 7/8] fixes and organizational improvements --- .../Analysis/CStarAlgebra/GelfandDuality.lean | 60 ++++++++++--------- 1 file changed, 32 insertions(+), 28 deletions(-) diff --git a/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean b/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean index 158700e20109d7..da9f33452ea06d 100644 --- a/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean +++ b/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean @@ -198,26 +198,26 @@ end Commutative section NonUnitalComm -variable {A : Type*} [NonUnitalCommCStarAlgebra A] +variable {A : Type*} [NonUnitalCommCStarAlgebra A] {a b : A} open scoped CStarAlgebra in open Unitization in -lemma CommCStarAlgebra.norm_add_eq_max {a b : A} (h : a * b = 0) : +lemma CommCStarAlgebra.norm_add_eq_max (h : a * b = 0) : ‖a + b‖ = max ‖a‖ ‖b‖ := by let f := gelfandStarTransform A⁺¹ ∘ inrNonUnitalAlgHom ℂ A have hf : Isometry f := gelfandTransform_isometry _ |>.comp isometry_inr simp_rw [← hf.norm_map_of_map_zero (by simp [f]), show f (a + b) = f a + f b by simp [f]] exact ContinuousMap.norm_add_eq_max <| by simpa [f] using congr(f $h) -lemma CommCStarAlgebra.nnnorm_add_eq_max {a b : A} (h : a * b = 0) : +lemma CommCStarAlgebra.nnnorm_add_eq_max (h : a * b = 0) : ‖a + b‖₊ = max ‖a‖₊ ‖b‖₊ := NNReal.eq <| CommCStarAlgebra.norm_add_eq_max h -lemma CommCStarAlgebra.norm_sub_eq_max {a b : A} (h : a * b = 0) : +lemma CommCStarAlgebra.norm_sub_eq_max (h : a * b = 0) : ‖a - b‖ = max ‖a‖ ‖b‖ := by simpa [sub_eq_add_neg] using norm_add_eq_max (a := a) (b := -b) (by simpa) -lemma CommCStarAlgebra.nnnorm_sub_eq_max {a b : A} (h : a * b = 0) : +lemma CommCStarAlgebra.nnnorm_sub_eq_max (h : a * b = 0) : ‖a - b‖₊ = max ‖a‖₊ ‖b‖₊ := NNReal.eq <| norm_sub_eq_max h @@ -238,67 +238,69 @@ end NonUnitalComm section NonUnital -variable {A : Type*} [NonUnitalCStarAlgebra A] +variable {A : Type*} [NonUnitalCStarAlgebra A] {a b : A} -open NonUnitalStarAlgebra in -lemma IsStarNormal.norm_add_eq_max {a b : A} (ha : IsStarNormal a) (hb : IsStarNormal b) +namespace IsStarNormal + +open scoped IsMulCommutative in +open NonUnitalStarAlgebra NonUnitalStarSubalgebra in +lemma norm_add_eq_max (ha : IsStarNormal a) (hb : IsStarNormal b) (hab₁ : Commute a b) (hab₂ : Commute a (star b)) (hab : a * b = 0) : ‖a + b‖ = max ‖a‖ ‖b‖ := by - /- Since `a` and `b` are normal and commute and commute with the `star` of the other, - the C⋆-subalgebra generated by `a` and `b` is commutative, and the result follows from the - correpsonding result for commutative C⋆-algebras. -/ + /- Since `a` and `b` are normal, commute, and commute with the `star` of the other, + the C⋆-subalgebra generated by `a` and `b` is commutative, and the conclusion follows from the + corresponding result for commutative C⋆-algebras. -/ -- TODO: once #36418 is merged, simplify the following using `IsMulCommutative`. let S : NonUnitalStarSubalgebra ℂ A := (adjoin ℂ {a, b}).topologicalClosure have hS : IsClosed (S : Set A) := (adjoin ℂ {a, b}).isClosed_topologicalClosure have hab₃ : Commute (star a) b := by simpa [commute_star_comm] - let _ : NonUnitalCommRing (adjoin ℂ {a, b}) := - adjoinNonUnitalCommRingOfComm ℂ (by grind) (by grind [commute_star_comm]) + have : IsMulCommutative (adjoin ℂ {a, b}) := + isMulCommutative_adjoin ℂ (by grind) (by grind [commute_star_comm]) let _ : NonUnitalCommRing S := (adjoin ℂ {a, b}).nonUnitalCommRingTopologicalClosure mul_comm let _ : NonUnitalCommCStarAlgebra S := { } - let c : S := ⟨a, subset_closure <| subset_adjoin _ _ <| by grind⟩ - let d : S := ⟨b, subset_closure <| subset_adjoin _ _ <| by grind⟩ - exact CommCStarAlgebra.norm_add_eq_max (a := c) (b := d) (by ext; simpa) + refine CommCStarAlgebra.norm_add_eq_max (A := S) (a := ⟨a, ?_⟩) (b := ⟨b, ?_⟩) (by ext; simpa) + all_goals apply le_topologicalClosure; aesop -lemma IsStarNormal.nnnorm_add_eq_max {a b : A} (ha : IsStarNormal a) (hb : IsStarNormal b) +lemma nnnorm_add_eq_max (ha : IsStarNormal a) (hb : IsStarNormal b) (hab₁ : Commute a b) (hab₂ : Commute a (star b)) (hab : a * b = 0) : ‖a + b‖₊ = max ‖a‖₊ ‖b‖₊ := NNReal.eq <| ha.norm_add_eq_max hb hab₁ hab₂ hab -lemma IsStarNormal.norm_sub_eq_max {a b : A} (ha : IsStarNormal a) (hb : IsStarNormal b) +lemma norm_sub_eq_max (ha : IsStarNormal a) (hb : IsStarNormal b) (hab₁ : Commute a b) (hab₂ : Commute a (star b)) (hab : a * b = 0) : ‖a - b‖ = max ‖a‖ ‖b‖ := by simpa [sub_eq_add_neg] using ha.norm_add_eq_max hb.neg hab₁.neg_right (by simpa using hab₂) (by simpa) -lemma IsStarNormal.nnnorm_sub_eq_max {a b : A} (ha : IsStarNormal a) (hb : IsStarNormal b) +lemma nnnorm_sub_eq_max (ha : IsStarNormal a) (hb : IsStarNormal b) (hab₁ : Commute a b) (hab₂ : Commute a (star b)) (hab : a * b = 0) : ‖a - b‖₊ = max ‖a‖₊ ‖b‖₊ := NNReal.eq <| ha.norm_sub_eq_max hb hab₁ hab₂ hab +end IsStarNormal + +namespace IsSelfAdjoint + open NonUnitalStarAlgebra in -lemma IsSelfAdjoint.norm_add_eq_max {a b : A} - (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) (hab : a * b = 0) : +lemma norm_add_eq_max (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) (hab : a * b = 0) : ‖a + b‖ = max ‖a‖ ‖b‖ := ha.isStarNormal.norm_add_eq_max hb.isStarNormal (by grind [commute_of_mul_eq_zero]) (by grind [commute_of_mul_eq_zero, hb.star_eq]) hab -lemma IsSelfAdjoint.nnnorm_add_eq_max {a b : A} - (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) (hab : a * b = 0) : +lemma nnnorm_add_eq_max (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) (hab : a * b = 0) : ‖a + b‖₊ = max ‖a‖₊ ‖b‖₊ := NNReal.eq <| ha.norm_add_eq_max hb hab -lemma IsSelfAdjoint.norm_sub_eq_max {a b : A} - (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) (hab : a * b = 0) : +lemma norm_sub_eq_max (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) (hab : a * b = 0) : ‖a - b‖ = max ‖a‖ ‖b‖ := by simpa [sub_eq_add_neg] using ha.norm_add_eq_max hb.neg (by simpa) -lemma IsSelfAdjoint.nnnorm_sub_eq_max {a b : A} - (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) (hab : a * b = 0) : +lemma nnnorm_sub_eq_max (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) (hab : a * b = 0) : ‖a - b‖₊ = max ‖a‖₊ ‖b‖₊ := NNReal.eq <| ha.norm_sub_eq_max hb hab open scoped Function in -lemma IsSelfAdjoint.nnnorm_sum_eq_sup {ι : Type*} {f : ι → A} (s : Finset ι) +lemma nnnorm_sum_eq_sup {ι : Type*} {f : ι → A} (s : Finset ι) (h : ∀ i ∈ s, IsSelfAdjoint (f i)) (h0 : Pairwise ((· * · = 0) on f)) : ‖∑ i ∈ s, f i‖₊ = s.sup (‖f ·‖₊) := by classical @@ -311,6 +313,8 @@ lemma IsSelfAdjoint.nnnorm_sum_eq_sup {ι : Type*} {f : ι → A} (s : Finset ι simpa [← ih] using h.1.nnnorm_add_eq_max (by cfc_tac) this simpa [Finset.mul_sum] using Finset.sum_eq_zero fun i hi ↦ h0 (by grind) +end IsSelfAdjoint + end NonUnital end ComplexCStarAlgebra From 716fc909dc3075bbad83736245d794b6c8a9f5ff Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Wed, 1 Apr 2026 15:57:23 -0500 Subject: [PATCH 8/8] another namespace --- .../Analysis/CStarAlgebra/GelfandDuality.lean | 21 +++++++------------ 1 file changed, 8 insertions(+), 13 deletions(-) diff --git a/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean b/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean index da9f33452ea06d..47d659a93d1161 100644 --- a/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean +++ b/Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean @@ -196,34 +196,29 @@ noncomputable def gelfandStarTransform : A ≃⋆ₐ[ℂ] C(characterSpace ℂ A end Commutative -section NonUnitalComm +namespace CommCStarAlgebra variable {A : Type*} [NonUnitalCommCStarAlgebra A] {a b : A} open scoped CStarAlgebra in open Unitization in -lemma CommCStarAlgebra.norm_add_eq_max (h : a * b = 0) : - ‖a + b‖ = max ‖a‖ ‖b‖ := by +lemma norm_add_eq_max (h : a * b = 0) : ‖a + b‖ = max ‖a‖ ‖b‖ := by let f := gelfandStarTransform A⁺¹ ∘ inrNonUnitalAlgHom ℂ A have hf : Isometry f := gelfandTransform_isometry _ |>.comp isometry_inr simp_rw [← hf.norm_map_of_map_zero (by simp [f]), show f (a + b) = f a + f b by simp [f]] exact ContinuousMap.norm_add_eq_max <| by simpa [f] using congr(f $h) -lemma CommCStarAlgebra.nnnorm_add_eq_max (h : a * b = 0) : - ‖a + b‖₊ = max ‖a‖₊ ‖b‖₊ := - NNReal.eq <| CommCStarAlgebra.norm_add_eq_max h +lemma nnnorm_add_eq_max (h : a * b = 0) : ‖a + b‖₊ = max ‖a‖₊ ‖b‖₊ := + NNReal.eq <| norm_add_eq_max h -lemma CommCStarAlgebra.norm_sub_eq_max (h : a * b = 0) : - ‖a - b‖ = max ‖a‖ ‖b‖ := by +lemma norm_sub_eq_max (h : a * b = 0) : ‖a - b‖ = max ‖a‖ ‖b‖ := by simpa [sub_eq_add_neg] using norm_add_eq_max (a := a) (b := -b) (by simpa) -lemma CommCStarAlgebra.nnnorm_sub_eq_max (h : a * b = 0) : - ‖a - b‖₊ = max ‖a‖₊ ‖b‖₊ := +lemma nnnorm_sub_eq_max (h : a * b = 0) : ‖a - b‖₊ = max ‖a‖₊ ‖b‖₊ := NNReal.eq <| norm_sub_eq_max h open scoped Function in -lemma CommCStarAlgebra.nnnorm_sum_eq_sup {ι : Type*} {f : ι → A} (s : Finset ι) - (h0 : Pairwise ((· * · = 0) on f)) : +lemma nnnorm_sum_eq_sup {ι : Type*} {f : ι → A} (s : Finset ι) (h0 : Pairwise ((· * · = 0) on f)) : ‖∑ i ∈ s, f i‖₊ = s.sup (‖f ·‖₊) := by classical induction s using Finset.induction with @@ -234,7 +229,7 @@ lemma CommCStarAlgebra.nnnorm_sum_eq_sup {ι : Type*} {f : ι → A} (s : Finset simpa [← ih] using nnnorm_add_eq_max this simpa [Finset.mul_sum] using Finset.sum_eq_zero fun i hi ↦ h0 (by grind) -end NonUnitalComm +end CommCStarAlgebra section NonUnital