Prod

📁 Source: Mathlib/MeasureTheory/Measure/Prod.lean

Statistics

Metric	Count
Definitions `prod`, `fst`, `prod`, `measureSpace`, `snd`	5
Theorems `comp_fst`, `comp_snd`, `lintegral_prod_left`, `lintegral_prod_left'`, `lintegral_prod_right`, `lintegral_prod_right'`, `prod_swap`, `prod`, `lintegral_prod_left`, `lintegral_prod_left'`, `lintegral_prod_right`, `lintegral_prod_right'`, `map_prodMk_left`, `map_prodMk_right`, `prod`, `prod`, `volume_prod`, `add_prod`, `ae_ae_comm`, `ae_ae_eq_curry_of_prod`, `ae_ae_eq_of_ae_eq_uncurry`, `ae_ae_of_ae_prod`, `ae_measure_lt_top`, `ae_prod_iff_ae_ae`, `ae_prod_mem_iff_ae_ae_mem`, `dirac_prod`, `dirac_prod_dirac`, `ext_prod`, `ext_prod_iff`, `ext_prod₃`, `ext_prod₃'`, `ext_prod₃_iff`, `ext_prod₃_iff'`, `instIsFiniteMeasure`, `instIsProbabilityMeasure`, `instIsZeroOrProbabilityMeasure`, `fst_add`, `fst_apply`, `fst_map_prodMk`, `fst_map_prodMk₀`, `fst_map_swap`, `fst_mono`, `fst_prod`, `fst_sum`, `fst_univ`, `fst_zero`, `instIsFiniteMeasureOnCompactsProdVolume`, `instIsFiniteMeasureProdVolume`, `instIsLocallyFiniteMeasureProdVolume`, `instIsOpenPosMeasureProdVolumeOfSFinite`, `instIsProbabilityMeasureProdVolume`, `instSFiniteFstOfProd`, `instSFiniteProdVolume`, `instSFiniteSndOfProd`, `instSigmaFiniteProdVolume`, `map_fst_prod`, `map_prod_map`, `map_snd_prod`, `measurePreserving_swap`, `measure_ae_null_of_prod_null`, `measure_prod_compl_eq_zero`, `measure_prod_null`, `measure_prod_null_of_ae_null`, `nullMeasurableSet_preimage_fst`, `nullMeasurableSet_preimage_snd`, `nullMeasurableSet_prod`, `nullMeasurableSet_prod_of_ne_zero`, `nullMeasurable_comp_fst`, `nullMeasurable_comp_snd`, `instIsFiniteMeasure`, `instIsFiniteMeasureOnCompacts`, `instIsLocallyFiniteMeasure`, `instIsOpenPosMeasure`, `instIsProbabilityMeasure`, `instNoAtoms_fst`, `instNoAtoms_snd`, `instSFinite`, `instSigmaFinite`, `prodAssoc_prod`, `prod_add`, `prod_apply`, `prod_apply_le`, `prod_apply_symm`, `prod_def`, `prod_dirac`, `prod_eq`, `prod_eq_generateFrom`, `prod_prod`, `prod_prod_le`, `prod_restrict`, `prod_smul_left`, `prod_sum`, `prod_sum_left`, `prod_sum_right`, `prod_swap`, `prod_zero`, `quasiMeasurePreserving_fst`, `quasiMeasurePreserving_snd`, `restrict_prod_eq_prod_univ`, `set_prod_ae_eq`, `instIsFiniteMeasure`, `instIsProbabilityMeasure`, `instIsZeroOrProbabilityMeasure`, `snd_add`, `snd_apply`, `snd_map_prodMk`, `snd_map_prodMk₀`, `snd_map_swap`, `snd_mono`, `snd_prod`, `snd_sum`, `snd_univ`, `snd_zero`, `volume_eq_prod`, `zero_prod`, `prod`, `skew_product`, `comp_fst`, `comp_snd`, `left_of_prod`, `of_preimage_fst`, `of_preimage_snd`, `prod`, `right_of_prod`, `fst`, `prodMap`, `prod_of_left`, `prod_of_right`, `snd`, `lintegral_lintegral`, `lintegral_lintegral_swap`, `lintegral_lintegral_symm`, `lintegral_prod`, `lintegral_prod_le`, `lintegral_prod_mul`, `lintegral_prod_swap`, `lintegral_prod_symm`, `lintegral_prod_symm'`, `measurePreserving_fst`, `measurePreserving_prodAssoc`, `measurePreserving_snd`, `measureReal_prod_prod`, `setLIntegral_prod`, `setLIntegral_prod_symm`, `volume_preserving_prodAssoc`, `measurable_measure_prodMk_left`, `measurable_measure_prodMk_left_finite`, `measurable_measure_prodMk_right`	148
Total	153

AEMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_fst` 📖	mathematical	`AEMeasurable`	`Prod.instMeasurableSpace` `MeasureTheory.Measure.prod`	—	`comp_quasiMeasurePreserving` `MeasureTheory.Measure.quasiMeasurePreserving_fst`
`comp_snd` 📖	mathematical	`AEMeasurable`	`Prod.instMeasurableSpace` `MeasureTheory.Measure.prod`	—	`comp_quasiMeasurePreserving` `MeasureTheory.Measure.quasiMeasurePreserving_snd`
`lintegral_prod_left` 📖	mathematical	`AEMeasurable` `ENNReal` `ENNReal.measurableSpace` `Prod.instMeasurableSpace` `MeasureTheory.Measure.prod`	`MeasureTheory.lintegral`	—	`lintegral_prod_left'`
`lintegral_prod_left'` 📖	mathematical	`AEMeasurable` `ENNReal` `ENNReal.measurableSpace` `Prod.instMeasurableSpace` `MeasureTheory.Measure.prod`	`MeasureTheory.lintegral`	—	`lintegral_prod_right'` `prod_swap`
`lintegral_prod_right` 📖	mathematical	`AEMeasurable` `ENNReal` `ENNReal.measurableSpace` `Prod.instMeasurableSpace` `MeasureTheory.Measure.prod`	`MeasureTheory.lintegral`	—	`lintegral_prod_right'`
`lintegral_prod_right'` 📖	mathematical	`AEMeasurable` `ENNReal` `ENNReal.measurableSpace` `Prod.instMeasurableSpace` `MeasureTheory.Measure.prod`	`MeasureTheory.lintegral`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Measurable.lintegral_prod_left` `Measurable.fun_comp` `Measurable.prodMk` `Measurable.snd` `measurable_id'` `Measurable.fst` `Filter.Eventually.mono` `MeasureTheory.Measure.ae_ae_of_ae_prod` `MeasureTheory.lintegral_congr_ae`
`prod_swap` 📖	—	`AEMeasurable` `Prod.instMeasurableSpace` `MeasureTheory.Measure.prod`	—	—	`comp_measurable` `MeasureTheory.Measure.prod_swap` `measurable_swap`

IsUnifLocDoublingMeasure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod` 📖	mathematical	—	`IsUnifLocDoublingMeasure` `Prod.pseudoMetricSpaceMax` `Prod.instMeasurableSpace` `MeasureTheory.Measure.prod`	—	`Nat.instAtLeastTwoHAddOfNat` `Filter.mp_mem` `eventually_measure_le_doublingConstant_mul` `Filter.univ_mem'` `closedBall_prod_same` `MeasureTheory.Measure.prod_prod` `le_imp_le_of_le_of_le` `mul_le_mul_left` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `le_refl` `mul_le_mul_right` `ENNReal.coe_mul` `mul_mul_mul_comm`

Measurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lintegral_prod_left` 📖	mathematical	`Measurable` `ENNReal` `Prod.instMeasurableSpace` `ENNReal.measurableSpace`	`MeasureTheory.lintegral`	—	`lintegral_prod_left'`
`lintegral_prod_left'` 📖	mathematical	`Measurable` `ENNReal` `Prod.instMeasurableSpace` `ENNReal.measurableSpace`	`MeasureTheory.lintegral`	—	`lintegral_prod_right'` `measurable_swap_iff`
`lintegral_prod_right` 📖	mathematical	`Measurable` `ENNReal` `Prod.instMeasurableSpace` `ENNReal.measurableSpace`	`MeasureTheory.lintegral`	—	`lintegral_prod_right'`
`lintegral_prod_right'` 📖	mathematical	`Measurable` `ENNReal` `Prod.instMeasurableSpace` `ENNReal.measurableSpace`	`MeasureTheory.lintegral`	—	`measurable_prodMk_left` `ennreal_induction` `const_mul` `MeasurableMul₂.toMeasurableMul` `ENNReal.instMeasurableMul₂` `measurable_measure_prodMk_left` `MeasureTheory.lintegral_indicator` `MeasureTheory.lintegral_const` `MeasureTheory.Measure.restrict_apply` `Set.univ_inter` `MeasureTheory.lintegral_add_left` `comp` `add` `ContinuousAdd.measurableMul₂` `ENNReal.borelSpace` `ENNReal.instSecondCountableTopology` `ENNReal.instContinuousAdd` `MeasureTheory.lintegral_iSup` `iSup` `ENNReal.instOrderTopology` `instCountableNat`
`map_prodMk_left` 📖	mathematical	—	`Measurable` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `MeasureTheory.Measure.instMeasurableSpace` `MeasureTheory.Measure.map`	—	`MeasureTheory.Measure.measurable_of_measurable_coe` `MeasureTheory.Measure.map_apply` `measurable_prodMk_left` `measurable_measure_prodMk_left`
`map_prodMk_right` 📖	mathematical	—	`Measurable` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `MeasureTheory.Measure.instMeasurableSpace` `MeasureTheory.Measure.map`	—	`MeasureTheory.Measure.measurable_of_measurable_coe` `MeasureTheory.Measure.map_apply` `measurable_prodMk_right` `measurable_measure_prodMk_right`

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lintegral_lintegral` 📖	mathematical	`AEMeasurable` `ENNReal` `ENNReal.measurableSpace` `Prod.instMeasurableSpace` `Measure.prod`	`lintegral`	—	`lintegral_prod`
`lintegral_lintegral_swap` 📖	mathematical	`AEMeasurable` `ENNReal` `ENNReal.measurableSpace` `Prod.instMeasurableSpace` `Measure.prod`	`lintegral`	—	`lintegral_lintegral` `lintegral_prod_symm`
`lintegral_lintegral_symm` 📖	mathematical	`AEMeasurable` `ENNReal` `ENNReal.measurableSpace` `Prod.instMeasurableSpace` `Measure.prod`	`lintegral`	—	`lintegral_prod_symm` `AEMeasurable.prod_swap`
`lintegral_prod` 📖	mathematical	`AEMeasurable` `ENNReal` `ENNReal.measurableSpace` `Prod.instMeasurableSpace` `Measure.prod`	`lintegral`	—	`Measure.prod_def` `Measure.lintegral_bind` `Measurable.aemeasurable` `Measurable.map_prodMk_left` `lintegral_congr_ae` `Filter.mp_mem` `Measure.instOuterMeasureClass` `AEMeasurable.ae_of_bind` `Filter.univ_mem'` `lintegral_map'` `AEMeasurable.prodMk` `aemeasurable_const` `aemeasurable_id`
`lintegral_prod_le` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `lintegral` `Prod.instMeasurableSpace` `Measure.prod`	—	`Measure.prod_def` `LE.le.trans` `Measure.lintegral_bind_le` `lintegral_mono` `lintegral_map_le`
`lintegral_prod_mul` 📖	mathematical	`AEMeasurable` `ENNReal` `ENNReal.measurableSpace`	`lintegral` `Prod.instMeasurableSpace` `Measure.prod` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`lintegral_prod` `AEMeasurable.mul` `ENNReal.instMeasurableMul₂` `AEMeasurable.comp_quasiMeasurePreserving` `QuasiMeasurePreserving.fst` `Measure.QuasiMeasurePreserving.id` `QuasiMeasurePreserving.snd` `lintegral_lintegral_mul`
`lintegral_prod_swap` 📖	mathematical	—	`lintegral` `Prod.instMeasurableSpace` `Measure.prod`	—	`MeasurePreserving.lintegral_comp_emb` `Measure.measurePreserving_swap` `MeasurableEquiv.measurableEmbedding`
`lintegral_prod_symm` 📖	mathematical	`AEMeasurable` `ENNReal` `ENNReal.measurableSpace` `Prod.instMeasurableSpace` `Measure.prod`	`lintegral`	—	`lintegral_prod_swap` `lintegral_prod` `AEMeasurable.prod_swap`
`lintegral_prod_symm'` 📖	mathematical	`Measurable` `ENNReal` `Prod.instMeasurableSpace` `ENNReal.measurableSpace`	`lintegral` `Measure.prod`	—	`lintegral_prod_symm` `Measurable.aemeasurable`
`measurePreserving_fst` 📖	mathematical	—	`MeasurePreserving` `Prod.instMeasurableSpace` `Measure.prod`	—	`measurable_fst` `IsScalarTower.right` `Measure.map_fst_prod` `IsProbabilityMeasure.measure_univ` `one_smul`
`measurePreserving_prodAssoc` 📖	mathematical	—	`MeasurePreserving` `Prod.instMeasurableSpace` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.prodAssoc` `Measure.prod`	—	`MeasurableEquiv.measurable` `Measure.ext` `measurable_prodMk_left` `Measure.map_apply` `Measure.prod_apply` `Measure.prod.instSFinite` `lintegral_prod` `Measurable.aemeasurable` `measurable_measure_prodMk_left`
`measurePreserving_snd` 📖	mathematical	—	`MeasurePreserving` `Prod.instMeasurableSpace` `Measure.prod`	—	`measurable_snd` `IsScalarTower.right` `Measure.map_snd_prod` `IsProbabilityMeasure.measure_univ` `one_smul`
`measureReal_prod_prod` 📖	mathematical	—	`Measure.real` `Prod.instMeasurableSpace` `Measure.prod` `SProd.sprod` `Set` `Set.instSProd` `Real` `Real.instMul`	—	`Measure.prod_prod` `ENNReal.toReal_mul`
`setLIntegral_prod` 📖	mathematical	`AEMeasurable` `ENNReal` `ENNReal.measurableSpace` `Prod.instMeasurableSpace` `Measure.restrict` `Measure.prod` `SProd.sprod` `Set` `Set.instSProd`	`lintegral`	—	`Measure.prod_restrict` `lintegral_prod` `instSFiniteRestrict`
`setLIntegral_prod_symm` 📖	mathematical	`AEMeasurable` `ENNReal` `ENNReal.measurableSpace` `Prod.instMeasurableSpace` `Measure.restrict` `Measure.prod` `SProd.sprod` `Set` `Set.instSProd`	`lintegral`	—	`Measure.prod_restrict` `lintegral_prod_swap` `instSFiniteRestrict` `setLIntegral_prod` `AEMeasurable.comp_measurable` `Measure.prod_swap` `measurable_swap`
`volume_preserving_prodAssoc` 📖	mathematical	—	`MeasurePreserving` `Prod.instMeasurableSpace` `MeasureSpace.toMeasurableSpace` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.prodAssoc` `MeasureSpace.volume` `Measure.prod.measureSpace`	—	`measurePreserving_prodAssoc`

MeasureTheory.Measure

Definitions

Name	Category	Theorems
`fst` 📖	CompOp	58 math math: `ProbabilityTheory.condCDF_ae_eq`, `ProbabilityTheory.lintegral_condCDF`, `fst.instIsFiniteMeasure`, `ProbabilityTheory.setLIntegral_preCDF_fst`, `ProbabilityTheory.integrable_preCDF`, `ProbabilityTheory.setIntegral_condCDF`, `fst_prod`, `snd_map_swap`, `MeasureTheory.AEStronglyMeasurable.ae_integrable_condKernel_iff`, `setIntegral_condKernel`, `fst_compProd`, `ProbabilityTheory.integrable_condCDF`, `setIntegral_condKernel_univ_left`, `fst_map_swap`, `integral_condKernel`, `ProbabilityTheory.isRatCondKernelCDF_preCDF`, `ProbabilityTheory.ofReal_condCDF_ae_eq`, `MeasureTheory.Integrable.condKernel_ae`, `setIntegral_condKernel_univ_right`, `condKernel_apply_of_ne_zero`, `ProbabilityTheory.preCDF_le_one`, `MeasureTheory.Integrable.norm_integral_condKernel`, `lintegral_condKernel`, `ProbabilityTheory.monotone_preCDF`, `fst.instIsZeroOrProbabilityMeasure`, `fst_apply`, `fst_univ`, `ProbabilityTheory.withDensity_preCDF`, `setLIntegral_condKernel`, `fst_add`, `lintegral_condKernel_mem`, `fst_mono`, `ProbabilityTheory.setIntegral_preCDF_fst`, `IicSnd_le_fst`, `MeasureTheory.AEStronglyMeasurable.integral_condKernel`, `ProbabilityTheory.integral_condCDF`, `ProbabilityTheory.isRatCondKernelCDFAux_preCDF`, `IsCondKernel.disintegrate`, `setLIntegral_condKernel_univ_left`, `fst_map_prodMk₀`, `ProbabilityTheory.isCondKernelCDF_condCDF`, `tendsto_IicSnd_atTop`, `instSFiniteFstOfProd`, `disintegrate`, `ProbabilityTheory.lintegral_preCDF_fst`, `ProbabilityTheory.setLIntegral_condCDF`, `setLIntegral_condKernel_univ_right`, `fst_map_prodMk`, `IicSnd_ac_fst`, `fst_zero`, `fst_sum`, `ProbabilityTheory.condKernel_const`, `MeasureTheory.Integrable.integral_norm_condKernel`, `MeasureTheory.Integrable.integral_condKernel`, `setLIntegral_condKernel_eq_measure_prod`, `IsCondKernel.apply_of_ne_zero`, `ProbabilityTheory.integral_preCDF_fst`, `fst.instIsProbabilityMeasure`
`prod` 📖	CompOp	217 math math: `MeasureTheory.quasiMeasurePreserving_add`, `prod_apply_symm`, `MeasureTheory.lintegral_prod_swap`, `MeasureTheory.quasiMeasurePreserving_add_swap`, `MeasureTheory.NullMeasurable.comp_snd`, `ProbabilityTheory.indepFun_prod`, `prod_eq_generateFrom`, `Measure.eq_prod_of_integral_prod_mul_prod_boundedContinuousFunction`, `MeasureTheory.measurePreserving_prod_mul_swap`, `MeasureTheory.quasiMeasurePreserving_inv_mul`, `Measure.eq_prod_of_integral_mul_boundedContinuousFunction`, `MeasureTheory.measurePreserving_prod_neg_add`, `prod.instNoAtoms_fst`, `MeasureTheory.MemLp.comp_snd`, `AbsolutelyContinuous.prod`, `MeasureTheory.quasiMeasurePreserving_div_of_right_invariant`, `prod.instSigmaFinite`, `MeasureTheory.Integrable.mul_prod`, `MeasureTheory.measurePreserving_prod_mul_swap_right`, `MeasureTheory.setIntegral_prod_swap`, `fst_prod`, `nullMeasurable_comp_snd`, `Real.integrable_prod_sub`, `map_fst_prod`, `MeasureTheory.measurePreserving_prod_div_swap`, `MeasureTheory.measurePreserving_prod_inv_mul_swap`, `prod.instIsOpenPosMeasure`, `MeasureTheory.MeasurePreserving.prod`, `nullMeasurableSet_region_between_co`, `MeasureTheory.setIntegral_prod_mul`, `MeasureTheory.ProbabilityMeasure.measurable_fun_prod`, `nullMeasurableSet_prod`, `MeasureTheory.measurePreserving_finTwoArrow_vec`, `prod_eq`, `nullMeasurableSet_regionBetween`, `prod.instIsAddLeftInvariant`, `MeasureTheory.measurePreserving_mul_prod_inv_right`, `MeasureTheory.Integrable.comp_snd`, `MeasureTheory.QuasiMeasurePreserving.prod_of_left`, `prod_prod_le`, `ProbabilityTheory.covariance_fst_snd_prod`, `MeasureTheory.ProbabilityMeasure.toMeasure_prod`, `MeasureTheory.prod_withDensity₀`, `lintegral_conv_eq_lintegral_sum`, `nullMeasurableSet_region_between_cc`, `nullMeasurableSet_preimage_fst`, `MeasureTheory.prod_withDensity_left`, `MeasureTheory.charFunDual_prod`, `Module.Basis.prod_addHaar`, `MeasureTheory.charFun_eq_prod_iff`, `AEMeasurable.comp_snd`, `MeasureTheory.quasiMeasurePreserving_neg_add_swap`, `ProbabilityTheory.Kernel.prod_apply`, `ae_prod_iff_ae_ae`, `prod_apply_le`, `Measure.eq_prod_of_integral_mul_prod_boundedContinuousFunction`, `pi_prod_map_IocProdIoc`, `MeasureTheory.charFunDual_eq_prod_iff`, `MeasureTheory.measurePreserving_prod_add_right`, `prod.instIsMulRightInvariant`, `prod_apply`, `ProbabilityTheory.Kernel.parallelComp_def`, `ae_prod_mem_iff_ae_ae_mem`, `MeasureTheory.measurePreserving_add_prod_neg_right`, `MeasureTheory.measurePreserving_arrowProdEquivProdArrow`, `FiniteAtFilter.prod`, `Measure.eq_prod_of_integral_prod_mul_prod_boundedContinuousFunction'`, `volume_regionBetween_eq_lintegral'`, `MeasureTheory.measurePreserving_prod_sub_swap`, `map_prod_map`, `MeasureTheory.measurePreserving_piFinTwo`, `MeasureTheory.quasiMeasurePreserving_neg_add`, `pi_prod_map_IicProdIoc`, `prod_swap`, `measure_prod_null_of_ae_null`, `MeasureTheory.measurePreserving_prod_div`, `prod_restrict`, `zero_prod`, `prod_prod`, `MeasureTheory.QuasiMeasurePreserving.prod_of_right`, `prod.instIsAddRightInvariant`, `prod.instIsProbabilityMeasure`, `quasiMeasurePreserving_fst`, `MeasureTheory.measurePreserving_prodAssoc`, `MeasureTheory.continuous_integral_integral`, `MeasureTheory.integral_prod_mul`, `MeasureTheory.quasiMeasurePreserving_sub_of_right_invariant`, `prod.instIsMulLeftInvariant`, `ProbabilityTheory.condDistrib_snd_prod`, `MeasureTheory.prod_withDensity_left₀`, `MeasureTheory.measurePreserving_piFinSuccAbove`, `dirac_prod_dirac`, `MeasureTheory.prod_withDensity_right₀`, `volume_eq_prod`, `quasiMeasurePreserving_snd`, `prod.instIsLocallyFiniteMeasure`, `MeasureTheory.integral_continuousLinearMap_prod`, `nullMeasurableSet_prod_of_ne_zero`, `Measure.eq_prod_of_integral_prod_mul_boundedContinuousFunction'`, `ProbabilityTheory.variance_add_prod`, `ProbabilityTheory.IsGaussian.map_rotation_eq_self`, `measurePreserving_homeomorphUnitSphereProd`, `MeasureTheory.Integrable.convolution_integrand`, `MeasureTheory.integral_continuousLinearMap_prod'`, `dirac_prod`, `MeasureTheory.pdf.indepFun_iff_pdf_prod_eq_pdf_mul_pdf`, `MeasureTheory.quasiMeasurePreserving_mul_swap`, `prod.instIsAddHaarMeasure`, `MeasureTheory.Integrable.comp_fst_iff`, `prod_dirac`, `MeasureTheory.Integrable.comp_fst`, `MeasureTheory.integrable_continuousLinearMap_prod'`, `set_prod_ae_eq`, `MeasureTheory.measurePreserving_prod_sub`, `MeasureTheory.MemLp.comp_fst`, `MeasureTheory.integral_prod_swap`, `MeasureTheory.measurePreserving_prod_add`, `MeasureTheory.measurePreserving_mul_prod`, `prod_sum_right`, `prod_add`, `MeasureTheory.quasiMeasurePreserving_sub`, `MeasureTheory.measurePreserving_prod_add_swap_right`, `ProbabilityTheory.variance_dual_prod'`, `prod_smul_right`, `MeasureTheory.measurePreserving_add_prod`, `MeasureTheory.charFunDual_prod'`, `volume_regionBetween_eq_integral'`, `MeasureTheory.integrable_swap_iff`, `prod_sum`, `MeasureTheory.Integrable.comp_snd_iff`, `prod.instIsHaarMeasure`, `MeasureTheory.measurePreserving_piFinsetUnion`, `MeasureTheory.integral_fun_fst`, `MeasureTheory.Integrable.op_fst_snd`, `prod_comp_left`, `MeasureTheory.AEStronglyMeasurable.comp_snd_iff`, `prod.instSFinite`, `MeasureTheory.lintegral_prod_le`, `MeasureTheory.hasFiniteIntegral_prod_iff`, `prod.instIsFiniteMeasure`, `prod.instNoAtoms_snd`, `prod.instIsFiniteMeasureOnCompacts`, `MeasureTheory.prod_withDensity`, `MeasureTheory.AEStronglyMeasurable.comp_fst`, `nullMeasurableSet_preimage_snd`, `MeasureTheory.measureReal_prod_prod`, `MeasureTheory.integrable_continuousLinearMap_prod`, `MeasureTheory.MeasurePreserving.skew_product`, `MeasureTheory.lintegral_prod_symm'`, `prod_comp_right`, `measure_prod_null`, `ProbabilityTheory.condDistrib_fst_prod`, `MeasureTheory.lintegral_prod_mul`, `ProbabilityTheory.variance_dual_prod`, `volume_regionBetween_eq_integral`, `prod_sum_left`, `ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map'`, `MeasureTheory.QuasiMeasurePreserving.prodMap`, `MeasureTheory.measurePreserving_prod_add_swap`, `nullMeasurableSet_region_between_oc`, `MeasureTheory.measurePreserving_prod_mul`, `prodAssoc_prod`, `MeasureTheory.Integrable.smul_prod`, `MeasureTheory.prod_withDensity_right`, `tprod_cons`, `ProbabilityTheory.Kernel.parallelComp_apply`, `add_prod`, `MeasureTheory.measurePreserving_prod_inv_mul`, `MeasureTheory.measurePreserving_sumPiEquivProdPi_symm`, `MeasureTheory.measurePreserving_snd`, `MeasureTheory.measurePreserving_mul_prod_inv`, `Measure.eq_prod_of_integral_mul_prod_boundedContinuousFunction'`, `MeasureTheory.AEStronglyMeasurable.comp_fst_iff`, `ProbabilityTheory.Kernel.prod_const`, `MeasureTheory.measurePreserving_piEquivPiSubtypeProd`, `ProbabilityTheory.instIsGaussianProdProdOfSecondCountableTopologyEither`, `measurePreserving_swap`, `pi_map_piOptionEquivProd`, `prod_zero`, `nullMeasurable_comp_fst`, `prod_def`, `ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map`, `ProbabilityTheory.indepFun_prod₀`, `MeasureTheory.integral_prod_smul`, `MeasureTheory.FiniteMeasure.measurable_fun_prod`, `ProbabilityTheory.rnDeriv_posterior_ae_prod`, `MeasureTheory.quasiMeasurePreserving_mul`, `MeasureTheory.measurePreserving_finTwoArrow`, `MeasureTheory.integral_fun_snd`, `MeasureTheory.AEStronglyMeasurable.convolution_integrand`, `MeasureTheory.NullMeasurableSet.prod`, `IsUnifLocDoublingMeasure.prod`, `lintegral_mconv_eq_lintegral_prod`, `MeasureTheory.measurePreserving_div_prod`, `MeasureTheory.charFun_prod`, `volume_regionBetween_eq_lintegral`, `MeasureTheory.charFunDual_eq_prod_iff'`, `MeasureTheory.AEStronglyMeasurable.comp_snd`, `restrict_prod_eq_prod_univ`, `MeasureTheory.measurePreserving_prod_neg_add_swap`, `map_snd_prod`, `MeasureTheory.measurePreserving_add_prod_neg`, `MeasureTheory.measurePreserving_sumPiEquivProdPi`, `MeasureTheory.NullMeasurable.comp_fst`, `snd_prod`, `MeasureTheory.FiniteMeasure.toMeasure_prod`, `MeasureTheory.quasiMeasurePreserving_div`, `AEMeasurable.comp_fst`, `MeasureTheory.measurePreserving_sub_prod`, `MeasureTheory.measurePreserving_prod_mul_right`, `ProbabilityTheory.IsGaussian.map_rotation_eq_self_of_forall_strongDual_eq_zero`, `prod_smul_left`, `compProd_const`, `measure_prod_compl_eq_zero`, `Measure.eq_prod_of_integral_prod_mul_boundedContinuousFunction`, `MeasureTheory.quasiMeasurePreserving_inv_mul_swap`, `MeasureTheory.measurePreserving_fst`
`snd` 📖	CompOp	18 math math: `comp_compProd_comm`, `snd_map_swap`, `snd_zero`, `snd_compProd`, `snd_map_prodMk₀`, `fst_map_swap`, `snd_sum`, `snd_mono`, `snd.instIsZeroOrProbabilityMeasure`, `snd_univ`, `snd_map_prodMk`, `snd_dirac_unit_compProd_const`, `snd_add`, `snd.instIsProbabilityMeasure`, `snd_apply`, `snd.instIsFiniteMeasure`, `instSFiniteSndOfProd`, `snd_prod`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_prod` 📖	mathematical	—	`prod` `MeasureTheory.Measure` `instAdd` `Prod.instMeasurableSpace`	—	`MeasureTheory.sum_sfiniteSeq` `sum_add_sum` `prod_sum` `instCountableNat` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `MeasureTheory.isFiniteMeasure_sfiniteSeq` `prod_eq` `MeasureTheory.Add.sigmaFinite` `prod_prod` `right_distrib` `Distrib.rightDistribClass`
`ae_ae_comm` 📖	mathematical	`MeasurableSet` `Prod.instMeasurableSpace` `setOf`	`Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass`	—	`instOuterMeasureClass` `ae_prod_iff_ae_ae` `prod_swap` `MeasureTheory.ae_map_iff` `Measurable.aemeasurable` `measurable_swap`
`ae_ae_eq_curry_of_prod` 📖	mathematical	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `instFunLike` `instOuterMeasureClass` `prod`	`Filter.Eventually`	—	`instOuterMeasureClass` `ae_ae_of_ae_prod`
`ae_ae_eq_of_ae_eq_uncurry` 📖	mathematical	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `instFunLike` `instOuterMeasureClass` `prod`	`Filter.Eventually`	—	`instOuterMeasureClass` `ae_ae_eq_curry_of_prod`
`ae_ae_of_ae_prod` 📖	—	`Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `instFunLike` `instOuterMeasureClass` `prod`	—	—	`instOuterMeasureClass` `measure_ae_null_of_prod_null`
`ae_measure_lt_top` 📖	mathematical	`MeasurableSet` `Prod.instMeasurableSpace`	`Filter.Eventually` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `instFunLike` `Set.preimage` `Top.top` `instTopENNReal` `MeasureTheory.ae` `instOuterMeasureClass`	—	`MeasureTheory.ae_lt_top` `measurable_measure_prodMk_left` `prod_apply`
`ae_prod_iff_ae_ae` 📖	mathematical	`MeasurableSet` `Prod.instMeasurableSpace` `setOf`	`Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `prod`	—	`measure_prod_null` `MeasurableSet.compl`
`ae_prod_mem_iff_ae_ae_mem` 📖	mathematical	`MeasurableSet` `Prod.instMeasurableSpace`	`Filter.Eventually` `Set` `Set.instMembership` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `prod`	—	`measure_prod_null` `MeasurableSet.compl`
`dirac_prod` 📖	mathematical	—	`prod` `dirac` `map` `Prod.instMeasurableSpace`	—	`MeasureTheory.sum_sfiniteSeq` `prod_sum_right` `instCountableNat` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `MeasureTheory.isFiniteMeasure_sfiniteSeq` `map_sum` `Measurable.aemeasurable` `measurable_prodMk_left` `prod_eq` `dirac.instSigmaFinite` `map_apply` `MeasurableSet.prod` `Set.mk_preimage_prod_right_eq_if` `MeasureTheory.measure_if` `dirac_apply'` `Set.indicator_mul_left` `one_mul`
`dirac_prod_dirac` 📖	mathematical	—	`prod` `dirac` `Prod.instMeasurableSpace`	—	`prod_dirac` `MeasureTheory.instSFiniteOfSigmaFinite` `dirac.instSigmaFinite` `map_dirac` `measurable_prodMk_right`
`ext_prod` 📖	—	`DFunLike.coe` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `Set` `ENNReal` `instFunLike` `SProd.sprod` `Set.instSProd`	—	—	`ext` `Set.univ_prod_univ` `MeasurableSet.univ` `MeasurableSpace.induction_on_inter` `generateFrom_prod` `isPiSystem_prod` `MeasureTheory.measure_empty` `instOuterMeasureClass` `MeasureTheory.measure_compl` `MeasureTheory.measure_ne_top` `MeasureTheory.measure_iUnion` `instCountableNat`
`ext_prod_iff` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `Set` `ENNReal` `instFunLike` `SProd.sprod` `Set.instSProd`	—	`ext_prod`
`ext_prod₃` 📖	—	`DFunLike.coe` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `Set` `ENNReal` `instFunLike` `SProd.sprod` `Set.instSProd`	—	—	`ext` `MeasurableSet.univ` `MeasurableSpace.induction_on_inter` `generateFrom_eq_prod` `MeasurableSpace.generateFrom_measurableSet` `generateFrom_prod` `isCountablySpanning_measurableSet` `IsCountablySpanning.prod` `IsPiSystem.prod` `MeasurableSpace.isPiSystem_measurableSet` `isPiSystem_prod` `MeasureTheory.measure_empty` `instOuterMeasureClass` `MeasureTheory.measure_compl` `MeasureTheory.measure_ne_top` `MeasureTheory.measure_iUnion` `instCountableNat`
`ext_prod₃'` 📖	—	`DFunLike.coe` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `Set` `ENNReal` `instFunLike` `SProd.sprod` `Set.instSProd`	—	—	`ext_prod₃_iff'`
`ext_prod₃_iff` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `Set` `ENNReal` `instFunLike` `SProd.sprod` `Set.instSProd`	—	`ext_prod₃`
`ext_prod₃_iff'` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `Set` `ENNReal` `instFunLike` `SProd.sprod` `Set.instSProd`	—	`MeasurableEquiv.map_measurableEquiv_injective` `ext_prod₃_iff` `isFiniteMeasure_map` `map_apply` `MeasurableEquiv.measurable` `MeasurableSet.prod` `Set.ext` `Equiv.prod_assoc_preimage`
`fst_add` 📖	mathematical	—	`fst` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `instAdd`	—	`map_add` `measurable_fst`
`fst_apply` 📖	mathematical	`MeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `fst` `Prod.instMeasurableSpace` `Set.preimage`	—	`fst.eq_1` `map_apply` `measurable_fst`
`fst_map_prodMk` 📖	mathematical	`Measurable`	`fst` `map` `Prod.instMeasurableSpace`	—	`fst_map_prodMk₀` `Measurable.aemeasurable`
`fst_map_prodMk₀` 📖	mathematical	`AEMeasurable`	`fst` `map` `Prod.instMeasurableSpace`	—	`ext` `fst_apply` `map_apply_of_aemeasurable` `AEMeasurable.prodMk` `measurable_fst` `Set.prod_univ` `Set.mk_preimage_prod` `Set.preimage_univ` `Set.inter_univ` `Mathlib.Tactic.Contrapose.contrapose₄` `Measurable.comp_aemeasurable` `map_of_not_aemeasurable` `fst_zero`
`fst_map_swap` 📖	mathematical	—	`fst` `map` `Prod.instMeasurableSpace` `snd`	—	`fst.eq_1` `map_map` `measurable_fst` `measurable_swap`
`fst_mono` 📖	mathematical	`MeasureTheory.Measure` `Prod.instMeasurableSpace` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`fst`	—	`map_mono` `measurable_fst`
`fst_prod` 📖	mathematical	—	`fst` `prod`	—	`ext` `fst_apply` `Set.prod_univ` `prod_prod` `MeasureTheory.IsProbabilityMeasure.measure_univ` `mul_one`
`fst_sum` 📖	mathematical	—	`fst` `sum` `Prod.instMeasurableSpace`	—	`map_sum` `Measurable.aemeasurable` `measurable_fst`
`fst_univ` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `fst` `Set.univ` `Prod.instMeasurableSpace`	—	`fst_apply` `MeasurableSet.univ` `Set.preimage_univ`
`fst_zero` 📖	mathematical	—	`fst` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `instZero`	—	`map_zero`
`instIsFiniteMeasureOnCompactsProdVolume` 📖	mathematical	—	`MeasureTheory.IsFiniteMeasureOnCompacts` `MeasureTheory.MeasureSpace.toMeasurableSpace` `prod.measureSpace` `instTopologicalSpaceProd` `MeasureTheory.MeasureSpace.volume`	—	`prod.instIsFiniteMeasureOnCompacts`
`instIsFiniteMeasureProdVolume` 📖	mathematical	—	`MeasureTheory.IsFiniteMeasure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `prod.measureSpace` `MeasureTheory.MeasureSpace.volume`	—	`prod.instIsFiniteMeasure`
`instIsLocallyFiniteMeasureProdVolume` 📖	mathematical	—	`MeasureTheory.IsLocallyFiniteMeasure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `prod.measureSpace` `instTopologicalSpaceProd` `MeasureTheory.MeasureSpace.volume`	—	`prod.instIsLocallyFiniteMeasure`
`instIsOpenPosMeasureProdVolumeOfSFinite` 📖	mathematical	—	`IsOpenPosMeasure` `instTopologicalSpaceProd` `MeasureTheory.MeasureSpace.toMeasurableSpace` `prod.measureSpace` `MeasureTheory.MeasureSpace.volume`	—	`prod.instIsOpenPosMeasure`
`instIsProbabilityMeasureProdVolume` 📖	mathematical	—	`MeasureTheory.IsProbabilityMeasure` `MeasureTheory.MeasureSpace.toMeasurableSpace` `prod.measureSpace` `MeasureTheory.MeasureSpace.volume`	—	`prod.instIsProbabilityMeasure`
`instSFiniteFstOfProd` 📖	mathematical	—	`MeasureTheory.SFinite` `fst`	—	`fst.eq_1` `instSFiniteMap`
`instSFiniteProdVolume` 📖	mathematical	—	`MeasureTheory.SFinite` `MeasureTheory.MeasureSpace.toMeasurableSpace` `prod.measureSpace` `MeasureTheory.MeasureSpace.volume`	—	`prod.instSFinite`
`instSFiniteSndOfProd` 📖	mathematical	—	`MeasureTheory.SFinite` `snd`	—	`snd.eq_1` `instSFiniteMap`
`instSigmaFiniteProdVolume` 📖	mathematical	—	`MeasureTheory.SigmaFinite` `MeasureTheory.MeasureSpace.toMeasurableSpace` `prod.measureSpace` `MeasureTheory.MeasureSpace.volume`	—	`prod.instSigmaFinite`
`map_fst_prod` 📖	mathematical	—	`map` `Prod.instMeasurableSpace` `prod` `ENNReal` `MeasureTheory.Measure` `instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right` `DFunLike.coe` `Set` `instFunLike` `Set.univ`	—	`ext` `IsScalarTower.right` `map_apply` `measurable_fst` `prod_prod` `mul_comm`
`map_prod_map` 📖	mathematical	`Measurable`	`prod` `map` `Prod.instMeasurableSpace`	—	`MeasureTheory.sum_sfiniteSeq` `map_sum` `Measurable.aemeasurable` `prod_sum` `instCountableNat` `instSFiniteMap` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `MeasureTheory.isFiniteMeasure_sfiniteSeq` `Measurable.prodMap` `prod_eq` `isFiniteMeasure_map` `map_apply` `MeasurableSet.prod` `prod_prod`
`map_snd_prod` 📖	mathematical	—	`map` `Prod.instMeasurableSpace` `prod` `ENNReal` `MeasureTheory.Measure` `instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right` `DFunLike.coe` `Set` `instFunLike` `Set.univ`	—	`ext` `IsScalarTower.right` `map_apply` `measurable_snd` `prod_prod`
`measurePreserving_swap` 📖	mathematical	—	`MeasureTheory.MeasurePreserving` `Prod.instMeasurableSpace` `prod`	—	`measurable_swap` `prod_swap`
`measure_ae_null_of_prod_null` 📖	mathematical	`DFunLike.coe` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `Set` `ENNReal` `instFunLike` `prod` `instZeroENNReal`	`Filter.EventuallyEq` `MeasureTheory.ae` `instOuterMeasureClass` `Set.preimage` `Pi.instZero`	—	`instOuterMeasureClass` `MeasureTheory.exists_measurable_superset_of_null` `Filter.eventuallyLE_antisymm_iff` `Filter.EventuallyLE.trans_eq` `Filter.Eventually.of_forall` `MeasureTheory.measure_mono` `Set.preimage_mono` `measure_prod_null` `zero_le` `ENNReal.instCanonicallyOrderedAdd`
`measure_prod_compl_eq_zero` 📖	mathematical	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `Compl.compl` `Set.instCompl` `instZeroENNReal`	`Prod.instMeasurableSpace` `prod` `SProd.sprod` `Set.instSProd`	—	`Set.compl_prod_eq_union` `MeasureTheory.measure_union_null_iff` `instOuterMeasureClass` `prod_prod` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero`
`measure_prod_null` 📖	mathematical	`MeasurableSet` `Prod.instMeasurableSpace`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `prod` `instZeroENNReal` `Filter.EventuallyEq` `MeasureTheory.ae` `instOuterMeasureClass` `Set.preimage` `Pi.instZero`	—	`instOuterMeasureClass` `prod_apply` `MeasureTheory.lintegral_eq_zero_iff` `measurable_measure_prodMk_left`
`measure_prod_null_of_ae_null` 📖	mathematical	`MeasurableSet` `Prod.instMeasurableSpace` `Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `DFunLike.coe` `Set` `Set.preimage` `Pi.instZero` `instZeroENNReal`	`prod`	—	`instOuterMeasureClass` `nonpos_iff_eq_zero` `ENNReal.instCanonicallyOrderedAdd` `prod_apply_le` `MeasureTheory.lintegral_congr_ae` `MeasureTheory.lintegral_const` `MulZeroClass.zero_mul`
`nullMeasurableSet_preimage_fst` 📖	mathematical	—	`MeasureTheory.NullMeasurableSet` `Prod.instMeasurableSpace` `Set.preimage` `prod`	—	`MeasureTheory.NullMeasurableSet.of_preimage_fst` `MeasureTheory.NullMeasurableSet.preimage` `quasiMeasurePreserving_fst`
`nullMeasurableSet_preimage_snd` 📖	mathematical	—	`MeasureTheory.NullMeasurableSet` `Prod.instMeasurableSpace` `Set.preimage` `prod`	—	`MeasureTheory.NullMeasurableSet.of_preimage_snd` `MeasureTheory.NullMeasurableSet.preimage` `quasiMeasurePreserving_snd`
`nullMeasurableSet_prod` 📖	mathematical	—	`MeasureTheory.NullMeasurableSet` `Prod.instMeasurableSpace` `SProd.sprod` `Set` `Set.instSProd` `prod` `DFunLike.coe` `MeasureTheory.Measure` `ENNReal` `instFunLike` `instZeroENNReal`	—	`eq_or_ne` `prod_prod` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero`
`nullMeasurableSet_prod_of_ne_zero` 📖	mathematical	—	`MeasureTheory.NullMeasurableSet` `Prod.instMeasurableSpace` `SProd.sprod` `Set` `Set.instSProd` `prod`	—	`MeasureTheory.NullMeasurableSet.left_of_prod` `MeasureTheory.NullMeasurableSet.right_of_prod` `MeasureTheory.NullMeasurableSet.prod`
`nullMeasurable_comp_fst` 📖	mathematical	—	`MeasureTheory.NullMeasurable` `Prod.instMeasurableSpace` `prod`	—	`nullMeasurableSet_preimage_fst`
`nullMeasurable_comp_snd` 📖	mathematical	—	`MeasureTheory.NullMeasurable` `Prod.instMeasurableSpace` `prod`	—	`nullMeasurableSet_preimage_snd`
`prodAssoc_prod` 📖	mathematical	—	`map` `Prod.instMeasurableSpace` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.prodAssoc` `prod`	—	`ext` `sum_apply` `Equiv.tsum_eq` `MeasureTheory.sum_sfiniteSeq` `prod_sum` `instCountableNat` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `MeasureTheory.isFiniteMeasure_sfiniteSeq` `map_sum` `Measurable.aemeasurable` `MeasurableEquiv.measurable` `instCountableProd` `prod.instSFinite` `prod_eq_generateFrom` `MeasurableSpace.generateFrom_measurableSet` `generateFrom_prod` `MeasurableSpace.isPiSystem_measurableSet` `isPiSystem_prod` `map_apply` `MeasurableSet.prod` `Set.mem_setOf_eq` `Equiv.prod_assoc_preimage` `prod_prod` `mul_assoc`
`prod_add` 📖	mathematical	—	`prod` `MeasureTheory.Measure` `instAdd` `Prod.instMeasurableSpace`	—	`MeasureTheory.sum_sfiniteSeq` `sum_add_sum` `prod_sum` `instCountableNat` `MeasureTheory.instSFiniteHAddMeasure` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `MeasureTheory.isFiniteMeasure_sfiniteSeq` `prod_eq` `MeasureTheory.Add.sigmaFinite` `prod_prod` `left_distrib` `Distrib.leftDistribClass`
`prod_apply` 📖	mathematical	`MeasurableSet` `Prod.instMeasurableSpace`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `prod` `MeasureTheory.lintegral` `Set.preimage`	—	`prod_def` `bind_apply` `Measurable.aemeasurable` `Measurable.map_prodMk_left` `map_apply` `measurable_prodMk_left`
`prod_apply_le` 📖	mathematical	`MeasurableSet` `Prod.instMeasurableSpace`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `instFunLike` `prod` `MeasureTheory.lintegral` `Set.preimage`	—	`prod_def` `map_apply` `measurable_prodMk_left` `bind_apply_le`
`prod_apply_symm` 📖	mathematical	`MeasurableSet` `Prod.instMeasurableSpace`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `prod` `MeasureTheory.lintegral` `Set.preimage`	—	`prod_swap` `map_apply` `measurable_swap` `prod_apply`
`prod_def` 📖	mathematical	—	`prod` `bind` `Prod.instMeasurableSpace` `map`	—	—
`prod_dirac` 📖	mathematical	—	`prod` `dirac` `map` `Prod.instMeasurableSpace`	—	`MeasureTheory.sum_sfiniteSeq` `prod_sum_left` `MeasureTheory.instSFiniteOfSigmaFinite` `dirac.instSigmaFinite` `map_sum` `Measurable.aemeasurable` `measurable_prodMk_right` `prod_eq` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `MeasureTheory.isFiniteMeasure_sfiniteSeq` `map_apply` `MeasurableSet.prod` `Set.mk_preimage_prod_left_eq_if` `MeasureTheory.measure_if` `dirac_apply'` `Set.indicator_mul_right` `mul_one`
`prod_eq` 📖	mathematical	`DFunLike.coe` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `Set` `ENNReal` `instFunLike` `SProd.sprod` `Set.instSProd` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	`prod`	—	`prod_eq_generateFrom` `MeasurableSpace.generateFrom_measurableSet` `MeasurableSpace.isPiSystem_measurableSet`
`prod_eq_generateFrom` 📖	mathematical	`MeasurableSpace.generateFrom` `IsPiSystem` `DFunLike.coe` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `Set` `ENNReal` `instFunLike` `SProd.sprod` `Set.instSProd` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	`prod`	—	`FiniteSpanningSetsIn.ext` `generateFrom_eq_prod` `FiniteSpanningSetsIn.isCountablySpanning` `IsPiSystem.prod` `prod_prod` `MeasureTheory.instSFiniteOfSigmaFinite` `FiniteSpanningSetsIn.sigmaFinite`
`prod_prod` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `Set` `ENNReal` `instFunLike` `prod` `SProd.sprod` `Set.instSProd` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`LE.le.antisymm` `prod_prod_le` `MeasureTheory.measurableSet_toMeasurable` `MeasureTheory.subset_toMeasurable` `measurable_measure_prodMk_left` `MeasureTheory.measure_mono` `instOuterMeasureClass` `Set.mk_mem_prod` `mul_le_mul_left` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `MeasureTheory.setLIntegral_const` `mul_comm` `MeasureTheory.setLIntegral_mono` `MeasureTheory.lintegral_mono'` `restrict_le_self` `le_rfl` `prod_apply` `MeasureTheory.measure_toMeasurable`
`prod_prod_le` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `Set` `instFunLike` `prod` `SProd.sprod` `Set.instSProd` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`MeasureTheory.measure_mono` `instOuterMeasureClass` `Set.prod_mono` `MeasureTheory.subset_toMeasurable` `prod_apply_le` `MeasurableSet.prod` `Set.mk_preimage_prod_right_eq_if` `MeasureTheory.measure_if` `MeasureTheory.lintegral_indicator` `MeasureTheory.measurableSet_toMeasurable` `MeasureTheory.lintegral_const` `restrict_apply_univ` `mul_comm` `MeasureTheory.measure_toMeasurable`
`prod_restrict` 📖	mathematical	—	`prod` `restrict` `Prod.instMeasurableSpace` `SProd.sprod` `Set` `Set.instSProd`	—	`MeasureTheory.sum_sfiniteSeq` `restrict_sum_of_countable` `instCountableNat` `prod_sum` `MeasureTheory.instSFiniteRestrict` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `MeasureTheory.isFiniteMeasure_sfiniteSeq` `instCountableProd` `prod_eq` `MeasureTheory.Restrict.sigmaFinite` `restrict_apply` `MeasurableSet.prod` `Set.prod_inter_prod` `prod_prod`
`prod_smul_left` 📖	mathematical	—	`prod` `ENNReal` `MeasureTheory.Measure` `instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right` `Prod.instMeasurableSpace`	—	`ext` `IsScalarTower.right` `prod_apply` `smul_apply` `MeasureTheory.lintegral_smul_measure`
`prod_sum` 📖	mathematical	`MeasureTheory.SFinite`	`prod` `sum` `Prod.instMeasurableSpace`	—	`prod_sum_left` `MeasureTheory.instSFiniteSumOfCountable` `prod_sum_right` `sum_sum`
`prod_sum_left` 📖	mathematical	—	`prod` `sum` `Prod.instMeasurableSpace`	—	`ext` `prod_apply` `MeasureTheory.lintegral_sum_measure` `sum_apply`
`prod_sum_right` 📖	mathematical	`MeasureTheory.SFinite`	`prod` `sum` `Prod.instMeasurableSpace`	—	`ext` `prod_apply` `MeasureTheory.instSFiniteSumOfCountable` `sum_apply` `measurable_prodMk_left` `MeasureTheory.lintegral_tsum` `Measurable.aemeasurable` `measurable_measure_prodMk_left`
`prod_swap` 📖	mathematical	—	`map` `Prod.instMeasurableSpace` `prod`	—	`ext` `sum_apply` `Equiv.tsum_eq` `MeasureTheory.sum_sfiniteSeq` `prod_sum` `instCountableNat` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `MeasureTheory.isFiniteMeasure_sfiniteSeq` `map_sum` `Measurable.aemeasurable` `measurable_swap` `prod_eq` `map_apply` `MeasurableSet.prod` `Set.preimage_swap_prod` `prod_prod` `mul_comm`
`prod_zero` 📖	mathematical	—	`prod` `MeasureTheory.Measure` `instZero` `Prod.instMeasurableSpace`	—	`prod_def` `IsScalarTower.right` `map_zero` `bind_const` `smul_zero`
`quasiMeasurePreserving_fst` 📖	mathematical	—	`QuasiMeasurePreserving` `Prod.instMeasurableSpace` `prod`	—	`measurable_fst` `map_apply` `Set.prod_univ` `nonpos_iff_eq_zero` `ENNReal.instCanonicallyOrderedAdd` `LE.le.trans_eq` `prod_prod_le` `MulZeroClass.zero_mul`
`quasiMeasurePreserving_snd` 📖	mathematical	—	`QuasiMeasurePreserving` `Prod.instMeasurableSpace` `prod`	—	`measurable_snd` `map_apply` `Set.univ_prod` `nonpos_iff_eq_zero` `ENNReal.instCanonicallyOrderedAdd` `LE.le.trans_eq` `prod_prod_le` `MulZeroClass.mul_zero`
`restrict_prod_eq_prod_univ` 📖	mathematical	—	`prod` `restrict` `Prod.instMeasurableSpace` `SProd.sprod` `Set` `Set.instSProd` `Set.univ`	—	`restrict_univ` `prod_restrict`
`set_prod_ae_eq` 📖	mathematical	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass`	`Prod.instMeasurableSpace` `prod` `SProd.sprod` `Set` `Set.instSProd`	—	`instOuterMeasureClass` `Filter.EventuallyEq.inter` `QuasiMeasurePreserving.preimage_ae_eq` `quasiMeasurePreserving_fst` `quasiMeasurePreserving_snd`
`snd_add` 📖	mathematical	—	`snd` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `instAdd`	—	`map_add` `measurable_snd`
`snd_apply` 📖	mathematical	`MeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `snd` `Prod.instMeasurableSpace` `Set.preimage`	—	`snd.eq_1` `map_apply` `measurable_snd`
`snd_map_prodMk` 📖	mathematical	`Measurable`	`snd` `map` `Prod.instMeasurableSpace`	—	`snd_map_prodMk₀` `Measurable.aemeasurable`
`snd_map_prodMk₀` 📖	mathematical	`AEMeasurable`	`snd` `map` `Prod.instMeasurableSpace`	—	`ext` `snd_apply` `map_apply_of_aemeasurable` `AEMeasurable.prodMk` `measurable_snd` `Set.univ_prod` `Set.mk_preimage_prod` `Set.preimage_univ` `Set.univ_inter` `Mathlib.Tactic.Contrapose.contrapose₄` `Measurable.comp_aemeasurable` `map_of_not_aemeasurable` `snd_zero`
`snd_map_swap` 📖	mathematical	—	`snd` `map` `Prod.instMeasurableSpace` `fst`	—	`snd.eq_1` `map_map` `measurable_snd` `measurable_swap`
`snd_mono` 📖	mathematical	`MeasureTheory.Measure` `Prod.instMeasurableSpace` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`snd`	—	`map_mono` `measurable_snd`
`snd_prod` 📖	mathematical	—	`snd` `prod`	—	`ext` `snd_apply` `Set.univ_prod` `prod_prod` `MeasureTheory.IsProbabilityMeasure.measure_univ` `one_mul`
`snd_sum` 📖	mathematical	—	`snd` `sum` `Prod.instMeasurableSpace`	—	`map_sum` `Measurable.aemeasurable` `measurable_snd`
`snd_univ` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `snd` `Set.univ` `Prod.instMeasurableSpace`	—	`snd_apply` `MeasurableSet.univ` `Set.preimage_univ`
`snd_zero` 📖	mathematical	—	`snd` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `instZero`	—	`map_zero`
`volume_eq_prod` 📖	mathematical	—	`MeasureTheory.MeasureSpace.volume` `prod.measureSpace` `prod` `MeasureTheory.MeasureSpace.toMeasurableSpace`	—	—
`zero_prod` 📖	mathematical	—	`prod` `MeasureTheory.Measure` `instZero` `Prod.instMeasurableSpace`	—	`prod_def` `bind_zero_left`

MeasureTheory.Measure.AbsolutelyContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod` 📖	mathematical	`MeasureTheory.Measure.AbsolutelyContinuous`	`Prod.instMeasurableSpace` `MeasureTheory.Measure.prod`	—	`MeasureTheory.Measure.measure_prod_null_of_ae_null` `Filter.Eventually.mono` `MeasureTheory.Measure.instOuterMeasureClass` `Filter.EventuallyEq.filter_mono` `MeasureTheory.Measure.measure_prod_null` `ae_le`

MeasureTheory.Measure.FiniteAtFilter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod` 📖	mathematical	`MeasureTheory.Measure.FiniteAtFilter`	`Prod.instMeasurableSpace` `MeasureTheory.Measure.prod` `SProd.sprod` `Filter` `Filter.instSProd`	—	`Filter.prod_mem_prod` `lt_imp_lt_of_le_of_le` `MeasureTheory.Measure.prod_prod_le` `le_refl` `ENNReal.mul_lt_top`

MeasureTheory.Measure.FiniteSpanningSetsIn

Definitions

Name	Category	Theorems
`prod` 📖	CompOp	—

MeasureTheory.Measure.IsUnifLocDoublingMeasure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`volume_prod` 📖	mathematical	—	`IsUnifLocDoublingMeasure` `Prod.pseudoMetricSpaceMax` `MeasureTheory.MeasureSpace.toMeasurableSpace` `MeasureTheory.Measure.prod.measureSpace` `MeasureTheory.MeasureSpace.volume`	—	`IsUnifLocDoublingMeasure.prod`

MeasureTheory.Measure.fst

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsFiniteMeasure` 📖	mathematical	—	`MeasureTheory.IsFiniteMeasure` `MeasureTheory.Measure.fst`	—	`eq_1` `MeasureTheory.Measure.isFiniteMeasure_map`
`instIsProbabilityMeasure` 📖	mathematical	—	`MeasureTheory.IsProbabilityMeasure` `MeasureTheory.Measure.fst`	—	`MeasureTheory.Measure.fst_univ` `MeasureTheory.IsProbabilityMeasure.measure_univ`
`instIsZeroOrProbabilityMeasure` 📖	mathematical	—	`MeasureTheory.IsZeroOrProbabilityMeasure` `MeasureTheory.Measure.fst`	—	`MeasureTheory.eq_zero_or_isProbabilityMeasure` `MeasureTheory.Measure.fst_zero` `MeasureTheory.instIsZeroOrProbabilityMeasureOfNatMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `instIsProbabilityMeasure`

MeasureTheory.Measure.prod

Definitions

Name	Category	Theorems
`measureSpace` 📖	CompOp	66 math math: `NumberField.mixedEmbedding.integral_comp_polarSpaceCoord_symm`, `NumberField.mixedEmbedding.fundamentalDomain_integerLattice`, `NumberField.mixedEmbedding.lintegral_comp_polarCoord_symm`, `MeasureTheory.Measure.IsUnifLocDoublingMeasure.volume_prod`, `Complex.integral_comp_pi_polarCoord_symm`, `MeasureTheory.Measure.instIsFiniteMeasureOnCompactsProdVolume`, `MeasureTheory.Measure.instIsLocallyFiniteMeasureProdVolume`, `NumberField.mixedEmbedding.instIsAddHaarMeasureMixedSpaceVolume`, `NumberField.mixedEmbedding.instNoAtomsMixedSpaceVolume`, `NumberField.mixedEmbedding.convexBodyLT_volume`, `MeasureTheory.volume_preserving_piFinsetUnion`, `NumberField.mixedEmbedding.fundamentalCone.volume_frontier_normLeOne`, `NumberField.mixedEmbedding.iUnion_negAt_plusPart_ae`, `MeasureTheory.Measure.instSFiniteProdVolume`, `NumberField.mixedEmbedding.fundamentalCone.volume_interior_eq_volume_closure`, `Complex.integral_comp_polarCoord_symm`, `NumberField.mixedEmbedding.convexBodySum_volume_eq_zero_of_le_zero`, `MeasureTheory.volume_preserving_prodAssoc`, `lintegral_comp_pi_polarCoord_symm`, `NumberField.mixedEmbedding.fundamentalDomain_idealLattice`, `MeasureTheory.Measure.instIsFiniteMeasureProdVolume`, `MeasureTheory.volume_preserving_piFinSuccAbove`, `integral_comp_polarCoord_symm`, `NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed`, `NumberField.mixedEmbedding.covolume_idealLattice`, `NumberField.mixedEmbedding.volume_preserving_negAt`, `MeasureTheory.hausdorffMeasure_prod_real`, `NumberField.mixedEmbedding.volume_preserving_mixedSpaceToRealMixedSpace_symm`, `MeasureTheory.Measure.volume_eq_prod`, `Complex.lintegral_comp_polarCoord_symm`, `Complex.volume_preserving_equiv_real_prod`, `NumberField.mixedEmbedding.covolume_integerLattice`, `NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis`, `NumberField.mixedEmbedding.volume_negAt_plusPart`, `NumberField.mixedEmbedding.convexBodyLT'_volume`, `MeasureTheory.Measure.instSigmaFiniteProdVolume`, `MeasureTheory.volume_preserving_piFinTwo`, `NumberField.mixedEmbedding.volume_eq_two_pow_mul_two_pi_pow_mul_integral`, `NumberField.mixedEmbedding.volume_preserving_homeoRealMixedSpacePolarSpace`, `NumberField.mixedEmbedding.volume_eq_zero`, `NumberField.mixedEmbedding.lintegral_comp_polarCoordReal_symm`, `MeasureTheory.volume_measurePreserving_arrowProdEquivProdArrow`, `instIsAddHaarMeasureProdRealVolume`, `lintegral_comp_polarCoord_symm`, `NumberField.mixedEmbedding.polarCoordReal_symm_target_ae_eq_univ`, `polarCoord_source_ae_eq_univ`, `NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis`, `Complex.lintegral_comp_pi_polarCoord_symm`, `NumberField.mixedEmbedding.instIsAddHaarMeasureRealMixedSpaceVolume`, `pi_polarCoord_symm_target_ae_eq_univ`, `NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm`, `NumberField.mixedEmbedding.fundamentalCone.volume_normLeOne`, `MeasureTheory.volume_preserving_finTwoArrow`, `MeasureTheory.Measure.instIsProbabilityMeasureProdVolume`, `NumberField.mixedEmbedding.volume_eq_two_pi_pow_mul_integral`, `NumberField.mixedEmbedding.convexBodySum_volume`, `NumberField.mixedEmbedding.integral_comp_polarCoord_symm`, `MeasureTheory.volume_measurePreserving_sumPiEquivProdPi`, `MeasureTheory.volume_preserving_piEquivPiSubtypeProd`, `MeasureTheory.volume_measurePreserving_sumPiEquivProdPi_symm`, `NumberField.mixedEmbedding.integral_comp_polarCoordReal_symm`, `integral_comp_pi_polarCoord_symm`, `NumberField.mixedEmbedding.volume_fundamentalDomain_stdBasis`, `NumberField.mixedEmbedding.volume_eq_two_pow_mul_volume_plusPart`, `MeasureTheory.Measure.instIsOpenPosMeasureProdVolumeOfSFinite`, `NumberField.mixedEmbedding.lintegral_comp_polarSpaceCoord_symm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsFiniteMeasure` 📖	mathematical	—	`MeasureTheory.IsFiniteMeasure` `Prod.instMeasurableSpace` `MeasureTheory.Measure.prod`	—	`Set.univ_prod_univ` `MeasureTheory.Measure.prod_prod` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `Ne.lt_top` `ENNReal.mul_ne_top` `MeasureTheory.measure_ne_top`
`instIsFiniteMeasureOnCompacts` 📖	mathematical	—	`MeasureTheory.IsFiniteMeasureOnCompacts` `Prod.instMeasurableSpace` `instTopologicalSpaceProd` `MeasureTheory.Measure.prod`	—	`MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Set.subset_prod` `MeasureTheory.Measure.prod_prod_le` `ENNReal.mul_lt_top` `IsCompact.measure_lt_top` `IsCompact.image` `continuous_fst` `continuous_snd`
`instIsLocallyFiniteMeasure` 📖	mathematical	—	`MeasureTheory.IsLocallyFiniteMeasure` `Prod.instMeasurableSpace` `instTopologicalSpaceProd` `MeasureTheory.Measure.prod`	—	`nhds_prod_eq` `MeasureTheory.Measure.FiniteAtFilter.prod` `MeasureTheory.Measure.finiteAt_nhds`
`instIsOpenPosMeasure` 📖	mathematical	—	`MeasureTheory.Measure.IsOpenPosMeasure` `instTopologicalSpaceProd` `Prod.instMeasurableSpace` `MeasureTheory.Measure.prod`	—	`isOpen_prod_iff` `ne_of_gt` `lt_of_lt_of_le` `MeasureTheory.Measure.prod_prod` `ENNReal.instCanonicallyOrderedAdd` `ENNReal.instNoZeroDivisors` `IsOpen.measure_pos` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass`
`instIsProbabilityMeasure` 📖	mathematical	—	`MeasureTheory.IsProbabilityMeasure` `Prod.instMeasurableSpace` `MeasureTheory.Measure.prod`	—	`Set.univ_prod_univ` `MeasureTheory.Measure.prod_prod` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `MeasureTheory.IsProbabilityMeasure.measure_univ` `mul_one`
`instNoAtoms_fst` 📖	mathematical	—	`MeasureTheory.NoAtoms` `Prod.instMeasurableSpace` `MeasureTheory.Measure.prod`	—	`nonpos_iff_eq_zero` `ENNReal.instCanonicallyOrderedAdd` `Set.singleton_prod_singleton` `MeasureTheory.Measure.prod_prod_le` `MeasureTheory.NoAtoms.measure_singleton` `MulZeroClass.zero_mul`
`instNoAtoms_snd` 📖	mathematical	—	`MeasureTheory.NoAtoms` `Prod.instMeasurableSpace` `MeasureTheory.Measure.prod`	—	`nonpos_iff_eq_zero` `ENNReal.instCanonicallyOrderedAdd` `Set.singleton_prod_singleton` `MeasureTheory.Measure.prod_prod_le` `MeasureTheory.NoAtoms.measure_singleton` `MulZeroClass.mul_zero`
`instSFinite` 📖	mathematical	—	`MeasureTheory.SFinite` `Prod.instMeasurableSpace` `MeasureTheory.Measure.prod`	—	`MeasureTheory.sum_sfiniteSeq` `MeasureTheory.Measure.prod_sum` `instCountableNat` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `MeasureTheory.isFiniteMeasure_sfiniteSeq` `MeasureTheory.instSFiniteSumOfCountable` `instCountableProd` `instSigmaFinite`
`instSigmaFinite` 📖	mathematical	—	`MeasureTheory.SigmaFinite` `Prod.instMeasurableSpace` `MeasureTheory.Measure.prod`	—	`MeasureTheory.Measure.FiniteSpanningSetsIn.sigmaFinite`

MeasureTheory.Measure.snd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsFiniteMeasure` 📖	mathematical	—	`MeasureTheory.IsFiniteMeasure` `MeasureTheory.Measure.snd`	—	`eq_1` `MeasureTheory.Measure.isFiniteMeasure_map`
`instIsProbabilityMeasure` 📖	mathematical	—	`MeasureTheory.IsProbabilityMeasure` `MeasureTheory.Measure.snd`	—	`MeasureTheory.Measure.snd_univ` `MeasureTheory.IsProbabilityMeasure.measure_univ`
`instIsZeroOrProbabilityMeasure` 📖	mathematical	—	`MeasureTheory.IsZeroOrProbabilityMeasure` `MeasureTheory.Measure.snd`	—	`MeasureTheory.eq_zero_or_isProbabilityMeasure` `MeasureTheory.Measure.snd_zero` `MeasureTheory.instIsZeroOrProbabilityMeasureOfNatMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `instIsProbabilityMeasure`

MeasureTheory.MeasurePreserving

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod` 📖	mathematical	`MeasureTheory.MeasurePreserving`	`Prod.instMeasurableSpace` `MeasureTheory.Measure.prod`	—	`Measurable.comp` `measurable` `measurable_snd` `skew_product` `MeasureTheory.ae_of_all` `MeasureTheory.Measure.instOuterMeasureClass` `map_eq`
`skew_product` 📖	mathematical	`MeasureTheory.MeasurePreserving` `Measurable` `Prod.instMeasurableSpace` `Filter.Eventually` `MeasureTheory.Measure` `MeasureTheory.Measure.map` `MeasureTheory.ae` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	`MeasureTheory.Measure.prod`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Measurable.prodMk` `Measurable.comp` `measurable` `measurable_fst` `eq_zero_or_neZero` `MeasureTheory.Measure.zero_prod` `MeasureTheory.Measure.map_zero` `map_eq` `Filter.Eventually.exists` `MeasureTheory.Measure.ae.neBot` `MeasureTheory.Measure.instSFiniteMap` `MeasureTheory.Measure.ext` `MeasureTheory.Measure.map_apply` `MeasureTheory.Measure.prod_apply` `lintegral_comp` `measurable_measure_prodMk_left` `MeasureTheory.lintegral_congr_ae` `Filter.mp_mem` `Filter.univ_mem'` `Measurable.of_uncurry_left` `measurable_prodMk_left` `Set.preimage_preimage`

MeasureTheory.NullMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_fst` 📖	mathematical	`MeasureTheory.NullMeasurable`	`Prod.instMeasurableSpace` `MeasureTheory.Measure.prod`	—	`comp_quasiMeasurePreserving` `MeasureTheory.Measure.quasiMeasurePreserving_fst`
`comp_snd` 📖	mathematical	`MeasureTheory.NullMeasurable`	`Prod.instMeasurableSpace` `MeasureTheory.Measure.prod`	—	`comp_quasiMeasurePreserving` `MeasureTheory.Measure.quasiMeasurePreserving_snd`

MeasureTheory.NullMeasurableSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`left_of_prod` 📖	—	`MeasureTheory.NullMeasurableSet` `Prod.instMeasurableSpace` `SProd.sprod` `Set` `Set.instSProd` `MeasureTheory.Measure.prod`	—	—	`right_of_prod` `Set.preimage_swap_prod` `preimage` `MeasureTheory.MeasurePreserving.quasiMeasurePreserving` `MeasureTheory.Measure.measurePreserving_swap`
`of_preimage_fst` 📖	—	`MeasureTheory.NullMeasurableSet` `Prod.instMeasurableSpace` `Set.preimage` `MeasureTheory.Measure.prod`	—	—	`left_of_prod` `Set.prod_univ` `MeasureTheory.Measure.instNeZeroENNRealCoeSetUniv`
`of_preimage_snd` 📖	—	`MeasureTheory.NullMeasurableSet` `Prod.instMeasurableSpace` `Set.preimage` `MeasureTheory.Measure.prod`	—	—	`right_of_prod` `Set.univ_prod` `MeasureTheory.Measure.instNeZeroENNRealCoeSetUniv`
`prod` 📖	mathematical	`MeasureTheory.NullMeasurableSet`	`Prod.instMeasurableSpace` `SProd.sprod` `Set` `Set.instSProd` `MeasureTheory.Measure.prod`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasurableSet.prod` `MeasureTheory.Measure.set_prod_ae_eq`
`right_of_prod` 📖	—	`MeasureTheory.NullMeasurableSet` `Prod.instMeasurableSpace` `SProd.sprod` `Set` `Set.instSProd` `MeasureTheory.Measure.prod`	—	—	`MeasureTheory.Measure.instOuterMeasureClass` `Filter.Frequently.exists` `Filter.Frequently.and_eventually` `MeasureTheory.frequently_ae_iff` `MeasureTheory.Measure.ae_ae_eq_curry_of_prod` `measurable_prodMk_left` `Set.mk_preimage_prod_right`

MeasureTheory.QuasiMeasurePreserving

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fst` 📖	—	`MeasureTheory.Measure.QuasiMeasurePreserving` `Prod.instMeasurableSpace` `MeasureTheory.Measure.prod`	—	—	`MeasureTheory.Measure.QuasiMeasurePreserving.comp` `MeasureTheory.Measure.quasiMeasurePreserving_fst`
`prodMap` 📖	mathematical	`MeasureTheory.Measure.QuasiMeasurePreserving`	`Prod.instMeasurableSpace` `MeasureTheory.Measure.prod`	—	`Measurable.prodMap` `MeasureTheory.Measure.QuasiMeasurePreserving.measurable` `MeasureTheory.Measure.map_prod_map` `MeasureTheory.Measure.AbsolutelyContinuous.prod` `MeasureTheory.Measure.QuasiMeasurePreserving.absolutelyContinuous`
`prod_of_left` 📖	mathematical	`Measurable` `Prod.instMeasurableSpace` `Filter.Eventually` `MeasureTheory.Measure.QuasiMeasurePreserving` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	`MeasureTheory.Measure.prod`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.prod_swap` `MeasureTheory.Measure.QuasiMeasurePreserving.comp` `prod_of_right` `Measurable.comp` `measurable_swap` `MeasureTheory.MeasurePreserving.quasiMeasurePreserving` `MeasureTheory.MeasurePreserving.symm` `Measurable.measurePreserving`
`prod_of_right` 📖	mathematical	`Measurable` `Prod.instMeasurableSpace` `Filter.Eventually` `MeasureTheory.Measure.QuasiMeasurePreserving` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	`MeasureTheory.Measure.prod`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.map_apply` `MeasureTheory.Measure.prod_apply` `Set.preimage_preimage` `MeasureTheory.lintegral_congr_ae` `Filter.Eventually.mono` `MeasureTheory.Measure.QuasiMeasurePreserving.preimage_null` `MeasureTheory.lintegral_zero`
`snd` 📖	—	`MeasureTheory.Measure.QuasiMeasurePreserving` `Prod.instMeasurableSpace` `MeasureTheory.Measure.prod`	—	—	`MeasureTheory.Measure.QuasiMeasurePreserving.comp` `MeasureTheory.Measure.quasiMeasurePreserving_snd`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`measurable_measure_prodMk_left` 📖	mathematical	`MeasurableSet` `Prod.instMeasurableSpace`	`Measurable` `ENNReal` `ENNReal.measurableSpace` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Set.preimage`	—	`MeasureTheory.sum_sfiniteSeq` `MeasureTheory.Measure.sum_apply_of_countable` `instCountableNat` `Measurable.ennreal_tsum` `measurable_measure_prodMk_left_finite` `MeasureTheory.isFiniteMeasure_sfiniteSeq`
`measurable_measure_prodMk_left_finite` 📖	mathematical	`MeasurableSet` `Prod.instMeasurableSpace`	`Measurable` `ENNReal` `ENNReal.measurableSpace` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Set.preimage`	—	`MeasurableSpace.induction_on_inter` `generateFrom_prod` `isPiSystem_prod` `MeasureTheory.measure_empty` `MeasureTheory.Measure.instOuterMeasureClass` `Set.mk_preimage_prod_right_eq_if` `MeasureTheory.measure_if` `Measurable.indicator` `measurable_const` `MeasureTheory.measure_compl` `measurable_prodMk_left` `MeasureTheory.measure_ne_top` `Measurable.const_sub` `MeasurableSub₂.toMeasurableSub` `ENNReal.instMeasurableSub₂` `Set.preimage_iUnion` `MeasureTheory.measure_iUnion` `instCountableNat` `Pairwise.mono` `Disjoint.preimage` `Measurable.ennreal_tsum`
`measurable_measure_prodMk_right` 📖	mathematical	`MeasurableSet` `Prod.instMeasurableSpace`	`Measurable` `ENNReal` `ENNReal.measurableSpace` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Set.preimage`	—	`measurable_measure_prodMk_left` `measurableSet_swap_iff`

---

← Back to Index