nnnorm_cfcₙ_le — Mathlib

English

In the NNReal setting, if f: ℝ≥0 → ℝ≥0 satisfies f x ≤ c on the spectrum of a, then the NN-norm of cfcₙ f a is at most c.

Русский

В NNReal: если f≤c на спектре a, то ‖cfcₙ f a‖₊ ≤ c.

LaTeX

$$$\forall x \in \sigma_n ℝ≥0 a,\; ‖f x‖ ≤ c \Rightarrow ‖cfc_n f a‖ ≤ c$$$

Lean4

theorem nnnorm_cfcₙ_le {f : 𝕜 → 𝕜} {a : A} {c : ℝ≥0} (h : ∀ x ∈ σₙ 𝕜 a, ‖f x‖₊ ≤ c) : ‖cfcₙ f a‖₊ ≤ c :=
  norm_cfcₙ_le h

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