English
For measurable f and g, the lintegral of max(f,g) equals the sum of the integrals over the regions where f ≤ g and where g < f, respectively, of g and f.
Русский
Для измеримых f и g линегральный интеграл от max(f,g) равен сумме интегралов по областям {f ≤ g} и {g < f} соответственно, т.е. по g на {f ≤ g} и по f на {g < f}.
LaTeX
$$$$\\int_{x} \\max(f(x), g(x)) \\, d\\mu = \\int_{x:\\, f(x) \\le g(x)} g(x) \\, d\\mu + \\int_{x:\\, g(x) < f(x)} f(x) \\, d\\mu.$$$$
Lean4
theorem lintegral_max {f g : α → ℝ≥0∞} (hf : Measurable f) (hg : Measurable g) :
∫⁻ x, max (f x) (g x) ∂μ = ∫⁻ x in {x | f x ≤ g x}, g x ∂μ + ∫⁻ x in {x | g x < f x}, f x ∂μ :=
by
have hm : MeasurableSet {x | f x ≤ g x} := measurableSet_le hf hg
rw [← lintegral_add_compl (fun x => max (f x) (g x)) hm]
simp only [← compl_setOf, ← not_le]
refine congr_arg₂ (· + ·) (setLIntegral_congr_fun hm ?_) (setLIntegral_congr_fun hm.compl ?_)
exacts [fun x => max_eq_right (a := f x) (b := g x), fun x (hx : ¬f x ≤ g x) => max_eq_left (not_le.1 hx).le]
