norm_cfcₙ_le — Mathlib

English

For nonunital algebras with a nonunital isometric continuous functional calculus, if f is bounded by c on the spectrum, then ‖cfcₙ f a‖ ≤ c.

Русский

Для неединичных алгебр с неединичным изометрическим непрерывным функциональным калькулятором: если ‖f x‖ ≤ c на спектре, то ‖cfcₙ f a‖ ≤ c.

LaTeX

$$$\forall x \in \sigma_n R a, \|f x\| ≤ c \Rightarrow \|cfc_n f a\| ≤ c$$$

Lean4

theorem norm_cfcₙ_le {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 <| h 0 (quasispectrum.zero_mem 𝕜 a)
  · simp only [← cfcₙ_apply f a, isLUB_le_iff (IsGreatest.norm_cfcₙ f a hf hf0 ha |>.isLUB)]
    rintro - ⟨x, hx, rfl⟩
    exact h x hx

Похожие утверждения