English
If f is integrable and nonnegative almost everywhere, and on s we have f ≤ 1 while on the complement s^c we have f ≤ 0, then ∫ f ≤ μ(s).
Русский
Если f интегрируема и неотрицательна почти всюду, и на s выполняется f ≤ 1, а на s^c f ≤ 0, то ∫ f ≤ μ(s).
LaTeX
$$$$\\int_X f(x)\\,d\\mu(x) \\le \\mu(s).$$$$
Lean4
theorem integral_le_measure {f : X → ℝ} {s : Set X} (hs : ∀ x ∈ s, f x ≤ 1) (h's : ∀ x ∈ sᶜ, f x ≤ 0) :
ENNReal.ofReal (∫ x, f x ∂μ) ≤ μ s := by
by_cases H : Integrable f μ; swap
· simp [integral_undef H]
let g x := max (f x) 0
have g_int : Integrable g μ := H.pos_part
have : ENNReal.ofReal (∫ x, f x ∂μ) ≤ ENNReal.ofReal (∫ x, g x ∂μ) :=
by
apply ENNReal.ofReal_le_ofReal
exact integral_mono H g_int (fun x ↦ le_max_left _ _)
apply this.trans
rw [ofReal_integral_eq_lintegral_ofReal g_int (Eventually.of_forall (fun x ↦ le_max_right _ _))]
apply lintegral_le_meas
· intro x
apply ENNReal.ofReal_le_of_le_toReal
by_cases H : x ∈ s
· simpa [g] using hs x H
· apply le_trans _ zero_le_one
simpa [g] using h's x H
· intro x hx
simpa [g] using h's x hx
