English
Under appropriate disjointness and finiteness assumptions, the average over s ∪ t lies in the open segment between the averages over s and t.
Русский
При корректных предположениях о непересечности и конечности, среднее по s ∪ t находится внутри открытого отрезка между средними по s и по t.
LaTeX
$$$\langle f \rangle_{μ|_{s\cup t}} \in \operatorname{openSegment}( \langle f \rangle_{μ|_s}, \langle f \rangle_{μ|_t} )$$$
Lean4
theorem average_union_mem_openSegment {f : α → E} {s t : Set α} (hd : AEDisjoint μ s t) (ht : NullMeasurableSet t μ)
(hs₀ : μ s ≠ 0) (ht₀ : μ t ≠ 0) (hsμ : μ s ≠ ∞) (htμ : μ t ≠ ∞) (hfs : IntegrableOn f s μ)
(hft : IntegrableOn f t μ) : ⨍ x in s ∪ t, f x ∂μ ∈ openSegment ℝ (⨍ x in s, f x ∂μ) (⨍ x in t, f x ∂μ) :=
by
replace hs₀ : 0 < μ.real s := ENNReal.toReal_pos hs₀ hsμ
replace ht₀ : 0 < μ.real t := ENNReal.toReal_pos ht₀ htμ
exact mem_openSegment_iff_div.mpr ⟨μ.real s, μ.real t, hs₀, ht₀, (average_union hd ht hsμ htμ hfs hft).symm⟩
