intervalIntegral_eq_integral_uIoc

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 \\text{Not AEStronglyMeasurable}(f, μ|_{Ioc(a,b)}) \\Rightarrow ∫ x \\in a..b f(x) ∂μ = 0$$$

Lean4

theorem intervalIntegral_eq_integral_uIoc (f : ℝ → E) (a b : ℝ) (μ : Measure ℝ) :
    ∫ x in a..b, f x ∂μ = (if a ≤ b then 1 else -1 : ℝ) • ∫ x in Ι a b, f x ∂μ :=
  by
  split_ifs with h
  · simp only [integral_of_le h, uIoc_of_le h, one_smul]
  · simp only [integral_of_ge (not_le.1 h).le, uIoc_of_ge (not_le.1 h).le, neg_one_smul]

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