Theorems · Theorem · measure theory

MeasureTheory.Integrable.fintype_prod_dep

∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : Fintype ι] [inst_1 : NormedCommRing 𝕜] {E : ι → Type u_3}
  {f : (i : ι) → E i → 𝕜} {mE : (i : ι) → MeasurableSpace (E i)} {μ : (i : ι) → MeasureTheory.Measure (E i)}
  [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)],
  (∀ (i : ι), MeasureTheory.Integrable (f i) (μ i)) →
    MeasureTheory.Integrable (fun x => ∏ i, f i (x i)) (MeasureTheory.Measure.pi μ)

On a finite product space, a product of integrable functions depending on each coordinate is integrable. Version with dependent target.

Defined in

Mathlib.MeasureTheory.Integral.Pi

Cited by

1 results in Mathlib

Foundations

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

Assumes

FintypeNormedCommRingMeasureTheory.SigmaFinite