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} [Fintype ι] [NormedCommRing 𝕜] {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} [Fintype ι] [NormedCommRing 𝕜] {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_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 → 𝕜) : ∫ (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_3} [(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} {ι : Type u_2} [Fintype ι] [RCLike 𝕜] {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} {ι : Type u_2} [Fintype ι] [RCLike 𝕜] {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} {ι : Type u_2} [Fintype ι] [RCLike 𝕜] {E : Type u_3} (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} {ι : Type u_2} [Fintype ι] [RCLike 𝕜] {E : Type u_3} (f : E → 𝕜) [MeasureSpace E] [SigmaFinite volume] : ∫ (x : ι → E), ∏ i : ι, f (x i) = (∫ (x : E), f x) ^ Fintype.card ι

theorem MeasureTheory.integrable_comp_eval {ι : Type u_2} [Fintype ι] {X : ι → Type u_3} {mX : (i : ι) → MeasurableSpace (X i)} {μ : (i : ι) → Measure (X i)} {E : Type u_4} [NormedAddCommGroup E] [∀ (i : ι), IsFiniteMeasure (μ i)] {i : ι} {f : X i → E} (hf : Integrable f (μ i)) : Integrable (fun (x : (i : ι) → X i) => f (x i)) (Measure.pi μ)

theorem MeasureTheory.integrable_eval {ι : Type u_2} [Fintype ι] {X : ι → Type u_3} {mX : (i : ι) → MeasurableSpace (X i)} {μ : (i : ι) → Measure (X i)} [(i : ι) → NormedAddCommGroup (X i)] [∀ (i : ι), IsFiniteMeasure (μ i)] {i : ι} (h : Integrable id (μ i)) : Integrable (fun (x : (i : ι) → X i) => x i) (Measure.pi μ)

theorem MeasureTheory.integral_comp_eval {ι : Type u_2} [Fintype ι] {X : ι → Type u_3} {mX : (i : ι) → MeasurableSpace (X i)} {μ : (i : ι) → Measure (X i)} {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [∀ (i : ι), IsProbabilityMeasure (μ i)] {i : ι} {f : X i → E} (hf : AEStronglyMeasurable f (μ i)) : ∫ (x : (i : ι) → X i), f (x i) ∂Measure.pi μ = ∫ (x : X i), f x ∂μ i

theorem MeasureTheory.integral_eval {ι : Type u_2} [Fintype ι] {X : ι → Type u_3} {mX : (i : ι) → MeasurableSpace (X i)} {μ : (i : ι) → Measure (X i)} [(i : ι) → NormedAddCommGroup (X i)] [(i : ι) → NormedSpace ℝ (X i)] [∀ (i : ι), IsProbabilityMeasure (μ i)] {i : ι} [OpensMeasurableSpace (X i)] [SecondCountableTopology (X i)] : ∫ (x : (i : ι) → X i), x i ∂Measure.pi μ = ∫ (x : X i), x ∂μ i