measure_le_integral — Mathlib

English

If f is integrable and nonnegative almost everywhere, and s is a set on which f ≥ 1, then the measure of s is bounded by the integral of f: μ(s) ≤ ∫ f dμ.

Русский

Если f интегрируема и неотрицательна почти всюду, и множество s удовлетворяет f ≥ 1 на s, то мера s не превышает интеграл от f: μ(s) ≤ ∫ f dμ.

LaTeX

$$$$\\mu(s) \\le \\int_X f(x)\\,d\\mu(x).$$$$

Lean4

theorem measure_le_integral {f : X → ℝ} (f_int : Integrable f μ) (f_nonneg : 0 ≤ᵐ[μ] f) {s : Set X}
    (hs : ∀ x ∈ s, 1 ≤ f x) : μ s ≤ ENNReal.ofReal (∫ x, f x ∂μ) :=
  by
  rw [ofReal_integral_eq_lintegral_ofReal f_int f_nonneg]
  apply meas_le_lintegral₀
  · exact ENNReal.continuous_ofReal.measurable.comp_aemeasurable f_int.1.aemeasurable
  · intro x hx
    simpa using ENNReal.ofReal_le_ofReal (hs x hx)

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