English
Let f be a compactly supported real-valued function on α and let a be a real number with a ≥ 0. Then applying nnrealPart after scaling by a equals scaling the nnrealPart of f by a converted to NNReal: (a · f)nnrealPart = a.toNNReal · fnnrealPart.
Русский
Пусть f — компактно поддерживаемая функция с вещественными значениями на множестве α, и пусть a ∈ ℝ с a ≥ 0. Тогда nnrealPart после масштабирования на a равен масштабированию nnrealPart самой функции f, причём коэффициент приведён к NNReal: (a · f).nnrealPart = a.toNNReal · f.nnrealPart.
LaTeX
$$$ (a \\cdot f)^{\\mathrm{nnrealPart}} = a^{\\mathbb{NN}} \\cdot f^{\\mathrm{nnrealPart}} \quad \\text{for } a \\ge 0,$$$
Lean4
theorem nnrealPart_smul_pos (f : C_c(α, ℝ)) {a : ℝ} (ha : 0 ≤ a) : (a • f).nnrealPart = a.toNNReal • f.nnrealPart :=
by
ext x
simp only [nnrealPart_apply, coe_smul, Pi.smul_apply, Real.coe_toNNReal', smul_eq_mul, NNReal.coe_mul, ha,
sup_of_le_left]
rcases le_total 0 (f x) with hfx | hfx
· simp [ha, hfx, mul_nonneg]
· simp [mul_nonpos_iff, ha, hfx]
