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 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) => โˆ 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) => โˆ 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) => โˆ 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), โˆ 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 โ†’ ๐•œ) [(i : ฮน) โ†’ MeasureTheory.MeasureSpace (E 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} [RCLike ๐•œ] {E : Type u_2} (ฮน : Type u_3) [Fintype ฮน] (f : E โ†’ ๐•œ) [MeasureTheory.MeasureSpace E] [MeasureTheory.SigmaFinite MeasureTheory.volume] :
โˆซ (x : ฮน โ†’ E), โˆ i : ฮน, f (x i) = (โˆซ (x : E), f x) ^ Fintype.card ฮน