MathlibAnnex/Analysis/CStarAlgebra/Representation/CompactlyRepresented.lean

Exact source · gss-v0.5.0

Fixed commit original · Raw UTF-8 source · Back to GSS Companion

Select a source link from a manuscript to highlight its exact range.

1/-2Copyright (c) 2026 Ryotaro Tanaka. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Ryotaro Tanaka5-/67import MathlibAnnex.Analysis.CStarAlgebra.FacialStructure.SimultaneousClipping8import MathlibAnnex.Analysis.InnerProductSpace.CompactOperatorIdeal9import MathlibAnnex.Analysis.InnerProductSpace.CompactSpectrum10import Mathlib.Analysis.CStarAlgebra.Projection11import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric12import Mathlib.Analysis.InnerProductSpace.Spectrum1314/-!15# Finite-rank spectral projections in faithfully compact representations1617A faithful representation whose every represented operator is compact contains18actual finite-rank projections.  The point which requires proof is membership in19the represented algebra: an ambient finite-rank approximation is not enough.2021For a nonzero positive represented compact operator we choose a nonzero22eigenvalue, isolate it by restricting to the orthogonal complement of its23eigenspace and using the Fredholm alternative, and apply a zero-preserving24continuous functional calculus cutoff.  The resulting element is a nonzero star25projection in the original nonunital C-star algebra.  Its represented range is26contained in the finite-dimensional eigenspace.2728No separability, countable basis, unitality, irreducibility, or pre-existing29rank-one element is assumed.30-/3132@[expose] public section3334set_option autoImplicit false35noncomputable section3637open Set Metric Module Module.End38open scoped CStarAlgebra ComplexConjugate Topology3940namespace MathlibAnnex.Analysis.CStarAlgebra4142universe u v43variable {A : Type u} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A]44variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]4546/-- A faithful representation is compactly represented when every represented47operator is compact in the original operator norm.  This is deliberately weaker48than `IsCompactOperatorModel`: no surjectivity onto all compact operators is49part of the definition. -/50def NonUnitalCStarRepresentation.IsCompactlyRepresented51    (pi : NonUnitalCStarRepresentation A H) : Prop :=52  Function.Injective pi ∧ ∀ a : A, IsCompactOperator (pi a)5354namespace NonUnitalCStarRepresentation5556/-- The normal-element version of the existing self-adjoint transport lemma. -/57theorem map_cfcₙ_eq_cfc_normal58    (pi : NonUnitalCStarRepresentation A H) (a : A) (ha : IsStarNormal a)59    (f : ℂ → ℂ) (hf : Continuous f) (hf0 : f 0 = 0) :60    pi (cfcₙ f a) = cfc f (pi a) := by61  rw [pi.map_cfcₙ f a hf.continuousOn hf0 (by fun_prop) ha (ha.map pi),62    cfcₙ_eq_cfc hf.continuousOn hf0]6364end NonUnitalCStarRepresentation656667/-- Radial peak used to isolate one nonzero point of a compact-operator68spectrum.  It is one at `μ`, vanishes outside the open `r`-ball, and is69zero at the origin when `r < ‖μ‖`. -/70def compactSpectralPeak (μ : ℂ) (r : ℝ) (z : ℂ) : ℂ :=71  ((max 0 (1 - ‖z - μ‖ / r) : ℝ) : ℂ)7273namespace compactSpectralPeak7475variable {μ z : ℂ} {r : ℝ}7677theorem continuous (hr : 0 < r) : Continuous (compactSpectralPeak μ r) := by78  unfold compactSpectralPeak79  fun_prop8081@[simp]82theorem apply_center (hr : r ≠ 0) : compactSpectralPeak μ r μ = 1 := by83  simp [compactSpectralPeak, hr]8485@[simp]86theorem apply_zero (hr : 0 < r) (hrμ : r ≤ ‖μ‖) :87    compactSpectralPeak μ r 0 = 0 := by88  have hdiv : 1 ≤ ‖μ‖ / r := (le_div_iff₀ hr).2 (by simpa only [one_mul] using hrμ)89  simp [compactSpectralPeak, norm_neg, max_eq_left, sub_nonpos.mpr hdiv]9091@[simp]92theorem apply_eq_zero_of_le_dist (hr : 0 < r) (h : r ≤ dist z μ) :93    compactSpectralPeak μ r z = 0 := by94  have hdiv : 1 ≤ ‖z - μ‖ / r := by95    rw [dist_eq_norm] at h96    exact (le_div_iff₀ hr).2 (by simpa only [one_mul] using h)97  simp [compactSpectralPeak, max_eq_left, sub_nonpos.mpr hdiv]9899@[simp]100theorem apply_eq_zero_or_one_on_isolated_spectrum101    {T : H →L[ℂ] H} (hr : 0 < r) (hμ : μ ∈ spectrum ℂ T)102    (hiso : ∀ z ∈ spectrum ℂ T, z ≠ μ → r ≤ dist z μ)103    {z : ℂ} (hz : z ∈ spectrum ℂ T) :104    compactSpectralPeak μ r z = 0 ∨ compactSpectralPeak μ r z = 1 := by105  by_cases h : z = μ106  · subst z107    exact Or.inr (apply_center hr.ne')108  · exact Or.inl (apply_eq_zero_of_le_dist hr (hiso z hz h))109110end compactSpectralPeak111112namespace NonUnitalCStarRepresentation113114/-- The isolated compact spectral projection in the source algebra. -/115def compactSpectralProjection116    (pi : NonUnitalCStarRepresentation A H) (a : A) (μ : ℂ) (r : ℝ) : A :=117  cfcₙ (compactSpectralPeak μ r) a118119/-- Functional calculus for the compact spectral peak is transported through120the given representation without changing the selected operator. -/121theorem compactSpectralProjection_apply122    (pi : NonUnitalCStarRepresentation A H) (a : A) (ha : IsStarNormal a)123    (μ : ℂ) {r : ℝ} (hr : 0 < r) (hrμ : r ≤ ‖μ‖) :124    pi (pi.compactSpectralProjection a μ r) =125      cfc (compactSpectralPeak μ r) (pi a) := by126  exact pi.map_cfcₙ_eq_cfc_normal a ha _127    (compactSpectralPeak.continuous hr)128    (compactSpectralPeak.apply_zero hr hrμ)129130/-- The represented peak is an actual nonzero finite-rank star projection. -/131theorem exists_nonzero_finite_rank_spectral_projection132    (pi : NonUnitalCStarRepresentation A H) (hpi : Function.Injective pi)133    (a : A) (ha : 0 ≤ a) (ha0 : a ≠ 0)134    (hcompact : IsCompactOperator (pi a)) :135    ∃ p : A,136      IsStarProjection p ∧ p ≠ 0 ∧137      FiniteDimensional ℂ (LinearMap.range (pi p).toLinearMap) ∧138      ∃ (μ : ℂ) (r : ℝ),139        μ ≠ 0 ∧ 0 < r ∧ r < ‖μ‖ ∧140        HasEigenvalue ((pi a) : Module.End ℂ H) μ ∧141        pi p = cfc (compactSpectralPeak μ r) (pi a) ∧142        (pi a) * (pi p) = μ • (pi p) := by143  have haSelf : IsSelfAdjoint a := IsSelfAdjoint.of_nonneg ha144  have hTSelf : (pi a).IsSymmetric := (haSelf.map pi).isSymmetric145  have hT0 : pi a ≠ 0 := fun h => ha0 (hpi (by simpa using h))146  obtain ⟨μ, r, hμ0, hr, hrμ, hμEig, hiso⟩ :=147    (pi a).exists_isolated_nonzero_eigenvalue hcompact hTSelf hT0148  let f : ℂ → ℂ := compactSpectralPeak μ r149  let p : A := pi.compactSpectralProjection a μ r150  let q : H →L[ℂ] H := cfc f (pi a)151  have hμspec : μ ∈ spectrum ℂ (pi a) :=152    (hcompact.hasEigenvalue_iff_mem_spectrum hμ0).1 hμEig153  have hf : Continuous f := compactSpectralPeak.continuous hr154  have hf0 : f 0 = 0 := compactSpectralPeak.apply_zero hr hrμ.le155  have hmap : pi p = q := by156    exact pi.compactSpectralProjection_apply a haSelf.isStarNormal μ hr hrμ.le157  have hqIdem : IsIdempotentElem q := by158    rw [IsIdempotentElem]159    change q * q = q160    rw [show q * q = cfc (fun z => f z * f z) (pi a) by161      exact (cfc_mul f f (pi a) hf.continuousOn hf.continuousOn).symm]162    apply cfc_congr163    intro z hz164    rcases compactSpectralPeak.apply_eq_zero_or_one_on_isolated_spectrum165      hr hμspec hiso hz with hz0 | hz1166    · simp [f, hz0]167    · simp [f, hz1]168  have hqNormal : IsStarNormal q :=169    cfc_predicate f (pi a)170  have hqProj : IsStarProjection q :=171    isStarProjection_iff_isIdempotentElem_and_isStarNormal.mpr ⟨hqIdem, hqNormal⟩172  have hpIdem : IsIdempotentElem p := by173    rw [IsIdempotentElem]174    apply hpi175    rw [map_mul, hmap, hqIdem.eq]176  have hpNormal : IsStarNormal p := by177    exact cfcₙ_predicate f a178  have hpProj : IsStarProjection p :=179    isStarProjection_iff_isIdempotentElem_and_isStarNormal.mpr ⟨hpIdem, hpNormal⟩180  have hq0 : q ≠ 0 := by181    intro hq182    have h1 : (1 : ℂ) ∈ spectrum ℂ q := by183      rw [cfc_map_spectrum f (pi a) (haSelf.map pi).isStarNormal hf.continuousOn]184      exact ⟨μ, hμspec, compactSpectralPeak.apply_center hr.ne'⟩185    obtain ⟨x, _, hx0⟩ :=186      ((hcompact.hasEigenvalue_iff_mem_spectrum hμ0).2 hμspec).exists_hasEigenvector187    letI : Nontrivial H := ⟨⟨x, 0, hx0⟩⟩188    rw [hq, CFC.spectrum_zero_eq (R := ℂ)] at h1189    exact one_ne_zero (Set.mem_singleton_iff.mp h1)190  have hp0 : p ≠ 0 := fun hp => hq0 (by rw [← hmap, hp, map_zero])191  have hTq : (pi a) * q = μ • q := by192    calc193      (pi a) * q = cfc (fun z : ℂ => z * f z) (pi a) := by194        have hmul := cfc_mul (fun z : ℂ => z) f (pi a)195          continuousOn_id hf.continuousOn196        rw [cfc_id' ℂ (pi a) (haSelf.map pi).isStarNormal] at hmul197        exact hmul.symm198      _ = cfc (fun z : ℂ => μ * f z) (pi a) := by199        apply cfc_congr200        intro z hz201        rcases compactSpectralPeak.apply_eq_zero_or_one_on_isolated_spectrum202          hr hμspec hiso hz with hz0 | hz1203        · simp [f, hz0]204        · have hzμ : z = μ := by205            by_contra h206            have := compactSpectralPeak.apply_eq_zero_of_le_dist hr (hiso z hz h)207            exact one_ne_zero (hz1.symm.trans this)208          simp [hzμ, hz1]209      _ = μ • q := by210        simpa [q] using cfc_smul μ f (pi a) hf.continuousOn211  have hrange : LinearMap.range q.toLinearMap ≤212      Module.End.eigenspace (pi a).toLinearMap μ := by213    rintro y ⟨x, rfl⟩214    rw [Module.End.mem_eigenspace_iff]215    simpa [ContinuousLinearMap.mul_apply] using congrArg (fun T : H →L[ℂ] H => T x) hTq216  haveI : FiniteDimensional ℂ217      (Module.End.eigenspace (pi a).toLinearMap μ) :=218    ContinuousLinearMap.finite_dimensional_eigenspace hcompact μ hμ0219  have hfinite : FiniteDimensional ℂ (LinearMap.range q.toLinearMap) :=220    Submodule.finiteDimensional_of_le hrange221  have hfinite' : FiniteDimensional ℂ (LinearMap.range (pi p).toLinearMap) := by222    rw [hmap]223    exact hfinite224  exact ⟨p, hpProj, hp0, hfinite', μ, r, hμ0, hr, hrμ, hμEig, hmap,225    by simpa only [hmap] using hTq⟩226227/-- The compact-representation hypothesis supplies the preceding projection228for every nonzero positive source element. -/229theorem exists_nonzero_finite_rank_projection_of_isCompactlyRepresented230    (pi : NonUnitalCStarRepresentation A H)231    (hpi : pi.IsCompactlyRepresented)232    (a : A) (ha : 0 ≤ a) (ha0 : a ≠ 0) :233    ∃ p : A, IsStarProjection p ∧ p ≠ 0 ∧234      FiniteDimensional ℂ (LinearMap.range (pi p).toLinearMap) := by235  obtain ⟨p, hp, hp0, hfin, -⟩ :=236    pi.exists_nonzero_finite_rank_spectral_projection hpi.1 a ha ha0 (hpi.2 a)237  exact ⟨p, hp, hp0, hfin⟩238239end NonUnitalCStarRepresentation240241end MathlibAnnex.Analysis.CStarAlgebra