IndepFun

📁 Source: Mathlib/Probability/Independence/Kernel/IndepFun.lean

Statistics

Metric	Count
Definitions IndepFun, IndepFun, iIndepFun	3
Theorems comp, comp₀, congr', meas_inter, measure_inter_preimage_eq_mul, neg_left, neg_right, ae_isProbabilityMeasure, comp, comp₀, cond_iInter, congr', iIndep, indepFun, indepFun_add_add, indepFun_add_left, indepFun_add_left₀, indepFun_add_mul₀, indepFun_add_right, indepFun_add_right₀, indepFun_div_div, indepFun_div_div₀, indepFun_div_left, indepFun_div_left₀, indepFun_div_right, indepFun_div_right₀, indepFun_finset, indepFun_finset_prod_of_notMem, indepFun_finset_prod_of_notMem₀, indepFun_finset_sum_of_notMem, indepFun_finset_sum_of_notMem₀, indepFun_finset₀, indepFun_mul_left, indepFun_mul_left₀, indepFun_mul_mul, indepFun_mul_mul₀, indepFun_mul_right, indepFun_mul_right₀, indepFun_prodMk, indepFun_prodMk_prodMk, indepFun_prodMk_prodMk₀, indepFun_prodMk₀, indepFun_prod_range_succ, indepFun_prod_range_succ₀, indepFun_sub_div₀, indepFun_sub_left, indepFun_sub_left₀, indepFun_sub_right, indepFun_sub_right₀, indepFun_sub_sub, indepFun_sum_range_succ, indepFun_sum_range_succ₀, meas_biInter, meas_iInter, measure_inter_preimage_eq_mul, of_precomp, of_subsingleton, precomp, iIndepFun_congr, iIndepFun_congr', iIndepFun_iff_measure_inter_preimage_eq_mul, iIndepFun_precomp_of_bijective, iIndepFun_zero_right, iIndepFun_indicator, indepFun_congr, indepFun_const_left, indepFun_const_right, indepFun_iff_compProd_map_prod_eq_compProd_prod_map_map, indepFun_iff_indepSet_preimage, indepFun_iff_measure_inter_preimage_eq_mul, indepFun_zero_left, indepFun_zero_right	72
Total	75

ProbabilityTheory

Definitions

Name	Category	Theorems
IndepFun 📖	MathDef	76 math math: indepFun_process_of_bcf, indepFun_prod, iIndepFun.indepFun_div_right, pi_indepFun_pi_of_prod_bcf, indicator_indepFun_pi_of_prod_bcf, iIndepFun.indepFun_finset_prod_of_notMem₀, iIndepFun.indepFun_add_left₀, IndepFun_iff_Indep, HasGaussianLaw.indepFun_of_covariance_strongDual, iIndepFun.indepFun_sum_range_succ₀, iIndepFun.indepFun_sub_left, iIndepFun.indepFun_prod_range_succ₀, iIndepFun.indepFun_div_left, iIndepFun.indepFun_mul_right₀, iIndepFun.indepFun_div_left₀, iIndepFun.indepFun_mul_right, indepFun_of_bcf, HasGaussianLaw.indepFun_of_covariance_eq_zero, process_indepFun_process_of_bcf, iIndepFun.indepFun_mul_mul, indicator_indepFun_pi_of_bcf, iIndepFun.indepFun_sum_range_succ, indicator_indepFun_process_of_bcf, indepFun_pi_of_bcf, iIndepFun.indepFun_div_div₀, indepFun_iff_charFunDual_prod', iIndepFun.indepFun_prod_range_succ, iIndepFun.indepFun_finset_sum_of_notMem, indepFun_iff_charFun_prod, process_indepFun_process_of_prod_bcf, pi_indepFun_pi_of_bcf, process_indepFun_of_prod_bcf, iIndepFun.indepFun_div_div, HasGaussianLaw.indepFun_of_covariance_eval, iIndepFun.indepFun_sub_div₀, MeasureTheory.pdf.indepFun_iff_pdf_prod_eq_pdf_mul_pdf, iIndepFun.indepFun_add_add, iIndepFun.indepFun_prodMk, iIndepFun.indepFun_mul_left₀, iIndepFun.indepFun_add_mul₀, pi_indepFun_of_prod_bcf, iIndepFun.indepFun_add_right₀, process_indepFun_of_bcf, iIndepFun.indepFun_add_left, indepFun_pi_of_prod_bcf, pi_indepFun_of_bcf, indepFun_const_left, iIndepFun.indepFun_sub_right, HasGaussianLaw.indepFun_of_covariance_inner, indepFun_process_of_prod_bcf, iIndepFun.indepFun_mul_left, indicator_indepFun_of_bcf, indepFun_iff_measure_inter_preimage_eq_mul, iIndepFun.indepFun_div_right₀, iIndepFun.indepFun_sub_left₀, iIndepFun.indepFun_prodMk_prodMk, indepFun_const_right, iIndepFun.indepFun_prodMk_prodMk₀, iIndepFun.indepFun, indepFun_iff_indepSet_preimage, IndepFun_iff, iIndepFun.indepFun_mul_mul₀, indepFun_iff_map_prod_eq_prod_map_map', indicator_indepFun_process_of_prod_bcf, iIndepFun.indepFun_finset_sum_of_notMem₀, indepFun_iff_integral_comp_mul, indepFun_iff_map_prod_eq_prod_map_map, indepFun_prod₀, iIndepFun.indepFun_sub_sub, iIndepFun.indepFun_add_right, iIndepFun.indepFun_sub_right₀, iIndepFun.indepFun_finset₀, iIndepFun.indepFun_finset_prod_of_notMem, iIndepFun.indepFun_prodMk₀, iIndepFun.indepFun_finset, indepFun_iff_charFunDual_prod

ProbabilityTheory.Kernel

Definitions

Name	Category	Theorems
IndepFun 📖	MathDef	47 math math: iIndepFun.indepFun_div_right, iIndepFun.indepFun_prod_range_succ₀, iIndepFun.indepFun_div_div₀, iIndepFun.indepFun_mul_mul, iIndepFun.indepFun_add_add, iIndepFun.indepFun_prodMk_prodMk, indepFun_congr, iIndepFun.indepFun_add_right₀, iIndepFun.indepFun_add_left₀, iIndepFun.indepFun_mul_mul₀, iIndepFun.indepFun_sub_right₀, iIndepFun.indepFun_prodMk₀, iIndepFun.indepFun_finset_sum_of_notMem₀, iIndepFun.indepFun_add_left, indepFun_iff_measure_inter_preimage_eq_mul, iIndepFun.indepFun_sum_range_succ, iIndepFun.indepFun_prodMk_prodMk₀, iIndepFun.indepFun_div_div, iIndepFun.indepFun_div_right₀, iIndepFun.indepFun_sub_left, iIndepFun.indepFun_sub_left₀, indepFun_const_left, iIndepFun.indepFun_mul_left, iIndepFun.indepFun_prod_range_succ, iIndepFun.indepFun_sub_div₀, iIndepFun.indepFun_finset_sum_of_notMem, iIndepFun.indepFun_sub_right, iIndepFun.indepFun_mul_left₀, iIndepFun.indepFun_finset_prod_of_notMem₀, iIndepFun.indepFun_sum_range_succ₀, iIndepFun.indepFun_mul_right, indepFun_zero_left, indepFun_iff_compProd_map_prod_eq_compProd_prod_map_map, iIndepFun.indepFun_finset, iIndepFun.indepFun_div_left, iIndepFun.indepFun, indepFun_zero_right, iIndepFun.indepFun_mul_right₀, iIndepFun.indepFun_add_right, iIndepFun.indepFun_finset₀, iIndepFun.indepFun_div_left₀, indepFun_iff_indepSet_preimage, iIndepFun.indepFun_prodMk, iIndepFun.indepFun_sub_sub, iIndepFun.indepFun_finset_prod_of_notMem, iIndepFun.indepFun_add_mul₀, indepFun_const_right
iIndepFun 📖	MathDef	7 math math: iIndepFun.of_subsingleton, iIndepFun_congr, iIndepFun_zero_right, iIndepFun_precomp_of_bijective, iIndepSet.iIndepFun_indicator, iIndepFun_congr', iIndepFun_iff_measure_inter_preimage_eq_mul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iIndepFun_congr 📖	mathematical	Filter.EventuallyEq MeasureTheory.Measure MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel instFunLike	iIndepFun	—	MeasureTheory.Measure.instOuterMeasureClass iIndep_congr
iIndepFun_congr' 📖	mathematical	Filter.Eventually Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel instFunLike	iIndepFun	—	MeasureTheory.Measure.instOuterMeasureClass iIndepFun.congr' Filter.mp_mem Filter.univ_mem' Filter.EventuallyEq.symm
iIndepFun_iff_measure_inter_preimage_eq_mul 📖	mathematical	—	iIndepFun Filter.Eventually ENNReal DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike Set.iInter Finset Finset.instMembership Set.preimage Finset.prod CommSemiring.toCommMonoid ENNReal.instCommSemiring MeasureTheory.ae MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass Set.iInter_congr_Prop Finset.prod_congr
iIndepFun_precomp_of_bijective 📖	mathematical	Function.Bijective	iIndepFun	—	iIndepFun.of_precomp Function.Bijective.surjective iIndepFun.precomp Function.Bijective.injective
iIndepFun_zero_right 📖	mathematical	—	iIndepFun MeasureTheory.Measure MeasureTheory.Measure.instZero	—	—
indepFun_congr 📖	mathematical	Filter.EventuallyEq MeasureTheory.Measure MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel instFunLike	IndepFun	—	MeasureTheory.Measure.instOuterMeasureClass indep_congr
indepFun_const_left 📖	mathematical	—	IndepFun	—	IndepFun.eq_1 MeasurableSpace.comap_const indep_bot_left
indepFun_const_right 📖	mathematical	—	IndepFun	—	IndepFun.symm indepFun_const_left
indepFun_iff_compProd_map_prod_eq_compProd_prod_map_map 📖	mathematical	Measurable	IndepFun MeasureTheory.Measure.compProd Prod.instMeasurableSpace map prod	—	MeasureTheory.Measure.instOuterMeasureClass indepFun_iff_measure_inter_preimage_eq_mul MeasureTheory.Measure.ext_prod₃_iff MeasureTheory.Measure.instIsFiniteMeasureProdCompProdOfIsFiniteKernel IsFiniteKernel.map MeasureTheory.Measure.compProd_apply MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite IsSFiniteKernel.map IsFiniteKernel.isSFiniteKernel MeasurableSet.prod IsSFiniteKernel.prod MeasureTheory.lintegral_congr_ae Set.ext Filter.mp_mem Filter.univ_mem' map_apply Measurable.prodMk MeasureTheory.Measure.map_apply Set.mk_preimage_prod prod_apply_prod map_apply' MeasureTheory.measure_empty MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite measurable_coe MeasurableSet.inter Measurable.mul ENNReal.instMeasurableMul₂ MeasureTheory.Measure.compProd_apply_prod
indepFun_iff_indepSet_preimage 📖	mathematical	Measurable	IndepFun IndepSet Set.preimage	—	MeasureTheory.Measure.instOuterMeasureClass indepFun_iff_measure_inter_preimage_eq_mul indepSet_iff_measure_inter_eq_mul
indepFun_iff_measure_inter_preimage_eq_mul 📖	mathematical	—	IndepFun Filter.Eventually ENNReal DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike Set.instInter Set.preimage Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring MeasureTheory.ae MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass
indepFun_zero_left 📖	mathematical	—	IndepFun ProbabilityTheory.Kernel instZero	—	—
indepFun_zero_right 📖	mathematical	—	IndepFun MeasureTheory.Measure MeasureTheory.Measure.instZero	—	—

ProbabilityTheory.Kernel.IndepFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	—	ProbabilityTheory.Kernel.IndepFun Measurable	—	—	MeasureTheory.Measure.instOuterMeasureClass Set.preimage_comp
comp₀ 📖	—	ProbabilityTheory.Kernel.IndepFun AEMeasurable MeasureTheory.Measure.bind DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike MeasureTheory.Measure.map	—	—	comp MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_of_ae_map congr' Filter.mp_mem MeasureTheory.Measure.ae_ae_of_ae_comp Filter.univ_mem'
congr' 📖	—	ProbabilityTheory.Kernel.IndepFun Filter.Eventually Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instFunLike	—	—	MeasureTheory.Measure.instOuterMeasureClass Filter.mp_mem Filter.univ_mem' Filter.EventuallyEq.fun_comp MeasureTheory.measure_congr Filter.EventuallyEq.inter
meas_inter 📖	mathematical	ProbabilityTheory.Kernel.IndepFun MeasurableSet MeasurableSpace.comap	Filter.Eventually ENNReal DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instFunLike Set.instInter Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring MeasureTheory.ae MeasureTheory.Measure.instOuterMeasureClass	—	—
measure_inter_preimage_eq_mul 📖	mathematical	ProbabilityTheory.Kernel.IndepFun MeasurableSet	Filter.Eventually ENNReal DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instFunLike Set.instInter Set.preimage Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring MeasureTheory.ae MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.Kernel.indepFun_iff_measure_inter_preimage_eq_mul
neg_left 📖	mathematical	ProbabilityTheory.Kernel.IndepFun	Pi.instNeg	—	comp MeasurableNeg.measurable_neg measurable_id
neg_right 📖	mathematical	ProbabilityTheory.Kernel.IndepFun	Pi.instNeg	—	comp measurable_id MeasurableNeg.measurable_neg

ProbabilityTheory.Kernel.iIndepFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_isProbabilityMeasure 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun	Filter.Eventually MeasureTheory.IsProbabilityMeasure DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	ProbabilityTheory.Kernel.iIndep.ae_isProbabilityMeasure iIndep
comp 📖	—	ProbabilityTheory.Kernel.iIndepFun Measurable	—	—	MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.Kernel.iIndepFun_iff_measure_inter_preimage_eq_mul Filter.mp_mem Filter.univ_mem' Set.iInter_congr_Prop Finset.prod_congr
comp₀ 📖	—	ProbabilityTheory.Kernel.iIndepFun AEMeasurable MeasureTheory.Measure.bind DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike MeasureTheory.Measure.map	—	—	comp MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_of_ae_map Filter.EventuallyEq.symm congr' MeasureTheory.Measure.ae_ae_of_ae_comp
cond_iInter 📖	mathematical	Measurable ProbabilityTheory.Kernel.iIndepFun Prod.instMeasurableSpace MeasurableSet MeasurableSpace.comap Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	ENNReal DFunLike.coe Set ProbabilityTheory.cond ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instFunLike Set.iInter Set.preimage Finset Finset.instMembership Finset.prod CommSemiring.toCommMonoid ENNReal.instCommSemiring	—	MeasureTheory.Measure.instOuterMeasureClass nonempty_fintype MeasurableSet.prod MeasurableSet.univ Set.ext MeasurableSet.inter Filter.mp_mem meas_iInter ae_isProbabilityMeasure Filter.univ_mem' ProbabilityTheory.cond_apply MeasurableSet.iInter Finite.to_countable Set.iInter_ite Set.iInter_univ Set.inter_univ Set.iInter_inter_distrib Set.iInter_congr Finset.prod_mul_distrib ENNReal.prod_inv_distrib MeasureTheory.measure_ne_top MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure Finset.prod_congr ENNReal.inv_mul_cancel Finset.prod_ite_mem Finset.univ_inter
congr' 📖	—	ProbabilityTheory.Kernel.iIndepFun Filter.Eventually Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instFunLike	—	—	MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.Kernel.iIndepFun_iff_measure_inter_preimage_eq_mul MeasureTheory.ae_ball_iff Finset.countable_toSet Filter.mp_mem Filter.univ_mem' MeasureTheory.measure_congr Finset.prod_congr
iIndep 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun	ProbabilityTheory.Kernel.iIndep MeasurableSpace.comap	—	—
indepFun 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun	ProbabilityTheory.Kernel.IndepFun	—	ProbabilityTheory.Kernel.iIndep.indep
indepFun_add_add 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun Measurable	ProbabilityTheory.Kernel.IndepFun Pi.instAdd	—	ProbabilityTheory.Kernel.IndepFun.comp indepFun_prodMk_prodMk MeasurableAdd₂.measurable_add
indepFun_add_left 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun Measurable	ProbabilityTheory.Kernel.IndepFun Pi.instAdd	—	indepFun_prodMk CompTriple.comp_eq CompTriple.instId_comp CompTriple.instIsIdId ProbabilityTheory.Kernel.IndepFun.comp Measurable.add measurable_fst measurable_snd measurable_id
indepFun_add_left₀ 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun AEMeasurable MeasureTheory.Measure.bind DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	ProbabilityTheory.Kernel.IndepFun Pi.instAdd	—	indepFun_prodMk₀ CompTriple.comp_eq CompTriple.instId_comp CompTriple.instIsIdId ProbabilityTheory.Kernel.IndepFun.comp Measurable.add measurable_fst measurable_snd measurable_id
indepFun_add_mul₀ 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun AEMeasurable MeasureTheory.Measure.bind DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	ProbabilityTheory.Kernel.IndepFun Pi.instAdd	—	ProbabilityTheory.Kernel.IndepFun.comp indepFun_prodMk_prodMk₀ MeasurableAdd₂.measurable_add
indepFun_add_right 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun Measurable	ProbabilityTheory.Kernel.IndepFun Pi.instAdd	—	ProbabilityTheory.Kernel.IndepFun.symm indepFun_add_left
indepFun_add_right₀ 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun AEMeasurable MeasureTheory.Measure.bind DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	ProbabilityTheory.Kernel.IndepFun Pi.instAdd	—	ProbabilityTheory.Kernel.IndepFun.symm indepFun_add_left₀
indepFun_div_div 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun Measurable	ProbabilityTheory.Kernel.IndepFun Pi.instDiv	—	ProbabilityTheory.Kernel.IndepFun.comp indepFun_prodMk_prodMk MeasurableDiv₂.measurable_div
indepFun_div_div₀ 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun AEMeasurable MeasureTheory.Measure.bind DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	ProbabilityTheory.Kernel.IndepFun Pi.instDiv	—	ProbabilityTheory.Kernel.IndepFun.comp indepFun_prodMk_prodMk₀ MeasurableDiv₂.measurable_div
indepFun_div_left 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun Measurable	ProbabilityTheory.Kernel.IndepFun Pi.instDiv	—	indepFun_prodMk CompTriple.comp_eq CompTriple.instId_comp CompTriple.instIsIdId ProbabilityTheory.Kernel.IndepFun.comp Measurable.div measurable_fst measurable_snd measurable_id
indepFun_div_left₀ 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun AEMeasurable MeasureTheory.Measure.bind DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	ProbabilityTheory.Kernel.IndepFun Pi.instDiv	—	indepFun_prodMk₀ CompTriple.comp_eq CompTriple.instId_comp CompTriple.instIsIdId ProbabilityTheory.Kernel.IndepFun.comp Measurable.div measurable_fst measurable_snd measurable_id
indepFun_div_right 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun Measurable	ProbabilityTheory.Kernel.IndepFun Pi.instDiv	—	ProbabilityTheory.Kernel.IndepFun.symm indepFun_div_left
indepFun_div_right₀ 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun AEMeasurable MeasureTheory.Measure.bind DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	ProbabilityTheory.Kernel.IndepFun Pi.instDiv	—	ProbabilityTheory.Kernel.IndepFun.symm indepFun_div_left₀
indepFun_finset 📖	mathematical	Disjoint Finset Finset.partialOrder Finset.instOrderBot ProbabilityTheory.Kernel.iIndepFun Measurable	ProbabilityTheory.Kernel.IndepFun MeasurableSpace.pi SetLike.instMembership Finset.instSetLike	—	eq_or_ne MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.Kernel.exists_ae_eq_isMarkovKernel ae_isProbabilityMeasure ProbabilityTheory.Kernel.IndepFun.congr Filter.EventuallyEq.symm IsPiSystem.comap isPiSystem_pi generateFrom_pi Finite.of_fintype MeasurableSpace.comap_generateFrom ProbabilityTheory.Kernel.IndepSets.indep ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel Measurable.comap_le measurable_pi_iff Finset.disjoint_right Finset.disjoint_left Set.ext congr Finset.mem_union Set.inter_univ Set.univ_inter Filter.mp_mem ProbabilityTheory.Kernel.iIndepFun_iff_measure_inter_preimage_eq_mul Filter.univ_mem' Finset.prod_union Finset.prod_congr
indepFun_finset_prod_of_notMem 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun Measurable Finset Finset.instMembership	ProbabilityTheory.Kernel.IndepFun Finset.prod Pi.commMonoid	—	Finset.mem_singleton_self measurable_pi_apply Finset.prod_congr Finset.prod_apply Finset.prod_coe_sort Finset.measurable_fun_prod ProbabilityTheory.Kernel.IndepFun.comp indepFun_finset Disjoint.symm Finset.disjoint_singleton_left
indepFun_finset_prod_of_notMem₀ 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun AEMeasurable MeasureTheory.Measure.bind DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike Finset Finset.instMembership	ProbabilityTheory.Kernel.IndepFun Finset.prod Pi.commMonoid	—	indepFun_finset_prod_of_notMem congr' MeasureTheory.Measure.ae_ae_of_ae_comp ProbabilityTheory.Kernel.IndepFun.congr' MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_all_iff Finite.to_countable Finite.of_fintype Filter.mp_mem Filter.univ_mem' Finset.prod_apply Finset.prod_congr Filter.EventuallyEq.symm
indepFun_finset_sum_of_notMem 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun Measurable Finset Finset.instMembership	ProbabilityTheory.Kernel.IndepFun Finset.sum Pi.addCommMonoid	—	Finset.mem_singleton_self measurable_pi_apply Finset.sum_congr Finset.sum_apply Finset.sum_coe_sort Finset.measurable_fun_sum ProbabilityTheory.Kernel.IndepFun.comp indepFun_finset Disjoint.symm Finset.disjoint_singleton_left
indepFun_finset_sum_of_notMem₀ 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun AEMeasurable MeasureTheory.Measure.bind DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike Finset Finset.instMembership	ProbabilityTheory.Kernel.IndepFun Finset.sum Pi.addCommMonoid	—	indepFun_finset_sum_of_notMem congr' MeasureTheory.Measure.ae_ae_of_ae_comp ProbabilityTheory.Kernel.IndepFun.congr' MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_all_iff Finite.to_countable Finite.of_fintype Filter.mp_mem Filter.univ_mem' Finset.sum_apply Finset.sum_congr Filter.EventuallyEq.symm
indepFun_finset₀ 📖	mathematical	Disjoint Finset Finset.partialOrder Finset.instOrderBot ProbabilityTheory.Kernel.iIndepFun AEMeasurable MeasureTheory.Measure.bind DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	ProbabilityTheory.Kernel.IndepFun MeasurableSpace.pi SetLike.instMembership Finset.instSetLike	—	indepFun_finset congr' MeasureTheory.Measure.ae_ae_of_ae_comp ProbabilityTheory.Kernel.IndepFun.congr' MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_all_iff Finite.to_countable Finite.of_fintype Filter.mp_mem Filter.univ_mem'
indepFun_mul_left 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun Measurable	ProbabilityTheory.Kernel.IndepFun Pi.instMul	—	indepFun_prodMk CompTriple.comp_eq CompTriple.instId_comp CompTriple.instIsIdId ProbabilityTheory.Kernel.IndepFun.comp Measurable.mul measurable_fst measurable_snd measurable_id
indepFun_mul_left₀ 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun AEMeasurable MeasureTheory.Measure.bind DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	ProbabilityTheory.Kernel.IndepFun Pi.instMul	—	indepFun_prodMk₀ CompTriple.comp_eq CompTriple.instId_comp CompTriple.instIsIdId ProbabilityTheory.Kernel.IndepFun.comp Measurable.mul measurable_fst measurable_snd measurable_id
indepFun_mul_mul 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun Measurable	ProbabilityTheory.Kernel.IndepFun Pi.instMul	—	ProbabilityTheory.Kernel.IndepFun.comp indepFun_prodMk_prodMk MeasurableMul₂.measurable_mul
indepFun_mul_mul₀ 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun AEMeasurable MeasureTheory.Measure.bind DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	ProbabilityTheory.Kernel.IndepFun Pi.instMul	—	ProbabilityTheory.Kernel.IndepFun.comp indepFun_prodMk_prodMk₀ MeasurableMul₂.measurable_mul
indepFun_mul_right 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun Measurable	ProbabilityTheory.Kernel.IndepFun Pi.instMul	—	ProbabilityTheory.Kernel.IndepFun.symm indepFun_mul_left
indepFun_mul_right₀ 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun AEMeasurable MeasureTheory.Measure.bind DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	ProbabilityTheory.Kernel.IndepFun Pi.instMul	—	ProbabilityTheory.Kernel.IndepFun.symm indepFun_mul_left₀
indepFun_prodMk 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun Measurable	ProbabilityTheory.Kernel.IndepFun Prod.instMeasurableSpace	—	Finset.mem_singleton_self measurable_pi_apply Finset.mem_insert_self Finset.mem_insert_of_mem Measurable.prod ProbabilityTheory.Kernel.IndepFun.comp indepFun_finset Finset.disjoint_singleton_right
indepFun_prodMk_prodMk 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun Measurable	ProbabilityTheory.Kernel.IndepFun Prod.instMeasurableSpace	—	Finset.mem_insert_self Finset.mem_insert_of_mem Finset.mem_singleton_self Measurable.prodMk measurable_pi_apply ProbabilityTheory.Kernel.IndepFun.comp indepFun_finset
indepFun_prodMk_prodMk₀ 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun AEMeasurable MeasureTheory.Measure.bind DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	ProbabilityTheory.Kernel.IndepFun Prod.instMeasurableSpace	—	indepFun_prodMk_prodMk congr' MeasureTheory.Measure.ae_ae_of_ae_comp ProbabilityTheory.Kernel.IndepFun.congr' Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass Filter.univ_mem'
indepFun_prodMk₀ 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun AEMeasurable MeasureTheory.Measure.bind DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	ProbabilityTheory.Kernel.IndepFun Prod.instMeasurableSpace	—	indepFun_prodMk congr' MeasureTheory.Measure.ae_ae_of_ae_comp ProbabilityTheory.Kernel.IndepFun.congr' Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass Filter.univ_mem' Filter.EventuallyEq.symm
indepFun_prod_range_succ 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun Measurable	ProbabilityTheory.Kernel.IndepFun Finset.prod Pi.commMonoid Finset.range	—	indepFun_finset_prod_of_notMem Finset.notMem_range_self
indepFun_prod_range_succ₀ 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun AEMeasurable MeasureTheory.Measure.bind DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	ProbabilityTheory.Kernel.IndepFun Finset.prod Pi.commMonoid Finset.range	—	indepFun_finset_prod_of_notMem₀ Finset.notMem_range_self
indepFun_sub_div₀ 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun AEMeasurable MeasureTheory.Measure.bind DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	ProbabilityTheory.Kernel.IndepFun Pi.instSub	—	ProbabilityTheory.Kernel.IndepFun.comp indepFun_prodMk_prodMk₀ MeasurableSub₂.measurable_sub
indepFun_sub_left 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun Measurable	ProbabilityTheory.Kernel.IndepFun Pi.instSub	—	indepFun_prodMk CompTriple.comp_eq CompTriple.instId_comp CompTriple.instIsIdId ProbabilityTheory.Kernel.IndepFun.comp Measurable.sub measurable_fst measurable_snd measurable_id
indepFun_sub_left₀ 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun AEMeasurable MeasureTheory.Measure.bind DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	ProbabilityTheory.Kernel.IndepFun Pi.instSub	—	indepFun_prodMk₀ CompTriple.comp_eq CompTriple.instId_comp CompTriple.instIsIdId ProbabilityTheory.Kernel.IndepFun.comp Measurable.sub measurable_fst measurable_snd measurable_id
indepFun_sub_right 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun Measurable	ProbabilityTheory.Kernel.IndepFun Pi.instSub	—	ProbabilityTheory.Kernel.IndepFun.symm indepFun_sub_left
indepFun_sub_right₀ 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun AEMeasurable MeasureTheory.Measure.bind DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	ProbabilityTheory.Kernel.IndepFun Pi.instSub	—	ProbabilityTheory.Kernel.IndepFun.symm indepFun_sub_left₀
indepFun_sub_sub 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun Measurable	ProbabilityTheory.Kernel.IndepFun Pi.instSub	—	ProbabilityTheory.Kernel.IndepFun.comp indepFun_prodMk_prodMk MeasurableSub₂.measurable_sub
indepFun_sum_range_succ 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun Measurable	ProbabilityTheory.Kernel.IndepFun Finset.sum Pi.addCommMonoid Finset.range	—	indepFun_finset_sum_of_notMem Finset.notMem_range_self
indepFun_sum_range_succ₀ 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun AEMeasurable MeasureTheory.Measure.bind DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	ProbabilityTheory.Kernel.IndepFun Finset.sum Pi.addCommMonoid Finset.range	—	indepFun_finset_sum_of_notMem₀ Finset.notMem_range_self
meas_biInter 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun MeasurableSet MeasurableSpace.comap	Filter.Eventually ENNReal DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instFunLike Set.iInter Finset Finset.instMembership Finset.prod CommSemiring.toCommMonoid ENNReal.instCommSemiring MeasureTheory.ae MeasureTheory.Measure.instOuterMeasureClass	—	ProbabilityTheory.Kernel.iIndep.meas_biInter iIndep
meas_iInter 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun MeasurableSet MeasurableSpace.comap	Filter.Eventually ENNReal DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instFunLike Set.iInter Finset.prod CommSemiring.toCommMonoid ENNReal.instCommSemiring Finset.univ MeasureTheory.ae MeasureTheory.Measure.instOuterMeasureClass	—	ProbabilityTheory.Kernel.iIndep.meas_iInter iIndep
measure_inter_preimage_eq_mul 📖	mathematical	ProbabilityTheory.Kernel.iIndepFun MeasurableSet	Filter.Eventually ENNReal DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instFunLike Set.iInter Finset Finset.instMembership Set.preimage Finset.prod CommSemiring.toCommMonoid ENNReal.instCommSemiring MeasureTheory.ae MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.Kernel.iIndepFun_iff_measure_inter_preimage_eq_mul
of_precomp 📖	—	ProbabilityTheory.Kernel.iIndepFun	—	—	ProbabilityTheory.Kernel.iIndep.of_precomp
of_subsingleton 📖	mathematical	—	ProbabilityTheory.Kernel.iIndepFun	—	—
precomp 📖	—	ProbabilityTheory.Kernel.iIndepFun	—	—	ProbabilityTheory.Kernel.iIndep.precomp

ProbabilityTheory.Kernel.iIndepSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iIndepFun_indicator 📖	mathematical	ProbabilityTheory.Kernel.iIndepSet	ProbabilityTheory.Kernel.iIndepFun Set.indicator	—	MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.Kernel.iIndepFun_iff_measure_inter_preimage_eq_mul Set.iInter_congr_Prop Set.indicator_const_preimage_eq_union Finset.prod_congr MeasurableSpace.measurableSet_generateFrom Set.mem_singleton MeasurableSet.union MeasurableSet.ite' MeasurableSet.empty MeasurableSet.compl

---

← Back to Index