integral_undef — Mathlib

English

If a ≤ b and f is not AEStronglyMeasurable on μ restricted to Ioc a b, then the interval integral is zero.

Русский

Если a ≤ b и f не AEStronglyMeasurable на μ|_{Ioc a b}, то интервальный интеграл равен нулю.

LaTeX

$$$a \\le b \\Rightarrow Not (AEStronglyMeasurable f (μ|_{Ioc(a,b)})) \\Rightarrow \\int x in a..b f(x) ∂μ = 0$$$

Lean4

nonrec theorem integral_undef (h : ¬IntervalIntegrable f μ a b) : ∫ x in a..b, f x ∂μ = 0 :=
  by
  rw [intervalIntegrable_iff] at h
  rw [intervalIntegral_eq_integral_uIoc, integral_undef h, smul_zero]

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