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∞): kernela ↦ (κ a).with_density (f a). It is defined ifκis s-finite. Iffis 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 bywith_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 β}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ]
(f : α → β → ennreal) :
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
- probability_theory.kernel.with_density κ f = dite (measurable (function.uncurry f)) (λ (hf : measurable (function.uncurry f)), ⟨λ (a : α), (⇑κ a).with_density (f a), _⟩) (λ (hf : ¬measurable (function.uncurry f)), 0)
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 : α → β → ennreal}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ]
(hf : ¬measurable (function.uncurry f)) :
@[protected]
theorem
probability_theory.kernel.with_density_apply
{α : 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 : α) :
⇑(probability_theory.kernel.with_density κ f) 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 : α → β → ennreal}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ]
(hf : measurable (function.uncurry f))
(a : α)
{s : set β}
(hs : measurable_set s) :
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) :
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)) :
theorem
probability_theory.kernel.with_density_add_left
{α : Type u_1}
{β : Type u_2}
{mα : measurable_space α}
{mβ : measurable_space β}
(κ η : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ]
[probability_theory.is_s_finite_kernel η]
(f : α → β → ennreal) :
theorem
probability_theory.kernel.with_density_kernel_sum
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{mα : measurable_space α}
{mβ : measurable_space β}
[countable ι]
(κ : ι → ↥(probability_theory.kernel α β))
(hκ : ∀ (i : ι), probability_theory.is_s_finite_kernel (κ i))
(f : α → β → ennreal) :
theorem
probability_theory.kernel.with_density_tsum
{α : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{mα : measurable_space α}
{mβ : measurable_space β}
[countable ι]
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ]
{f : ι → α → β → ennreal}
(hf : ∀ (i : ι), measurable (function.uncurry (f i))) :
probability_theory.kernel.with_density κ (∑' (n : ι), f n) = probability_theory.kernel.sum (λ (n : ι), probability_theory.kernel.with_density κ (f 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 : α → β → ennreal}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_finite_kernel κ]
{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 : α → β → ennreal}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_finite_kernel κ]
(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 : α → β → ennreal}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ]
(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 β}
(κ : ↥(probability_theory.kernel α β))
[probability_theory.is_s_finite_kernel κ]
(f : α → β → nnreal) :
probability_theory.is_s_finite_kernel (probability_theory.kernel.with_density κ (λ (a : α) (b : β), ↑(f a b)))
For a s-finite kernel κ and a function f : α → β → ℝ≥0, with_density κ f is s-finite.