average_pair — Mathlib

English

If f and g are integrable, then the average of the pair (f,g) is the pair of the averages: average_μ (x ↦ (f(x), g(x))) = (average_μ f, average_μ g).

Русский

Если f и g интегрируемы, то среднее пары (f,g) равно паре средних: average_μ (f,g) = (average_μ f, average_μ g).

LaTeX

$$$\operatorname{average}_\mu \big( (f,g) \big) = \big( \operatorname{average}_\mu f, \operatorname{average}_\mu g \big)$$$

Lean4

theorem average_pair [CompleteSpace E] {f : α → E} {g : α → F} (hfi : Integrable f μ) (hgi : Integrable g μ) :
    ⨍ x, (f x, g x) ∂μ = (⨍ x, f x ∂μ, ⨍ x, g x ∂μ) :=
  integral_pair hfi.to_average hgi.to_average

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