integral_integral_indicator — Mathlib

English

Let κ be a kernel, μ a measure on X, f: X→Y→E, and s⊆X measurable. Then the iterated integral of s.indicator (f · y) equals the integral over s of the inner integral: ∫∫ s.indicator (f( x, y)) dκ x dμ(x) dy = ∫_{x∈s} ∫ f(x, y) dκ x dμ(x).

Русский

Пусть κ — ядро, μ — мера на X, f: X→Y→E, s — измеримое подмножество X. Тогда двойной интеграл с индикатором равен интегралу по s от внутреннего интеграла: ...

LaTeX

$$$ \\int x, \\int y, s.indicator (f · y) x \\, dκ x \, dμ x = \\int x \\in s, \\int y, f x y \\ dκ x \\, dμ x $$$

Lean4

theorem integral_integral_indicator (μ : Measure X) (f : X → Y → E) {s : Set X} (hs : MeasurableSet s) :
    ∫ x, ∫ y, s.indicator (f · y) x ∂κ x ∂μ = ∫ x in s, ∫ y, f x y ∂κ x ∂μ := by
  simp_rw [← integral_indicator hs, Kernel.integral_indicator₂]

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