mathlib3 documentation

probability.kernel.with_density

With Density #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

For an s-finite kernel κ : kernel α β and a function f : α → β → ℝ≥0∞ which is finite everywhere, we define with_density κ f as the kernel a ↦ (κ a).with_density (f a). This is an s-finite kernel.

Main definitions #

Main statements #

Kernel with image (κ a).with_density (f a) if function.uncurry f is measurable, and with image 0 otherwise. If function.uncurry f is measurable, it satisfies ∫⁻ b, g b ∂(with_density κ f hf a) = ∫⁻ b, f a b * g b ∂(κ a).

Equations
Instances for probability_theory.kernel.with_density
theorem probability_theory.kernel.lintegral_with_density {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {f : α β ennreal} (κ : (probability_theory.kernel α β)) [probability_theory.is_s_finite_kernel κ] (hf : measurable (function.uncurry f)) (a : α) {g : β ennreal} (hg : measurable g) :
∫⁻ (b : β), g b (probability_theory.kernel.with_density κ f) a = ∫⁻ (b : β), f a b * g b κ a
theorem probability_theory.kernel.integral_with_density {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {κ : (probability_theory.kernel α β)} {E : Type u_3} [normed_add_comm_group E] [normed_space E] [complete_space E] {f : β E} [probability_theory.is_s_finite_kernel κ] {a : α} {g : α β nnreal} (hg : measurable (function.uncurry g)) :
(b : β), f b (probability_theory.kernel.with_density κ (λ (a : α) (b : β), (g a b))) a = (b : β), g a b f b κ a

If a kernel κ is finite and a function f : α → β → ℝ≥0∞ is bounded, then with_density κ f is finite.

Auxiliary lemma for is_s_finite_kernel_with_density. If a kernel κ is finite, then with_density κ f is s-finite.

For a s-finite kernel κ and a function f : α → β → ℝ≥0∞ which is everywhere finite, with_density κ f is s-finite.

@[protected, instance]

For a s-finite kernel κ and a function f : α → β → ℝ≥0, with_density κ f is s-finite.