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α : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (f : α → β → ENNReal) : ProbabilityTheory.Kernel α β

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

• κ.withDensity f = if hf : Measurable (Function.uncurry f) then { toFun := fun (a : α) => (κ a).withDensity (f a), measurable' := ⋯ } else 0

theorem ProbabilityTheory.Kernel.withDensity_of_not_measurable {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β → ENNReal} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (hf : ¬Measurable (Function.uncurry f)) : κ.withDensity f = 0

theorem ProbabilityTheory.Kernel.withDensity_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β → ENNReal} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (hf : Measurable (Function.uncurry f)) (a : α) : (κ.withDensity f) a = (κ a).withDensity (f a)

theorem ProbabilityTheory.Kernel.withDensity_apply' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β → ENNReal} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (hf : Measurable (Function.uncurry f)) (a : α) (s : Set β) : ((κ.withDensity f) a) s = ∫⁻ (b : β) in s, f a b ∂κ a

theorem ProbabilityTheory.Kernel.withDensity_congr_ae {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] {f : α → β → ENNReal} {g : α → β → ENNReal} (hf : Measurable (Function.uncurry f)) (hg : Measurable (Function.uncurry g)) (hfg : ∀ (a : α), f a =ᵐ[κ a] g a) : κ.withDensity f = κ.withDensity g

theorem ProbabilityTheory.Kernel.withDensity_absolutelyContinuous {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] (f : α → β → ENNReal) (a : α) : ((κ.withDensity f) a).AbsolutelyContinuous (κ a)

@[simp]

theorem ProbabilityTheory.Kernel.withDensity_one {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] : κ.withDensity 1 = κ

@[simp]

theorem ProbabilityTheory.Kernel.withDensity_one' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] : (κ.withDensity fun (x : α) (x : β) => 1) = κ

@[simp]

theorem ProbabilityTheory.Kernel.withDensity_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] : κ.withDensity 0 = 0

@[simp]

theorem ProbabilityTheory.Kernel.withDensity_zero' {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] : (κ.withDensity fun (x : α) (x : β) => 0) = 0

theorem ProbabilityTheory.Kernel.lintegral_withDensity {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β → ENNReal} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (hf : Measurable (Function.uncurry f)) (a : α) {g : β → ENNReal} (hg : Measurable g) : ∫⁻ (b : β), g b ∂(κ.withDensity f) a = ∫⁻ (b : β), f a b * g b ∂κ a

theorem ProbabilityTheory.Kernel.integral_withDensity {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : β → E} [ProbabilityTheory.IsSFiniteKernel κ] {a : α} {g : α → β → NNReal} (hg : Measurable (Function.uncurry g)) : ∫ (b : β), f b ∂(κ.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α : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] [ProbabilityTheory.IsSFiniteKernel η] (f : α → β → ENNReal) : (κ + η).withDensity f = κ.withDensity f + η.withDensity f

theorem ProbabilityTheory.Kernel.withDensity_kernel_sum {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [Countable ι] (κ : ι → ProbabilityTheory.Kernel α β) (hκ : ∀ (i : ι), ProbabilityTheory.IsSFiniteKernel (κ i)) (f : α → β → ENNReal) : (ProbabilityTheory.Kernel.sum κ).withDensity f = ProbabilityTheory.Kernel.sum fun (i : ι) => (κ i).withDensity f

theorem ProbabilityTheory.Kernel.withDensity_add_right {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {f : α → β → ENNReal} {g : α → β → ENNReal} (hf : Measurable (Function.uncurry f)) (hg : Measurable (Function.uncurry g)) : κ.withDensity (f + g) = κ.withDensity f + κ.withDensity g

theorem ProbabilityTheory.Kernel.withDensity_sub_add_cancel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {f : α → β → ENNReal} {g : α → β → ENNReal} (hf : Measurable (Function.uncurry f)) (hg : Measurable (Function.uncurry g)) (hfg : ∀ (a : α), g a ≤ᵐ[κ a] f a) : (κ.withDensity fun (a : α) (x : β) => f a x - g a x) + κ.withDensity g = κ.withDensity f

theorem ProbabilityTheory.Kernel.withDensity_tsum {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [Countable ι] (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] {f : ι → α → β → ENNReal} (hf : ∀ (i : ι), Measurable (Function.uncurry (f i))) : κ.withDensity (∑' (n : ι), f n) = ProbabilityTheory.Kernel.sum fun (n : ι) => κ.withDensity (f n)

theorem ProbabilityTheory.Kernel.isFiniteKernel_withDensity_of_bounded {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β → ENNReal} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] {B : ENNReal} (hB_top : B ≠ ⊤) (hf_B : ∀ (a : α) (b : β), f a b ≤ B) : ProbabilityTheory.IsFiniteKernel (κ.withDensity f)

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α : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β → ENNReal} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] (hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤) : ProbabilityTheory.IsSFiniteKernel (κ.withDensity f)

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α : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β → ENNReal} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤) : ProbabilityTheory.IsSFiniteKernel (κ.withDensity f)

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α : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (f : α → β → NNReal) : ProbabilityTheory.IsSFiniteKernel (κ.withDensity fun (a : α) (b : β) => ↑(f a b))

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α : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ] {f : α → β → NNReal} {g : α → β → ENNReal} (hf : Measurable (Function.uncurry f)) (hg : Measurable (Function.uncurry g)) : (κ.withDensity fun (a : α) (x : β) => ↑(f a x) * g a x) = (κ.withDensity fun (a : α) (x : β) => ↑(f a x)).withDensity g