English
For measurable f,g and any set s, the integral of max(f,g) over s equals the sum of the integrals over s ∩ {f ≤ g} of g and s ∩ {g < f} of f.
Русский
Для измеримых f,g и множества s интеграл от max(f,g) по s равен сумме интегралов по s ∩ {f ≤ g} для g и по s ∩ {g < f} для f.
LaTeX
$$$$\\int_{a\\in s} \\max(f(a), g(a)) \\, d\\mu = \\int_{a\\in s \\cap \\{f(a) \\le g(a)\\}} g(a) \\, d\\mu + \\int_{a\\in s \\cap \\{g(a) < f(a)\\}} f(a) \\, d\\mu.$$$$
Lean4
theorem setLIntegral_max {f g : α → ℝ≥0∞} (hf : Measurable f) (hg : Measurable g) (s : Set α) :
∫⁻ x in s, max (f x) (g x) ∂μ = ∫⁻ x in s ∩ {x | f x ≤ g x}, g x ∂μ + ∫⁻ x in s ∩ {x | g x < f x}, f x ∂μ :=
by
rw [lintegral_max hf hg, restrict_restrict, restrict_restrict, inter_comm s, inter_comm s]
exacts [measurableSet_lt hg hf, measurableSet_le hf hg]
