average_congr — Mathlib

English

If f and g are almost everywhere equal with respect to μ, their averages are equal: average_μ(f) = average_μ(g).

Русский

Если функции f и g совпадают почти всюду по μ, их средние значения совпадают.

LaTeX

$$$\text{If } f =_{\mu} g \text{ then } \operatorname{average}_\mu f = \operatorname{average}_\mu g.$$$

Lean4

theorem average_congr {f g : α → E} (h : f =ᵐ[μ] g) : ⨍ x, f x ∂μ = ⨍ x, g x ∂μ := by
  simp only [average_eq, integral_congr_ae h]

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