Lemmas about kernels and measures with density #
theorem
MeasureTheory.map_withDensity_comp
{α : Type u_1}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mγ : MeasurableSpace γ}
{μ : Measure α}
{g : α → γ}
{f : γ → ENNReal}
(hg : Measurable g)
(hf : Measurable f)
:
theorem
MeasureTheory.map_equiv_withDensity
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
{e : α ≃ᵐ β}
{f : α → ENNReal}
(hf : Measurable f)
:
theorem
MeasureTheory.map_swap_withDensity_comp_snd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure (α × β)}
{f : β → ENNReal}
(hf : Measurable f)
:
Measure.map Prod.swap (μ.withDensity fun (ab : α × β) => f ab.2) = (Measure.map Prod.swap μ).withDensity fun (ba : β × α) => f ba.1
theorem
MeasureTheory.Measure.compProd_withDensity_left
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
[SFinite μ]
{κ : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsSFiniteKernel κ]
{f : α → ENNReal}
(hf : Measurable f)
:
theorem
MeasureTheory.Measure.compProd_withDensity_withDensity
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
[SFinite μ]
{κ : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsSFiniteKernel κ]
{f : α → ENNReal}
{g : α → β → ENNReal}
(hf : Measurable f)
(hg : Measurable (Function.uncurry g))
[ProbabilityTheory.IsSFiniteKernel (κ.withDensity g)]
:
(μ.withDensity f).compProd (κ.withDensity g) = (μ.compProd κ).withDensity fun (ac : α × β) => f ac.1 * g ac.1 ac.2
theorem
MeasureTheory.Measure.compProd_eq_compProd_withDensity_comp_snd
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : Measure α}
[SFinite μ]
{κ η : ProbabilityTheory.Kernel α β}
[ProbabilityTheory.IsSFiniteKernel κ]
[ProbabilityTheory.IsSFiniteKernel η]
{f : β → ENNReal}
(hf : Measurable f)
(h : ⇑κ =ᵐ[μ] ⇑(η.withDensity fun (x : α) (b : β) => f b))
:
theorem
ProbabilityTheory.Kernel.comp_withDensity_eq_withDensity_comp
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{κ : Kernel α β}
[IsSFiniteKernel κ]
{f : β → ENNReal}
(hf : Measurable f)
:
theorem
ProbabilityTheory.Kernel.compProd_withDensity_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ}
{κ : Kernel α β}
{η : Kernel (α × β) γ}
{f : α → β → ENNReal}
[IsSFiniteKernel κ]
[IsSFiniteKernel η]
[IsSFiniteKernel (κ.withDensity f)]
(hf : Measurable (Function.uncurry f))
:
theorem
ProbabilityTheory.Kernel.withDensity_rnDeriv_eq'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ η : Kernel α β}
[MeasurableSpace.CountableOrCountablyGenerated α β]
[IsFiniteKernel κ]
[IsFiniteKernel η]
(h : ∀ (a : α), (κ a).AbsolutelyContinuous (η a))
: