English
For any nonnegative scalar c, any finite measure μ, and any bounded nonnegative test function f, the testAgainstNN operation scales the measure by c: (c · μ).testAgainstNN f = c · μ.testAgainstNN f.
Русский
Для любого неотрицательного скаляра c, любой конечной меры μ и любой ограниченной неотрицательной тест-функции f выполняется масштабирование операции testAgainstNN по мере: (c · μ).testAgainstNN f = c · μ.testAgainstNN f.
LaTeX
$$$ \forall c \in \mathbb{R}_{\ge 0}, \; \forall \mu : \text{FiniteMeasure } \Omega, \; \forall f : \Omega \to^{} \mathbb{R}_{\ge 0}, (c \cdot \mu).testAgainstNN f = c \cdot \mu.testAgainstNN f.$$$
Lean4
@[simp]
theorem smul_testAgainstNN_apply (c : ℝ≥0) (μ : FiniteMeasure Ω) (f : Ω →ᵇ ℝ≥0) :
(c • μ).testAgainstNN f = c • μ.testAgainstNN f := by
simp only [testAgainstNN, toMeasure_smul, smul_eq_mul, ← ENNReal.smul_toNNReal, ENNReal.smul_def,
lintegral_smul_measure]
