integral_pos_iff_support_of_nonneg_ae

English

For f ≥ 0 a.e. and integrable, the integral is positive iff the μ-measure of the support of f is positive.

Русский

Для функции f ≥ 0 a.e. интегрируемой интеграл положителен тогда и только тогда, когда мера поддержки f положительна.

LaTeX

$$$0 < \int a \\, f(a) \\, d\\\\mu \\\\iff 0 < \\\\mu(\\\\mathrm{Supp} f)$$$

Lean4

theorem integral_pos_iff_support_of_nonneg_ae {f : α → ℝ} (hf : 0 ≤ᵐ[μ] f) (hfi : Integrable f μ) :
    (0 < ∫ x, f x ∂μ) ↔ 0 < μ (Function.support f) := by
  simp_rw [(integral_nonneg_of_ae hf).lt_iff_ne, pos_iff_ne_zero, Ne, @eq_comm ℝ 0,
    integral_eq_zero_iff_of_nonneg_ae hf hfi, Filter.EventuallyEq, ae_iff, Pi.zero_apply, Function.support]

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