LeanMachineLearning exposition

MeasureTheory.Measure.compProd_withDensity_left🔗

Minimal Lean file

compProd_withDensity_left🔗

LemmaMeasureTheory.Measure.compProd_withDensity_left
Details

No docstring.

🔗theorem
MeasureTheory.Measure.compProd_withDensity_left.{u_1, u_2}
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {μ : Measure α} [SFinite μ]
  {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ] {f : α → ENNReal}
  (hf : Measurable f) :
  compProd (withDensity μ f) κ =
    withDensity (compProd μ κ) fun ab => f (Prod.fst ab)
MeasureTheory.Measure.compProd_withDensity_left.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {μ : Measure α}
  [SFinite μ]
  {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ]
  {f : α → ENNReal} (hf : Measurable f) :
  compProd (withDensity μ f) κ =
    withDensity (compProd μ κ) fun ab =>
      f (Prod.fst ab)

Code

lemma compProd_withDensity_left [SFinite μ] {κ : Kernel α β} [IsSFiniteKernel κ] {f : α → ℝ≥0∞}
    (hf : Measurable f) : (μ.withDensity f) ⊗ₘ κ = (μ ⊗ₘ κ).withDensity (fun ab ↦ f ab.1)
Used by (4)

Actions: Source · Open Issue

Proof
by
  refine ext_of_lintegral _ fun g hg ↦ ?_
  calc ∫⁻ ab, g ab ∂((μ.withDensity f) ⊗ₘ κ)
      = ∫⁻ a, ∫⁻ b, g (a, b) ∂κ a ∂(μ.withDensity f) :=
        lintegral_compProd hg
    _ = ∫⁻ a, f a * ∫⁻ b, g (a, b) ∂κ a ∂μ :=
        lintegral_withDensity_eq_lintegral_mul _ hf hg.lintegral_kernel_prod_right'
    _ = ∫⁻ a, ∫⁻ b, f a * g (a, b) ∂κ a ∂μ :=
        lintegral_congr fun a ↦ (lintegral_const_mul _ (by fun_prop)).symm
    _ = ∫⁻ ab, (fun ab ↦ f ab.1) ab * g ab ∂(μ ⊗ₘ κ) :=
        (lintegral_compProd ((hf.comp measurable_fst).mul hg)).symm
    _ = ∫⁻ ab, g ab ∂((μ ⊗ₘ κ).withDensity (fun ab ↦ f ab.1)) :=
        (lintegral_withDensity_eq_lintegral_mul _ (hf.comp measurable_fst) hg).symm