withDensity_apply' — Mathlib

English

If κ is finite, and f: α→γ→ℝ≥0∞ is such that κ.withDensity f is finite, then for measurable hf, and any a, the RN derivative satisfies (κ.withDensity f).rnDeriv κ a =ᵐ[κ a] f a.

Русский

Если κ конечное ядро и κ.withDensity f конечное, то при измеримой f выполняется (κ.withDensity f).rnDeriv κ a =ᵐ[κ a] f a.

LaTeX

$$(κ.withDensity f).rnDeriv κ a =ᵐ[κ a] f a$$

Lean4

protected theorem withDensity_apply' (κ : Kernel α β) [IsSFiniteKernel κ] (hf : Measurable (Function.uncurry f)) (a : α)
    (s : Set β) : withDensity κ f a s = ∫⁻ b in s, f a b ∂κ a := by
  rw [Kernel.withDensity_apply κ hf, withDensity_apply' _ s]

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