English
For any scalar c (in the appropriate scalar space) and any bounded nonnegative test function f, μ.testAgainstNN (c • f) = c • μ.testAgainstNN f.
Русский
Для любого скаляра c и любой ограниченной неотрицательной тест-функции f выполняется однородность: μ.testAgainstNN (c • f) = c • μ.testAgainstNN f.
LaTeX
$$$ \forall c, \forall \mu : \text{FiniteMeasure } \Omega, \forall f : \Omega \to^{} \mathbb{R}_{\ge 0}, \; \mu.testAgainstNN (c \cdot f) = c \cdot \mu.testAgainstNN f.$$$
Lean4
theorem testAgainstNN_smul [IsScalarTower R ℝ≥0 ℝ≥0] [PseudoMetricSpace R] [Zero R] [IsBoundedSMul R ℝ≥0]
(μ : FiniteMeasure Ω) (c : R) (f : Ω →ᵇ ℝ≥0) : μ.testAgainstNN (c • f) = c • μ.testAgainstNN f :=
by
simp only [← ENNReal.coe_inj, BoundedContinuousFunction.coe_smul, testAgainstNN_coe_eq, ENNReal.coe_smul]
simp_rw [← smul_one_smul ℝ≥0∞ c (f _ : ℝ≥0∞), ← smul_one_smul ℝ≥0∞ c (lintegral _ _ : ℝ≥0∞), smul_eq_mul]
exact lintegral_const_mul (c • (1 : ℝ≥0∞)) f.measurable_coe_ennreal_comp
