integral_eq_sum_of_subset — Mathlib

English

For simple real-valued functions, the norm of the positive part equals the positive part function.

Русский

Норма положительной части простой функции равна самой положительной части.

LaTeX

$$$$\mathrm{posPart}(f)\map\|\cdot\| = \mathrm{posPart}(f).$$$$

Lean4

/-- The Bochner integral is equal to a sum over any set that includes `f.range` (except `0`). -/
theorem integral_eq_sum_of_subset [DecidablePred fun x : F => x ≠ 0] {f : α →ₛ F} {s : Finset F}
    (hs : {x ∈ f.range | x ≠ 0} ⊆ s) : f.integral μ = ∑ x ∈ s, μ.real (f ⁻¹' { x }) • x :=
  by
  rw [SimpleFunc.integral_eq_sum_filter, Finset.sum_subset hs]
  rintro x - hx; rw [Finset.mem_filter, not_and_or, Ne, Classical.not_not] at hx
  rcases hx.symm with (rfl | hx)
  · simp
  rw [SimpleFunc.mem_range] at hx
  rw [preimage_eq_empty] <;> simp [Set.disjoint_singleton_left, hx]

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