diff --git a/Mathlib.lean b/Mathlib.lean index e90ee6329b3f6..a47002564a638 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -1000,6 +1000,7 @@ import Mathlib.Analysis.BoxIntegral.Partition.Measure import Mathlib.Analysis.BoxIntegral.Partition.Split import Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction import Mathlib.Analysis.BoxIntegral.Partition.Tagged +import Mathlib.Analysis.CStarAlgebra.ApproximateUnit import Mathlib.Analysis.CStarAlgebra.Basic import Mathlib.Analysis.CStarAlgebra.Classes import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic diff --git a/Mathlib/Algebra/Algebra/Quasispectrum.lean b/Mathlib/Algebra/Algebra/Quasispectrum.lean index 63ac30ba8df9a..712888eb8d3ff 100644 --- a/Mathlib/Algebra/Algebra/Quasispectrum.lean +++ b/Mathlib/Algebra/Algebra/Quasispectrum.lean @@ -360,6 +360,14 @@ lemma quasispectrum_eq_spectrum_inr' (R S : Type*) {A : Type*} [Semifield R] apply forall_congr' fun x ↦ ?_ rw [not_iff_not, Units.smul_def, Units.smul_def, ← inr_smul, ← inr_neg, isQuasiregular_inr_iff] +lemma quasispectrum_inr_eq (R S : Type*) {A : Type*} [Semifield R] + [Field S] [NonUnitalRing A] [Algebra R S] [Module S A] [IsScalarTower S A A] + [SMulCommClass S A A] [Module R A] [IsScalarTower R S A] (a : A) : + quasispectrum R (a : Unitization S A) = quasispectrum R a := by + rw [quasispectrum_eq_spectrum_union_zero, quasispectrum_eq_spectrum_inr' R S] + apply Set.union_eq_self_of_subset_right + simpa using zero_mem_spectrum_inr _ _ _ + end Unitization /-- A class for `𝕜`-algebras with a partial order where the ordering is compatible with the diff --git a/Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean b/Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean new file mode 100644 index 0000000000000..c797e3c1f5044 --- /dev/null +++ b/Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean @@ -0,0 +1,112 @@ +/- +Copyright (c) 2024 Jireh Loreaux. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jireh Loreaux +-/ +import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order +import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric +import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow + +/-! # Positive contractions in a C⋆-algebra form an approximate unit + +This file will show (although it does not yet) that the collection of positive contractions (of norm +strictly less than one) in a possibly non-unital C⋆-algebra form an approximate unit. The key step +is to show that this set is directed using the continuous functional calculus applied with the +functions `fun x : ℝ≥0, 1 - (1 + x)⁻¹` and `fun x : ℝ≥0, x * (1 - x)⁻¹`, which are inverses on +the interval `{x : ℝ≥0 | x < 1}`. + +## Main declarations + ++ `CFC.monotoneOn_one_sub_one_add_inv`: the function `f := fun x : ℝ≥0, 1 - (1 + x)⁻¹` is + *operator monotone* on `Set.Ici (0 : A)` (i.e., `cfcₙ f` is monotone on `{x : A | 0 ≤ x}`). ++ `Set.InvOn.one_sub_one_add_inv`: the functions `f := fun x : ℝ≥0, 1 - (1 + x)⁻¹` and + `g := fun x : ℝ≥0, x * (1 - x)⁻¹` are inverses on `{x : ℝ≥0 | x < 1}`. ++ `CStarAlgebra.directedOn_nonneg_ball`: the set `{x : A | 0 ≤ x} ∩ Metric.ball 0 1` is directed. + +## TODO + ++ Prove the approximate identity result by following Ken Davidson's proof in + "C*-Algebras by Example" + +-/ + +variable {A : Type*} [NonUnitalCStarAlgebra A] + +local notation "σₙ" => quasispectrum +local notation "σ" => spectrum + +open Unitization NNReal CStarAlgebra + +variable [PartialOrder A] [StarOrderedRing A] + +lemma CFC.monotoneOn_one_sub_one_add_inv : + MonotoneOn (cfcₙ (fun x : ℝ≥0 ↦ 1 - (1 + x)⁻¹)) (Set.Ici (0 : A)) := by + intro a ha b hb hab + simp only [Set.mem_Ici] at ha hb + rw [← inr_le_iff .., nnreal_cfcₙ_eq_cfc_inr a _, nnreal_cfcₙ_eq_cfc_inr b _] + have h_cfc_one_sub (c : A⁺¹) (hc : 0 ≤ c := by cfc_tac) : + cfc (fun x : ℝ≥0 ↦ 1 - (1 + x)⁻¹) c = 1 - cfc (·⁻¹ : ℝ≥0 → ℝ≥0) (1 + c) := by + rw [cfc_tsub _ _ _ (fun x _ ↦ by simp) (hg := by fun_prop (disch := intro _ _; positivity)), + cfc_const_one ℝ≥0 c] + rw [cfc_comp' (·⁻¹) (1 + ·) c ?_, cfc_add .., cfc_const_one ℝ≥0 c, cfc_id' ℝ≥0 c] + refine continuousOn_id.inv₀ ?_ + rintro - ⟨x, -, rfl⟩ + simp only [id_def] + positivity + rw [← inr_le_iff a b (.of_nonneg ha) (.of_nonneg hb)] at hab + rw [← inr_nonneg_iff] at ha hb + rw [h_cfc_one_sub (a : A⁺¹), h_cfc_one_sub (b : A⁺¹)] + gcongr + rw [← CFC.rpow_neg_one_eq_cfc_inv, ← CFC.rpow_neg_one_eq_cfc_inv] + exact rpow_neg_one_le_rpow_neg_one (add_nonneg zero_le_one ha) (by gcongr) <| + isUnit_of_le isUnit_one zero_le_one <| le_add_of_nonneg_right ha + +lemma Set.InvOn.one_sub_one_add_inv : Set.InvOn (fun x ↦ 1 - (1 + x)⁻¹) (fun x ↦ x * (1 - x)⁻¹) + {x : ℝ≥0 | x < 1} {x : ℝ≥0 | x < 1} := by + have h1_add {x : ℝ≥0} : 0 < 1 + (x : ℝ) := by positivity + have : (fun x : ℝ≥0 ↦ x * (1 + x)⁻¹) = fun x ↦ 1 - (1 + x)⁻¹ := by + ext x + field_simp + simp [sub_mul, inv_mul_cancel₀ h1_add.ne'] + rw [← this] + constructor + all_goals intro x (hx : x < 1) + · have : 0 < 1 - x := tsub_pos_of_lt hx + field_simp [tsub_add_cancel_of_le hx.le, tsub_tsub_cancel_of_le hx.le] + · field_simp [mul_tsub] + +lemma norm_cfcₙ_one_sub_one_add_inv_lt_one (a : A) : + ‖cfcₙ (fun x : ℝ≥0 ↦ 1 - (1 + x)⁻¹) a‖ < 1 := + nnnorm_cfcₙ_nnreal_lt fun x _ ↦ tsub_lt_self zero_lt_one (by positivity) + +-- the calls to `fun_prop` with a discharger set off the linter +set_option linter.style.multiGoal false in +lemma CStarAlgebra.directedOn_nonneg_ball : + DirectedOn (· ≤ ·) ({x : A | 0 ≤ x} ∩ Metric.ball 0 1) := by + let f : ℝ≥0 → ℝ≥0 := fun x => 1 - (1 + x)⁻¹ + let g : ℝ≥0 → ℝ≥0 := fun x => x * (1 - x)⁻¹ + suffices ∀ a b : A, 0 ≤ a → 0 ≤ b → ‖a‖ < 1 → ‖b‖ < 1 → + a ≤ cfcₙ f (cfcₙ g a + cfcₙ g b) by + rintro a ⟨(ha₁ : 0 ≤ a), ha₂⟩ b ⟨(hb₁ : 0 ≤ b), hb₂⟩ + simp only [Metric.mem_ball, dist_zero_right] at ha₂ hb₂ + refine ⟨cfcₙ f (cfcₙ g a + cfcₙ g b), ⟨by simp, ?_⟩, ?_, ?_⟩ + · simpa only [Metric.mem_ball, dist_zero_right] using norm_cfcₙ_one_sub_one_add_inv_lt_one _ + · exact this a b ha₁ hb₁ ha₂ hb₂ + · exact add_comm (cfcₙ g a) (cfcₙ g b) ▸ this b a hb₁ ha₁ hb₂ ha₂ + rintro a b ha₁ - ha₂ - + calc + a = cfcₙ (f ∘ g) a := by + conv_lhs => rw [← cfcₙ_id ℝ≥0 a] + refine cfcₙ_congr (Set.InvOn.one_sub_one_add_inv.1.eqOn.symm.mono fun x hx ↦ ?_) + exact lt_of_le_of_lt (le_nnnorm_of_mem_quasispectrum hx) ha₂ + _ = cfcₙ f (cfcₙ g a) := by + rw [cfcₙ_comp f g a ?_ (by simp [f, tsub_self]) ?_ (by simp [g]) ha₁] + · fun_prop (disch := intro _ _; positivity) + · have (x) (hx : x ∈ σₙ ℝ≥0 a) : 1 - x ≠ 0 := by + refine tsub_pos_of_lt ?_ |>.ne' + exact lt_of_le_of_lt (le_nnnorm_of_mem_quasispectrum hx) ha₂ + fun_prop (disch := assumption) + _ ≤ cfcₙ f (cfcₙ g a + cfcₙ g b) := by + have hab' : cfcₙ g a ≤ cfcₙ g a + cfcₙ g b := le_add_of_nonneg_right cfcₙ_nonneg_of_predicate + exact CFC.monotoneOn_one_sub_one_add_inv cfcₙ_nonneg_of_predicate + (cfcₙ_nonneg_of_predicate.trans hab') hab' diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean index a2cba0b1582a9..4a903ec4b4fda 100644 --- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean +++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean @@ -180,16 +180,16 @@ instance IsStarNormal.instNonUnitalContinuousFunctionalCalculus {A : Type*} [NonUnitalCStarAlgebra A] : NonUnitalContinuousFunctionalCalculus ℂ (IsStarNormal : A → Prop) := RCLike.nonUnitalContinuousFunctionalCalculus Unitization.isStarNormal_inr -open Unitization in +open Unitization CStarAlgebra in lemma inr_comp_cfcₙHom_eq_cfcₙAux {A : Type*} [NonUnitalCStarAlgebra A] (a : A) [ha : IsStarNormal a] : (inrNonUnitalStarAlgHom ℂ A).comp (cfcₙHom ha) = cfcₙAux (isStarNormal_inr (R := ℂ) (A := A)) a ha := by have h (a : A) := isStarNormal_inr (R := ℂ) (A := A) (a := a) refine @UniqueNonUnitalContinuousFunctionalCalculus.eq_of_continuous_of_map_id _ _ _ _ _ _ _ _ _ _ _ inferInstance inferInstance _ (σₙ ℂ a) _ _ rfl _ _ ?_ ?_ ?_ - · show Continuous (fun f ↦ (cfcₙHom ha f : Unitization ℂ A)); fun_prop + · show Continuous (fun f ↦ (cfcₙHom ha f : A⁺¹)); fun_prop · exact isClosedEmbedding_cfcₙAux @(h) a ha |>.continuous - · trans (a : Unitization ℂ A) + · trans (a : A⁺¹) · congrm(inr $(cfcₙHom_id ha)) · exact cfcₙAux_id @(h) a ha |>.symm @@ -586,12 +586,13 @@ section NonnegSpectrumClass variable {A : Type*} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] +open scoped CStarAlgebra in instance CStarAlgebra.instNonnegSpectrumClass' : NonnegSpectrumClass ℝ A where quasispectrum_nonneg_of_nonneg a ha := by rw [Unitization.quasispectrum_eq_spectrum_inr' _ ℂ] -- should this actually be an instance on the `Unitization`? (probably scoped) - let _ := CStarAlgebra.spectralOrder (Unitization ℂ A) - have := CStarAlgebra.spectralOrderedRing (Unitization ℂ A) + let _ := CStarAlgebra.spectralOrder A⁺¹ + have := CStarAlgebra.spectralOrderedRing A⁺¹ apply spectrum_nonneg_of_nonneg rw [StarOrderedRing.nonneg_iff] at ha ⊢ have := AddSubmonoid.mem_map_of_mem (Unitization.inrNonUnitalStarAlgHom ℂ A) ha @@ -693,4 +694,43 @@ lemma cfcₙ_nnreal_eq_real {a : A} (f : ℝ≥0 → ℝ≥0) (ha : 0 ≤ a := b end NNRealEqRealNonUnital +section cfc_inr + +open CStarAlgebra + +variable {A : Type*} [NonUnitalCStarAlgebra A] + +open scoped NonUnitalContinuousFunctionalCalculus in +/-- This lemma requires a lot from type class synthesis, and so one should instead favor the bespoke +versions for `ℝ≥0`, `ℝ`, and `ℂ`. -/ +lemma Unitization.cfcₙ_eq_cfc_inr {R : Type*} [Semifield R] [StarRing R] [MetricSpace R] + [TopologicalSemiring R] [ContinuousStar R] [Module R A] [IsScalarTower R A A] + [SMulCommClass R A A] [CompleteSpace R] [Algebra R ℂ] [IsScalarTower R ℂ A] + {p : A → Prop} {p' : A⁺¹ → Prop} [NonUnitalContinuousFunctionalCalculus R p] + [ContinuousFunctionalCalculus R p'] + [UniqueNonUnitalContinuousFunctionalCalculus R (Unitization ℂ A)] + (hp : ∀ {a : A}, p' (a : A⁺¹) ↔ p a) (a : A) (f : R → R) (hf₀ : f 0 = 0 := by cfc_zero_tac) : + cfcₙ f a = cfc f (a : A⁺¹) := by + by_cases h : ContinuousOn f (σₙ R a) ∧ p a + · obtain ⟨hf, ha⟩ := h + rw [← cfcₙ_eq_cfc (quasispectrum_inr_eq R ℂ a ▸ hf)] + exact (inrNonUnitalStarAlgHom ℂ A).map_cfcₙ f a + · obtain (hf | ha) := not_and_or.mp h + · rw [cfcₙ_apply_of_not_continuousOn a hf, inr_zero, + cfc_apply_of_not_continuousOn _ (quasispectrum_eq_spectrum_inr' R ℂ a ▸ hf)] + · rw [cfcₙ_apply_of_not_predicate a ha, inr_zero, + cfc_apply_of_not_predicate _ (not_iff_not.mpr hp |>.mpr ha)] + +lemma Unitization.complex_cfcₙ_eq_cfc_inr (a : A) (f : ℂ → ℂ) (hf₀ : f 0 = 0 := by cfc_zero_tac) : + cfcₙ f a = cfc f (a : A⁺¹) := + Unitization.cfcₙ_eq_cfc_inr isStarNormal_inr .. + +/-- note: the version for `ℝ≥0`, `Unization.nnreal_cfcₙ_eq_cfc_inr`, can be found in +`Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order` -/ +lemma Unitization.real_cfcₙ_eq_cfc_inr (a : A) (f : ℝ → ℝ) (hf₀ : f 0 = 0 := by cfc_zero_tac) : + cfcₙ f a = cfc f (a : A⁺¹) := + Unitization.cfcₙ_eq_cfc_inr isSelfAdjoint_inr .. + +end cfc_inr + end diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean index 0ab77c3d67964..9db6bea20c69d 100644 --- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean +++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean @@ -106,6 +106,20 @@ lemma norm_cfc_le_iff (f : 𝕜 → 𝕜) (a : A) {c : ℝ} (hc : 0 ≤ c) (ha : p a := by cfc_tac) : ‖cfc f a‖ ≤ c ↔ ∀ x ∈ σ 𝕜 a, ‖f x‖ ≤ c := ⟨fun h _ hx ↦ norm_apply_le_norm_cfc f a hx hf ha |>.trans h, norm_cfc_le hc⟩ +lemma norm_cfc_lt {f : 𝕜 → 𝕜} {a : A} {c : ℝ} (hc : 0 < c) (h : ∀ x ∈ σ 𝕜 a, ‖f x‖ < c) : + ‖cfc f a‖ < c := by + obtain (_ | _) := subsingleton_or_nontrivial A + · simpa [Subsingleton.elim (cfc f a) 0] + · refine cfc_cases (‖·‖ < c) a f (by simpa) fun hf ha ↦ ?_ + simp only [← cfc_apply f a, (IsGreatest.norm_cfc f a hf ha |>.lt_iff)] + rintro - ⟨x, hx, rfl⟩ + exact h x hx + +lemma norm_cfc_lt_iff (f : 𝕜 → 𝕜) (a : A) {c : ℝ} (hc : 0 < c) + (hf : ContinuousOn f (σ 𝕜 a) := by cfc_cont_tac) + (ha : p a := by cfc_tac) : ‖cfc f a‖ < c ↔ ∀ x ∈ σ 𝕜 a, ‖f x‖ < c := + ⟨fun h _ hx ↦ norm_apply_le_norm_cfc f a hx hf ha |>.trans_lt h, norm_cfc_lt hc⟩ + open NNReal lemma nnnorm_cfc_le {f : 𝕜 → 𝕜} {a : A} (c : ℝ≥0) (h : ∀ x ∈ σ 𝕜 a, ‖f x‖₊ ≤ c) : @@ -117,6 +131,15 @@ lemma nnnorm_cfc_le_iff (f : 𝕜 → 𝕜) (a : A) (c : ℝ≥0) (ha : p a := by cfc_tac) : ‖cfc f a‖₊ ≤ c ↔ ∀ x ∈ σ 𝕜 a, ‖f x‖₊ ≤ c := norm_cfc_le_iff f a c.2 +lemma nnnorm_cfc_lt {f : 𝕜 → 𝕜} {a : A} {c : ℝ≥0} (hc : 0 < c) (h : ∀ x ∈ σ 𝕜 a, ‖f x‖₊ < c) : + ‖cfc f a‖₊ < c := + norm_cfc_lt hc h + +lemma nnnorm_cfc_lt_iff (f : 𝕜 → 𝕜) (a : A) {c : ℝ≥0} (hc : 0 < c) + (hf : ContinuousOn f (σ 𝕜 a) := by cfc_cont_tac) + (ha : p a := by cfc_tac) : ‖cfc f a‖₊ < c ↔ ∀ x ∈ σ 𝕜 a, ‖f x‖₊ < c := + norm_cfc_lt_iff f a hc + end NormedRing namespace SpectrumRestricts @@ -251,6 +274,19 @@ lemma norm_cfcₙ_le_iff (f : 𝕜 → 𝕜) (a : A) (c : ℝ) (ha : p a := by cfc_tac) : ‖cfcₙ f a‖ ≤ c ↔ ∀ x ∈ σₙ 𝕜 a, ‖f x‖ ≤ c := ⟨fun h _ hx ↦ norm_apply_le_norm_cfcₙ f a hx hf hf₀ ha |>.trans h, norm_cfcₙ_le⟩ +lemma norm_cfcₙ_lt {f : 𝕜 → 𝕜} {a : A} {c : ℝ} (h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖ < c) : + ‖cfcₙ f a‖ < c := by + refine cfcₙ_cases (‖·‖ < c) a f ?_ fun hf hf0 ha ↦ ?_ + · simpa using (norm_nonneg _).trans_lt <| h 0 (quasispectrum.zero_mem 𝕜 a) + · simp only [← cfcₙ_apply f a, (IsGreatest.norm_cfcₙ f a hf hf0 ha |>.lt_iff)] + rintro - ⟨x, hx, rfl⟩ + exact h x hx + +lemma norm_cfcₙ_lt_iff (f : 𝕜 → 𝕜) (a : A) (c : ℝ) + (hf : ContinuousOn f (σₙ 𝕜 a) := by cfc_cont_tac) (hf₀ : f 0 = 0 := by cfc_zero_tac) + (ha : p a := by cfc_tac) : ‖cfcₙ f a‖ < c ↔ ∀ x ∈ σₙ 𝕜 a, ‖f x‖ < c := + ⟨fun h _ hx ↦ norm_apply_le_norm_cfcₙ f a hx hf hf₀ ha |>.trans_lt h, norm_cfcₙ_lt⟩ + open NNReal lemma nnnorm_cfcₙ_le {f : 𝕜 → 𝕜} {a : A} {c : ℝ≥0} (h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖₊ ≤ c) : @@ -262,6 +298,15 @@ lemma nnnorm_cfcₙ_le_iff (f : 𝕜 → 𝕜) (a : A) (c : ℝ≥0) (ha : p a := by cfc_tac) : ‖cfcₙ f a‖₊ ≤ c ↔ ∀ x ∈ σₙ 𝕜 a, ‖f x‖₊ ≤ c := norm_cfcₙ_le_iff f a c.1 hf hf₀ ha +lemma nnnorm_cfcₙ_lt {f : 𝕜 → 𝕜} {a : A} {c : ℝ≥0} (h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖₊ < c) : + ‖cfcₙ f a‖₊ < c := + norm_cfcₙ_lt h + +lemma nnnorm_cfcₙ_lt_iff (f : 𝕜 → 𝕜) (a : A) (c : ℝ≥0) + (hf : ContinuousOn f (σₙ 𝕜 a) := by cfc_cont_tac) (hf₀ : f 0 = 0 := by cfc_zero_tac) + (ha : p a := by cfc_tac) : ‖cfcₙ f a‖₊ < c ↔ ∀ x ∈ σₙ 𝕜 a, ‖f x‖₊ < c := + norm_cfcₙ_lt_iff f a c.1 hf hf₀ ha + end NormedRing namespace QuasispectrumRestricts @@ -442,6 +487,21 @@ lemma nnnorm_cfc_nnreal_le_iff (f : ℝ≥0 → ℝ≥0) (a : A) (c : ℝ≥0) (ha : 0 ≤ a := by cfc_tac) : ‖cfc f a‖₊ ≤ c ↔ ∀ x ∈ σ ℝ≥0 a, f x ≤ c := ⟨fun h _ hx ↦ apply_le_nnnorm_cfc_nnreal f a hx hf ha |>.trans h, nnnorm_cfc_nnreal_le⟩ +lemma nnnorm_cfc_nnreal_lt {f : ℝ≥0 → ℝ≥0} {a : A} {c : ℝ≥0} (hc : 0 < c) + (h : ∀ x ∈ σ ℝ≥0 a, f x < c) : ‖cfc f a‖₊ < c := by + obtain (_ | _) := subsingleton_or_nontrivial A + · rw [Subsingleton.elim (cfc f a) 0] + simpa + · refine cfc_cases (‖·‖₊ < c) a f (by simpa) fun hf ha ↦ ?_ + simp only [← cfc_apply f a, (IsGreatest.nnnorm_cfc_nnreal f a hf ha |>.lt_iff)] + rintro - ⟨x, hx, rfl⟩ + exact h x hx + +lemma nnnorm_cfc_nnreal_lt_iff (f : ℝ≥0 → ℝ≥0) (a : A) {c : ℝ≥0} (hc : 0 < c) + (hf : ContinuousOn f (σ ℝ≥0 a) := by cfc_cont_tac) + (ha : 0 ≤ a := by cfc_tac) : ‖cfc f a‖₊ < c ↔ ∀ x ∈ σ ℝ≥0 a, f x < c := + ⟨fun h _ hx ↦ apply_le_nnnorm_cfc_nnreal f a hx hf ha |>.trans_lt h, nnnorm_cfc_nnreal_lt hc⟩ + end Unital section NonUnital @@ -483,6 +543,19 @@ lemma nnnorm_cfcₙ_nnreal_le_iff (f : ℝ≥0 → ℝ≥0) (a : A) (c : ℝ≥0 (ha : 0 ≤ a := by cfc_tac) : ‖cfcₙ f a‖₊ ≤ c ↔ ∀ x ∈ σₙ ℝ≥0 a, f x ≤ c := ⟨fun h _ hx ↦ apply_le_nnnorm_cfcₙ_nnreal f a hx hf hf₀ ha |>.trans h, nnnorm_cfcₙ_nnreal_le⟩ +lemma nnnorm_cfcₙ_nnreal_lt {f : ℝ≥0 → ℝ≥0} {a : A} {c : ℝ≥0} (h : ∀ x ∈ σₙ ℝ≥0 a, f x < c) : + ‖cfcₙ f a‖₊ < c := by + refine cfcₙ_cases (‖·‖₊ < c) a f ?_ fun hf hf0 ha ↦ ?_ + · simpa using zero_le (f 0) |>.trans_lt <| h 0 (quasispectrum.zero_mem ℝ≥0 _) -- sorry + · simp only [← cfcₙ_apply f a, (IsGreatest.nnnorm_cfcₙ_nnreal f a hf hf0 ha |>.lt_iff)] + rintro - ⟨x, hx, rfl⟩ + exact h x hx + +lemma nnnorm_cfcₙ_nnreal_lt_iff (f : ℝ≥0 → ℝ≥0) (a : A) (c : ℝ≥0) + (hf : ContinuousOn f (σₙ ℝ≥0 a) := by cfc_cont_tac) (hf₀ : f 0 = 0 := by cfc_zero_tac) + (ha : 0 ≤ a := by cfc_tac) : ‖cfcₙ f a‖₊ < c ↔ ∀ x ∈ σₙ ℝ≥0 a, f x < c := + ⟨fun h _ hx ↦ apply_le_nnnorm_cfcₙ_nnreal f a hx hf hf₀ ha |>.trans_lt h, nnnorm_cfcₙ_nnreal_lt⟩ + end NonUnital end NNReal diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean index 75e4270e64c96..0be6a81f50b0a 100644 --- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean +++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean @@ -14,7 +14,7 @@ import Mathlib.Topology.ContinuousMap.StarOrdered This file contains various basic facts about star-ordered rings (i.e. mainly C⋆-algebras) that depend on the continuous functional calculus. -We also put an order instance on `Unitization ℂ A` when `A` is a C⋆-algebra via +We also put an order instance on `A⁺¹ := Unitization ℂ A` when `A` is a C⋆-algebra via the spectral order. ## Main theorems @@ -35,28 +35,66 @@ the spectral order. continuous functional calculus, normal, selfadjoint -/ -open scoped NNReal +open scoped NNReal CStarAlgebra + +local notation "σₙ" => quasispectrum + +theorem cfc_tsub {A : Type*} [TopologicalSpace A] [Ring A] [PartialOrder A] [StarRing A] + [StarOrderedRing A] [Algebra ℝ A] [TopologicalRing A] + [ContinuousFunctionalCalculus ℝ (IsSelfAdjoint : A → Prop)] + [UniqueContinuousFunctionalCalculus ℝ A] [NonnegSpectrumClass ℝ A] (f g : ℝ≥0 → ℝ≥0) + (a : A) (hfg : ∀ x ∈ spectrum ℝ≥0 a, g x ≤ f x) (ha : 0 ≤ a := by cfc_tac) + (hf : ContinuousOn f (spectrum ℝ≥0 a) := by cfc_cont_tac) + (hg : ContinuousOn g (spectrum ℝ≥0 a) := by cfc_cont_tac) : + cfc (fun x ↦ f x - g x) a = cfc f a - cfc g a := by + have ha' := SpectrumRestricts.nnreal_of_nonneg ha + have : (spectrum ℝ a).EqOn (fun x ↦ ((f x.toNNReal - g x.toNNReal : ℝ≥0) : ℝ)) + (fun x ↦ f x.toNNReal - g x.toNNReal) := + fun x hx ↦ NNReal.coe_sub <| hfg _ <| ha'.apply_mem hx + rw [cfc_nnreal_eq_real, cfc_nnreal_eq_real, cfc_nnreal_eq_real, cfc_congr this] + refine cfc_sub _ _ a ?_ ?_ + all_goals + exact continuous_subtype_val.comp_continuousOn <| + ContinuousOn.comp ‹_› continuous_real_toNNReal.continuousOn <| ha'.image ▸ Set.mapsTo_image .. + +theorem cfcₙ_tsub {A : Type*} [TopologicalSpace A] [NonUnitalRing A] [PartialOrder A] [StarRing A] + [StarOrderedRing A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [TopologicalRing A] + [NonUnitalContinuousFunctionalCalculus ℝ (IsSelfAdjoint : A → Prop)] + [UniqueNonUnitalContinuousFunctionalCalculus ℝ A] [NonnegSpectrumClass ℝ A] (f g : ℝ≥0 → ℝ≥0) + (a : A) (hfg : ∀ x ∈ σₙ ℝ≥0 a, g x ≤ f x) (ha : 0 ≤ a := by cfc_tac) + (hf : ContinuousOn f (σₙ ℝ≥0 a) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) + (hg : ContinuousOn g (σₙ ℝ≥0 a) := by cfc_cont_tac) (hg0 : g 0 = 0 := by cfc_zero_tac) : + cfcₙ (fun x ↦ f x - g x) a = cfcₙ f a - cfcₙ g a := by + have ha' := QuasispectrumRestricts.nnreal_of_nonneg ha + have : (σₙ ℝ a).EqOn (fun x ↦ ((f x.toNNReal - g x.toNNReal : ℝ≥0) : ℝ)) + (fun x ↦ f x.toNNReal - g x.toNNReal) := + fun x hx ↦ NNReal.coe_sub <| hfg _ <| ha'.apply_mem hx + rw [cfcₙ_nnreal_eq_real, cfcₙ_nnreal_eq_real, cfcₙ_nnreal_eq_real, cfcₙ_congr this] + refine cfcₙ_sub _ _ a ?_ (by simpa) ?_ + all_goals + exact continuous_subtype_val.comp_continuousOn <| + ContinuousOn.comp ‹_› continuous_real_toNNReal.continuousOn <| ha'.image ▸ Set.mapsTo_image .. namespace Unitization variable {A : Type*} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] -instance instPartialOrder : PartialOrder (Unitization ℂ A) := +instance instPartialOrder : PartialOrder A⁺¹ := CStarAlgebra.spectralOrder _ -instance instStarOrderedRing : StarOrderedRing (Unitization ℂ A) := +instance instStarOrderedRing : StarOrderedRing A⁺¹ := CStarAlgebra.spectralOrderedRing _ lemma inr_le_iff (a b : A) (ha : IsSelfAdjoint a := by cfc_tac) (hb : IsSelfAdjoint b := by cfc_tac) : - (a : Unitization ℂ A) ≤ (b : Unitization ℂ A) ↔ a ≤ b := by + (a : A⁺¹) ≤ (b : A⁺¹) ↔ a ≤ b := by -- TODO: prove the more general result for star monomorphisms and use it here. rw [← sub_nonneg, ← sub_nonneg (a := b), StarOrderedRing.nonneg_iff_spectrum_nonneg (R := ℝ) _, ← inr_sub ℂ b a, ← Unitization.quasispectrum_eq_spectrum_inr' ℝ ℂ] exact StarOrderedRing.nonneg_iff_quasispectrum_nonneg _ |>.symm @[simp, norm_cast] -lemma inr_nonneg_iff {a : A} : 0 ≤ (a : Unitization ℂ A) ↔ 0 ≤ a := by +lemma inr_nonneg_iff {a : A} : 0 ≤ (a : A⁺¹) ↔ 0 ≤ a := by by_cases ha : IsSelfAdjoint a · exact inr_zero ℂ (A := A) ▸ inr_le_iff 0 a · refine ⟨?_, ?_⟩ @@ -64,6 +102,10 @@ lemma inr_nonneg_iff {a : A} : 0 ≤ (a : Unitization ℂ A) ↔ 0 ≤ a := by · exact isSelfAdjoint_inr (R := ℂ) |>.mp <| .of_nonneg h · exact .of_nonneg h +lemma nnreal_cfcₙ_eq_cfc_inr (a : A) (f : ℝ≥0 → ℝ≥0) + (hf₀ : f 0 = 0 := by cfc_zero_tac) : cfcₙ f a = cfc f (a : A⁺¹) := + cfcₙ_eq_cfc_inr inr_nonneg_iff .. + end Unitization /-- `cfc_le_iff` only applies to a scalar ring where `R` is an actual `Ring`, and not a `Semiring`. @@ -326,7 +368,7 @@ 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 : Unitization ℂ A, 0 ≤ a → a ≤ b → ‖a‖ ≤ ‖b‖ by + suffices ∀ a b : A⁺¹, 0 ≤ a → a ≤ b → ‖a‖ ≤ ‖b‖ by 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]) @@ -346,12 +388,12 @@ lemma norm_le_norm_of_nonneg_of_le {a b : A} (ha : 0 ≤ a := by cfc_tac) (hab : lemma conjugate_le_norm_smul {a b : A} (hb : IsSelfAdjoint b := by cfc_tac) : star a * b * a ≤ ‖b‖ • (star a * a) := by - suffices ∀ a b : Unitization ℂ A, IsSelfAdjoint b → star a * b * a ≤ ‖b‖ • (star a * a) by + suffices ∀ a b : A⁺¹, IsSelfAdjoint b → star a * b * a ≤ ‖b‖ • (star a * a) by rw [← Unitization.inr_le_iff _ _ (by aesop) ((IsSelfAdjoint.all _).smul (.star_mul_self a))] simpa [Unitization.norm_inr] using this a b <| hb.inr ℂ intro a b hb calc - star a * b * a ≤ star a * (algebraMap ℝ (Unitization ℂ A) ‖b‖) * a := + star a * b * a ≤ star a * (algebraMap ℝ A⁺¹ ‖b‖) * a := conjugate_le_conjugate hb.le_algebraMap_norm_self _ _ = ‖b‖ • (star a * a) := by simp [Algebra.algebraMap_eq_smul_one] @@ -364,7 +406,7 @@ lemma conjugate_le_norm_smul' {a b : A} (hb : IsSelfAdjoint b := by cfc_tac) : /-- The set of nonnegative elements in a C⋆-algebra is closed. -/ lemma isClosed_nonneg : IsClosed {a : A | 0 ≤ a} := by - suffices IsClosed {a : Unitization ℂ A | 0 ≤ a} by + suffices IsClosed {a : A⁺¹ | 0 ≤ a} by rw [Unitization.isometry_inr (𝕜 := ℂ) |>.isClosedEmbedding.closed_iff_image_closed] convert this.inter <| (Unitization.isometry_inr (𝕜 := ℂ)).isClosedEmbedding.isClosed_range ext a diff --git a/Mathlib/Analysis/CStarAlgebra/Spectrum.lean b/Mathlib/Analysis/CStarAlgebra/Spectrum.lean index ad5459084d830..87f11464c1150 100644 --- a/Mathlib/Analysis/CStarAlgebra/Spectrum.lean +++ b/Mathlib/Analysis/CStarAlgebra/Spectrum.lean @@ -86,6 +86,16 @@ theorem spectrum.subset_circle_of_unitary {u : E} (h : u ∈ unitary E) : end UnitarySpectrum +section Quasispectrum + +open scoped NNReal in +lemma CStarAlgebra.le_nnnorm_of_mem_quasispectrum {A : Type*} [NonUnitalCStarAlgebra A] + {a : A} {x : ℝ≥0} (hx : x ∈ quasispectrum ℝ≥0 a) : x ≤ ‖a‖₊ := by + rw [Unitization.quasispectrum_eq_spectrum_inr' ℝ≥0 ℂ] at hx + simpa [Unitization.nnnorm_inr] using spectrum.le_nnnorm_of_mem hx + +end Quasispectrum + section ComplexScalars open Complex diff --git a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow.lean b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow.lean index fda3885c78a00..00bb998dcc04b 100644 --- a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow.lean +++ b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow.lean @@ -287,6 +287,11 @@ lemma rpow_neg_one_eq_inv (a : Aˣ) (ha : (0 : A) ≤ a := by cfc_tac) : refine a.inv_eq_of_mul_eq_one_left ?_ |>.symm simpa [rpow_one (a : A)] using rpow_neg_mul_rpow 1 (spectrum.zero_not_mem ℝ≥0 a.isUnit) +lemma rpow_neg_one_eq_cfc_inv {A : Type*} [PartialOrder A] [NormedRing A] [StarRing A] + [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus ℝ≥0 ((0 : A) ≤ ·)] (a : A) : + a ^ (-1 : ℝ) = cfc (·⁻¹ : ℝ≥0 → ℝ≥0) a := + cfc_congr fun x _ ↦ NNReal.rpow_neg_one x + lemma rpow_neg [UniqueContinuousFunctionalCalculus ℝ≥0 A] (a : Aˣ) (x : ℝ) (ha' : (0 : A) ≤ a := by cfc_tac) : (a : A) ^ (-x) = (↑a⁻¹ : A) ^ x := by suffices h₁ : ContinuousOn (fun z ↦ z ^ x) (Inv.inv '' (spectrum ℝ≥0 (a : A))) by diff --git a/Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean b/Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean index 6bb261df3d76d..45a907bb85745 100644 --- a/Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean +++ b/Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean @@ -364,6 +364,9 @@ noncomputable instance [MetricSpace R] [Zero R]: MetricSpace C(α, R)₀ := noncomputable instance [NormedAddCommGroup R] : Norm C(α, R)₀ where norm f := ‖(f : C(α, R))‖ +lemma norm_def [NormedAddCommGroup R] (f : C(α, R)₀) : ‖f‖ = ‖(f : C(α, R))‖ := + rfl + noncomputable instance [NormedCommRing R] : NonUnitalNormedCommRing C(α, R)₀ where dist_eq f g := NormedAddGroup.dist_eq (f : C(α, R)) g norm_mul f g := NormedRing.norm_mul (f : C(α, R)) g