setIntegral_deterministic' — Mathlib

English

Restricting the deterministic integral to a set s yields the indicator of membership of g a in s times f(g a).

Русский

Ограничение детерминированного интеграла на множество s даёт индикатор принадлежности g(a) множеству s, умноженный на f(g(a)).

LaTeX

$$$\\int x \\ in s \\, f(x) \\, d\\deterministic(g)(a) = \\mathbb{1}_{s}(g(a)) f(g(a))$$$

Lean4

theorem setIntegral_deterministic' (hg : Measurable g) (hf : StronglyMeasurable f) {s : Set β} (hs : MeasurableSet s)
    [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' hf _ hs]

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