# mathlib3documentation

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 #

• probability_theory.kernel.with_density κ (f : α → β → ℝ≥0∞): kernel a ↦ (κ a).with_density (f a). It is defined if κ is s-finite. If f is finite everywhere, then this is also an s-finite kernel. The class of s-finite kernels is the smallest class of kernels that contains finite kernels and which is stable by with_density. Integral: ∫⁻ b, g b ∂(with_density κ f a) = ∫⁻ b, f a b * g b ∂(κ a)

## Main statements #

• probability_theory.kernel.lintegral_with_density: ∫⁻ b, g b ∂(with_density κ f a) = ∫⁻ b, f a b * g b ∂(κ a)
noncomputable def probability_theory.kernel.with_density {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (κ : ) (f : α ) :

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.with_density_of_not_measurable {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {f : α } (κ : ) (hf : ¬) :
@[protected]
theorem probability_theory.kernel.with_density_apply {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {f : α } (κ : ) (hf : measurable ) (a : α) :
= (κ a).with_density (f a)
theorem probability_theory.kernel.with_density_apply' {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {f : α } (κ : ) (hf : measurable ) (a : α) {s : set β} (hs : measurable_set s) :
s = ∫⁻ (b : β) in s, f a b κ a
theorem probability_theory.kernel.lintegral_with_density {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {f : α } (κ : ) (hf : measurable ) (a : α) {g : β ennreal} (hg : measurable g) :
∫⁻ (b : β), g b = ∫⁻ (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 β} {κ : } {E : Type u_3} [ E] {f : β E} {a : α} {g : α } (hg : measurable ) :
(b : β), f b (λ (a : α) (b : β), (g a b))) a = (b : β), g a b f b κ a
theorem probability_theory.kernel.with_density_add_left {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (κ η : ) (f : α ) :
theorem probability_theory.kernel.with_density_kernel_sum {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : measurable_space α} {mβ : measurable_space β} [countable ι] (κ : ι ) (hκ : (i : ι), ) (f : α ) :
theorem probability_theory.kernel.with_density_tsum {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : measurable_space α} {mβ : measurable_space β} [countable ι] (κ : ) {f : ι α } (hf : (i : ι), measurable (function.uncurry (f i))) :
(∑' (n : ι), f n) = probability_theory.kernel.sum (λ (n : ι),
theorem probability_theory.kernel.is_finite_kernel_with_density_of_bounded {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {f : α } (κ : ) {B : ennreal} (hB_top : B ) (hf_B : (a : α) (b : β), f a b B) :

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

theorem probability_theory.kernel.is_s_finite_kernel_with_density_of_is_finite_kernel {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {f : α } (κ : ) (hf_ne_top : (a : α) (b : β), f a b ) :

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

theorem probability_theory.kernel.is_s_finite_kernel.with_density {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} {f : α } (κ : ) (hf_ne_top : (a : α) (b : β), f a b ) :

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

@[protected, instance]
def probability_theory.kernel.with_density.probability_theory.is_s_finite_kernel {α : Type u_1} {β : Type u_2} {mα : measurable_space α} {mβ : measurable_space β} (κ : ) (f : α ) :
probability_theory.is_s_finite_kernel (λ (a : α) (b : β), (f a b)))

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