cfcₙ_nonpos — Mathlib

English

If there is a predicate ensuring nonnegativity on the spectrum, then cfc_n f a is nonnegative.

Русский

Если существует предикат, гарантирующий неотрицательность на спектре, то cfc_n f a неотрицателен.

LaTeX

$$$$ (\\forall x, x\\in σ_n R a \\Rightarrow f(x) \\ge 0) \\Rightarrow 0 \\le cfc\\!_n f a $$$$

Lean4

theorem cfcₙ_nonpos (f : R → R) (a : A) (h : ∀ x ∈ σₙ R a, f x ≤ 0) : cfcₙ f a ≤ 0 :=
  by
  by_cases hf : ContinuousOn f (σₙ R a) ∧ f 0 = 0
  · obtain ⟨h₁, h₂⟩ := hf
    simpa using cfcₙ_mono h
  · simp only [not_and_or] at hf
    obtain (hf | hf) := hf
    · simp only [cfcₙ_apply_of_not_continuousOn _ hf, le_rfl]
    · simp only [cfcₙ_apply_of_not_map_zero _ hf, le_rfl]

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