setIntegral_deterministic — Mathlib

English

For a measurable g, the set-restricted deterministic integral equals the integral over the restricted set of the kernel at a.

Русский

Для измеримого g интегралdeterministic по ограниченному множеству равен интегралу по ограниченному множеству ядра в a.

LaTeX

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

Lean4

@[simp]
theorem setIntegral_deterministic [MeasurableSingletonClass β] (hg : Measurable g) (s : Set β) [Decidable (g a ∈ s)] :
    ∫ x in s, f x ∂deterministic g hg a = if g a ∈ s then f (g a) else 0 := by
  rw [deterministic_apply, setIntegral_dirac f _ s]

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