LeanMachineLearning exposition

ProbabilityTheory.Kernel.comp_withDensity_eq_withDensity_comp🔗

Minimal Lean file

comp_withDensity_eq_withDensity_comp🔗

LemmaProbabilityTheory.Kernel.comp_withDensity_eq_withDensity_comp
Details

No docstring.

🔗theorem
ProbabilityTheory.Kernel.comp_withDensity_eq_withDensity_comp.{u_1, u_2}
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ : Kernel α β} [IsSFiniteKernel κ] {f : β → ENNReal}
  (hf : Measurable f) :
  MeasureTheory.Measure.bind μ ⇑(withDensity κ fun x b => f b) =
    MeasureTheory.Measure.withDensity (MeasureTheory.Measure.bind μ ⇑κ)
      f
ProbabilityTheory.Kernel.comp_withDensity_eq_withDensity_comp.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {μ : MeasureTheory.Measure α}
  {κ : Kernel α β} [IsSFiniteKernel κ]
  {f : β → ENNReal} (hf : Measurable f) :
  MeasureTheory.Measure.bind μ
      ⇑(withDensity κ fun x b => f b) =
    MeasureTheory.Measure.withDensity
      (MeasureTheory.Measure.bind μ ⇑κ) f

Code

lemma comp_withDensity_eq_withDensity_comp {κ : Kernel α β} [IsSFiniteKernel κ] {f : β → ℝ≥0∞}
    (hf : Measurable f) : (κ.withDensity (fun _ b ↦ f b)) ∘ₘ μ = (κ ∘ₘ μ).withDensity f
Used by (1)

Actions: Source · Open Issue

Proof
by
  refine Measure.ext_of_lintegral _ fun g hg ↦ ?_
  calc ∫⁻ b, g b ∂((κ.withDensity (fun _ b ↦ f b)) ∘ₘ μ)
      = ∫⁻ a, ∫⁻ b, g b ∂(κ.withDensity (fun _ b ↦ f b)) a ∂μ :=
        Measure.lintegral_bind (measurable _).aemeasurable hg.aemeasurable
    _ = ∫⁻ a, ∫⁻ b, f b * g b ∂κ a ∂μ := by
        congr with a
        exact lintegral_withDensity _ (by fun_prop) _ hg
    _ = ∫⁻ b, f b * g b ∂(κ ∘ₘ μ) :=
        (Measure.lintegral_bind (measurable _).aemeasurable (hf.mul hg).aemeasurable).symm
    _ = ∫⁻ b, g b ∂((κ ∘ₘ μ).withDensity f) :=
        (lintegral_withDensity_eq_lintegral_mul _ hf hg).symm