Theorems · Definition · measure theory
MeasureTheory.Measure.pi
{ι : Type u_4} →
{α : ι → Type u_5} →
[Fintype ι] →
[inst : (i : ι) → MeasurableSpace (α i)] →
((i : ι) → MeasureTheory.Measure (α i)) → MeasureTheory.Measure ((i : ι) → α i)Measure.pi μ is the finite product of the measures {μ i | i : ι}.
It is defined to be measure corresponding to MeasureTheory.OuterMeasure.pi.
- Defined in
- Mathlib.MeasureTheory.Constructions.Pi
- Cited by
- 130 results in Mathlib
- Foundations
- Depth 193 from the axioms, rests on 4,730 definitions · uses propext, Classical.choice, Quot.sound
- Assumes
- FintypeMeasurableSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MeasurableSpacestatement · cited by 13,106
- MeasureTheory.Measurestatement · cited by 10,939
- Fintypestatement · cited by 7,736
Cited by136
Results whose statement or proof uses this declaration.
- MeasureTheory.Measure.pi_pistatement · cited by 31
- MeasureTheory.lmarginalproof · cited by 28
- MeasureTheory.Measure.pi_eqstatement · cited by 19
- ProbabilityTheory.stdGaussianproof · cited by 14
- MeasureTheory.Measure.ae_eq_set_pistatement · cited by 9
- MeasureTheory.volume_pistatement · cited by 7
- MeasureTheory.measurePreserving_piCongrLeftstatement and proof · cited by 7
- MeasureTheory.Measure.pi_of_emptystatement · cited by 6
- ProbabilityTheory.iIndepFun_iff_map_fun_eq_pi_mapstatement and proof · cited by 6
- MeasureTheory.piContent_cylinderstatement · cited by 5
- MeasureTheory.Measure.infinitePiNatproof · cited by 5
- MeasureTheory.Measure.infinitePi_map_restrictstatement · cited by 5