setLAverage_congr_fun_ae — Mathlib

English

If s is measurable and f and g are equal on s, then laverage over s of f equals laverage over s of g.

Русский

Если s измеримо, и f и g совпадают на s, то среднее по s одинаковое для f и g.

LaTeX

$$$s\\text{MeasurableSet} \\Rightarrow (f=g\\text{ on } s) \\Rightarrow \\laverage_{\\mu}(f) = \\laverage_{\\mu}(g)\\text{ on } s$$$

Lean4

theorem setLAverage_congr_fun_ae (hs : MeasurableSet s) (h : ∀ᵐ x ∂μ, x ∈ s → f x = g x) :
    ⨍⁻ x in s, f x ∂μ = ⨍⁻ x in s, g x ∂μ := by simp only [laverage_eq, setLIntegral_congr_fun_ae hs h]

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