InfinitePi

📁 Source: Mathlib/Probability/Independence/InfinitePi.lean

Statistics

Metric	Count
Definitions	0
Theorems iIndepFun_iff_map_fun_eq_infinitePi_map, iIndepFun_iff_map_fun_eq_infinitePi_map₀, iIndepFun_iff_map_fun_eq_infinitePi_map₀', iIndepFun_infinitePi, iIndepFun_uncurry, iIndepFun_uncurry', iIndepFun_uncurry_infinitePi, iIndepFun_uncurry_infinitePi'	8
Total	8

ProbabilityTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iIndepFun_iff_map_fun_eq_infinitePi_map 📖	mathematical	Measurable	iIndepFun MeasureTheory.Measure.map MeasurableSpace.pi MeasureTheory.Measure.infinitePi	—	iIndepFun_iff_map_fun_eq_infinitePi_map₀ Measurable.aemeasurable measurable_pi_iff
iIndepFun_iff_map_fun_eq_infinitePi_map₀ 📖	mathematical	AEMeasurable MeasurableSpace.pi	iIndepFun MeasureTheory.Measure.map MeasureTheory.Measure.infinitePi	—	MeasureTheory.Measure.isProbabilityMeasure_map AEMeasurable.eval MeasureTheory.Measure.eq_infinitePi Set.ext MeasureTheory.Measure.map_apply Finset.measurable_restrict MeasurableSet.univ_pi Finite.to_countable Finite.of_fintype AEMeasurable.map_map_of_aemeasurable Measurable.aemeasurable iIndepFun_iff_map_fun_eq_pi_map iIndepFun_iff_finset MeasureTheory.Measure.pi_pi MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.Measure.isFiniteMeasure_map MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure Finset.prod_congr Finset.prod_coe_sort MeasureTheory.Measure.infinitePi_map_restrict
iIndepFun_iff_map_fun_eq_infinitePi_map₀' 📖	mathematical	AEMeasurable	iIndepFun MeasureTheory.Measure.map MeasurableSpace.pi MeasureTheory.Measure.infinitePi	—	iIndepFun_iff_map_fun_eq_infinitePi_map₀ aemeasurable_pi_iff
iIndepFun_infinitePi 📖	mathematical	MeasureTheory.IsProbabilityMeasure Measurable	iIndepFun MeasurableSpace.pi MeasureTheory.Measure.infinitePi	—	iIndepFun_iff_map_fun_eq_infinitePi_map MeasureTheory.Measure.instIsProbabilityMeasureForallInfinitePi Measurable.fun_comp measurable_pi_apply MeasureTheory.Measure.infinitePi_map_pi MeasureTheory.Measure.infinitePi_map_eval MeasureTheory.Measure.map_map
iIndepFun_uncurry 📖	—	Measurable iIndepFun MeasurableSpace.pi	—	—	iIndepFun.isProbabilityMeasure MeasureTheory.Measure.isProbabilityMeasure_map Measurable.aemeasurable measurable_pi_lambda iIndepFun_iff_map_fun_eq_infinitePi_map MeasurableEquiv.map_measurableEquiv_injective MeasureTheory.Measure.map_map MeasurableEquiv.measurable MeasureTheory.Measure.infinitePi_map_piCurry
iIndepFun_uncurry' 📖	—	Measurable iIndepFun MeasurableSpace.pi	—	—	iIndepFun.of_precomp Equiv.surjective iIndepFun_uncurry
iIndepFun_uncurry_infinitePi 📖	mathematical	MeasureTheory.IsProbabilityMeasure Measurable	iIndepFun MeasurableSpace.pi MeasureTheory.Measure.infinitePi	—	iIndepFun_uncurry Measurable.fun_comp measurable_pi_apply iIndepFun_infinitePi MeasureTheory.Measure.instIsProbabilityMeasureForallInfinitePi measurable_pi_lambda iIndepFun_iff_map_fun_eq_infinitePi_map MeasureTheory.Measure.map_map MeasureTheory.Measure.infinitePi_map_pi MeasureTheory.Measure.infinitePi_map_eval MeasureTheory.Measure.isProbabilityMeasure_map Measurable.aemeasurable
iIndepFun_uncurry_infinitePi' 📖	mathematical	MeasureTheory.IsProbabilityMeasure Measurable	iIndepFun MeasurableSpace.pi MeasureTheory.Measure.infinitePi	—	iIndepFun.of_precomp Equiv.surjective iIndepFun_uncurry_infinitePi

---

← Back to Index