lintegral_kernel_prod_right'' — Mathlib

English

If f is measurable on α × β, then the function a ↦ ∫⁻ b, f(a,b) dη(a,b) is measurable.

Русский

Если f измеримо на α × β, то функция a ↦ ∫⁻ b f(a,b) dη(a,b) измерима.

LaTeX

$$$\\text{Measurable}\\bigl(a \\mapsto \\int⁻ b\\, f(a,b) \\, d\\eta(a,b)\\bigr)$$$

Lean4

@[fun_prop]
theorem _root_.Measurable.lintegral_kernel_prod_right'' {f : β × γ → ℝ≥0∞} (hf : Measurable f) :
    Measurable fun x => ∫⁻ y, f (x, y) ∂η (a, x) :=
  by
  change
    Measurable
      ((fun x => ∫⁻ y, (fun u : (α × β) × γ => f (u.1.2, u.2)) (x, y) ∂η x) ∘ fun x => (a, x))
        -- Porting note: specified `κ`, `f`.

  refine
    (Measurable.lintegral_kernel_prod_right' (κ := η) (f := (fun u ↦ f (u.fst.snd, u.snd))) ?_).comp
      measurable_prodMk_left
  fun_prop

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