English
For μ a finite measure and f1, f2 bounded nonnegative functions, testAgainstNN respects addition: μ.testAgainstNN (f1 + f2) = μ.testAgainstNN f1 + μ.testAgainstNN f2.
Русский
Для μ — конечная мера и двух ограниченных неотрицательных функций f1, f2 выполняется аддитивность testAgainstNN: μ.testAgainstNN(f1 + f2) = μ.testAgainstNN f1 + μ.testAgainstNN f2.
LaTeX
$$$ \forall \mu : \text{FiniteMeasure } \Omega, \; \forall f_1, f_2 : \Omega \to^{} \mathbb{R}_{\ge 0}, \; \mu.testAgainstNN (f_1 + f_2) = \mu.testAgainstNN f_1 + \mu.testAgainstNN f_2.$$$
Lean4
theorem testAgainstNN_add (μ : FiniteMeasure Ω) (f₁ f₂ : Ω →ᵇ ℝ≥0) :
μ.testAgainstNN (f₁ + f₂) = μ.testAgainstNN f₁ + μ.testAgainstNN f₂ :=
by
simp only [← ENNReal.coe_inj, BoundedContinuousFunction.coe_add, ENNReal.coe_add, Pi.add_apply, testAgainstNN_coe_eq]
exact lintegral_add_left (BoundedContinuousFunction.measurable_coe_ennreal_comp _) _
