Integration with respect to a finite product of measures #
theorem
MeasureTheory.integral_fin_nat_prod_eq_prod
{𝕜 : Type u_1}
[IsROrC 𝕜]
{n : ℕ}
{E : Fin n → Type u_2}
[(i : Fin n) → MeasureTheory.MeasureSpace (E i)]
[∀ (i : Fin n), MeasureTheory.SigmaFinite MeasureTheory.volume]
(f : (i : Fin n) → E i → 𝕜)
:
(∫ (x : (i : Fin n) → E i), Finset.prod Finset.univ fun (i : Fin n) => f i (x i)) = Finset.prod Finset.univ fun (i : Fin n) => ∫ (x : E i), f i x
A version of Fubini's theorem in n variables, for a natural number n.
theorem
MeasureTheory.integral_fintype_prod_eq_prod
{𝕜 : Type u_1}
[IsROrC 𝕜]
(ι : Type u_2)
[Fintype ι]
{E : ι → Type u_3}
(f : (i : ι) → E i → 𝕜)
[(i : ι) → MeasureTheory.MeasureSpace (E i)]
[∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume]
:
(∫ (x : (i : ι) → E i), Finset.prod Finset.univ fun (i : ι) => f i (x i)) = Finset.prod Finset.univ fun (i : ι) => ∫ (x : E i), f i x
A version of Fubini's theorem with the variables indexed by a general finite type.
theorem
MeasureTheory.integral_fintype_prod_eq_pow
{𝕜 : Type u_1}
[IsROrC 𝕜]
{E : Type u_2}
(ι : Type u_3)
[Fintype ι]
(f : E → 𝕜)
[MeasureTheory.MeasureSpace E]
[MeasureTheory.SigmaFinite MeasureTheory.volume]
:
(∫ (x : ι → E), Finset.prod Finset.univ fun (i : ι) => f (x i)) = (∫ (x : E), f x) ^ Fintype.card ι