integral_non_aestronglyMeasurable

English

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

Русский

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

LaTeX

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

Lean4

nonrec theorem integral_non_aestronglyMeasurable (hf : ¬AEStronglyMeasurable f (μ.restrict (Ι a b))) :
    ∫ x in a..b, f x ∂μ = 0 := by
  rw [intervalIntegral_eq_integral_uIoc, integral_non_aestronglyMeasurable hf, smul_zero]

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