# With Density #

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

## Main definitions #

• ProbabilityTheory.kernel.withDensity κ (f : α → β → ℝ≥0∞): kernel a ↦ (κ a).withDensity (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 withDensity. Integral: ∫⁻ b, g b ∂(withDensity κ f a) = ∫⁻ b, f a b * g b ∂(κ a)

## Main statements #

• ProbabilityTheory.kernel.lintegral_withDensity: ∫⁻ b, g b ∂(withDensity κ f a) = ∫⁻ b, f a b * g b ∂(κ a)
noncomputable def ProbabilityTheory.kernel.withDensity {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) (f : αβENNReal) :
()

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

Equations
• = if hf : then fun (a : α) => (κ a).withDensity (f a), else 0
Instances For
theorem ProbabilityTheory.kernel.withDensity_of_not_measurable {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {f : αβENNReal} (κ : ()) (hf : ) :
theorem ProbabilityTheory.kernel.withDensity_apply {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {f : αβENNReal} (κ : ()) (hf : ) (a : α) :
= (κ a).withDensity (f a)
theorem ProbabilityTheory.kernel.withDensity_apply' {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {f : αβENNReal} (κ : ()) (hf : ) (a : α) (s : Set β) :
() s = ∫⁻ (b : β) in s, f a bκ a
theorem ProbabilityTheory.kernel.withDensity_congr_ae {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) {f : αβENNReal} {g : αβENNReal} (hf : ) (hg : ) (hfg : ∀ (a : α), f a =ᵐ[κ a] g a) :
theorem ProbabilityTheory.kernel.withDensity_absolutelyContinuous {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} (f : αβENNReal) (a : α) :
().AbsolutelyContinuous (κ a)
@[simp]
theorem ProbabilityTheory.kernel.withDensity_one {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) :
@[simp]
theorem ProbabilityTheory.kernel.withDensity_one' {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) :
(ProbabilityTheory.kernel.withDensity κ fun (x : α) (x : β) => 1) = κ
@[simp]
theorem ProbabilityTheory.kernel.withDensity_zero {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) :
@[simp]
theorem ProbabilityTheory.kernel.withDensity_zero' {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) :
(ProbabilityTheory.kernel.withDensity κ fun (x : α) (x : β) => 0) = 0
theorem ProbabilityTheory.kernel.lintegral_withDensity {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {f : αβENNReal} (κ : ()) (hf : ) (a : α) {g : βENNReal} (hg : ) :
∫⁻ (b : β), g b = ∫⁻ (b : β), f a b * g bκ a
theorem ProbabilityTheory.kernel.integral_withDensity {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {E : Type u_4} [] {f : βE} {a : α} {g : αβNNReal} (hg : ) :
∫ (b : β), f b(ProbabilityTheory.kernel.withDensity κ fun (a : α) (b : β) => (g a b)) a = ∫ (b : β), g a b f bκ a
theorem ProbabilityTheory.kernel.withDensity_add_left {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) (η : ()) (f : αβENNReal) :
theorem ProbabilityTheory.kernel.withDensity_kernel_sum {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : } {mβ : } [] (κ : ι()) (hκ : ∀ (i : ι), ) (f : αβENNReal) :
theorem ProbabilityTheory.kernel.withDensity_add_right {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {f : αβENNReal} {g : αβENNReal} (hf : ) (hg : ) :
theorem ProbabilityTheory.kernel.withDensity_sub_add_cancel {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {f : αβENNReal} {g : αβENNReal} (hf : ) (hg : ) (hfg : ∀ (a : α), g a ≤ᵐ[κ a] f a) :
(ProbabilityTheory.kernel.withDensity κ fun (a : α) (x : β) => f a x - g a x) + =
theorem ProbabilityTheory.kernel.withDensity_tsum {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : } {mβ : } [] (κ : ()) {f : ιαβENNReal} (hf : ∀ (i : ι), Measurable (Function.uncurry (f i))) :
theorem ProbabilityTheory.kernel.isFiniteKernel_withDensity_of_bounded {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {f : αβENNReal} (κ : ()) {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 withDensity κ f is finite.

theorem ProbabilityTheory.kernel.isSFiniteKernel_withDensity_of_isFiniteKernel {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {f : αβENNReal} (κ : ()) (hf_ne_top : ∀ (a : α) (b : β), f a b ) :

Auxiliary lemma for IsSFiniteKernel.withDensity. If a kernel κ is finite, then withDensity κ f is s-finite.

theorem ProbabilityTheory.kernel.IsSFiniteKernel.withDensity {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {f : αβENNReal} (κ : ()) (hf_ne_top : ∀ (a : α) (b : β), f a b ) :

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

instance ProbabilityTheory.kernel.instIsSFiniteKernelWithDensityOfNNReal {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) (f : αβNNReal) :

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

Equations
• =
theorem ProbabilityTheory.kernel.withDensity_mul {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {f : αβNNReal} {g : αβENNReal} (hf : ) (hg : ) :
(ProbabilityTheory.kernel.withDensity κ fun (a : α) (x : β) => (f a x) * g a x) = ProbabilityTheory.kernel.withDensity (ProbabilityTheory.kernel.withDensity κ fun (a : α) (x : β) => (f a x)) g