integral_fintype_prod_volume_eq_pow

English

Same pow equality as above but in the finite-index-volume setting: the product of volumes yields the nth power of the integral.

Русский

Та же равенство степени для объема: произведение объемов равно n-ой степени интеграла.

LaTeX

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

Lean4

theorem integral_fintype_prod_volume_eq_pow {E : Type*} (f : E → 𝕜) [MeasureSpace E]
    [SigmaFinite (volume : Measure E)] : ∫ x : ι → E, ∏ i, f (x i) = (∫ x, f x) ^ (card ι) :=
  integral_fintype_prod_eq_pow _

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