setLAverage_congr_fun — Mathlib

English

If hs is measurable and f,g agree on s, then the laverage over μ.restrict s of f equals that of g.

Русский

Если hs измеримо и f и g совпадают на s, то laverage на μ.restrict s совпадает.

LaTeX

$$$\\text{MeasurableSet } hs \\Rightarrow (EqOn\\ f\\ g\\ s) \\Rightarrow laverage_{μ.restrict s}(f) = laverage_{μ.restrict s}(g)$$$

Lean4

theorem setLAverage_congr_fun (hs : MeasurableSet s) (h : EqOn f g s) : ⨍⁻ x in s, f x ∂μ = ⨍⁻ x in s, g x ∂μ := by
  simp only [laverage_eq, setLIntegral_congr_fun hs h]

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