withDensity_rnDeriv_eq — Mathlib

English

If κ a ≪ η a, then η.withDensity (κ.rnDeriv η) a = κ a.

Русский

Если κ a ≪ η a, то η.withDensity(κ.rnDeriv η) a = κ a.

LaTeX

$$$ \\eta.withDensity (κ.rnDeriv η) a = κ a $$$

Lean4

theorem withDensity_rnDeriv_eq [IsFiniteKernel κ] [IsFiniteKernel η] {a : α} (h : κ a ≪ η a) :
    η.withDensity (κ.rnDeriv η) a = κ a := by
  rw [Kernel.withDensity_apply]
  swap; · exact κ.measurable_rnDeriv _
  have h_ae := κ.rnDeriv_eq_rnDeriv_measure (η := η) (a := a)
  rw [MeasureTheory.withDensity_congr_ae h_ae, (κ a).withDensity_rnDeriv_eq _ h]

Похожие утверждения