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} [RCLike 𝕜] {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 → 𝕜} (hf : ∀ (i : Fin n), MeasureTheory.Integrable (f i) MeasureTheory.volume) : MeasureTheory.Integrable (fun (x : (i : Fin n) → E i) => Finset.univ.prod fun (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} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] {E : ι → Type u_3} {f : (i : ι) → E i → 𝕜} [(i : ι) → MeasureTheory.MeasureSpace (E i)] [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume] (hf : ∀ (i : ι), MeasureTheory.Integrable (f i) MeasureTheory.volume) : MeasureTheory.Integrable (fun (x : (i : ι) → E i) => Finset.univ.prod fun (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} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] {E : Type u_3} {f : ι → E → 𝕜} [MeasureTheory.MeasureSpace E] [MeasureTheory.SigmaFinite MeasureTheory.volume] (hf : ∀ (i : ι), MeasureTheory.Integrable (f i) MeasureTheory.volume) : MeasureTheory.Integrable (fun (x : ι → E) => Finset.univ.prod fun (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} [RCLike 𝕜] {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.univ.prod fun (i : Fin n) => f i (x i)) = Finset.univ.prod 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} [RCLike 𝕜] (ι : 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.univ.prod fun (i : ι) => f i (x i)) = Finset.univ.prod 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} [RCLike 𝕜] {E : Type u_2} (ι : Type u_3) [Fintype ι] (f : E → 𝕜) [MeasureTheory.MeasureSpace E] [MeasureTheory.SigmaFinite MeasureTheory.volume] : (∫ (x : ι → E), Finset.univ.prod fun (i : ι) => f (x i)) = (∫ (x : E), f x) ^ Fintype.card ι