laverage_union_mem_segment — Mathlib

English

Multiplication and laverage on restricted sets commute with the measure on Ω.

Русский

Умножение и среднее на ограниченных множествах совместимы с мерой на Ω.

LaTeX

$$$\\laverage_{μ}(f) = \\dfrac{1}{μ(Ω)} × ∫ f\, dμ$$$

Lean4

theorem laverage_union_mem_segment (hd : AEDisjoint μ s t) (ht : NullMeasurableSet t μ) (hsμ : μ s ≠ ∞)
    (htμ : μ t ≠ ∞) : ⨍⁻ x in s ∪ t, f x ∂μ ∈ [⨍⁻ x in s, f x ∂μ -[ℝ≥0∞] ⨍⁻ x in t, f x ∂μ] :=
  by
  by_cases hs₀ : μ s = 0
  · rw [← ae_eq_empty] at hs₀
    rw [restrict_congr_set (hs₀.union EventuallyEq.rfl), empty_union]
    exact right_mem_segment _ _ _
  · refine ⟨μ s / (μ s + μ t), μ t / (μ s + μ t), zero_le _, zero_le _, ?_, (laverage_union hd ht).symm⟩
    rw [← ENNReal.add_div, ENNReal.div_self (add_eq_zero.not.2 fun h => hs₀ h.1) (add_ne_top.2 ⟨hsμ, htμ⟩)]

Похожие утверждения