Theorems · Definition · probability
MeasureTheory.inducedFamily
{X : ℕ → Type u_1} →
[inst : (n : ℕ) → MeasurableSpace (X n)] →
((n : ℕ) → MeasureTheory.Measure ((i : ↥(Finset.Iic n)) → X ↑i)) →
(S : Finset ℕ) → MeasureTheory.Measure ((k : ↥S) → X ↑k)Given a family of measures μ : (n : ℕ) → Measure (Π i : Iic n, X i), we can define a family
of measures indexed by Finset ℕ by projecting the measures.
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 196 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- MeasurableSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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
- MeasureTheory.Measure.mapproof · cited by 858
- Finset.supproof · cited by 530
- Finset.Iicstatement and proof · cited by 280
- Finset.restrict₂proof · cited by 44
Cited by5
Results whose statement or proof uses this declaration.
- ProbabilityTheory.Kernel.isProjectiveMeasureFamily_partialTrajstatement · cited by 5
- MeasureTheory.inducedFamily_Iicstatement · cited by 3
- ProbabilityTheory.Kernel.isProjectiveLimit_trajFunstatement and proof · cited by 2
- MeasureTheory.isProjectiveMeasureFamily_inducedFamilystatement · cited by 1
- ProbabilityTheory.Kernel.measurable_trajFunproof · cited by 0