MeasureTheory.integral_fintype_prod_eq_prod
theorem MeasureTheory.integral_fintype_prod_eq_prod :
∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (ι : Type u_2) [inst_1 : Fintype ι] {E : ι → Type u_3} (f : (i : ι) → E i → 𝕜)
[inst_2 : (i : ι) → MeasureTheory.MeasureSpace (E i)]
[inst_3 : ∀ (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
This theorem is a generalization of Fubini's theorem, applied to functions indexed by variables from a finite type. It states that for any Real or Complex number type 𝕜, any finite type ι, and any family of types E indexed by ι, if we have a function f from each E i to 𝕜, and each of the E i has a measure space structure such that the measure is sigma-finite, then the integral over all the E i's of the product of f i (x i) for all i in the finite set ι, is equal to the product over all i in the finite set ι of the integral over E i of f i x. In essence, this theorem allows us to interchange the order of integrals and finite products.
More concisely: If 𝕜 is a Real or Complex number type, ι is a finite type, and for each i in ι, E\_i has a sigma-finite measure space structure, then the integral over the product space ∏\_{i ∈ ι} E\_i of the function f(x) = ∏\_{i ∈ ι} f\_i(x\_i) equals the product of the integrals ∏\_{i ∈ ι} ∫\_{E\_i} f\_i(x\_i) dμ\_i, where dμ\_i denotes the measure on E\_i.
|
MeasureTheory.integral_fin_nat_prod_eq_prod
theorem MeasureTheory.integral_fin_nat_prod_eq_prod :
∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : ℕ} {E : Fin n → Type u_2}
[inst_1 : (i : Fin n) → MeasureTheory.MeasureSpace (E i)]
[inst_2 : ∀ (i : Fin n), MeasureTheory.SigmaFinite MeasureTheory.volume] (f : (i : Fin n) → E i → 𝕜),
(∫ (x : (i : Fin n) → E i), Finset.univ.prod fun i => f i (x i)) = Finset.univ.prod fun i => ∫ (x : E i), f i x
This theorem is a version of Fubini's theorem for multiple variables, specifically for a finite natural number `n`. It states that for any type `𝕜` which is a Real Complete Lattice (RCLike), any natural number `n`, and any family of types `E` indexed by `Fin n`, given that each `E i` is a measure space and also sigma-finite with respect to the volume measure, for any function `f` from `E i` to `𝕜`, the integral of the product of `f i (x i)` over all `i` in the universal finite set is equal to the product of the integral of `f i x` over all `i` in the universal finite set.
More concisely: For any Real Complete Lattice 𝕜, given a finite number n and a family {E i | i ∈ Fin n} of σ-finite measure spaces with respect to volume measure, if for each f : E i → 𝕜, the function integrable over i, then ∫∏i=1n f i(xi) dV = ∏i=1n ∫idi f i(xi) dVi.
|