integral_eq_sum_filter — Mathlib

English

The family weightedSMul defines a dominated FinMeasAdditive structure with respect to the measure μ.

Русский

WeightedSMul образует доминированную FinMeasAdditive структуру относительно меры μ.

LaTeX

$$$$DominatedFinMeasAdditive\, μ\, (weightedSMul μ) 1.$$$$

Lean4

theorem integral_eq_sum_filter [DecidablePred fun x : F => x ≠ 0] {m : MeasurableSpace α} (f : α →ₛ F) (μ : Measure α) :
    f.integral μ = ∑ x ∈ {x ∈ f.range | x ≠ 0}, μ.real (f ⁻¹' { x }) • x := by
  simp_rw [integral_def, setToSimpleFunc_eq_sum_filter, weightedSMul_apply]

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