map_lintegral — Mathlib

English

For a simple function f: α → ENNReal, under a subset condition on range, the lintegral equals a finite sum over the range.

Русский

Для простой функции f: α → ENNReal при условии подмножества диапазона линегральный интеграл равен конечной сумме по диапазону.

LaTeX

$$$ f.lintegral\ μ = \sum_{x \in s} x \cdot μ(f^{-1}({x})) $$$

Lean4

/-- Calculate the integral of `(g ∘ f)`, where `g : β → ℝ≥0∞` and `f : α →ₛ β`. -/
theorem map_lintegral (g : β → ℝ≥0∞) (f : α →ₛ β) : (f.map g).lintegral μ = ∑ x ∈ f.range, g x * μ (f ⁻¹' { x }) :=
  by
  simp only [lintegral, range_map]
  refine Finset.sum_image' _ fun b hb => ?_
  rcases mem_range.1 hb with ⟨a, rfl⟩
  rw [map_preimage_singleton, ← f.sum_measure_preimage_singleton, Finset.mul_sum]
  refine Finset.sum_congr ?_ ?_
  · congr
  · grind

Похожие утверждения