nnnorm_cfcₙ_nnreal_le — Mathlib

English

For NNReal f, a, c, if ∀ x ∈ spectrum a, f x < c, then the NN-norm of cfcₙ f a is strictly less than c.

Русский

Для NNReal f, a, c: если ∀ x в спектре a, f x < c, то nnnorm cfcₙ f a < c.

LaTeX

$$$\forall x \in σ a, \; f x < c \Rightarrow \text{nnnorm}(cfc f a) < c$$$

Lean4

theorem nnnorm_cfcₙ_nnreal_le {f : ℝ≥0 → ℝ≥0} {a : A} {c : ℝ≥0} (h : ∀ x ∈ σₙ ℝ≥0 a, f x ≤ c) : ‖cfcₙ f a‖₊ ≤ c :=
  by
  refine cfcₙ_cases (‖·‖₊ ≤ c) a f (by simp) fun hf hf0 ha ↦ ?_
  simp only [← cfcₙ_apply f a, isLUB_le_iff (IsGreatest.nnnorm_cfcₙ_nnreal f a hf hf0 ha |>.isLUB)]
  rintro - ⟨x, hx, rfl⟩
  exact h x hx

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