lintegral_withDensity — Mathlib

English

For all a and measurable g, the lintegral withDensity κ f at a of g equals the lintegral under κ a of f a b · g b.

Русский

Для кажд°ого a и измеримой функции g выполняется равенство линегрального интеграла с плотностью: ∫ g d(withDensity κ f a) = ∫ f(a,b) g(b) dκ_a(b).

LaTeX

$$$ \int g \; d(\text{withDensity } κ f a) = \int f(a,b) \cdot g(b) \, d(κ a)(b) $$$

Lean4

theorem lintegral_withDensity (κ : Kernel α β) [IsSFiniteKernel κ] (hf : Measurable (Function.uncurry f)) (a : α)
    {g : β → ℝ≥0∞} (hg : Measurable g) : ∫⁻ b, g b ∂withDensity κ f a = ∫⁻ b, f a b * g b ∂κ a :=
  by
  rw [Kernel.withDensity_apply _ hf, lintegral_withDensity_eq_lintegral_mul _ (Measurable.of_uncurry_left hf) hg]
  simp_rw [Pi.mul_apply]

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