integral_indicator₂ — Mathlib

English

For any f: α→β→E and set s ⊆ α, the integral of s.indicator(f·) over κ a equals the indicator of s at a times the inner integral.

Русский

Для любой f: α→β→E и множества s ⊆ α выполняется: интеграл от s.indicator(f·) по κ равен s.indicator(∫ f) в точке a.

LaTeX

$$$\\int y, s.indicator (f \\cdot y) a \\, dκ a = s.indicator \\left( a \\mapsto \\int y, f a y \\, dκ a \\right)$$$

Lean4

theorem integral_indicator₂ (f : α → β → E) (s : Set α) (a : α) :
    ∫ y, s.indicator (f · y) a ∂κ a = s.indicator (fun x ↦ ∫ y, f x y ∂κ x) a := by by_cases ha : a ∈ s <;> simp [ha]

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