integral_deterministic' — Mathlib

English

If g is measurable, then the integral of a deterministic kernel equals the value of f at g a.

Русский

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

LaTeX

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

Lean4

theorem integral_deterministic' (hg : Measurable g) (hf : StronglyMeasurable f) :
    ∫ x, f x ∂deterministic g hg a = f (g a) := by rw [deterministic_apply, integral_dirac' _ _ hf]

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