English
Let κ, η be finite kernels from α to γ and s a measurable subset of γ. For each a ∈ α, the integral over s of the Radon–Nikodym derivative of κ with respect to η at a is bounded above by the η-measure of s under κ a; i.e. the total density on s does not exceed κ a (s).
Русский
Пусть κ, η — конечные ядра α → γ; пусть s ⊆ γ — измеримое множество. Для каждого a ∈ α выполняется неравенство: ∫_s rnDeriv(κ, η; a)(c) dη(a)(c) ≤ κ(a)(s).
LaTeX
$$$ \\int^{-}_{c \\in s} \\kappa.rnDeriv \\eta a c \\, \\partial \\eta a \\le \\kappa a s $$$
Lean4
theorem setLIntegral_rnDeriv_le {κ η : Kernel α γ} [IsFiniteKernel κ] [IsFiniteKernel η] {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' _ s]
exact (κ a).withDensity_rnDeriv_le _ _
