English
If κ is s-finite and f,g are suitable measurable functions, then κ.withDensity (λ a x, f a x * g a x) equals (κ.withDensity (λ a x, f a x)).withDensity g.
Русский
Если κ — s-финитное ядро и f, g удовлетворяют условиям измеримости, тогда κ.withDensity(λ a x, f a x · g a x) равно (κ.withDensity(λ a x, f a x)).withDensity g.
LaTeX
$$$\\mathrm{withDensity}\\;\\kappa\\; (\\lambda a x. f(a,x) \\cdot g(a,x)) = \\mathrm{withDensity}(\\mathrm{withDensity}\\;\\kappa\\; (\\lambda a x. f(a,x))\\; g)$$$
Lean4
nonrec theorem withDensity_mul [IsSFiniteKernel κ] {f : α → β → ℝ≥0} {g : α → β → ℝ≥0∞}
(hf : Measurable (Function.uncurry f)) (hg : Measurable (Function.uncurry g)) :
withDensity κ (fun a x ↦ f a x * g a x) = withDensity (withDensity κ fun a x ↦ f a x) g :=
by
ext a : 1
rw [Kernel.withDensity_apply]
swap; · fun_prop
change
(Measure.withDensity (κ a) ((fun x ↦ (f a x : ℝ≥0∞)) * (fun x ↦ (g a x : ℝ≥0∞)))) =
(withDensity (withDensity κ fun a x ↦ f a x) g) a
rw [withDensity_mul]
· rw [Kernel.withDensity_apply _ hg, Kernel.withDensity_apply]
exact measurable_coe_nnreal_ennreal.comp hf
· fun_prop
· fun_prop
