fintype_prod — Mathlib

English

Let ι be finite and E_i, f_i, μ_i as above. Then the function x ↦ ∏_{i∈ι} f_i(x_i) is Integrable with respect to π μ.

Русский

Пусть ι конечен. Тогда функция x ↦ ∏_{i∈ι} f_i(x_i) интегрируема по мере произведения π μ.

LaTeX

$$$\\operatorname{Integrable}\\left( x \\mapsto \\prod_{i} f_i(x_i) \\right)\\left( \\operatorname{Measure.pi} \\mu \\right)$$$

Lean4

/-- On a finite product space, a product of integrable functions depending on each coordinate is
integrable. -/
theorem fintype_prod {E : Type*} {f : ι → E → 𝕜} {mE : MeasurableSpace E} {μ : ι → Measure E} [∀ i, SigmaFinite (μ i)]
    (hf : ∀ i, Integrable (f i) (μ i)) : Integrable (fun (x : ι → E) ↦ ∏ i, f i (x i)) (Measure.pi μ) :=
  Integrable.fintype_prod_dep hf

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