mul_prod — Mathlib

English

If f and g are integrable with respect to μ and ν respectively, then the pointwise product z ↦ f(z1) · g(z2) is integrable with respect to μ×ν.

Русский

Если f и g интегрируемы по μ и ν, тогда z ↦ f(z1)·g(z2) интегрируемо по μ×ν.

LaTeX

$$$\mathrm{Integrable}(f, μ) \land \mathrm{Integrable}(g, ν) \Rightarrow \mathrm{Integrable}(z \mapsto f(z_1) \cdot g(z_2), μ×ν)$$$

Lean4

theorem mul_prod {L : Type*} [NormedRing L] {f : α → L} {g : β → L} (hf : Integrable f μ) (hg : Integrable g ν) :
    Integrable (fun z : α × β => f z.1 * g z.2) (μ.prod ν) :=
  hf.smul_prod hg

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