English
If s and t are essentially disjoint and sufficiently nontrivial, the average over their union equals a convex combination of the averages over each set, with weights proportional to μ-real masses of s and t.
Русский
Если s и t практически более не пересекаются и неслабо непусты, среднее по объединению s ∪ t равно выпуклой комбинации средних по s и по t с весами, пропорциональными массами μ-real на s и t.
LaTeX
$$$\operatorname{average}_{\mu|_{s\cup t}} f = \left( \frac{\mu.real(s)}{\mu.real(s)+\mu.real(t)} \right) \operatorname{average}_{\mu|_s} f + \left( \frac{\mu.real(t)}{\mu.real(s)+\mu.real(t)} \right) \operatorname{average}_{\mu|_t} f$$$
Lean4
theorem average_union {f : α → E} {s t : Set α} (hd : AEDisjoint μ s t) (ht : NullMeasurableSet t μ) (hsμ : μ s ≠ ∞)
(htμ : μ t ≠ ∞) (hfs : IntegrableOn f s μ) (hft : IntegrableOn f t μ) :
⨍ x in s ∪ t, f x ∂μ =
(μ.real s / (μ.real s + μ.real t)) • ⨍ x in s, f x ∂μ + (μ.real t / (μ.real s + μ.real t)) • ⨍ x in t, f x ∂μ :=
by
haveI := Fact.mk hsμ.lt_top; haveI := Fact.mk htμ.lt_top
rw [restrict_union₀ hd ht, average_add_measure hfs hft, measureReal_restrict_apply_univ,
measureReal_restrict_apply_univ]
