Theorems · Theorem · measure theory

Finset.aemeasurable_fun_prod

∀ {M : Type u_2} {ι : Type u_3} {α : Type u_4} [inst : CommMonoid M] [inst_1 : MeasurableSpace M] [MeasurableMul₂ M]
  {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ι → α → M} (s : Finset ι),
  (∀ i ∈ s, AEMeasurable (f i) μ) → AEMeasurable (fun a => ∏ i ∈ s, f i a) μ

Defined in: Mathlib.MeasureTheory.Group.Arithmetic
Cited by: 1 results in Mathlib
Foundations: Depth 179 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommMonoid MeasurableSpace MeasurableMul₂

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Finsetstatement and proof · cited by 13,712
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
Finset.prodstatement · cited by 2,356
CommMonoidstatement and proof · cited by 2,264
AEMeasurablestatement and proof · cited by 840
MeasurableMul₂statement and proof · cited by 139
Finset.aemeasurable_prodproof · cited by 3

Cited by1

Results whose statement or proof uses this declaration.

ENNReal.lintegral_prod_norm_pow_leproof · cited by 1