English
If μ and ν are finite measures, the average with respect to μ+ν is a convex combination of the averages with respect to μ and ν, with weights proportional to μ(α) and ν(α).
Русский
Если μ и ν — конечные меры, среднее по сумме μ+ν является выпуклой комбинацией средних по μ и ν, взвешенной массами μ(α) и ν(α).
LaTeX
$$$\operatorname{average}_{\mu+\nu} f = \left( \frac{\mu(\mathrm{univ})}{\mu(\mathrm{univ})+\nu(\mathrm{univ})} \right) \operatorname{average}_\mu f + \left( \frac{\nu(\mathrm{univ})}{\mu(\mathrm{univ})+\nu(\mathrm{univ})} \right) \operatorname{average}_\nu f$$$
Lean4
theorem average_add_measure [IsFiniteMeasure μ] {ν : Measure α} [IsFiniteMeasure ν] {f : α → E} (hμ : Integrable f μ)
(hν : Integrable f ν) :
⨍ x, f x ∂(μ + ν) =
(μ.real univ / (μ.real univ + ν.real univ)) • ⨍ x, f x ∂μ +
(ν.real univ / (μ.real univ + ν.real univ)) • ⨍ x, f x ∂ν :=
by
simp only [div_eq_inv_mul, mul_smul, measure_smul_average, ← smul_add, ← integral_add_measure hμ hν]
rw [average_eq, measureReal_add_apply]
