setLIntegral_rnDeriv — Mathlib

English

Assume κ, η are finite kernels α → γ and s is a measurable set. If κ a is absolutely continuous with respect to η a, then the RN-derivative integrates exactly to the κ-measure of s: ∫_s κ.rnDeriv η a = κ a(s).

Русский

Пусть κ, η — конечные ядра α → γ; s — измеримое множество. При условии κ a ≪ η a верно: ∫_s κ.rnDeriv η a = κ a(s).

LaTeX

$$$ \\int^{-}_{c \\in s} \\kappa.rnDeriv \\eta a c \\, \\partial \\eta a = \\kappa a s $$$

Lean4

theorem setLIntegral_rnDeriv {κ η : Kernel α γ} [IsFiniteKernel κ] [IsFiniteKernel η] {a : α} (h : κ a ≪ η a)
    {s : Set γ} (hs : MeasurableSet s) : ∫⁻ c in s, κ.rnDeriv η a c ∂η a = κ a s := by
  rw [setLIntegral_congr_fun_ae hs ((κ.rnDeriv_eq_rnDeriv_measure).mono (fun x hx _ ↦ hx)), ← withDensity_apply _ hs,
    (κ a).withDensity_rnDeriv_eq _ h]

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