integralSum_neg — Mathlib

English

For any integrand f, vol, and partition π, the integral sum is linear with respect to negation: integralSum(-f) = - integralSum(f).

Русский

Для интегрируемого f, объема vol и разбиения π сумма интеграла от −f равна отрицанию суммы интеграла от f: ∫(−f) = −∫f.

LaTeX

$$$\mathrm{integralSum}(-f)\;\mathrm{vol}\;\pi = -\mathrm{integralSum}(f)\;\mathrm{vol}\;\pi$$$

Lean4

@[simp]
theorem integralSum_neg (f : ℝⁿ → E) (vol : ι →ᵇᵃ E →L[ℝ] F) (π : TaggedPrepartition I) :
    integralSum (-f) vol π = -integralSum f vol π := by
  simp only [integralSum, Pi.neg_apply, (vol _).map_neg, Finset.sum_neg_distrib]

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