English
If f is a simple function α → ENNReal and s is a Finset of ENNReal obeying a subset condition, then f.lintegral μ equals the finite sum over s of x times μ(preimage {x}).
Русский
Пусть f — простая функция α → ENNReal, а s — конечный набор ENNReal, удовлетворяющий условиям подмножества; тогда линегральный интеграл равен конечной сумме по s: ∑_{x∈s} x μ(f^{-1}({x})).
LaTeX
$$$ f.lintegral\ μ = \sum_{x \in s} x \cdot μ\left(f^{-1} \{x\}\right) $$$
Lean4
theorem lintegral_eq_of_subset (f : α →ₛ ℝ≥0∞) {s : Finset ℝ≥0∞} (hs : ∀ x, f x ≠ 0 → μ (f ⁻¹' {f x}) ≠ 0 → f x ∈ s) :
f.lintegral μ = ∑ x ∈ s, x * μ (f ⁻¹' { x }) :=
by
refine Finset.sum_bij_ne_zero (fun r _ _ => r) ?_ ?_ ?_ ?_
· simpa only [forall_mem_range, mul_ne_zero_iff, and_imp]
· intros
assumption
· intro b _ hb
refine ⟨b, ?_, hb, rfl⟩
rw [mem_range, ← preimage_singleton_nonempty]
exact nonempty_of_measure_ne_zero (mul_ne_zero_iff.1 hb).2
· intros
rfl
