laverage_congr — Mathlib

English

If f and g agree almost everywhere on a set s, then their laverages over s are equal.

Русский

Если f и g совпадают почти повсюду на s, то их средние значения по s равны.

LaTeX

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

Lean4

theorem laverage_congr {f g : α → ℝ≥0∞} (h : f =ᵐ[μ] g) : ⨍⁻ x, f x ∂μ = ⨍⁻ x, g x ∂μ := by
  simp only [laverage_eq, lintegral_congr_ae h]

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