withDensity_apply — Mathlib

English

If f is measurable in uncurry form, then the value of withDensity κ f at a equals (κ a).withDensity (f a).

Русский

Если f измерима в виде uncurry, то для каждого a: (withDensity κ f) a = (κ a).withDensity (f a).

LaTeX

$$withDensity κ f a = (κ a).withDensity (f a)$$

Lean4

protected theorem withDensity_apply (κ : Kernel α β) [IsSFiniteKernel κ] (hf : Measurable (Function.uncurry f))
    (a : α) : withDensity κ f a = (κ a).withDensity (f a) := by
  classical
  rw [withDensity, dif_pos hf]
  rfl

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