Exact source: MathlibAnnex/Analysis/CStarAlgebra/ExactInterpolation.lean
Pinned GitHub source · Raw UTF-8 source
Back to Full operator image in finite dimension
1import MathlibAnnex.Analysis.CStarAlgebra.Kadison2import Mathlib.Analysis.InnerProductSpace.PiL23import Mathlib.Analysis.InnerProductSpace.StarOrder4import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute5import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric6import Mathlib.LinearAlgebra.FiniteDimensional.Basic78/-!9# Exact finite-dimensional self-adjoint interpolation1011This file upgrades norm-budget Kadison approximation to exact interpolation on a12finite-dimensional subspace. The proof converts coordinate errors to a restricted13operator-norm error, corrects the self-adjoint residual on the orthogonal projection,14and sums explicitly controlled geometric corrections. In particular, it never15assumes that independently selected one-shot approximants converge.16-/1718set_option autoImplicit false1920open scoped InnerProductSpace CStarAlgebra ENNReal lp21open MathlibAnnex.Analysis.CStarAlgebra22open MathlibAnnex.Analysis.InnerProductSpace2324namespace MathlibAnnex.Analysis.CStarAlgebra2526theorem norm_comp_starProjection_le_sum27 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]28 [CompleteSpace H] (E : Submodule ℂ H) [E.HasOrthogonalProjection]29 [FiniteDimensional ℂ E] (D : H →L[ℂ] H) :30 ‖D * E.starProjection‖ ≤31 ∑ i : Fin (Module.finrank ℂ E),32 ‖D ((stdOrthonormalBasis ℂ E i : E) : H)‖ := by33 let b : OrthonormalBasis (Fin (Module.finrank ℂ E)) ℂ E :=34 stdOrthonormalBasis ℂ E35 rw [show E.starProjection =36 ∑ i, InnerProductSpace.rankOne ℂ ((b i : E) : H) ((b i : E) : H) by37 exact b.starProjection_eq_sum_rankOne]38 rw [Finset.mul_sum]39 calc40 ‖∑ i, D * InnerProductSpace.rankOne ℂ ((b i : E) : H) ((b i : E) : H)‖ ≤41 ∑ i, ‖D * InnerProductSpace.rankOne ℂ ((b i : E) : H) ((b i : E) : H)‖ :=42 norm_sum_le _ _43 _ = ∑ i, ‖D ((b i : E) : H)‖ := by44 apply Finset.sum_congr rfl45 intro i _46 rw [show D * InnerProductSpace.rankOne ℂ ((b i : E) : H) ((b i : E) : H) =47 InnerProductSpace.rankOne ℂ (D ((b i : E) : H)) ((b i : E) : H) by48 exact InnerProductSpace.comp_rankOne _ _ D]49 have hbnorm : ‖((b i : E) : H)‖ = 1 := b.norm_eq_one i50 rw [InnerProductSpace.norm_rankOne, hbnorm, mul_one]5152/-- The self-adjoint residual supported on a projection. -/53def projectionResidual54 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]55 (R P : H →L[ℂ] H) : H →L[ℂ] H :=56 R * P + P * R - P * R * P5758theorem isSelfAdjoint_projectionResidual59 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]60 [CompleteSpace H] {R P : H →L[ℂ] H}61 (hR : IsSelfAdjoint R) (hP : IsSelfAdjoint P) :62 IsSelfAdjoint (projectionResidual R P) := by63 rw [IsSelfAdjoint]64 simp only [projectionResidual, star_sub, star_add, star_mul,65 hR.star_eq, hP.star_eq]66 noncomm_ring6768theorem projectionResidual_mul69 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]70 [CompleteSpace H] {R P : H →L[ℂ] H} (hP : P * P = P) :71 projectionResidual R P * P = R * P := by72 simp only [projectionResidual, add_mul, sub_mul, mul_assoc, hP]73 abel7475theorem norm_projectionResidual_le76 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]77 [CompleteSpace H] {R P : H →L[ℂ] H}78 (hR : IsSelfAdjoint R) (hP : IsSelfAdjoint P) (hPnorm : ‖P‖ ≤ 1) :79 ‖projectionResidual R P‖ ≤ 3 * ‖R * P‖ := by80 have hPR : ‖P * R‖ = ‖R * P‖ := by81 calc82 ‖P * R‖ = ‖star (R * P)‖ := by rw [star_mul, hR.star_eq, hP.star_eq]83 _ = ‖R * P‖ := norm_star _84 have hPRP : ‖P * R * P‖ ≤ ‖R * P‖ := by85 calc86 ‖P * R * P‖ = ‖P * (R * P)‖ := by rw [mul_assoc]87 _ ≤ ‖P‖ * ‖R * P‖ := norm_mul_le _ _88 _ ≤ 1 * ‖R * P‖ := mul_le_mul_of_nonneg_right hPnorm (norm_nonneg _)89 _ = ‖R * P‖ := one_mul _90 calc91 ‖projectionResidual R P‖ ≤ ‖R * P + P * R‖ + ‖P * R * P‖ := by92 exact norm_sub_le (R * P + P * R) (P * R * P)93 _ ≤ (‖R * P‖ + ‖P * R‖) + ‖P * R * P‖ := by94 gcongr95 exact norm_add_le (R * P) (P * R)96 _ ≤ (‖R * P‖ + ‖R * P‖) + ‖R * P‖ := by97 rw [hPR]98 gcongr99 _ = 3 * ‖R * P‖ := by ring100101theorem exists_selfAdjoint_norm_le_and_norm_sub_mul_starProjection_lt102 {A H : Type*} [CStarAlgebra A]103 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]104 [Nontrivial H] (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H))105 (hpi : StarAlgHom.IsIrreducible pi)106 (E : Submodule ℂ H) [E.HasOrthogonalProjection] [FiniteDimensional ℂ E]107 (T : H →L[ℂ] H) (hT : IsSelfAdjoint T)108 {epsilon : ℝ} (hepsilon : 0 < epsilon) :109 ∃ a : A, IsSelfAdjoint a ∧ ‖a‖ ≤ ‖T‖ ∧110 ‖(pi a - T) * E.starProjection‖ < epsilon := by111 classical112 let b : OrthonormalBasis (Fin (Module.finrank ℂ E)) ℂ E :=113 stdOrthonormalBasis ℂ E114 let delta : ℝ := epsilon / ((Module.finrank ℂ E : ℝ) + 1)115 have hdelta : 0 < delta := by116 dsimp [delta]117 positivity118 obtain ⟨a, ha, hanorm, happ⟩ :=119 pi.exists_selfAdjoint_atomic_apply_sub_norm_lt_of_irreducible_norm_le120 hpi (fun i => ((b i : E) : H)) T hT hdelta121 refine ⟨a, ha, hanorm, ?_⟩122 have hcoord : ∀ i : Fin (Module.finrank ℂ E),123 ‖(pi a - T) ((b i : E) : H)‖ < delta := by124 intro i125 have hle := lp.norm_apply_le_norm (by norm_num : (2 : ℝ≥0∞) ≠ 0)126 (atomicRepresentation (fun _ : Fin (Module.finrank ℂ E) => pi) a127 (finiteHilbertSum (fun i => ((b i : E) : H))) -128 diagonal (fun _ : Fin (Module.finrank ℂ E) => T) ‖T‖129 (norm_nonneg T) (fun _ => le_rfl)130 (finiteHilbertSum (fun i => ((b i : E) : H)))) i131 have hpoint :132 ‖(pi a - T) ((b i : E) : H)‖ ≤133 ‖atomicRepresentation (fun _ : Fin (Module.finrank ℂ E) => pi) a134 (finiteHilbertSum (fun i => ((b i : E) : H))) -135 diagonal (fun _ : Fin (Module.finrank ℂ E) => T) ‖T‖136 (norm_nonneg T) (fun _ => le_rfl)137 (finiteHilbertSum (fun i => ((b i : E) : H)))‖ := by138 simpa [sub_apply, atomicRepresentation_apply,139 diagonal_apply, finiteHilbertSum_apply] using hle140 exact hpoint.trans_lt happ141 calc142 ‖(pi a - T) * E.starProjection‖ ≤143 ∑ i : Fin (Module.finrank ℂ E),144 ‖(pi a - T) ((b i : E) : H)‖ :=145 norm_comp_starProjection_le_sum E (pi a - T)146 _ ≤ ∑ _i : Fin (Module.finrank ℂ E), delta := by147 exact Finset.sum_le_sum fun i _ => (hcoord i).le148 _ = (Module.finrank ℂ E : ℝ) * delta := by simp149 _ < epsilon := by150 have hlt : (Module.finrank ℂ E : ℝ) <151 (Module.finrank ℂ E : ℝ) + 1 := by linarith152 calc153 (Module.finrank ℂ E : ℝ) * delta <154 ((Module.finrank ℂ E : ℝ) + 1) * delta :=155 mul_lt_mul_of_pos_right hlt hdelta156 _ = epsilon := by157 dsimp [delta]158 field_simp159160private structure InterpolationState161 {A H : Type*} [CStarAlgebra A]162 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]163 (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H))164 (E : Submodule ℂ H) [E.HasOrthogonalProjection]165 (T : H →L[ℂ] H) (n : ℕ) where166 value : A167 isSelfAdjoint : IsSelfAdjoint value168 error_lt : ‖(T - pi value) * E.starProjection‖ < ‖T‖ / 6 / 2 ^ n169170private theorem exists_initialState171 {A H : Type*} [CStarAlgebra A]172 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]173 [Nontrivial H] (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H))174 (hpi : StarAlgHom.IsIrreducible pi)175 (E : Submodule ℂ H) [E.HasOrthogonalProjection] [FiniteDimensional ℂ E]176 (T : H →L[ℂ] H) (hT : IsSelfAdjoint T) (hTnorm : 0 < ‖T‖) :177 ∃ s : InterpolationState pi E T 0, ‖s.value‖ ≤ ‖T‖ := by178 obtain ⟨a, ha, hanorm, happ⟩ :=179 exists_selfAdjoint_norm_le_and_norm_sub_mul_starProjection_lt180 pi hpi E T hT (by positivity : 0 < ‖T‖ / 6)181 refine ⟨⟨a, ha, ?_⟩, hanorm⟩182 have hid : (T - pi a) * E.starProjection = -(pi a - T) * E.starProjection := by183 noncomm_ring184 rw [hid, neg_mul, norm_neg]185 simpa only [pow_zero, div_one] using happ186187private theorem exists_nextState188 {A H : Type*} [CStarAlgebra A]189 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]190 [Nontrivial H] (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H))191 (hpi : StarAlgHom.IsIrreducible pi)192 (E : Submodule ℂ H) [E.HasOrthogonalProjection] [FiniteDimensional ℂ E]193 (T : H →L[ℂ] H) (hT : IsSelfAdjoint T) (hTnorm : 0 < ‖T‖)194 (n : ℕ) (s : InterpolationState pi E T n) :195 ∃ t : InterpolationState pi E T (n + 1),196 IsSelfAdjoint (t.value - s.value) ∧197 ‖t.value - s.value‖ ≤ ‖T‖ / 2 / 2 ^ n := by198 let P : H →L[ℂ] H := E.starProjection199 let R : H →L[ℂ] H := T - pi s.value200 let B : H →L[ℂ] H := projectionResidual R P201 have hP : IsSelfAdjoint P := isSelfAdjoint_starProjection E202 have hR : IsSelfAdjoint R := hT.sub (s.isSelfAdjoint.map pi)203 have hB : IsSelfAdjoint B := isSelfAdjoint_projectionResidual hR hP204 have hBP : B * P = R * P := by205 exact projectionResidual_mul E.isIdempotentElem_starProjection206 have hBnorm : ‖B‖ < ‖T‖ / 2 / 2 ^ n := by207 calc208 ‖B‖ ≤ 3 * ‖R * P‖ :=209 norm_projectionResidual_le hR hP E.starProjection_norm_le210 _ < 3 * (‖T‖ / 6 / 2 ^ n) := by211 gcongr212 exact s.error_lt213 _ = ‖T‖ / 2 / 2 ^ n := by ring214 have heps : 0 < ‖T‖ / 6 / 2 ^ (n + 1) := by positivity215 obtain ⟨c, hc, hcnorm, hcapp⟩ :=216 exists_selfAdjoint_norm_le_and_norm_sub_mul_starProjection_lt217 pi hpi E B hB heps218 let tval : A := s.value + c219 have htself : IsSelfAdjoint tval := s.isSelfAdjoint.add hc220 have hterror : ‖(T - pi tval) * P‖ < ‖T‖ / 6 / 2 ^ (n + 1) := by221 have hid : (T - pi tval) * P = -(pi c - B) * P := by222 calc223 (T - pi tval) * P = (R - pi c) * P := by224 simp only [R, tval, map_add]225 noncomm_ring226 _ = B * P - pi c * P := by rw [sub_mul, ← hBP]227 _ = (B - pi c) * P := by rw [sub_mul]228 _ = -(pi c - B) * P := by noncomm_ring229 rw [hid, neg_mul, norm_neg]230 simpa [P] using hcapp231 refine ⟨⟨tval, htself, ?_⟩, ?_, ?_⟩232 · exact hterror233 · simpa [tval] using hc234 · simpa [tval] using hcnorm.trans hBnorm.le235236private noncomputable def initialState237 {A H : Type*} [CStarAlgebra A]238 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]239 [Nontrivial H] (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H))240 (hpi : StarAlgHom.IsIrreducible pi)241 (E : Submodule ℂ H) [E.HasOrthogonalProjection] [FiniteDimensional ℂ E]242 (T : H →L[ℂ] H) (hT : IsSelfAdjoint T) (hTnorm : 0 < ‖T‖) :243 InterpolationState pi E T 0 :=244 Classical.choose (exists_initialState pi hpi E T hT hTnorm)245246private theorem initialState_norm_le247 {A H : Type*} [CStarAlgebra A]248 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]249 [Nontrivial H] (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H))250 (hpi : StarAlgHom.IsIrreducible pi)251 (E : Submodule ℂ H) [E.HasOrthogonalProjection] [FiniteDimensional ℂ E]252 (T : H →L[ℂ] H) (hT : IsSelfAdjoint T) (hTnorm : 0 < ‖T‖) :253 ‖(initialState pi hpi E T hT hTnorm).value‖ ≤ ‖T‖ :=254 (Classical.choose_spec (exists_initialState pi hpi E T hT hTnorm))255256private noncomputable def nextState257 {A H : Type*} [CStarAlgebra A]258 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]259 [Nontrivial H] (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H))260 (hpi : StarAlgHom.IsIrreducible pi)261 (E : Submodule ℂ H) [E.HasOrthogonalProjection] [FiniteDimensional ℂ E]262 (T : H →L[ℂ] H) (hT : IsSelfAdjoint T) (hTnorm : 0 < ‖T‖)263 (n : ℕ) (s : InterpolationState pi E T n) : InterpolationState pi E T (n + 1) :=264 Classical.choose (exists_nextState pi hpi E T hT hTnorm n s)265266private theorem isSelfAdjoint_nextState_sub267 {A H : Type*} [CStarAlgebra A]268 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]269 [Nontrivial H] (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H))270 (hpi : StarAlgHom.IsIrreducible pi)271 (E : Submodule ℂ H) [E.HasOrthogonalProjection] [FiniteDimensional ℂ E]272 (T : H →L[ℂ] H) (hT : IsSelfAdjoint T) (hTnorm : 0 < ‖T‖)273 (n : ℕ) (s : InterpolationState pi E T n) :274 IsSelfAdjoint275 ((nextState pi hpi E T hT hTnorm n s).value - s.value) :=276 (Classical.choose_spec277 (exists_nextState pi hpi E T hT hTnorm n s)).1278279private theorem nextState_sub_norm_le280 {A H : Type*} [CStarAlgebra A]281 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]282 [Nontrivial H] (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H))283 (hpi : StarAlgHom.IsIrreducible pi)284 (E : Submodule ℂ H) [E.HasOrthogonalProjection] [FiniteDimensional ℂ E]285 (T : H →L[ℂ] H) (hT : IsSelfAdjoint T) (hTnorm : 0 < ‖T‖)286 (n : ℕ) (s : InterpolationState pi E T n) :287 ‖(nextState pi hpi E T hT hTnorm n s).value - s.value‖ ≤288 ‖T‖ / 2 / 2 ^ n :=289 (Classical.choose_spec290 (exists_nextState pi hpi E T hT hTnorm n s)).2291292theorem exists_selfAdjoint_norm_le_two_mul_and_sub_mul_starProjection_eq_zero293 {A H : Type*} [CStarAlgebra A]294 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]295 [Nontrivial H] (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H))296 (hpi : StarAlgHom.IsIrreducible pi)297 (E : Submodule ℂ H) [E.HasOrthogonalProjection] [FiniteDimensional ℂ E]298 (T : H →L[ℂ] H) (hT : IsSelfAdjoint T) :299 ∃ a : A, IsSelfAdjoint a ∧ ‖a‖ ≤ 2 * ‖T‖ ∧300 (T - pi a) * E.starProjection = 0 := by301 classical302 by_cases hTzero : ‖T‖ = 0303 · have hT' : T = 0 := norm_eq_zero.mp hTzero304 refine ⟨0, .zero A, ?_, ?_⟩305 · simp [hTzero]306 · simp [hT']307 have hTnorm : 0 < ‖T‖ := lt_of_le_of_ne (norm_nonneg T) (Ne.symm hTzero)308 let s0 : InterpolationState pi E T 0 :=309 initialState pi hpi E T hT hTnorm310 let s : ∀ n : ℕ, InterpolationState pi E T n := fun n =>311 Nat.rec s0 (fun n t => nextState pi hpi E T hT hTnorm n t) n312 let c : ℕ → A := fun n => (s (n + 1)).value - (s n).value313 have hs0norm : ‖(s 0).value‖ ≤ ‖T‖ := by314 simpa [s, s0] using initialState_norm_le pi hpi E T hT hTnorm315 have hcself (n : ℕ) : IsSelfAdjoint (c n) := by316 simpa [c, s] using317 isSelfAdjoint_nextState_sub pi hpi E T hT hTnorm n (s n)318 have hcnorm (n : ℕ) : ‖c n‖ ≤ ‖T‖ / 2 / 2 ^ n := by319 simpa [c, s] using320 nextState_sub_norm_le pi hpi E T hT hTnorm n (s n)321 have hcsum : Summable c :=322 (summable_geometric_two' ‖T‖).of_norm_bounded hcnorm323 have hcnormsum : Summable (fun n => ‖c n‖) :=324 (summable_geometric_two' ‖T‖).of_nonneg_of_le325 (fun n => norm_nonneg (c n)) hcnorm326 have hspartial (n : ℕ) :327 (s n).value = (s 0).value + ∑ i ∈ Finset.range n, c i := by328 induction n with329 | zero => simp330 | succ n ih =>331 calc332 (s (n + 1)).value = (s n).value + c n := by333 simp only [c]334 abel335 _ = (s 0).value + (∑ i ∈ Finset.range n, c i) + c n := by rw [ih]336 _ = (s 0).value + ∑ i ∈ Finset.range (n + 1), c i := by337 rw [Finset.sum_range_succ]338 abel339 let a : A := (s 0).value + ∑' n, c n340 have hsumself : IsSelfAdjoint (∑' n, c n) := by341 rw [IsSelfAdjoint, tsum_star]342 apply tsum_congr343 intro n344 exact (hcself n).star_eq345 have haself : IsSelfAdjoint a := (s 0).isSelfAdjoint.add hsumself346 have hanorm : ‖a‖ ≤ 2 * ‖T‖ := by347 calc348 ‖a‖ ≤ ‖(s 0).value‖ + ‖∑' n, c n‖ := by349 exact norm_add_le _ _350 _ ≤ ‖T‖ + ∑' n, ‖c n‖ :=351 add_le_add hs0norm (norm_tsum_le_tsum_norm hcnormsum)352 _ ≤ ‖T‖ + ∑' n : ℕ, ‖T‖ / 2 / 2 ^ n := by353 exact add_le_add le_rfl354 (Summable.tsum_le_tsum hcnorm hcnormsum (summable_geometric_two' ‖T‖))355 _ = 2 * ‖T‖ := by rw [tsum_geometric_two']; ring356 have hstendsto : Filter.Tendsto (fun n => (s n).value) Filter.atTop (nhds a) := by357 have hsumtendsto := hcsum.hasSum.tendsto_sum_nat358 have hconst : Filter.Tendsto (fun _ : ℕ => (s 0).value) Filter.atTop359 (nhds (s 0).value) := tendsto_const_nhds360 have hadd := hconst.add hsumtendsto361 rw [show (fun n => (s n).value) =362 (fun n => (s 0).value + ∑ i ∈ Finset.range n, c i) by363 funext n364 exact hspartial n]365 simpa only [a] using hadd366 let piL : A →L[ℂ] (H →L[ℂ] H) :=367 pi.toAlgHom.toLinearMap.mkContinuous 1 fun x => by368 change ‖pi x‖ ≤ 1 * ‖x‖369 simpa only [one_mul] using NonUnitalStarAlgHom.norm_apply_le pi x370 have hpistendsto :371 Filter.Tendsto (fun n => pi (s n).value) Filter.atTop (nhds (pi a)) := by372 have hcont : Continuous piL := piL.continuous373 change Filter.Tendsto (fun n => piL (s n).value) Filter.atTop (nhds (piL a))374 exact (hcont.tendsto a).comp hstendsto375 have hrestendsto :376 Filter.Tendsto (fun n => (T - pi (s n).value) * E.starProjection)377 Filter.atTop (nhds ((T - pi a) * E.starProjection)) := by378 exact (tendsto_const_nhds.sub hpistendsto).mul tendsto_const_nhds379 have hgeom :380 Filter.Tendsto (fun n : ℕ => ‖T‖ / 6 / 2 ^ n) Filter.atTop (nhds 0) := by381 have hpow : Filter.Tendsto (fun n : ℕ => (1 / 2 : ℝ) ^ n)382 Filter.atTop (nhds 0) :=383 tendsto_pow_atTop_nhds_zero_of_lt_one (r := (1 / 2 : ℝ)) (by norm_num) (by norm_num)384 have hid : (fun n : ℕ => ‖T‖ / 6 / 2 ^ n) =385 (fun n : ℕ => (‖T‖ / 6) * (1 / 2 : ℝ) ^ n) := by386 funext n387 simp only [div_eq_mul_inv, one_mul, inv_pow]388 rw [hid]389 convert tendsto_const_nhds.mul hpow using 1390 simp391 have hresnormzero :392 Filter.Tendsto (fun n => ‖(T - pi (s n).value) * E.starProjection‖)393 Filter.atTop (nhds 0) :=394 squeeze_zero (fun n => norm_nonneg _)395 (fun n => (s n).error_lt.le) hgeom396 have hreszero :397 Filter.Tendsto (fun n => (T - pi (s n).value) * E.starProjection)398 Filter.atTop (nhds 0) :=399 tendsto_zero_iff_norm_tendsto_zero.mpr hresnormzero400 refine ⟨a, haself, hanorm, ?_⟩401 exact tendsto_nhds_unique hrestendsto hreszero402403/-- Coarse norm-controlled exact self-adjoint interpolation on a finite-dimensional404subspace. The factor `2` is the geometric-correction bound; no convergence of405independently selected one-shot approximants is assumed. -/406theorem exists_selfAdjoint_norm_le_two_mul_and_eq_on407 {A H : Type*} [CStarAlgebra A]408 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]409 [Nontrivial H] (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H))410 (hpi : StarAlgHom.IsIrreducible pi)411 (E : Submodule ℂ H) [E.HasOrthogonalProjection] [FiniteDimensional ℂ E]412 (T : H →L[ℂ] H) (hT : IsSelfAdjoint T) :413 ∃ a : A, IsSelfAdjoint a ∧ ‖a‖ ≤ 2 * ‖T‖ ∧414 ∀ x : H, x ∈ E → pi a x = T x := by415 obtain ⟨a, ha, hanorm, hexact⟩ :=416 exists_selfAdjoint_norm_le_two_mul_and_sub_mul_starProjection_eq_zero417 pi hpi E T hT418 refine ⟨a, ha, hanorm, fun x hx => ?_⟩419 have happ := congrArg (fun S : H →L[ℂ] H => S x) hexact420 have hproj : E.starProjection x = x := E.starProjection_eq_self_iff.mpr hx421 have hzero : T x - pi a x = 0 := by422 simpa [ContinuousLinearMap.comp_apply, hproj] using happ423 exact (sub_eq_zero.mp hzero).symm424425/-- The finite enlargement generated by `E` and its image under `T`. -/426noncomputable def finiteReduction427 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]428 (E : Submodule ℂ H) (T : H →L[ℂ] H) : Submodule ℂ H :=429 E ⊔ E.map T.toLinearMap430431noncomputable instance instFiniteDimensionalFiniteReduction432 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]433 (E : Submodule ℂ H) [FiniteDimensional ℂ E] (T : H →L[ℂ] H) :434 FiniteDimensional ℂ (finiteReduction E T) := by435 dsimp [finiteReduction]436 exact Submodule.finiteDimensional_sup E (E.map T.toLinearMap)437438/-- Compression of `T` to the finite enlargement `E + T(E)`, extended by zero439on its orthogonal complement. -/440noncomputable def finiteCompression441 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]442 [CompleteSpace H] (E : Submodule ℂ H) [FiniteDimensional ℂ E]443 (T : H →L[ℂ] H) : H →L[ℂ] H :=444 let F := finiteReduction E T445 F.starProjection * T * F.starProjection446447theorem isSelfAdjoint_finiteCompression448 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]449 [CompleteSpace H] (E : Submodule ℂ H) [FiniteDimensional ℂ E]450 (T : H →L[ℂ] H) (hT : IsSelfAdjoint T) :451 IsSelfAdjoint (finiteCompression E T) := by452 let F := finiteReduction E T453 exact hT.conj_starProjection F454455theorem finiteCompression_nonneg456 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]457 [CompleteSpace H] (E : Submodule ℂ H) [FiniteDimensional ℂ E]458 (T : H →L[ℂ] H) (hT : 0 ≤ T) :459 0 ≤ finiteCompression E T := by460 let F := finiteReduction E T461 let c := CFC.sqrt T462 have hcself : IsSelfAdjoint c := IsSelfAdjoint.of_nonneg (CFC.sqrt_nonneg T)463 have hcsq : c * c = T := by464 simpa only [c] using CFC.sqrt_mul_sqrt_self T hT465 rw [show finiteCompression E T = star (c * F.starProjection) *466 (c * F.starProjection) by467 change F.starProjection * T * F.starProjection =468 star (c * F.starProjection) * (c * F.starProjection)469 rw [star_mul, (isSelfAdjoint_starProjection F).star_eq, hcself.star_eq]470 calc471 F.starProjection * T * F.starProjection =472 F.starProjection * (c * c) * F.starProjection :=473 congrArg (fun R : H →L[ℂ] H =>474 F.starProjection * R * F.starProjection) hcsq.symm475 _ = F.starProjection * c * (c * F.starProjection) := by476 simp only [mul_assoc]]477 exact star_mul_self_nonneg _478479theorem norm_finiteCompression_le480 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]481 [CompleteSpace H] (E : Submodule ℂ H) [FiniteDimensional ℂ E]482 (T : H →L[ℂ] H) : ‖finiteCompression E T‖ ≤ ‖T‖ := by483 let F := finiteReduction E T484 calc485 ‖finiteCompression E T‖ ≤ ‖F.starProjection‖ * ‖T‖ * ‖F.starProjection‖ := by486 exact (norm_mul_le _ _).trans487 (mul_le_mul_of_nonneg_right (norm_mul_le _ _) (norm_nonneg _))488 _ ≤ 1 * ‖T‖ * 1 := by gcongr <;> exact F.starProjection_norm_le489 _ = ‖T‖ := by ring490491theorem finiteCompression_apply_of_mem492 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]493 [CompleteSpace H] (E : Submodule ℂ H) [FiniteDimensional ℂ E]494 (T : H →L[ℂ] H) {x : H} (hx : x ∈ E) :495 finiteCompression E T x = T x := by496 let F := finiteReduction E T497 have hxF : x ∈ F := (show E ≤ F from le_sup_left) hx498 have hTxF : T x ∈ F := by499 apply (show E.map T.toLinearMap ≤ F from le_sup_right)500 exact ⟨x, hx, rfl⟩501 simp [finiteCompression, F, F.starProjection_eq_self_iff.mpr hxF,502 F.starProjection_eq_self_iff.mpr hTxF]503504theorem finiteCompression_supported505 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]506 [CompleteSpace H] (E : Submodule ℂ H) [FiniteDimensional ℂ E]507 (T : H →L[ℂ] H) :508 let F := finiteReduction E T509 F.starProjection * finiteCompression E T = finiteCompression E T ∧510 finiteCompression E T * F.starProjection = finiteCompression E T := by511 let F := finiteReduction E T512 have hP : F.starProjection * F.starProjection = F.starProjection :=513 F.isIdempotentElem_starProjection514 change F.starProjection * (F.starProjection * T * F.starProjection) =515 F.starProjection * T * F.starProjection ∧516 (F.starProjection * T * F.starProjection) * F.starProjection =517 F.starProjection * T * F.starProjection518 constructor519 · calc520 F.starProjection * (F.starProjection * T * F.starProjection) =521 (F.starProjection * F.starProjection) * T * F.starProjection := by522 noncomm_ring523 _ = F.starProjection * T * F.starProjection := by rw [hP]524 · calc525 (F.starProjection * T * F.starProjection) * F.starProjection =526 F.starProjection * T * (F.starProjection * F.starProjection) := by527 noncomm_ring528 _ = F.starProjection * T * F.starProjection := by rw [hP]529530/-- The geometric exact interpolation applied to the finite compression on531`E + T(E)`. The represented witness and the compression agree on the whole532finite enlargement, so that enlargement reduces the represented witness. This533is the CFC-ready coarse-bound stage of the sharp Kadison argument. -/534theorem exists_selfAdjoint_finiteReduction_norm_le_two_mul535 {A H : Type*} [CStarAlgebra A]536 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]537 [Nontrivial H] (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H))538 (hpi : StarAlgHom.IsIrreducible pi)539 (E : Submodule ℂ H) [FiniteDimensional ℂ E]540 (T : H →L[ℂ] H) (hT : IsSelfAdjoint T) :541 let F := finiteReduction E T542 let S := finiteCompression E T543 ∃ a : A, IsSelfAdjoint a ∧ ‖a‖ ≤ 2 * ‖T‖ ∧544 pi a * F.starProjection = S ∧ F.starProjection * pi a = S ∧545 ∀ x : H, x ∈ E → pi a x = T x := by546 let F := finiteReduction E T547 let S := finiteCompression E T548 have hSself : IsSelfAdjoint S := isSelfAdjoint_finiteCompression E T hT549 obtain ⟨a, haself, hanormS, hexact⟩ :=550 exists_selfAdjoint_norm_le_two_mul_and_sub_mul_starProjection_eq_zero551 pi hpi F S hSself552 have hSnorm : ‖S‖ ≤ ‖T‖ := norm_finiteCompression_le E T553 have hanorm : ‖a‖ ≤ 2 * ‖T‖ := hanormS.trans (by gcongr)554 have hSsupport := finiteCompression_supported E T555 have hright : pi a * F.starProjection = S := by556 have hsub : S * F.starProjection - pi a * F.starProjection = 0 := by557 simpa only [sub_mul] using hexact558 calc559 pi a * F.starProjection = S * F.starProjection :=560 (sub_eq_zero.mp hsub).symm561 _ = S := hSsupport.2562 have hleft : F.starProjection * pi a = S := by563 calc564 F.starProjection * pi a = star (pi a * F.starProjection) := by565 rw [star_mul, haself.map pi |>.star_eq,566 (isSelfAdjoint_starProjection F).star_eq]567 _ = star S := by rw [hright]568 _ = S := hSself.star_eq569 refine ⟨a, haself, hanorm, hright, hleft, fun x hx => ?_⟩570 have hxF : x ∈ F := (show E ≤ F from le_sup_left) hx571 have happ := congrArg (fun R : H →L[ℂ] H => R x) hright572 have hproj : F.starProjection x = x := F.starProjection_eq_self_iff.mpr hxF573 simpa [hproj, S, finiteCompression_apply_of_mem E T hx] using happ574575/-! ## Functional calculus on a reducing projection -/576577/-- On the commutant of a star projection, multiplication by that projection578is a non-unital star algebra homomorphism. This is the small corner map used579to transport clipping through a reducing finite-dimensional summand. -/580noncomputable def centralizerRightMul581 {B : Type*} [CStarAlgebra B] (q : B) (hq : IsStarProjection q) :582 (StarSubalgebra.centralizer ℂ ({q} : Set B)) →⋆ₙₐ[ℂ] B where583 toFun x := (x : B) * q584 map_zero' := by simp585 map_add' x y := by simp [add_mul]586 map_smul' c x := by simp587 map_mul' x y := by588 have hy : q * (y : B) = (y : B) * q := by589 have hy' :=590 (StarSubalgebra.mem_centralizer_iff (R := ℂ)591 (s := ({q} : Set B)) (z := (y : B))).mp y.property q (by simp)592 exact hy'.1593 calc594 ((x : B) * (y : B)) * q = (x : B) * (y : B) * (q * q) := by595 rw [hq.isIdempotentElem.eq]596 _ = (x : B) * ((y : B) * q) * q := by simp only [mul_assoc]597 _ = (x : B) * (q * (y : B)) * q := by rw [hy]598 _ = ((x : B) * q) * ((y : B) * q) := by simp only [mul_assoc]599 map_star' x := by600 have hx : q * star (x : B) = star (x : B) * q := by601 have hx' :=602 (StarSubalgebra.mem_centralizer_iff (R := ℂ)603 (s := ({q} : Set B)) (z := (star x : B))).mp604 (star_mem x.property) q (by simp)605 exact hx'.1606 calc607 star (x : B) * q = q * star (x : B) := hx.symm608 _ = star q * star (x : B) := by rw [hq.isSelfAdjoint.star_eq]609 _ = star ((x : B) * q) := by rw [star_mul]610611/-- A continuous real function fixing zero respects equality after a common612reducing star projection. The proof uses the non-unital corner homomorphism,613so no polynomial-approximation hierarchy is introduced. -/614theorem cfc_mul_eq_of_mul_eq615 {B : Type*} [CStarAlgebra B] {a b q : B}616 (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b)617 (hq : IsStarProjection q) (haq : Commute a q) (hbq : Commute b q)618 (hab : a * q = b * q) (f : ℝ → ℝ) (hf : Continuous f)619 (hf0 : f 0 = 0) :620 cfc f a * q = cfc f b * q := by621 let C : StarSubalgebra ℂ B :=622 StarSubalgebra.centralizer ℂ ({q} : Set B)623 letI : IsClosed (C : Set B) := by624 dsimp only [C]625 rw [StarSubalgebra.coe_centralizer]626 exact Set.isClosed_centralizer _627 have haC : a ∈ C := by628 rw [StarSubalgebra.mem_centralizer_iff]629 intro z hz630 simp only [Set.mem_singleton_iff] at hz631 subst z632 constructor633 · exact haq.eq.symm634 · simpa [hq.isSelfAdjoint.star_eq] using haq.eq.symm635 have hbC : b ∈ C := by636 rw [StarSubalgebra.mem_centralizer_iff]637 intro z hz638 simp only [Set.mem_singleton_iff] at hz639 subst z640 constructor641 · exact hbq.eq.symm642 · simpa [hq.isSelfAdjoint.star_eq] using hbq.eq.symm643 let ac : C := ⟨a, haC⟩644 let bc : C := ⟨b, hbC⟩645 have hacself : IsSelfAdjoint ac := by646 rw [isSelfAdjoint_iff]647 exact Subtype.ext ha.star_eq648 have hbcself : IsSelfAdjoint bc := by649 rw [isSelfAdjoint_iff]650 exact Subtype.ext hb.star_eq651 let ι : C →⋆ₐ[ℂ] B := C.subtype652 let r : C →⋆ₙₐ[ℂ] B := centralizerRightMul q hq653 have hιa : ι (cfcₙ f ac) = cfcₙ f a := by654 simpa [ι, ac] using655 (ι.toNonUnitalStarAlgHom.map_cfcₙ f ac656 (hf := hf.continuousOn) (hf₀ := hf0)657 (hφ := continuous_subtype_val) (ha := hacself) (hφa := ha))658 have hιb : ι (cfcₙ f bc) = cfcₙ f b := by659 simpa [ι, bc] using660 (ι.toNonUnitalStarAlgHom.map_cfcₙ f bc661 (hf := hf.continuousOn) (hf₀ := hf0)662 (hφ := continuous_subtype_val) (ha := hbcself) (hφa := hb))663 have hra := r.map_cfcₙ f ac664 (hf := hf.continuousOn) (hf₀ := hf0) (hφ := by fun_prop)665 (ha := hacself) (hφa := by cfc_tac)666 have hrb := r.map_cfcₙ f bc667 (hf := hf.continuousOn) (hf₀ := hf0) (hφ := by fun_prop)668 (ha := hbcself) (hφa := by cfc_tac)669 rw [show r ac = a * q by rfl] at hra670 rw [show r bc = b * q by rfl] at hrb671 calc672 cfc f a * q = cfcₙ f a * q := by673 rw [cfcₙ_eq_cfc hf.continuousOn hf0]674 _ = r (cfcₙ f ac) := by rw [← hιa]; rfl675 _ = cfcₙ f (a * q) := hra676 _ = cfcₙ f (b * q) := by rw [hab]677 _ = r (cfcₙ f bc) := hrb.symm678 _ = cfcₙ f b * q := by rw [← hιb]; rfl679 _ = cfc f b * q := by rw [cfcₙ_eq_cfc hf.continuousOn hf0]680681/-- Sharp norm-controlled exact self-adjoint interpolation on a682finite-dimensional subspace. The coarse exact witness is first made reducing683on `E + T(E)` and is then clipped by continuous functional calculus. -/684theorem exists_selfAdjoint_norm_le_and_eq_on685 {A H : Type*} [CStarAlgebra A]686 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]687 [Nontrivial H] (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H))688 (hpi : StarAlgHom.IsIrreducible pi)689 (E : Submodule ℂ H) [FiniteDimensional ℂ E]690 (T : H →L[ℂ] H) (hT : IsSelfAdjoint T) :691 ∃ a : A, IsSelfAdjoint a ∧ ‖a‖ ≤ ‖T‖ ∧692 ∀ x : H, x ∈ E → pi a x = T x := by693 let F := finiteReduction E T694 let S := finiteCompression E T695 let q : H →L[ℂ] H := F.starProjection696 obtain ⟨a, ha, -, hright, hleft, -⟩ :=697 exists_selfAdjoint_finiteReduction_norm_le_two_mul pi hpi E T hT698 have hSself : IsSelfAdjoint S := isSelfAdjoint_finiteCompression E T hT699 have hSnorm : ‖S‖ ≤ ‖T‖ := norm_finiteCompression_le E T700 have hSsupport := finiteCompression_supported E T701 have hinterval : -‖T‖ ≤ ‖T‖ :=702 (neg_nonpos.mpr (norm_nonneg T)).trans (norm_nonneg T)703 let f : ℝ → ℝ := fun x =>704 (Set.projIcc (-‖T‖) ‖T‖ hinterval x : ℝ)705 have hf : Continuous f := by706 dsimp only [f]707 fun_prop708 have hf0 : f 0 = 0 := by709 dsimp only [f]710 simp [Set.projIcc_of_mem, norm_nonneg]711 have hfnorm (x : ℝ) : ‖f x‖ ≤ ‖T‖ := by712 have hx := (Set.projIcc (-‖T‖) ‖T‖ hinterval x).property713 change |(Set.projIcc (-‖T‖) ‖T‖ hinterval x : ℝ)| ≤ ‖T‖714 exact abs_le.mpr hx715 have hfix : cfc f S = S := by716 calc717 cfc f S = cfc (fun x : ℝ => x) S := by718 apply cfc_congr719 intro x hx720 have hxnorm : ‖x‖ ≤ ‖S‖ := spectrum.norm_le_norm_of_mem hx721 have hxbound : -‖T‖ ≤ x ∧ x ≤ ‖T‖ := by722 rw [Real.norm_eq_abs, abs_le] at hxnorm723 exact ⟨(neg_le_neg hSnorm).trans hxnorm.1,724 hxnorm.2.trans hSnorm⟩725 dsimp only [f]726 exact congrArg Subtype.val727 (Set.projIcc_of_mem hinterval hxbound)728 _ = S := cfc_id' ℝ S729 have haq : Commute (pi a) q := by730 rw [commute_iff_eq]731 exact hright.trans hleft.symm732 have hSq : Commute S q := by733 rw [commute_iff_eq]734 exact hSsupport.2.trans hSsupport.1.symm735 let b : A := cfc f a736 have hbself : IsSelfAdjoint b := IsSelfAdjoint.cfc737 have hbnorm : ‖b‖ ≤ ‖T‖ := by738 exact norm_cfc_le (norm_nonneg T) fun x _ => hfnorm x739 have hpib : pi b = cfc f (pi a) := by740 exact StarAlgHomClass.map_cfc pi f a741 (hf := hf.continuousOn) (hφ := by fun_prop)742 (ha := ha) (hφa := ha.map pi)743 have hfcq : cfc f (pi a) * q = S := by744 calc745 cfc f (pi a) * q = cfc f S * q :=746 cfc_mul_eq_of_mul_eq (ha.map pi) hSself747 isStarProjection_starProjection haq hSq748 (hright.trans hSsupport.2.symm) f hf hf0749 _ = S := by rw [hfix, hSsupport.2]750 refine ⟨b, hbself, hbnorm, fun x hx => ?_⟩751 have hxF : x ∈ F := (show E ≤ F from le_sup_left) hx752 have hqx : q x = x := F.starProjection_eq_self_iff.mpr hxF753 have happ := congrArg (fun R : H →L[ℂ] H => R x) hfcq754 rw [hpib]755 simpa [ContinuousLinearMap.comp_apply, hqx, S,756 finiteCompression_apply_of_mem E T hx] using happ757758/-- Sharp positive exact interpolation on a finite-dimensional subspace.759The self-adjoint exact interpolant on the reducing enlargement is clipped to760the interval `[0, ‖T‖]`; the common reducing corner makes this second clipping761preserve the prescribed vectors exactly. -/762theorem exists_nonneg_norm_le_and_eq_on763 {A H : Type*} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]764 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]765 [Nontrivial H] (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H))766 (hpi : StarAlgHom.IsIrreducible pi)767 (E : Submodule ℂ H) [FiniteDimensional ℂ E]768 (T : H →L[ℂ] H) (hT : 0 ≤ T) :769 ∃ a : A, 0 ≤ a ∧ ‖a‖ ≤ ‖T‖ ∧770 ∀ x : H, x ∈ E → pi a x = T x := by771 let F := finiteReduction E T772 let S := finiteCompression E T773 let q : H →L[ℂ] H := F.starProjection774 have hTself : IsSelfAdjoint T := IsSelfAdjoint.of_nonneg hT775 have hSself : IsSelfAdjoint S := isSelfAdjoint_finiteCompression E T hTself776 have hSnonneg : 0 ≤ S := finiteCompression_nonneg E T hT777 have hSnorm : ‖S‖ ≤ ‖T‖ := norm_finiteCompression_le E T778 have hSsupport := finiteCompression_supported E T779 obtain ⟨a, ha, -, haexact⟩ :=780 exists_selfAdjoint_norm_le_and_eq_on pi hpi F S hSself781 have hright : pi a * q = S := by782 apply ContinuousLinearMap.ext783 intro x784 change pi a (q x) = S x785 rw [haexact (q x) (F.starProjection_apply_mem x)]786 have happ := congrArg (fun R : H →L[ℂ] H => R x) hSsupport.2787 simpa [ContinuousLinearMap.comp_apply] using happ788 have hleft : q * pi a = S := by789 calc790 q * pi a = star (pi a * q) := by791 rw [star_mul, ha.map pi |>.star_eq,792 (isSelfAdjoint_starProjection F).star_eq]793 _ = star S := by rw [hright]794 _ = S := hSself.star_eq795 have haq : Commute (pi a) q := by796 rw [commute_iff_eq]797 exact hright.trans hleft.symm798 have hSq : Commute S q := by799 rw [commute_iff_eq]800 exact hSsupport.2.trans hSsupport.1.symm801 have hinterval : 0 ≤ ‖T‖ := norm_nonneg T802 let f : ℝ → ℝ := fun x =>803 (Set.projIcc 0 ‖T‖ hinterval x : ℝ)804 have hf : Continuous f := by805 dsimp only [f]806 fun_prop807 have hf0 : f 0 = 0 := by808 dsimp only [f]809 simp810 have hfnonneg (x : ℝ) : 0 ≤ f x := by811 exact (Set.projIcc 0 ‖T‖ hinterval x).property.1812 have hfnorm (x : ℝ) : ‖f x‖ ≤ ‖T‖ := by813 rw [Real.norm_eq_abs, abs_of_nonneg (hfnonneg x)]814 exact (Set.projIcc 0 ‖T‖ hinterval x).property.2815 have hfix : cfc f S = S := by816 calc817 cfc f S = cfc (fun x : ℝ => x) S := by818 apply cfc_congr819 intro x hx820 have hxlower : 0 ≤ x := spectrum_nonneg_of_nonneg hSnonneg hx821 have hxnorm : ‖x‖ ≤ ‖S‖ := spectrum.norm_le_norm_of_mem hx822 have hxupper : x ≤ ‖T‖ := by823 rw [Real.norm_eq_abs, abs_of_nonneg hxlower] at hxnorm824 exact hxnorm.trans hSnorm825 dsimp only [f]826 exact congrArg Subtype.val827 (Set.projIcc_of_mem hinterval ⟨hxlower, hxupper⟩)828 _ = S := cfc_id' ℝ S829 let b : A := cfc f a830 have hbnonneg : 0 ≤ b := cfc_nonneg fun x _ => hfnonneg x831 have hbnorm : ‖b‖ ≤ ‖T‖ := by832 exact norm_cfc_le (norm_nonneg T) fun x _ => hfnorm x833 have hpib : pi b = cfc f (pi a) := by834 exact StarAlgHomClass.map_cfc pi f a835 (hf := hf.continuousOn) (hφ := by fun_prop)836 (ha := ha) (hφa := ha.map pi)837 have hfcq : cfc f (pi a) * q = S := by838 calc839 cfc f (pi a) * q = cfc f S * q :=840 cfc_mul_eq_of_mul_eq (ha.map pi) hSself841 isStarProjection_starProjection haq hSq842 (hright.trans hSsupport.2.symm) f hf hf0843 _ = S := by rw [hfix, hSsupport.2]844 refine ⟨b, hbnonneg, hbnorm, fun x hx => ?_⟩845 have hxF : x ∈ F := (show E ≤ F from le_sup_left) hx846 have hqx : q x = x := F.starProjection_eq_self_iff.mpr hxF847 have happ := congrArg (fun R : H →L[ℂ] H => R x) hfcq848 rw [hpib]849 simpa [ContinuousLinearMap.comp_apply, hqx, S,850 finiteCompression_apply_of_mem E T hx] using happ851852/-- Positive-contraction form of finite-dimensional exact interpolation. -/853theorem exists_positive_contraction_eq_on854 {A H : Type*} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]855 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]856 [Nontrivial H] (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H))857 (hpi : StarAlgHom.IsIrreducible pi)858 (E : Submodule ℂ H) [FiniteDimensional ℂ E]859 (T : H →L[ℂ] H) (hT : 0 ≤ T) (hTnorm : ‖T‖ ≤ 1) :860 ∃ a : A, 0 ≤ a ∧ ‖a‖ ≤ 1 ∧861 ∀ x : H, x ∈ E → pi a x = T x := by862 obtain ⟨a, ha, hanorm, haexact⟩ :=863 exists_nonneg_norm_le_and_eq_on pi hpi E T hT864 exact ⟨a, ha, hanorm.trans hTnorm, haexact⟩865866/-- Sharp exact finite-dimensional interpolation with the algebra witness867supported in a prescribed projection corner. Only the requested finite868subspace is required to be mapped into the represented corner. -/869theorem StarAlgHom.exists_cornerSupported_selfAdjoint_norm_le_and_eq_on_of_apply870 {A H : Type*} [CStarAlgebra A]871 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]872 [Nontrivial H] (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H))873 (hpi : StarAlgHom.IsIrreducible pi)874 {e : A} (he : IsStarProjection e)875 (E : Submodule ℂ H) [FiniteDimensional ℂ E]876 (hE : ∀ x : H, x ∈ E → pi e x = x)877 (T : H →L[ℂ] H) (hT : IsSelfAdjoint T)878 (hTE : ∀ x : H, x ∈ E → pi e (T x) = T x) :879 ∃ a : A, IsSelfAdjoint a ∧ ‖a‖ ≤ ‖T‖ ∧880 e * a = a ∧ a * e = a ∧ ∀ x : H, x ∈ E → pi a x = T x := by881 obtain ⟨b, hbself, hbnorm, hbexact⟩ :=882 exists_selfAdjoint_norm_le_and_eq_on pi hpi E T hT883 let a : A := e * b * e884 have haself : IsSelfAdjoint a := by885 rw [IsSelfAdjoint]886 simp only [a, star_mul, he.isSelfAdjoint.star_eq, hbself.star_eq]887 exact (mul_assoc e b e).symm888 have hanorm : ‖a‖ ≤ ‖T‖ := by889 calc890 ‖a‖ ≤ ‖e‖ * ‖b‖ * ‖e‖ := by891 exact (norm_mul_le _ _).trans892 (mul_le_mul_of_nonneg_right (norm_mul_le _ _) (norm_nonneg _))893 _ ≤ 1 * ‖T‖ * 1 := by894 gcongr <;> exact he.norm_le895 _ = ‖T‖ := by ring896 have haleft : e * a = a := by897 dsimp [a]898 calc899 e * (e * b * e) = (e * e) * b * e := by noncomm_ring900 _ = e * b * e := by rw [he.isIdempotentElem.eq]901 have haright : a * e = a := by902 dsimp [a]903 calc904 e * b * e * e = e * b * (e * e) := by noncomm_ring905 _ = e * b * e := by rw [he.isIdempotentElem.eq]906 refine ⟨a, haself, hanorm, haleft, haright, fun x hx => ?_⟩907 have hmap : pi a = pi e * pi b * pi e := by simp [a]908 rw [hmap]909 change pi e (pi b (pi e x)) = T x910 rw [hE x hx, hbexact x hx]911 exact hTE x hx912913/-- Compatibility wrapper using the former global range hypothesis. -/914theorem StarAlgHom.exists_cornerSupported_selfAdjoint_norm_le_and_eq_on915 {A H : Type*} [CStarAlgebra A]916 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]917 [Nontrivial H] (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H))918 (hpi : StarAlgHom.IsIrreducible pi)919 {e : A} (he : IsStarProjection e)920 (E : Submodule ℂ H) [E.HasOrthogonalProjection] [FiniteDimensional ℂ E]921 (hE : ∀ x : H, x ∈ E → pi e x = x)922 (T : H →L[ℂ] H) (hT : IsSelfAdjoint T)923 (hTrange : pi e * T = T) :924 ∃ a : A, IsSelfAdjoint a ∧ ‖a‖ ≤ ‖T‖ ∧925 e * a = a ∧ a * e = a ∧ ∀ x : H, x ∈ E → pi a x = T x := by926 apply pi.exists_cornerSupported_selfAdjoint_norm_le_and_eq_on_of_apply927 hpi he E hE T hT928 intro x _hx929 exact congrArg (fun S : H →L[ℂ] H => S x) hTrange930931/-- Positive sharp interpolation supported in an arbitrary projection corner.932The support projection is the corner unit; it is not identified with the933ambient unit. -/934theorem StarAlgHom.exists_cornerSupported_nonneg_norm_le_and_eq_on_of_apply935 {A H : Type*} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]936 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]937 [Nontrivial H] (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H))938 (hpi : StarAlgHom.IsIrreducible pi)939 {e : A} (he : IsStarProjection e)940 (E : Submodule ℂ H) [FiniteDimensional ℂ E]941 (hE : ∀ x : H, x ∈ E → pi e x = x)942 (T : H →L[ℂ] H) (hT : 0 ≤ T)943 (hTE : ∀ x : H, x ∈ E → pi e (T x) = T x) :944 ∃ a : A, 0 ≤ a ∧ ‖a‖ ≤ ‖T‖ ∧945 e * a = a ∧ a * e = a ∧ ∀ x : H, x ∈ E → pi a x = T x := by946 obtain ⟨b, hbnonneg, hbnorm, hbexact⟩ :=947 exists_nonneg_norm_le_and_eq_on pi hpi E T hT948 let a : A := e * b * e949 have hanonneg : 0 ≤ a := by950 simpa only [a, he.isSelfAdjoint.star_eq] using951 (star_right_conjugate_nonneg hbnonneg e)952 have hanorm : ‖a‖ ≤ ‖T‖ := by953 calc954 ‖a‖ ≤ ‖e‖ * ‖b‖ * ‖e‖ := by955 exact (norm_mul_le _ _).trans956 (mul_le_mul_of_nonneg_right (norm_mul_le _ _) (norm_nonneg _))957 _ ≤ 1 * ‖T‖ * 1 := by958 gcongr <;> exact he.norm_le959 _ = ‖T‖ := by ring960 have haleft : e * a = a := by961 dsimp [a]962 calc963 e * (e * b * e) = (e * e) * b * e := by noncomm_ring964 _ = e * b * e := by rw [he.isIdempotentElem.eq]965 have haright : a * e = a := by966 dsimp [a]967 calc968 e * b * e * e = e * b * (e * e) := by noncomm_ring969 _ = e * b * e := by rw [he.isIdempotentElem.eq]970 refine ⟨a, hanonneg, hanorm, haleft, haright, fun x hx => ?_⟩971 have hmap : pi a = pi e * pi b * pi e := by simp [a]972 rw [hmap]973 change pi e (pi b (pi e x)) = T x974 rw [hE x hx, hbexact x hx]975 exact hTE x hx976977/-- Compatibility wrapper using the former global range hypothesis. -/978theorem StarAlgHom.exists_cornerSupported_nonneg_norm_le_and_eq_on979 {A H : Type*} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]980 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]981 [Nontrivial H] (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H))982 (hpi : StarAlgHom.IsIrreducible pi)983 {e : A} (he : IsStarProjection e)984 (E : Submodule ℂ H) [E.HasOrthogonalProjection] [FiniteDimensional ℂ E]985 (hE : ∀ x : H, x ∈ E → pi e x = x)986 (T : H →L[ℂ] H) (hT : 0 ≤ T)987 (hTrange : pi e * T = T) :988 ∃ a : A, 0 ≤ a ∧ ‖a‖ ≤ ‖T‖ ∧989 e * a = a ∧ a * e = a ∧ ∀ x : H, x ∈ E → pi a x = T x := by990 apply pi.exists_cornerSupported_nonneg_norm_le_and_eq_on_of_apply991 hpi he E hE T hT992 intro x _hx993 exact congrArg (fun S : H →L[ℂ] H => S x) hTrange994995/-- Positive-contraction interpolation supported in an arbitrary projection996corner. -/997theorem StarAlgHom.exists_cornerSupported_positive_contraction_eq_on_of_apply998 {A H : Type*} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]999 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]1000 [Nontrivial H] (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H))1001 (hpi : StarAlgHom.IsIrreducible pi)1002 {e : A} (he : IsStarProjection e)1003 (E : Submodule ℂ H) [FiniteDimensional ℂ E]1004 (hE : ∀ x : H, x ∈ E → pi e x = x)1005 (T : H →L[ℂ] H) (hT : 0 ≤ T) (hTnorm : ‖T‖ ≤ 1)1006 (hTE : ∀ x : H, x ∈ E → pi e (T x) = T x) :1007 ∃ a : A, 0 ≤ a ∧ ‖a‖ ≤ 1 ∧1008 e * a = a ∧ a * e = a ∧ ∀ x : H, x ∈ E → pi a x = T x := by1009 obtain ⟨a, ha, hanorm, haleft, haright, haexact⟩ :=1010 pi.exists_cornerSupported_nonneg_norm_le_and_eq_on_of_apply1011 hpi he E hE T hT hTE1012 exact ⟨a, ha, hanorm.trans hTnorm, haleft, haright, haexact⟩10131014/-- Compatibility wrapper using the former global range hypothesis. -/1015theorem StarAlgHom.exists_cornerSupported_positive_contraction_eq_on1016 {A H : Type*} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]1017 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]1018 [Nontrivial H] (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H))1019 (hpi : StarAlgHom.IsIrreducible pi)1020 {e : A} (he : IsStarProjection e)1021 (E : Submodule ℂ H) [E.HasOrthogonalProjection] [FiniteDimensional ℂ E]1022 (hE : ∀ x : H, x ∈ E → pi e x = x)1023 (T : H →L[ℂ] H) (hT : 0 ≤ T) (hTnorm : ‖T‖ ≤ 1)1024 (hTrange : pi e * T = T) :1025 ∃ a : A, 0 ≤ a ∧ ‖a‖ ≤ 1 ∧1026 e * a = a ∧ a * e = a ∧ ∀ x : H, x ∈ E → pi a x = T x := by1027 apply pi.exists_cornerSupported_positive_contraction_eq_on_of_apply1028 hpi he E hE T hT hTnorm1029 intro x _hx1030 exact congrArg (fun S : H →L[ℂ] H => S x) hTrange10311032/-- Compatibility form of corner-supported exact interpolation with the old1033factor-two estimate. New callers should use the sharp theorem above. -/1034theorem StarAlgHom.exists_cornerSupported_selfAdjoint_norm_le_two_mul_and_eq_on1035 {A H : Type*} [CStarAlgebra A]1036 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]1037 [Nontrivial H] (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H))1038 (hpi : StarAlgHom.IsIrreducible pi)1039 {e : A} (he : IsStarProjection e)1040 (E : Submodule ℂ H) [E.HasOrthogonalProjection] [FiniteDimensional ℂ E]1041 (hE : ∀ x : H, x ∈ E → pi e x = x)1042 (T : H →L[ℂ] H) (hT : IsSelfAdjoint T)1043 (hTrange : pi e * T = T) :1044 ∃ a : A, IsSelfAdjoint a ∧ ‖a‖ ≤ 2 * ‖T‖ ∧1045 e * a = a ∧ a * e = a ∧ ∀ x : H, x ∈ E → pi a x = T x := by1046 obtain ⟨a, ha, hanorm, haleft, haright, haexact⟩ :=1047 pi.exists_cornerSupported_selfAdjoint_norm_le_and_eq_on1048 hpi he E hE T hT hTrange1049 have hanorm' : ‖a‖ ≤ 2 * ‖T‖ :=1050 hanorm.trans (by nlinarith [norm_nonneg T])1051 exact ⟨a, ha, hanorm', haleft, haright, haexact⟩10521053end MathlibAnnex.Analysis.CStarAlgebra