Documentation Verification Report

IndepFun

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

Statistics

MetricCount
DefinitionsIndepFun, IndepFun, iIndepFun
3
Theoremscomp, 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
Total75

ProbabilityTheory

Definitions

NameCategoryTheorems
IndepFun 📖MathDef
76 mathmath: 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

NameCategoryTheorems
IndepFun 📖MathDef
47 mathmath: 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 mathmath: 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

NameKindAssumesProvesValidatesDepends On
iIndepFun_congr 📖mathematicalFilter.EventuallyEq
MeasureTheory.Measure
MeasureTheory.ae
MeasureTheory.Measure.instFunLike
MeasureTheory.Measure.instOuterMeasureClass
DFunLike.coe
ProbabilityTheory.Kernel
instFunLike
iIndepFun—MeasureTheory.Measure.instOuterMeasureClass
iIndep_congr
iIndepFun_congr' 📖mathematicalFilter.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 📖mathematicalFunction.BijectiveiIndepFun—iIndepFun.of_precomp
Function.Bijective.surjective
iIndepFun.precomp
Function.Bijective.injective
iIndepFun_zero_right 📖mathematical—iIndepFun
MeasureTheory.Measure
MeasureTheory.Measure.instZero
——
indepFun_congr 📖mathematicalFilter.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 📖mathematicalMeasurableIndepFun
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 📖mathematicalMeasurableIndepFun
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

NameKindAssumesProvesValidatesDepends 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 📖mathematicalProbabilityTheory.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 📖mathematicalProbabilityTheory.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 📖mathematicalProbabilityTheory.Kernel.IndepFunPi.instNeg—comp
MeasurableNeg.measurable_neg
measurable_id
neg_right 📖mathematicalProbabilityTheory.Kernel.IndepFunPi.instNeg—comp
measurable_id
MeasurableNeg.measurable_neg

ProbabilityTheory.Kernel.iIndepFun

Theorems

NameKindAssumesProvesValidatesDepends On
ae_isProbabilityMeasure 📖mathematicalProbabilityTheory.Kernel.iIndepFunFilter.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 📖mathematicalMeasurable
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 📖mathematicalProbabilityTheory.Kernel.iIndepFunProbabilityTheory.Kernel.iIndep
MeasurableSpace.comap
——
indepFun 📖mathematicalProbabilityTheory.Kernel.iIndepFunProbabilityTheory.Kernel.IndepFun—ProbabilityTheory.Kernel.iIndep.indep
indepFun_add_add 📖mathematicalProbabilityTheory.Kernel.iIndepFun
Measurable
ProbabilityTheory.Kernel.IndepFun
Pi.instAdd
—ProbabilityTheory.Kernel.IndepFun.comp
indepFun_prodMk_prodMk
MeasurableAdd₂.measurable_add
indepFun_add_left 📖mathematicalProbabilityTheory.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₀ 📖mathematicalProbabilityTheory.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₀ 📖mathematicalProbabilityTheory.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 📖mathematicalProbabilityTheory.Kernel.iIndepFun
Measurable
ProbabilityTheory.Kernel.IndepFun
Pi.instAdd
—ProbabilityTheory.Kernel.IndepFun.symm
indepFun_add_left
indepFun_add_right₀ 📖mathematicalProbabilityTheory.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 📖mathematicalProbabilityTheory.Kernel.iIndepFun
Measurable
ProbabilityTheory.Kernel.IndepFun
Pi.instDiv
—ProbabilityTheory.Kernel.IndepFun.comp
indepFun_prodMk_prodMk
MeasurableDiv₂.measurable_div
indepFun_div_div₀ 📖mathematicalProbabilityTheory.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 📖mathematicalProbabilityTheory.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₀ 📖mathematicalProbabilityTheory.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 📖mathematicalProbabilityTheory.Kernel.iIndepFun
Measurable
ProbabilityTheory.Kernel.IndepFun
Pi.instDiv
—ProbabilityTheory.Kernel.IndepFun.symm
indepFun_div_left
indepFun_div_right₀ 📖mathematicalProbabilityTheory.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 📖mathematicalDisjoint
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 📖mathematicalProbabilityTheory.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₀ 📖mathematicalProbabilityTheory.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 📖mathematicalProbabilityTheory.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₀ 📖mathematicalProbabilityTheory.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₀ 📖mathematicalDisjoint
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 📖mathematicalProbabilityTheory.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₀ 📖mathematicalProbabilityTheory.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 📖mathematicalProbabilityTheory.Kernel.iIndepFun
Measurable
ProbabilityTheory.Kernel.IndepFun
Pi.instMul
—ProbabilityTheory.Kernel.IndepFun.comp
indepFun_prodMk_prodMk
MeasurableMul₂.measurable_mul
indepFun_mul_mul₀ 📖mathematicalProbabilityTheory.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 📖mathematicalProbabilityTheory.Kernel.iIndepFun
Measurable
ProbabilityTheory.Kernel.IndepFun
Pi.instMul
—ProbabilityTheory.Kernel.IndepFun.symm
indepFun_mul_left
indepFun_mul_right₀ 📖mathematicalProbabilityTheory.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 📖mathematicalProbabilityTheory.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 📖mathematicalProbabilityTheory.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₀ 📖mathematicalProbabilityTheory.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₀ 📖mathematicalProbabilityTheory.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 📖mathematicalProbabilityTheory.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₀ 📖mathematicalProbabilityTheory.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₀ 📖mathematicalProbabilityTheory.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 📖mathematicalProbabilityTheory.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₀ 📖mathematicalProbabilityTheory.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 📖mathematicalProbabilityTheory.Kernel.iIndepFun
Measurable
ProbabilityTheory.Kernel.IndepFun
Pi.instSub
—ProbabilityTheory.Kernel.IndepFun.symm
indepFun_sub_left
indepFun_sub_right₀ 📖mathematicalProbabilityTheory.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 📖mathematicalProbabilityTheory.Kernel.iIndepFun
Measurable
ProbabilityTheory.Kernel.IndepFun
Pi.instSub
—ProbabilityTheory.Kernel.IndepFun.comp
indepFun_prodMk_prodMk
MeasurableSub₂.measurable_sub
indepFun_sum_range_succ 📖mathematicalProbabilityTheory.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₀ 📖mathematicalProbabilityTheory.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 📖mathematicalProbabilityTheory.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 📖mathematicalProbabilityTheory.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 📖mathematicalProbabilityTheory.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

NameKindAssumesProvesValidatesDepends On
iIndepFun_indicator 📖mathematicalProbabilityTheory.Kernel.iIndepSetProbabilityTheory.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