Theorems · Theorem · measure theory

MeasureTheory.Integrable.fin_nat_prod

∀ {𝕜 : Type u_1} [inst : NormedCommRing 𝕜] {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 → 𝕜},
  (∀ (i : Fin n), MeasureTheory.Integrable (f i) (μ i)) →
    MeasureTheory.Integrable (fun x => ∏ i, f i (x i)) (MeasureTheory.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.

Defined in

Mathlib.MeasureTheory.Integral.Pi

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedCommRingMeasureTheory.SigmaFinite