# Integration with respect to a finite product of measures #

On a finite product of measure spaces, we show that a product of integrable functions each depending on a single coordinate is integrable, in MeasureTheory.integrable_fintype_prod, and that its integral is the product of the individual integrals, in MeasureTheory.integral_fintype_prod_eq_prod.

theorem MeasureTheory.Integrable.fin_nat_prod {𝕜 : Type u_1} [] {n : } {E : Fin nType u_2} [(i : Fin n) → ] [∀ (i : Fin n), MeasureTheory.SigmaFinite MeasureTheory.volume] {f : (i : Fin n) → E i𝕜} (hf : ∀ (i : Fin n), MeasureTheory.Integrable (f i) MeasureTheory.volume) :
MeasureTheory.Integrable (fun (x : (i : Fin n) → E i) => i : Fin n, f i (x i)) MeasureTheory.volume

On a finite product space in n variables, for a natural number n, a product of integrable functions depending on each coordinate is integrable.

theorem MeasureTheory.Integrable.fintype_prod_dep {𝕜 : Type u_1} [] {ι : Type u_2} [] {E : ιType u_3} {f : (i : ι) → E i𝕜} [(i : ι) → ] [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume] (hf : ∀ (i : ι), MeasureTheory.Integrable (f i) MeasureTheory.volume) :
MeasureTheory.Integrable (fun (x : (i : ι) → E i) => i : ι, f i (x i)) MeasureTheory.volume

On a finite product space, a product of integrable functions depending on each coordinate is integrable. Version with dependent target.

theorem MeasureTheory.Integrable.fintype_prod {𝕜 : Type u_1} [] {ι : Type u_2} [] {E : Type u_3} {f : ιE𝕜} [MeasureTheory.SigmaFinite MeasureTheory.volume] (hf : ∀ (i : ι), MeasureTheory.Integrable (f i) MeasureTheory.volume) :
MeasureTheory.Integrable (fun (x : ιE) => i : ι, f i (x i)) MeasureTheory.volume

On a finite product space, a product of integrable functions depending on each coordinate is integrable.

theorem MeasureTheory.integral_fin_nat_prod_eq_prod {𝕜 : Type u_1} [] {n : } {E : Fin nType u_2} [(i : Fin n) → ] [∀ (i : Fin n), MeasureTheory.SigmaFinite MeasureTheory.volume] (f : (i : Fin n) → E i𝕜) :
∫ (x : (i : Fin n) → E i), i : Fin n, f i (x i) = 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} [] (ι : Type u_2) [] {E : ιType u_3} (f : (i : ι) → E i𝕜) [(i : ι) → ] [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume] :
∫ (x : (i : ι) → E i), i : ι, f i (x i) = 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} [] {E : Type u_2} (ι : Type u_3) [] (f : E𝕜) [MeasureTheory.SigmaFinite MeasureTheory.volume] :
∫ (x : ιE), i : ι, f (x i) = (∫ (x : E), f x) ^