integrable_inner — Mathlib

English

The function a ↦ ⟪f(a), g(a)⟫ is integrable with respect to μ.

Русский

Функция a ↦ ⟪f(a), g(a)⟫ интегрируема по μ.

LaTeX

$$$\\text{Integrable}(a \\mapsto ⟪f(a), g(a)⟫)\\quad(μ)$$$

Lean4

theorem integrable_inner (f g : α →₂[μ] E) : Integrable (fun x : α => ⟪f x, g x⟫) μ :=
  (integrable_congr
        (AEEqFun.coeFn_mk (fun x => ⟪f x, g x⟫) ((Lp.aestronglyMeasurable f).inner (Lp.aestronglyMeasurable g)))).mp
    (AEEqFun.integrable_iff_mem_L1.mpr (mem_L1_inner f g))

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