setLIntegral_deterministic — Mathlib

English

General deterministic set integral formula with indicator: ∫⁻ x in s, f x ∂deterministic g hg a = if g a ∈ s then f(g a) else 0.

Русский

Обобщенная формула детерминированного интеграла по множеству: если g(a)∈s, то интеграл равен f(g(a)), иначе 0.

LaTeX

$$$\int^{\! in\;s} f x \partial\deterministic g hg a = if g a \in s then f(g a) else 0$$$

Lean4

@[simp]
theorem setLIntegral_deterministic {f : β → ℝ≥0∞} {g : α → β} {a : α} (hg : Measurable g) [MeasurableSingletonClass β]
    (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, setLIntegral_dirac f s]

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