integral_prod_mul — Mathlib

English

Given E,F,G normed, L a continuous linear map, and integrable components, L is integrable on μ×ν.

Русский

Пусть E,F,G – нормированные пространства, L – непрерывное линейное отображение, и соответствующие компоненты интегрируемы; тогда L интегрируемо по μ×ν.

LaTeX

$$$$\\text{Integrable } L \\text{ on } μ×ν \\Rightarrow \\text{Integrable } L \\text{ on } μ×ν.$$$$

Lean4

theorem integral_prod_mul {L : Type*} [RCLike L] (f : α → L) (g : β → L) :
    ∫ z, f z.1 * g z.2 ∂μ.prod ν = (∫ x, f x ∂μ) * ∫ y, g y ∂ν :=
  integral_prod_smul f g

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