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∞): kernela ↦ (κ a).withDensity (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 bywithDensity. 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
- ProbabilityTheory.kernel.withDensity κ f = if hf : Measurable (Function.uncurry f) 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α : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : α → β → ENNReal}
(κ : ↥(ProbabilityTheory.kernel α β))
[ProbabilityTheory.IsSFiniteKernel κ]
(hf : ¬Measurable (Function.uncurry f))
:
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 : α)
:
(ProbabilityTheory.kernel.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 β)
:
↑↑((ProbabilityTheory.kernel.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 : α), (κ a).ae.EventuallyEq (f a) (g a))
:
theorem
ProbabilityTheory.kernel.withDensity_absolutelyContinuous
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)}
[ProbabilityTheory.IsSFiniteKernel κ]
(f : α → β → ENNReal)
(a : α)
:
((ProbabilityTheory.kernel.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 κ]
:
@[simp]
theorem
ProbabilityTheory.kernel.withDensity_one'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : ↥(ProbabilityTheory.kernel α β))
[ProbabilityTheory.IsSFiniteKernel κ]
:
(ProbabilityTheory.kernel.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 κ]
:
@[simp]
theorem
ProbabilityTheory.kernel.withDensity_zero'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : ↥(ProbabilityTheory.kernel α β))
[ProbabilityTheory.IsSFiniteKernel κ]
:
(ProbabilityTheory.kernel.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 ∂(ProbabilityTheory.kernel.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 ∂(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α : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ : ↥(ProbabilityTheory.kernel α β))
(η : ↥(ProbabilityTheory.kernel α β))
[ProbabilityTheory.IsSFiniteKernel κ]
[ProbabilityTheory.IsSFiniteKernel η]
(f : α → β → ENNReal)
:
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.withDensity (ProbabilityTheory.kernel.sum κ) f = ProbabilityTheory.kernel.sum fun (i : ι) => ProbabilityTheory.kernel.withDensity (κ i) 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))
:
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 : α), (κ a).ae.EventuallyLE (g a) (f a))
:
(ProbabilityTheory.kernel.withDensity κ fun (a : α) (x : β) => f a x - g a x) + ProbabilityTheory.kernel.withDensity κ g = ProbabilityTheory.kernel.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)))
:
ProbabilityTheory.kernel.withDensity κ (∑' (n : ι), f n) = ProbabilityTheory.kernel.sum fun (n : ι) => ProbabilityTheory.kernel.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)
:
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 ≠ ⊤)
:
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 ≠ ⊤)
:
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 (ProbabilityTheory.kernel.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))
:
(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