norm_cfcₙ_lt — Mathlib

English

In the nonunital setting, if hc: 0 < c and h: ∀ x ∈ σₙ 𝕜 a, ‖f x‖ < c, then ‖cfcₙ f a‖ < c.

Русский

В неединичном случае, если 0 < c и для всех x в спектре 𝕜 a выполняется ‖f x‖ < c, тогда ‖cfcₙ f a‖ < c.

LaTeX

$$$0 < c \land \Big( \forall x \in \sigma_n 𝕜 a, \|f x\| < c \Big) \Rightarrow \|cfc_n f a\| < c$$$

Lean4

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

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