integral_indicator₂ — Mathlib

English

For a function f and a set s, the integral over y of s.indicator (f · y) at b equals s.indicator of the integral over y of f x y at b.

Русский

Для функции f и множества s интеграл по y от s.indicator(f · y) в точке b равен индикатору от интеграла по y функции x ↦ f(x, y) в точке b.

LaTeX

$$$\\int y\, s.indicator (f · y) b \\, d\\mu = s.indicator \\left( \\int y\, f_x(y) \\ d\\mu \\right) b$$$

Lean4

theorem integral_indicator₂ {β : Type*} (f : β → α → G) (s : Set β) (b : β) :
    ∫ y, s.indicator (f · y) b ∂μ = s.indicator (fun x ↦ ∫ y, f x y ∂μ) b := by by_cases hb : b ∈ s <;> simp [hb]

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