nnnorm_cfc_nnreal_le — Mathlib

English

For NNReal-valued f and a, if ∀ x ∈ spectrum a, f x ≤ c, then the NN-norm of cfc f a is ≤ c.

Русский

Для NNReal-функций и элемента a, если ∀ x в спектре a, f x ≤ c, то cfc f a имеет NN-норму ≤ c.

LaTeX

$$$\forall x \in \sigma a,\; f x \le c \Rightarrow \|cfc f a\|_+ \le 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
  obtain (_ | _) := subsingleton_or_nontrivial A
  · rw [Subsingleton.elim (cfc f a) 0]
    simp
  · refine cfc_cases (‖·‖₊ ≤ c) a f (by simp) fun hf ha ↦ ?_
    simp only [← cfc_apply f a, isLUB_le_iff (IsGreatest.nnnorm_cfc_nnreal f a hf ha |>.isLUB)]
    rintro - ⟨x, hx, rfl⟩
    exact h x hx

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