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_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.withDensity_rnDeriv_eq'
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{κ η : Kernel α β}
[MeasurableSpace.CountableOrCountablyGenerated α β]
[IsFiniteKernel κ]
[IsFiniteKernel η]
(h : ∀ (a : α), (κ a).AbsolutelyContinuous (η a))
: