lintegral_eq_of_subset' — Mathlib

English

If f is a simple function α → ENNReal with range excluding 0 and the nonzero range is contained in s, then f.lintegral μ equals the sum over s of x times μ(preimage {x}).

Русский

Если диапазон f исключает ноль и ненулевой диапазон содержится в s, тогда линегральный интеграл f равен сумме по s: ∑ x∈s x μ(f⁻¹({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 : f.range \ {0} ⊆ s) :
    f.lintegral μ = ∑ x ∈ s, x * μ (f ⁻¹' { x }) :=
  f.lintegral_eq_of_subset fun x hfx _ => hs <| Finset.mem_sdiff.2 ⟨f.mem_range_self x, mt Finset.mem_singleton.1 hfx⟩

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