English
For a general scalar c in the ambient field, setToSimpleFunc respects the scalar action: setToSimpleFunc T (c • f) = c • setToSimpleFunc T f, under a compatibility assumption h_smul.
Русский
Для произвольного скаляра c действует совместно: setToSimpleFunc T (c • f) = c • setToSimpleFunc T f, при условии совместимости h_smul.
LaTeX
$$$ setToSimpleFunc T (c \cdot f) = c \cdot setToSimpleFunc T f $$$
Lean4
theorem setToSimpleFunc_smul {E} [NormedAddCommGroup E] [SMulZeroClass 𝕜 E] [NormedSpace ℝ E] [DistribSMul 𝕜 F]
(T : Set α → E →L[ℝ] F) (h_add : FinMeasAdditive μ T) (h_smul : ∀ c : 𝕜, ∀ s x, T s (c • x) = c • T s x) (c : 𝕜)
{f : α →ₛ E} (hf : Integrable f μ) : setToSimpleFunc T (c • f) = c • setToSimpleFunc T f :=
calc
setToSimpleFunc T (c • f) = ∑ x ∈ f.range, T (f ⁻¹' { x }) (c • x) := by
rw [smul_eq_map c f, map_setToSimpleFunc T h_add hf]; dsimp only; rw [smul_zero]
_ = ∑ x ∈ f.range, c • T (f ⁻¹' { x }) x := (Finset.sum_congr rfl fun b _ => by rw [h_smul])
_ = c • setToSimpleFunc T f := by simp only [setToSimpleFunc, smul_sum]
