LeanMachineLearning exposition

ProbabilityTheory.Kernel.compProd_withDensity_left🔗

Minimal Lean file

compProd_withDensity_left🔗

LemmaProbabilityTheory.Kernel.compProd_withDensity_left
Details

No docstring.

🔗theorem
ProbabilityTheory.Kernel.compProd_withDensity_left.{u_1, u_2, u_3}
  {α : 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)) :
  compProd (withDensity κ f) η =
    withDensity (compProd κ η) fun a bc => f a (Prod.fst bc)
ProbabilityTheory.Kernel.compProd_withDensity_left.{u_1,
    u_2, u_3}
  {α : 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)) :
  compProd (withDensity κ f) η =
    withDensity (compProd κ η) fun a bc =>
      f a (Prod.fst bc)

Code

lemma compProd_withDensity_left {κ : Kernel α β} {η : Kernel (α × β) γ} {f : α → β → ℝ≥0∞}
    [IsSFiniteKernel κ] [IsSFiniteKernel η] [IsSFiniteKernel (κ.withDensity f)]
    (hf : Measurable (Function.uncurry f)) :
    (κ.withDensity f) ⊗ₖ η = (κ ⊗ₖ η).withDensity (fun a bc ↦ f a bc.1)
Body uses (1)
Used by (1)

Actions: Source · Open Issue

Proof
by
  ext a : 1
  calc ((κ.withDensity f) ⊗ₖ η) a
      = (κ a).withDensity (f a) ⊗ₘ η.sectR a := by
        rw [compProd_apply_eq_compProd_sectR, Kernel.withDensity_apply _ hf]
    _ = ((κ a) ⊗ₘ (η.sectR a)).withDensity (fun bc ↦ f a bc.1) :=
        Measure.compProd_withDensity_left (by fun_prop)
    _ = ((κ ⊗ₖ η).withDensity (fun a bc ↦ f a bc.1)) a := by
        rw [← compProd_apply_eq_compProd_sectR, Kernel.withDensity_apply _ (by fun_prop)]