English
Under a spectrum-restriction framework, there exists an isometric continuous functional calculus on A when given a spectrum-restriction data f: C(S, R) and a suitable isometry halg between R and S, ensuring p 0 and the spectrum relation p a ↔ q a ∧ SpectrumRestricts a f.
Русский
В рамках ограничения спектра существует изометрический непрерывный функциональный калькулятор на A при данных отношениях спектра f и изометрии между R и S, обеспечивающих совместимость условий.
LaTeX
$$SpectrumRestricts.isometric_cfc (f : C(S, R)) (halg : Isometry (algebraMap R S)) (h0 : p 0) (h : ∀ a, p a ↔ q a ∧ SpectrumRestricts a f) : IsometricContinuousFunctionalCalculus R A p$$
Lean4
protected theorem isometric_cfc (f : C(S, R)) (halg : Isometry (algebraMap R S)) (h0 : p 0)
(h : ∀ a, p a ↔ q a ∧ QuasispectrumRestricts a f) : NonUnitalIsometricContinuousFunctionalCalculus R A p
where
toNonUnitalContinuousFunctionalCalculus := QuasispectrumRestricts.cfc f halg.isUniformEmbedding h0 h
isometric a
ha := by
obtain ⟨ha', haf⟩ := h a |>.mp ha
have := QuasispectrumRestricts.cfc f halg.isUniformEmbedding h0 h
rw [cfcₙHom_eq_restrict f halg.isUniformEmbedding ha ha' haf]
refine .of_dist_eq fun g₁ g₂ ↦ ?_
simp only [nonUnitalStarAlgHom_apply, isometry_cfcₙHom a ha' |>.dist_eq]
refine le_antisymm ?_ ?_
all_goals refine ContinuousMap.dist_le dist_nonneg |>.mpr fun x ↦ ?_
· simpa [halg.dist_eq] using ContinuousMap.dist_apply_le_dist _
· let x' : σₙ S a := Subtype.map (algebraMap R S) (fun _ ↦ quasispectrum.algebraMap_mem S) x
apply le_of_eq_of_le ?_ <| ContinuousMap.dist_apply_le_dist x'
simp only [ContinuousMap.coe_coe, ContinuousMapZero.comp_apply, ContinuousMapZero.coe_mk, ContinuousMap.coe_mk,
StarAlgHom.ofId_apply, halg.dist_eq, x']
congr! 2
all_goals ext; exact haf.left_inv _ |>.symm
