Exact source: MathlibAnnex/Analysis/CStarAlgebra/Compression.lean
Pinned GitHub source · Raw UTF-8 source
Back to The matching GNS fiber retains exactly its cyclic line
1import Mathlib.Analysis.InnerProductSpace.Adjoint2import MathlibAnnex.Analysis.InnerProductSpace.CommonFixed34/-!5Compression of a norm-convergent source flag inside a continuous Hilbert-space6representation. The conclusion is a matrix-coefficient identity on the common7fixed space; no bidual or transport of strong limits through representations is8used.9-/1011set_option autoImplicit false1213open Filter1415namespace MathlibAnnex.Analysis.CStarAlgebra1617variable {A H : Type*}18variable [NormedRing A] [NormedAlgebra ℂ A] [StarRing A]19variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]2021/--22If a compression error tends to zero in the source norm, then its matrix23coefficient vanishes on vectors fixed by every member of the flag. Continuity24of the representation is explicit; C*-representations supply it by standard25contractivity.26-/27theorem inner_map_eq_of_compression_tendsto28 (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (hpi : Continuous pi)29 (q : ℕ → A) (phi : A →ₗ[ℂ] ℂ) (b : A) (x y : H)30 (hq_star : ∀ n, star (q n) = q n)31 (hx : ∀ n, pi (q n) x = x) (hy : ∀ n, pi (q n) y = y)32 (hcompression :33 Tendsto (fun n ↦ q n * b * q n - (phi b) • q n) atTop (nhds 0)) :34 inner ℂ x (pi b y) = phi b * inner ℂ x y := by35 have hop :36 Tendsto (fun n ↦ pi (q n * b * q n - (phi b) • q n)) atTop (nhds 0) := by37 change Tendsto (pi ∘ fun n ↦ q n * b * q n - (phi b) • q n) atTop (nhds 0)38 simpa only [map_zero] using (hpi.tendsto 0).comp hcompression39 have happ :40 Tendsto (fun n ↦ pi (q n * b * q n - (phi b) • q n) y) atTop (nhds 0) := by41 simpa [Function.comp_def] using42 ((ContinuousLinearMap.apply ℂ H y).continuous.tendsto 0).comp hop43 have hinner :44 Tendsto45 (fun n ↦ inner ℂ x (pi (q n * b * q n - (phi b) • q n) y))46 atTop (nhds 0) := by47 simpa using tendsto_const_nhds.inner happ48 have hcoeff (n : ℕ) :49 inner ℂ x (pi (q n * b * q n - (phi b) • q n) y) =50 inner ℂ x (pi b y) - phi b * inner ℂ x y := by51 have hself : ContinuousLinearMap.adjoint (pi (q n)) = pi (q n) := by52 calc53 ContinuousLinearMap.adjoint (pi (q n)) = star (pi (q n)) := by54 rw [ContinuousLinearMap.star_eq_adjoint]55 _ = pi (star (q n)) := (map_star pi (q n)).symm56 _ = pi (q n) := by rw [hq_star n]57 calc58 inner ℂ x (pi (q n * b * q n - (phi b) • q n) y) =59 inner ℂ x (pi (q n) (pi b (pi (q n) y))) -60 inner ℂ x ((phi b) • pi (q n) y) := by61 simp only [map_sub, map_mul, map_smul, ContinuousLinearMap.sub_apply,62 ContinuousLinearMap.mul_apply, ContinuousLinearMap.smul_apply, inner_sub_right]63 _ = inner ℂ x (pi (q n) (pi b y)) -64 inner ℂ x ((phi b) • y) := by rw [hy n]65 _ = inner ℂ (pi (q n) x) (pi b y) -66 inner ℂ x ((phi b) • y) := by67 simpa [hself] using68 (ContinuousLinearMap.adjoint_inner_right (pi (q n)) x (pi b y))69 _ = inner ℂ x (pi b y) - phi b * inner ℂ x y := by70 rw [hx n, inner_smul_right]71 have hconstant :72 Tendsto73 (fun _ : ℕ ↦ inner ℂ x (pi b y) - phi b * inner ℂ x y)74 atTop (nhds 0) :=75 hinner.congr' (Filter.Eventually.of_forall fun n ↦ hcoeff n)76 have hconst :77 Tendsto78 (fun _ : ℕ ↦ inner ℂ x (pi b y) - phi b * inner ℂ x y)79 atTop (nhds (inner ℂ x (pi b y) - phi b * inner ℂ x y)) :=80 tendsto_const_nhds81 have hz : inner ℂ x (pi b y) - phi b * inner ℂ x y = 0 :=82 tendsto_nhds_unique hconst hconstant83 exact sub_eq_zero.mp hz8485/--86Operator form of compression onto a supplied orthogonal projection whose range87is contained in the common fixed space. This is the manuscript's compression88formula, still without moving a strong limit through `pi`.89-/90theorem projection_comp_map_comp_projection_eq91 (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (hpi : Continuous pi)92 (q : ℕ → A) (phi : A →ₗ[ℂ] ℂ) (b : A)93 (hq_star : ∀ n, star (q n) = q n)94 (hcompression :95 Tendsto (fun n ↦ q n * b * q n - (phi b) • q n) atTop (nhds 0))96 (P : H →L[ℂ] H) (hP_star : ContinuousLinearMap.adjoint P = P)97 (hP_idem : P * P = P)98 (hP_fixed : ∀ (n : ℕ) (z : H), pi (q n) (P z) = P z) :99 P * pi b * P = (phi b) • P := by100 apply ContinuousLinearMap.ext101 intro z102 apply ext_inner_left ℂ103 intro w104 have hcoeff := inner_map_eq_of_compression_tendsto pi hpi q phi b (P w) (P z)105 hq_star (fun n ↦ hP_fixed n w) (fun n ↦ hP_fixed n z) hcompression106 have hPPinner : inner ℂ (P w) (P z) = inner ℂ w (P z) := by107 have hPP : P (P z) = P z := by108 have := congrArg (fun T : H →L[ℂ] H ↦ T z) hP_idem109 simpa using this110 calc111 inner ℂ (P w) (P z) =112 inner ℂ w (ContinuousLinearMap.adjoint P (P z)) := by113 symm114 exact ContinuousLinearMap.adjoint_inner_right P w (P z)115 _ = inner ℂ w (P z) := by rw [hP_star, hPP]116 calc117 inner ℂ w ((P * pi b * P) z) = inner ℂ w (P (pi b (P z))) := rfl118 _ = inner ℂ (P w) (pi b (P z)) := by119 simpa [hP_star] using120 (ContinuousLinearMap.adjoint_inner_right P w (pi b (P z)))121 _ = phi b * inner ℂ (P w) (P z) := hcoeff122 _ = phi b * inner ℂ w (P z) := congrArg (fun c : ℂ ↦ phi b * c) hPPinner123 _ = inner ℂ w (((phi b) • P) z) := by124 simp [inner_smul_right]125126/--127Compression formula for the actual orthogonal projection onto the common fixed128space of the represented flag.129-/130theorem commonFixedProjection_comp_map_comp_eq131 (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (hpi : Continuous pi)132 (q : ℕ → A) (phi : A →ₗ[ℂ] ℂ) (b : A)133 (hq_star : ∀ n, star (q n) = q n)134 (hcompression :135 Tendsto (fun n ↦ q n * b * q n - (phi b) • q n) atTop (nhds 0)) :136 let P := MathlibAnnex.Analysis.InnerProductSpace.commonFixedProjection137 (fun n ↦ pi (q n))138 P * pi b * P = (phi b) • P := by139 let Q : ℕ → H →L[ℂ] H := fun n ↦ pi (q n)140 let P := MathlibAnnex.Analysis.InnerProductSpace.commonFixedProjection Q141 exact projection_comp_map_comp_projection_eq pi hpi q phi b hq_star hcompression P142 (MathlibAnnex.Analysis.InnerProductSpace.adjoint_commonFixedProjection Q)143 (MathlibAnnex.Analysis.InnerProductSpace.commonFixedProjection_idempotent Q)144 (fun n z ↦ MathlibAnnex.Analysis.InnerProductSpace.commonFixedProjection_apply_fixed Q n z)145146/--147A compression projection is rank one when the chosen vector is cyclic for the148whole representation. The density hypothesis is essential: without it this149does not identify an ambient common-fixed projection of arbitrary150multiplicity.151-/152theorem projection_eq_rankOne_of_dense_orbit153 (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (phi : A →ₗ[ℂ] ℂ)154 (P : H →L[ℂ] H) (eta : H)155 (hPeta : P eta = eta)156 (hcompression : ∀ b : A, P * pi b * P = (phi b) • P)157 (hphi : ∀ b : A, phi b = inner ℂ eta (pi b eta))158 (hdense : DenseRange (fun b : A ↦ pi b eta)) :159 P = InnerProductSpace.rankOne ℂ eta eta := by160 apply ContinuousLinearMap.ext161 intro x162 induction x using hdense.induction_on with163 | hp => apply isClosed_eq <;> fun_prop164 | ih b =>165 have happ := congrArg (fun T : H →L[ℂ] H ↦ T eta) (hcompression b)166 have hPb : P (pi b eta) = phi b • eta := by167 simpa [hPeta] using happ168 calc169 P (pi b eta) = phi b • eta := hPb170 _ = inner ℂ eta (pi b eta) • eta := by rw [hphi b]171 _ = InnerProductSpace.rankOne ℂ eta eta (pi b eta) := by172 rw [InnerProductSpace.rankOne_apply]173174end MathlibAnnex.Analysis.CStarAlgebra