English
Let f be a simple function and μ a measure. The lintegral is bilinear in its two arguments: it is linear in the function and linear in the measure. Equivalently, for all simple f, μ, ν and all scalars c ≥ 0, we have f.lintegral(μ + ν) = f.lintegral(μ) + f.lintegral(ν), (f + g).lintegral(μ) = f.lintegral(μ) + g.lintegral(μ), f.lintegral(c • μ) = c • f.lintegral(μ), and (c • f).lintegral(μ) = c • f.lintegral(μ).
Русский
Пусть f — простая функция, μ — мера. Линеаризованный интеграл линегра́ла по мере и по функции является билинейной по своим аргументаам: линейность по f и линейность по μ. То есть для всех f,g, μ, ν и скаляра c ≥ 0 выполняется f.lintegral(μ + ν) = f.lintegral(μ) + f.lintegral(ν), (f + g).lintegral(μ) = f.lintegral(μ) + g.lintegral(μ), f.lintegral(c • μ) = c • f.lintegral(μ), и (c • f).lintegral(μ) = c • f.lintegral(μ).
LaTeX
$$$\\forall f,g: α \\toₛ ℝ_{≥0}^{∞}, \\forall μ,ν, c \\ge 0,\\; f.lintegral(μ+ν) = f.lintegral(μ) + f.lintegral(ν) \\wedge (f+g).lintegral(μ) = f.lintegral(μ) + g.lintegral(μ) \\wedge f.lintegral(c \\cdot μ) = c \\cdot f.lintegral(μ) \\wedge (c \\cdot f).lintegral(μ) = c \\cdot f.lintegral(μ).$$$
Lean4
/-- Integral of a simple function `α →ₛ ℝ≥0∞` as a bilinear map. -/
def lintegralₗ {m : MeasurableSpace α} : (α →ₛ ℝ≥0∞) →ₗ[ℝ≥0∞] Measure α →ₗ[ℝ≥0∞] ℝ≥0∞
where
toFun
f :=
{ toFun := lintegral f
map_add' := by simp [lintegral, mul_add, Finset.sum_add_distrib]
map_smul' := fun c μ => by simp [lintegral, mul_left_comm _ c, Finset.mul_sum, Measure.smul_apply c] }
map_add' f g := LinearMap.ext fun _ => add_lintegral f g
map_smul' c f := LinearMap.ext fun _ => const_mul_lintegral f c
