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} [NormedCommRing 𝕜] {n : ℕ} {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)} [∀ (i : Fin n), SigmaFinite (μ i)] {f : (i : Fin n) → E i → 𝕜} (hf : ∀ (i : Fin n), Integrable (f i) (μ i)) : Integrable (fun (x : (i : Fin n) → E i) => ∏ i : Fin n, f i (x i)) (Measure.pi μ)

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} [NormedCommRing 𝕜] [Fintype ι] {E : ι → Type u_3} {f : (i : ι) → E i → 𝕜} {mE : (i : ι) → MeasurableSpace (E i)} {μ : (i : ι) → Measure (E i)} [∀ (i : ι), SigmaFinite (μ i)] (hf : ∀ (i : ι), Integrable (f i) (μ i)) : Integrable (fun (x : (i : ι) → E i) => ∏ i : ι, f i (x i)) (Measure.pi μ)

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} [NormedCommRing 𝕜] [Fintype ι] {E : Type u_3} {f : ι → E → 𝕜} {mE : MeasurableSpace E} {μ : ι → Measure E} [∀ (i : ι), SigmaFinite (μ i)] (hf : ∀ (i : ι), Integrable (f i) (μ i)) : Integrable (fun (x : ι → E) => ∏ i : ι, f i (x i)) (Measure.pi μ)

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} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)} [∀ (i : Fin n), SigmaFinite (μ i)] (f : (i : Fin n) → E i → 𝕜) : ∫ (x : (i : Fin n) → E i), ∏ i : Fin n, f i (x i) ∂Measure.pi μ = ∏ i : Fin n, ∫ (x : E i), f i x ∂μ i

A version of Fubini's theorem in n variables, for a natural number n.

theorem MeasureTheory.integral_fin_nat_prod_volume_eq_prod {𝕜 : Type u_1} [RCLike 𝕜] {n : ℕ} {E : Fin n → Type u_2} [(i : Fin n) → MeasureSpace (E i)] [∀ (i : Fin n), SigmaFinite 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} [RCLike 𝕜] (ι : Type u_2) [Fintype ι] {E : ι → Type u_3} (f : (i : ι) → E i → 𝕜) {mE : (i : ι) → MeasurableSpace (E i)} {μ : (i : ι) → Measure (E i)} [∀ (i : ι), SigmaFinite (μ i)] : ∫ (x : (i : ι) → E i), ∏ i : ι, f i (x i) ∂Measure.pi μ = ∏ i : ι, ∫ (x : E i), f i x ∂μ i

A version of Fubini's theorem with the variables indexed by a general finite type.

theorem MeasureTheory.integral_fintype_prod_volume_eq_prod {𝕜 : Type u_1} [RCLike 𝕜] (ι : Type u_2) [Fintype ι] {E : ι → Type u_3} (f : (i : ι) → E i → 𝕜) [(i : ι) → MeasureSpace (E i)] [∀ (i : ι), SigmaFinite 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} [RCLike 𝕜] {E : Type u_2} (ι : Type u_3) [Fintype ι] (f : E → 𝕜) {mE : MeasurableSpace E} {μ : Measure E} [SigmaFinite μ] : (∫ (x : ι → E), ∏ i : ι, f (x i) ∂Measure.pi fun (x : ι) => μ) = (∫ (x : E), f x ∂μ) ^ Fintype.card ι

theorem MeasureTheory.integral_fintype_prod_volume_eq_pow {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} (ι : Type u_3) [Fintype ι] (f : E → 𝕜) [MeasureSpace E] [SigmaFinite volume] : ∫ (x : ι → E), ∏ i : ι, f (x i) = (∫ (x : E), f x) ^ Fintype.card ι