LeanMachineLearning exposition

ProbabilityTheory.Kernel.withDensity_rnDeriv_eq'🔗

Minimal Lean file

withDensity_rnDeriv_eq'🔗

LemmaProbabilityTheory.Kernel.withDensity_rnDeriv_eq'
Details

No docstring.

🔗theorem
ProbabilityTheory.Kernel.withDensity_rnDeriv_eq'.{u_1, u_2}
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {κ η : Kernel α β}
  [MeasurableSpace.CountableOrCountablyGenerated α β] [IsFiniteKernel κ]
  [IsFiniteKernel η]
  (h :
    ∀ (a : α), MeasureTheory.Measure.AbsolutelyContinuous (κ a) (η a)) :
  withDensity η (rnDeriv κ η) = κ
ProbabilityTheory.Kernel.withDensity_rnDeriv_eq'.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {κ η : Kernel α β}
  [MeasurableSpace.CountableOrCountablyGenerated
      α β]
  [IsFiniteKernel κ] [IsFiniteKernel η]
  (h :
    ∀ (a : α),
      MeasureTheory.Measure.AbsolutelyContinuous
        (κ a) (η a)) :
  withDensity η (rnDeriv κ η) = κ

Code

lemma withDensity_rnDeriv_eq' {κ η : Kernel α β} [MeasurableSpace.CountableOrCountablyGenerated α β]
    [IsFiniteKernel κ] [IsFiniteKernel η] (h : ∀ a, κ a ≪ η a) :
    η.withDensity (κ.rnDeriv η) = κ
Used by (1)

Actions: Source · Open Issue

Proof
Kernel.ext fun a ↦ withDensity_rnDeriv_eq (h a)