Documentation

Mathlib.MeasureTheory.Integral.Pi

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 nType 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.prod Finset.univ 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.prod Finset.univ 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.prod Finset.univ 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 nType 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} [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.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} [RCLike 𝕜] {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 ι