English
Under suitable hypotheses, the average over s ∪ t belongs to the open segment between the averages over s and t.
Русский
При подходящих гипотезах среднее по s ∪ t лежит в открытом отрезке между средними по s и по t.
LaTeX
$$$\langle f \rangle_{μ|_{s\cup t}} \in \left( \langle f \rangle_{μ|_s}, \langle f \rangle_{μ|_t} \right)$$$
Lean4
theorem average_union_mem_segment {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 ∂μ ∈ [⨍ x in s, f x ∂μ -[ℝ] ⨍ x in t, f x ∂μ] :=
by
by_cases hse : μ s = 0
· rw [← ae_eq_empty] at hse
rw [restrict_congr_set (hse.union EventuallyEq.rfl), empty_union]
exact right_mem_segment _ _ _
· refine
mem_segment_iff_div.mpr
⟨μ.real s, μ.real t, ENNReal.toReal_nonneg, ENNReal.toReal_nonneg, ?_,
(average_union hd ht hsμ htμ hfs hft).symm⟩
calc
0 < μ.real s := ENNReal.toReal_pos hse hsμ
_ ≤ _ := le_add_of_nonneg_right ENNReal.toReal_nonneg
