English
The laverage with respect to μ+ν equals a weighted combination of laverages with respect to μ and ν.
Русский
Среднее по сумме мер μ+ν равно взвешенной сумме средних по μ и ν.
LaTeX
$$$\\laverage_{μ+ν}(f) = \\dfrac{μ univ}{μ univ + ν univ} \\cdot \\laverage_{μ} f + \\dfrac{ν univ}{μ univ + ν univ} \\cdot \\laverage_{ν} f$$$
Lean4
theorem laverage_add_measure :
⨍⁻ x, f x ∂(μ + ν) = μ univ / (μ univ + ν univ) * ⨍⁻ x, f x ∂μ + ν univ / (μ univ + ν univ) * ⨍⁻ x, f x ∂ν :=
by
by_cases hμ : IsFiniteMeasure μ; swap
· rw [not_isFiniteMeasure_iff] at hμ
simp [laverage_eq, hμ]
by_cases hν : IsFiniteMeasure ν; swap
· rw [not_isFiniteMeasure_iff] at hν
simp [laverage_eq, hν]
simp only [← ENNReal.mul_div_right_comm, measure_mul_laverage, ← ENNReal.add_div, ← lintegral_add_measure,
← Measure.add_apply, ← laverage_eq]
