integral_average_sub — Mathlib

English

Under appropriate null-disjointness and integrability assumptions, the average over s ∪ t equals the weighted average of averages over s and t.

Русский

При заданных условиях непересечения и интегрируемости среднее по s ∪ t равно взвешенному среднему по s и t.

LaTeX

$$$\operatorname{average}_{\mu|_{s\cup t}} f = \frac{\mu.real(s)}{\mu.real(s) + \mu.real(t)} \operatorname{average}_{\mu|_s} f + \frac{\mu.real(t)}{\mu.real(s) + \mu.real(t)} \operatorname{average}_{\mu|_t} f$$$

Lean4

theorem integral_average_sub [IsFiniteMeasure μ] (hf : Integrable f μ) : ∫ x, ⨍ a, f a ∂μ - f x ∂μ = 0 := by
  rw [integral_sub (integrable_const _) hf, integral_average, sub_self]

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