integral_pos_iff_support_of_nonneg_ae

English

If f is nonnegative almost everywhere and interval-integrable on the unordered interval between a and b, then 0 < ∫ x in a..b f x ∂μ iff a < b and 0 < μ (support f ∩ Ioc a b).

Русский

Если f неотрицательно почти всюду и интегрируема на unordered-интервале между a и b, то 0 < ∫_a^b f ⇔ a < b и 0 < μ(поддержка f ∩ Ioc a b).

LaTeX

$$$(0 < \\int x in a..b, f x \\ d\\mu) \\iff (a < b \\\\wedge 0 < \\mu (\\mathrm{support}(f) \\cap Ioc(a,b))).$$$

Lean4

/-- If `f` is nonnegative a.e.-everywhere and it is integrable on the unordered interval
`Set.uIoc a b`, then its integral over `a..b` is positive if and only if `a < b` and the
measure of `Function.support f ∩ Set.Ioc a b` is positive. -/
theorem integral_pos_iff_support_of_nonneg_ae (hf : 0 ≤ᵐ[μ] f) (hfi : IntervalIntegrable f μ a b) :
    (0 < ∫ x in a..b, f x ∂μ) ↔ a < b ∧ 0 < μ (support f ∩ Ioc a b) :=
  integral_pos_iff_support_of_nonneg_ae' (ae_mono Measure.restrict_le_self hf) hfi

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