English
For any scalar c, integral of f scaled by c equals scaling of the integral of f, provided integrable.
Русский
Интеграл от масштабированной функции равен масштабированию интеграла исходной функции.
LaTeX
$$$\text{integral } I l (f) vol \Rightarrow \text{integral } I l (c \cdot f) vol = c \cdot \text{integral } I l f vol$$$
Lean4
/-- The integral of a nonnegative function w.r.t. a volume generated by a locally-finite measure is
nonnegative. -/
theorem integral_nonneg {g : ℝⁿ → ℝ} (hg : ∀ x ∈ Box.Icc I, 0 ≤ g x) (μ : Measure ℝⁿ) [IsLocallyFiniteMeasure μ] :
0 ≤ integral I l g μ.toBoxAdditive.toSMul :=
by
by_cases hgi : Integrable I l g μ.toBoxAdditive.toSMul
· refine ge_of_tendsto' hgi.hasIntegral fun π => sum_nonneg fun J _ => ?_
exact mul_nonneg ENNReal.toReal_nonneg (hg _ <| π.tag_mem_Icc _)
· rw [integral, dif_neg hgi]
