lintegral_compProd — Mathlib

English

The lintegral over the compProd equals the iterated lintegral with curry/uncurry transformation, for measurable f.

Русский

Лебегов интеграл над compProd равен повторному интегралу после преобразования карри/ункури для измеримой f.

LaTeX

$$$$ \int bc f(b,c) \; d(κ ⊗ₖ η)(a) = \int b \int c f(b,c) \; dη(a,b) \; dκ(a). $$$$

Lean4

/-- Lebesgue integral against the composition-product of two kernels. -/
theorem lintegral_compProd (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel (α × β) γ) [IsSFiniteKernel η] (a : α)
    {f : β × γ → ℝ≥0∞} (hf : Measurable f) : ∫⁻ bc, f bc ∂(κ ⊗ₖ η) a = ∫⁻ b, ∫⁻ c, f (b, c) ∂η (a, b) ∂κ a :=
  by
  let g := Function.curry f
  change ∫⁻ bc, f bc ∂(κ ⊗ₖ η) a = ∫⁻ b, ∫⁻ c, g b c ∂η (a, b) ∂κ a
  rw [← lintegral_compProd']
  · simp_rw [g, Function.curry_apply]
  · simp_rw [g, Function.uncurry_curry]; exact hf

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