integral_deterministic — Mathlib

English

If g is measurable, the integral with respect to deterministic g equals the value f at g a.

Русский

Если g измеримо, то интеграл по детерминированному ядру равен f(g(a)).

LaTeX

$$$\\int x \\, f(x) \\, d\\deterministic(g)(a) = f(g(a))$$$

Lean4

@[simp]
theorem integral_deterministic [MeasurableSingletonClass β] (hg : Measurable g) :
    ∫ x, f x ∂deterministic g hg a = f (g a) := by rw [deterministic_apply, integral_dirac _ (g a)]

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