setAverage_congr_fun — Mathlib

English

If s and t are a.e.-equivalent, then averages of f over μ restricted to s and t are equal.

Русский

Если снижения по множествам s и t совпадают почти повсюду, их средние значения совпадают.

LaTeX

$$$\langle f \rangle_{μ|_s} = \langle f \rangle_{μ|_t} \quad (s =_{a.e.,μ} t)$$$

Lean4

theorem setAverage_congr_fun (hs : MeasurableSet s) (h : ∀ᵐ x ∂μ, x ∈ s → f x = g x) :
    ⨍ x in s, f x ∂μ = ⨍ x in s, g x ∂μ := by simp only [average_eq, setIntegral_congr_ae hs h]

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