setIntegral_re_add_im — Mathlib

English

Let f: X → 𝕜 be a nonnegative measurable density and g: X → E be integrable under μ.withDensity f. Then ∫ g d(μ.withDensity f) = ∫ f x · g(x) dμ.

Русский

Пусть f — плотность, неотрицательная и измеримая, и g: X → E интегрируема по μ с плотностью f. Тогда интеграл по μ с плотностью f равен интегралу по μ умноженному на density: ∫ g d(μ.withDensity f) = ∫ f(x) g(x) dμ.

LaTeX

$$$\\int_X g(x) \\,d(\\mu.withDensity f) = \\int_X f(x)\\, g(x) \\,d\\mu$$$

Lean4

theorem setIntegral_re_add_im {f : X → 𝕜} {i : Set X} (hf : IntegrableOn f i μ) :
    ((∫ x in i, RCLike.re (f x) ∂μ : ℝ) : 𝕜) + (∫ x in i, RCLike.im (f x) ∂μ : ℝ) * RCLike.I = ∫ x in i, f x ∂μ :=
  integral_re_add_im hf

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