integral_eq_zero_iff_of_le_of_nonneg_ae

English

If the support of f is contained in the interval Ioc a b, then the interval integral over a..b equals the unrestricted integral over μ.

Русский

Если опора функции содержится в Ioc(a,b), то интеграл по интервалу равен интегралу по всей мере.

LaTeX

$$$ \\text{If } \\operatorname{supp} f \\subseteq Ioc(a,b), \\; \\int_{a}^{b} f(x) \\, dμ = \\int_{ℝ} f(x) \\, dμ $$$

Lean4

theorem integral_eq_zero_iff_of_le_of_nonneg_ae (hab : a ≤ b) (hf : 0 ≤ᵐ[μ.restrict (Ioc a b)] f)
    (hfi : IntervalIntegrable f μ a b) : ∫ x in a..b, f x ∂μ = 0 ↔ f =ᵐ[μ.restrict (Ioc a b)] 0 := by
  rw [integral_of_le hab, integral_eq_zero_iff_of_nonneg_ae hf hfi.1]

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