min_zero — Mathlib

English

If f has finite integral, then so does the function x ↦ c · f(x) for any constant c.

Русский

Если у функции f конечный интеграл, то и функция x ↦ c · f(x) имеет конечный интеграл для любого константного c.

LaTeX

$$$HasFiniteIntegral f μ \Rightarrow \forall c, HasFiniteIntegral (x \mapsto c \cdot f(x)) μ$$$

Lean4

@[fun_prop]
theorem min_zero {f : α → ℝ} (hf : HasFiniteIntegral f μ) : HasFiniteIntegral (fun a => min (f a) 0) μ :=
  hf.mono <| Eventually.of_forall fun x => by simpa [abs_le] using neg_abs_le _

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