LeanMachineLearning exposition

MeasureTheory.Measure.compProd_withDensity_withDensity🔗

Minimal Lean file

compProd_withDensity_withDensity🔗

LemmaMeasureTheory.Measure.compProd_withDensity_withDensity
Details

No docstring.

🔗theorem
MeasureTheory.Measure.compProd_withDensity_withDensity.{u_1, u_2}
  {α : 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
      (ProbabilityTheory.Kernel.withDensity κ g)] :
  compProd (withDensity μ f)
      (ProbabilityTheory.Kernel.withDensity κ g) =
    withDensity (compProd μ κ) fun ac =>
      f (Prod.fst ac) * g (Prod.fst ac) (Prod.snd ac)
MeasureTheory.Measure.compProd_withDensity_withDensity.{u_1,
    u_2}
  {α : 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
      (ProbabilityTheory.Kernel.withDensity
        κ g)] :
  compProd (withDensity μ f)
      (ProbabilityTheory.Kernel.withDensity
        κ g) =
    withDensity (compProd μ κ) fun ac =>
      f (Prod.fst ac) *
        g (Prod.fst ac) (Prod.snd ac)

Code

lemma compProd_withDensity_withDensity [SFinite μ] {κ : Kernel α β} [IsSFiniteKernel κ]
    {f : α → ℝ≥0∞} {g : α → β → ℝ≥0∞} (hf : Measurable f) (hg : Measurable (Function.uncurry g))
    [IsSFiniteKernel (κ.withDensity g)] :
    (μ.withDensity f) ⊗ₘ (κ.withDensity g) =
      (μ ⊗ₘ κ).withDensity (fun ac ↦ f ac.1 * g ac.1 ac.2)
Body uses (1)
Used by (1)

Actions: Source · Open Issue

Proof
by
  rw [compProd_withDensity hg, compProd_withDensity_left hf]
  exact (withDensity_mul _ (hf.comp measurable_fst) hg).symm