integral_withDensity — Mathlib

English

If f and g are such that ∀ a, f a =ᵐ[κ a] g a and both are measurable in uncurry, then κ.withDensity f = κ.withDensity g.

Русский

Если для всех a выполняется f a =ᵐ[κ a] g a и f,g измеримы по определению, тогда κ.withDensity f = κ.withDensity g.

LaTeX

$$$ (\forall a, f a =^{\text{a.e.}}_{κ a} g a) \Rightarrow κ.withDensity f = κ.withDensity g $$$

Lean4

theorem integral_withDensity {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : β → E} [IsSFiniteKernel κ]
    {a : α} {g : α → β → ℝ≥0} (hg : Measurable (Function.uncurry g)) :
    ∫ b, f b ∂withDensity κ (fun a b => g a b) a = ∫ b, g a b • f b ∂κ a :=
  by
  rw [Kernel.withDensity_apply, integral_withDensity_eq_integral_smul]
  · fun_prop
  · fun_prop

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