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)
:
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
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))
:
κ.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 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)
:
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))
:
theorem
ProbabilityTheory.Kernel.withDensity_add_left
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
(κ η : 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.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 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 g : α → β → ENNReal}
(hf : Measurable (Function.uncurry f))
(hg : Measurable (Function.uncurry g))
(hfg : ∀ (a : α), g a ≤ᵐ[κ a] f a)
:
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))
: