integral_fintype_prod_eq_pow — Mathlib

English

Let E be a space with a measure μ, and f: E → 𝕜. Then, for finite ι, the integral over the product equals the nth power of a single-integral: ∫_{ι→E} ∏ f(x_i) dπμ = (∫_E f dμ)^{card(ι)}.

Русский

Пусть E снабжено мерой μ, f: E → 𝕜. Тогда для конечного множества индексов ∫ по произведению функций равно (∫ f dμ)^{card(ι)}.

LaTeX

$$$$\\int x:ι\\to E,\\; \\prod_i f(x_i)\\,d(\\pi\\mu)=\\left(\\int_E f\,d\\mu\\right)^{\\mathrm{card}(ι)}$$$$

Lean4

theorem integral_fintype_prod_eq_pow {E : Type*} (f : E → 𝕜) {mE : MeasurableSpace E} {μ : Measure E} [SigmaFinite μ] :
    ∫ x : ι → E, ∏ i, f (x i) ∂(Measure.pi (fun _ ↦ μ)) = (∫ x, f x ∂μ) ^ (card ι) := by
  rw [integral_fintype_prod_eq_prod, Finset.prod_const, card]

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