lintegral_rnDeriv — Mathlib

English

Let κ, η be finite kernels α → γ with κ a ≪ η a for each a ∈ α. Then the integral of κ.rnDeriv η a over all γ with respect to η a equals the total mass κ a(univ): ∫ κ.rnDeriv η a dη a = κ a(univ).

Русский

Пусть κ, η — конечные ядра α → γ и ∀ a, κ a ≪ η a. Тогда ∫ κ.rnDeriv η a dη a = κ a(γ).

LaTeX

$$$ \\int^- c, \\kappa.rnDeriv \\eta a c \\partial \\eta a = \\kappa a(\\mathrm{univ}) $$$

Lean4

theorem lintegral_rnDeriv {κ η : Kernel α γ} [IsFiniteKernel κ] [IsFiniteKernel η] {a : α} (h : κ a ≪ η a) :
    ∫⁻ c, κ.rnDeriv η a c ∂η a = κ a univ := by rw [← setLIntegral_univ, setLIntegral_rnDeriv h MeasurableSet.univ]

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