integral_eq — Mathlib

English

The operator norm of weightedSMul is bounded by μ.real s, i.e., ∥weightedSMul μ s∥ ≤ μ.real s.

Русский

Нормa оператора weightedSMul по множеству s ограничена μ.real s.

LaTeX

$$$$\|weightedSMul\, μ\, s\| ≤ μ.real\, s.$$$$

Lean4

theorem integral_eq {m : MeasurableSpace α} (μ : Measure α) (f : α →ₛ F) :
    f.integral μ = ∑ x ∈ f.range, μ.real (f ⁻¹' { x }) • x := by simp [integral, setToSimpleFunc, weightedSMul_apply]

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