English
Let ι be a finite index set. For each i in ι, let E_i be a measure space and f_i: E_i → 𝕜 be integrable with respect to μ_i. Then the function on the product space (Π_i E_i) defined by x ↦ ∏_{i∈ι} f_i(x_i) is integrable with respect to the product measure π μ.
Русский
Пусть ι — конечный индексный набор. Пусть для каждого i в ι имеется измеримое пространство E_i и функции f_i: E_i → 𝕜 интегрируемые относительно μ_i. Тогда функция на произведении пространств (Π_i E_i), заданная 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. Version with dependent target. -/
theorem fintype_prod_dep {E : ι → Type*} {f : (i : ι) → E i → 𝕜} {mE : ∀ i, MeasurableSpace (E i)}
{μ : (i : ι) → Measure (E i)} [∀ i, SigmaFinite (μ i)] (hf : ∀ i, Integrable (f i) (μ i)) :
Integrable (fun (x : (i : ι) → E i) ↦ ∏ i, f i (x i)) (Measure.pi μ) :=
by
let e := (equivFin ι).symm
simp_rw [← (measurePreserving_piCongrLeft _ e).integrable_comp_emb (MeasurableEquiv.measurableEmbedding _), ←
e.prod_comp, MeasurableEquiv.coe_piCongrLeft, Function.comp_def, Equiv.piCongrLeft_apply_apply]
exact .fin_nat_prod (fun i ↦ hf _)
