Theorems · Theorem · measure theory

MeasureTheory.integral_fin_nat_prod_eq_prod

∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : ℕ} {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)}
  {μ : (i : Fin n) → MeasureTheory.Measure (E i)} [∀ (i : Fin n), MeasureTheory.SigmaFinite (μ i)]
  (f : (i : Fin n) → E i → 𝕜),
  ∫ (x : (i : Fin n) → E i), ∏ i, f i (x i) ∂MeasureTheory.Measure.pi μ = ∏ i, ∫ (x : E i), f i x ∂μ i

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

Defined in

Mathlib.MeasureTheory.Integral.Pi

Cited by

2 results in Mathlib

Foundations

Depth 267 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeMeasureTheory.SigmaFinite