Prod

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

Statistics

Metric	Count
Definitions	0
Theorems comp_fst, comp_fst_iff, comp_snd, comp_snd_iff, integral_prod_right', of_comp_fst, of_comp_snd, prodMk_left, prodMk_right, prod_swap, comp_fst, comp_fst_iff, comp_snd, comp_snd_iff, integral_norm_prod_left, integral_norm_prod_right, integral_prod_left, integral_prod_right, mul_prod, of_comp_fst, of_comp_snd, op_fst_snd, prod_left_ae, prod_right_ae, smul_prod, swap, swap, integrable_measure_prodMk_left, integral_prod_left, integral_prod_left', integral_prod_right, integral_prod_right', continuous_integral_integral, hasFiniteIntegral_prod_iff, hasFiniteIntegral_prod_iff', integrable_continuousLinearMap_prod, integrable_continuousLinearMap_prod', integrable_prod_iff, integrable_prod_iff', integrable_swap_iff, integral_continuousLinearMap_prod, integral_continuousLinearMap_prod', integral_fn_integral_add, integral_fn_integral_sub, integral_fun_fst, integral_fun_snd, integral_integral, integral_integral_add, integral_integral_add', integral_integral_sub, integral_integral_sub', integral_integral_swap, integral_integral_swap_of_hasCompactSupport, integral_integral_symm, integral_prod, integral_prod_mul, integral_prod_smul, integral_prod_swap, integral_prod_symm, intervalIntegral_integral_swap, lintegral_fn_integral_sub, setIntegral_prod, setIntegral_prod_mul, setIntegral_prod_swap, measurableSet_integrable	65
Total	65

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_integral_integral 📖	mathematical	—	Continuous AEEqFun Prod.instMeasurableSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Measure.prod AddSubgroup AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike Lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Lp.instNormedAddCommGroup fact_one_le_one_ennreal integral AEEqFun.cast	—	SeminormedAddCommGroup.toIsTopologicalAddGroup fact_one_le_one_ennreal continuous_iff_continuousAt tendsto_integral_of_L1 Integrable.integral_prod_left L1.integrable_coeFn Filter.Eventually.of_forall lintegral_fn_integral_sub tendsto_of_tendsto_of_tendsto_of_le_of_le ENNReal.instOrderTopology tendsto_const_nhds StronglyMeasurable.enorm StronglyMeasurable.sub IsTopologicalAddGroup.to_continuousSub Lp.stronglyMeasurable lintegral_prod Measurable.aemeasurable Filter.Tendsto.comp Continuous.tendsto ENNReal.continuous_ofReal tendsto_iff_norm_sub_tendsto_zero Filter.tendsto_id zero_le ENNReal.instCanonicallyOrderedAdd lintegral_mono enorm_integral_le_lintegral_enorm
hasFiniteIntegral_prod_iff 📖	mathematical	StronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Prod.instMeasurableSpace	HasFiniteIntegral ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddGroup.toContinuousENorm Measure.prod Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass Real NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Norm.norm NormedAddCommGroup.toNorm	—	Measure.instOuterMeasureClass lintegral_prod Measurable.aemeasurable StronglyMeasurable.enorm Filter.univ_mem' norm_nonneg integral_eq_lintegral_of_nonneg_ae StronglyMeasurable.aestronglyMeasurable StronglyMeasurable.comp_measurable StronglyMeasurable.norm measurable_prodMk_left Real.enorm_eq_ofReal ENNReal.toReal_nonneg ofReal_norm_eq_enorm ae_lt_top Measurable.lintegral_prod_right' LT.lt.ne lintegral_congr_ae Filter.mp_mem ENNReal.ofReal_toReal lt_top_iff_ne_top
hasFiniteIntegral_prod_iff' 📖	mathematical	AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Prod.instMeasurableSpace Measure.prod	HasFiniteIntegral ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddGroup.toContinuousENorm Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass Real NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Norm.norm NormedAddCommGroup.toNorm	—	Measure.instOuterMeasureClass hasFiniteIntegral_congr hasFiniteIntegral_prod_iff Filter.eventually_congr Filter.mp_mem Measure.ae_ae_of_ae_prod Filter.EventuallyEq.symm Filter.univ_mem' integral_congr_ae Filter.EventuallyEq.fun_comp
integrable_continuousLinearMap_prod 📖	mathematical	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	Prod.instMeasurableSpace DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceProd Prod.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Prod.instModule NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike Measure.prod	—	integrable_continuousLinearMap_prod' ContinuousLinearMap.integrable_comp RingHomIsometric.ids RingHomCompTriple.ids
integrable_continuousLinearMap_prod' 📖	mathematical	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike ContinuousLinearMap.comp instTopologicalSpaceProd Prod.instAddCommMonoid Prod.instModule RingHomCompTriple.ids ContinuousLinearMap.inl ContinuousLinearMap.inr	Prod.instMeasurableSpace Measure.prod	—	RingHomCompTriple.ids ContinuousLinearMap.comp_inl_add_comp_inr Integrable.add IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup Integrable.comp_fst IsZeroOrProbabilityMeasure.toIsFiniteMeasure instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure Integrable.comp_snd instSFiniteOfSigmaFinite IsFiniteMeasure.toSigmaFinite
integrable_prod_iff 📖	mathematical	AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Prod.instMeasurableSpace Measure.prod	Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass Real Real.pseudoMetricSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Norm.norm NormedAddCommGroup.toNorm	—	Measure.instOuterMeasureClass AEStronglyMeasurable.prodMk_left AEStronglyMeasurable.integral_prod_right' AEStronglyMeasurable.norm
integrable_prod_iff' 📖	mathematical	AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Prod.instMeasurableSpace Measure.prod	Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass Real Real.pseudoMetricSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Norm.norm NormedAddCommGroup.toNorm	—	Measure.instOuterMeasureClass integrable_swap_iff integrable_prod_iff AEStronglyMeasurable.prod_swap
integrable_swap_iff 📖	mathematical	—	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace Measure.prod	—	MeasurePreserving.integrable_comp_emb Measure.measurePreserving_swap MeasurableEquiv.measurableEmbedding
integral_continuousLinearMap_prod 📖	mathematical	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	integral Prod.instMeasurableSpace Measure.prod DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceProd Prod.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Prod.instModule NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ContinuousLinearMap.comp RingHomCompTriple.ids ContinuousLinearMap.inl ContinuousLinearMap.inr	—	integral_continuousLinearMap_prod' ContinuousLinearMap.integrable_comp RingHomIsometric.ids RingHomCompTriple.ids
integral_continuousLinearMap_prod' 📖	mathematical	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike ContinuousLinearMap.comp instTopologicalSpaceProd Prod.instAddCommMonoid Prod.instModule RingHomCompTriple.ids ContinuousLinearMap.inl ContinuousLinearMap.inr	integral Prod.instMeasurableSpace Measure.prod AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	RingHomCompTriple.ids ContinuousLinearMap.comp_inl_add_comp_inr MemLp.integrable le_rfl Measure.prod.instIsFiniteMeasure IsZeroOrProbabilityMeasure.toIsFiniteMeasure instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure MemLp.comp_fst memLp_one_iff_integrable MemLp.comp_snd instSFiniteOfSigmaFinite IsFiniteMeasure.toSigmaFinite integral_add integral_prod integral_const probReal_univ one_smul
integral_fn_integral_add 📖	mathematical	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace Measure.prod	integral AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	integral_congr_ae Filter.mp_mem Measure.instOuterMeasureClass Integrable.prod_right_ae Filter.univ_mem' integral_add
integral_fn_integral_sub 📖	mathematical	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace Measure.prod	integral SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	integral_congr_ae Filter.mp_mem Measure.instOuterMeasureClass Integrable.prod_right_ae Filter.univ_mem' integral_sub
integral_fun_fst 📖	mathematical	—	integral Prod.instMeasurableSpace Measure.prod Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField Measure.real Set.univ	—	integral_prod_swap integral_fun_snd
integral_fun_snd 📖	mathematical	—	integral Prod.instMeasurableSpace Measure.prod Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField Measure.real Set.univ	—	one_smul integral_const Real.instCompleteSpace mul_one integral_prod_smul
integral_integral 📖	mathematical	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace Measure.prod	integral	—	integral_prod
integral_integral_add 📖	mathematical	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace Measure.prod	integral AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	integral_fn_integral_add integral_add Integrable.integral_prod_left
integral_integral_add' 📖	mathematical	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace Measure.prod	integral Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	integral_integral_add
integral_integral_sub 📖	mathematical	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace Measure.prod	integral SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	integral_fn_integral_sub integral_sub Integrable.integral_prod_left
integral_integral_sub' 📖	mathematical	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace Measure.prod	integral Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	integral_integral_sub
integral_integral_swap 📖	mathematical	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace Measure.prod	integral	—	integral_integral integral_prod_symm
integral_integral_swap_of_hasCompactSupport 📖	mathematical	Continuous instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup HasCompactSupport NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	integral	—	IsCompact.measure_lt_top IsCompact.image continuous_fst continuous_snd setIntegral_eq_integral_of_forall_compl_eq_zero Mathlib.Tactic.Contrapose.contrapose₂ Set.mem_image_of_mem subset_tsupport integral_zero integral_integral_swap instSFiniteOfSigmaFinite IsFiniteMeasure.toSigmaFinite Restrict.isFiniteMeasure integrableOn_iff_integrable_of_support_subset PseudoEMetricSpace.pseudoMetrizableSpace StronglyMeasurable.aestronglyMeasurable HasCompactSupport.stronglyMeasurable_of_prod Continuous.bounded_above_of_compact_support HasFiniteIntegral.of_bounded isFiniteMeasureRestrict Measure.prod.instIsFiniteMeasure Filter.Eventually.of_forall Measure.instOuterMeasureClass
integral_integral_symm 📖	mathematical	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace Measure.prod	integral	—	integral_prod_symm Integrable.swap
integral_prod 📖	mathematical	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace Measure.prod	integral	—	Integrable.induction integral_indicator measurable_prodMk_left setIntegral_const integral_smul_const integral_toReal Measurable.aemeasurable measurable_measure_prodMk_left Measure.ae_measure_lt_top LT.lt.ne Measure.prod_apply integral_add' integral_integral_add' isClosed_eq SeminormedAddCommGroup.toIsTopologicalAddGroup fact_one_le_one_ennreal TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace continuous_integral continuous_integral_integral Measure.instOuterMeasureClass integral_congr_ae Filter.EventuallyEq.symm Filter.mp_mem Measure.ae_ae_of_ae_prod Filter.univ_mem' ae_eq_symm integral_def
integral_prod_mul 📖	mathematical	—	integral NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Prod.instMeasurableSpace Measure.prod Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing	—	integral_prod_smul
integral_prod_smul 📖	mathematical	—	integral Prod.instMeasurableSpace Measure.prod SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing InnerProductSpace.toNormedSpace Real Real.instRCLike RCLike.toInnerProductSpaceReal	—	integral_prod integral_smul NormedSpace.toNormSMulClass IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace integral_smul_const Mathlib.Tactic.Contrapose.contrapose₂ Integrable.smul_prod integral_undef zero_smul smul_zero integral_def
integral_prod_swap 📖	mathematical	—	integral Prod.instMeasurableSpace Measure.prod	—	MeasurePreserving.integral_comp Measure.measurePreserving_swap MeasurableEquiv.measurableEmbedding
integral_prod_symm 📖	mathematical	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace Measure.prod	integral	—	integral_prod_swap integral_prod Integrable.swap
intervalIntegral_integral_swap 📖	mathematical	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Real Prod.instMeasurableSpace MeasureSpace.toMeasurableSpace Real.measureSpace Measure.prod Measure.restrict MeasureSpace.volume Set.uIoc Real.linearOrder	intervalIntegral integral	—	le_total intervalIntegral.integral_of_le integral_integral_swap instSFiniteRestrict instSFiniteOfSigmaFinite Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real Real.borelSpace SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal Set.uIoc_of_le intervalIntegral.integral_of_ge Set.uIoc_of_ge integral_neg
lintegral_fn_integral_sub 📖	mathematical	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace Measure.prod	lintegral integral SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	lintegral_congr_ae Filter.mp_mem Measure.instOuterMeasureClass Integrable.prod_right_ae Filter.univ_mem' integral_sub
setIntegral_prod 📖	mathematical	IntegrableOn Prod.instMeasurableSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup SProd.sprod Set Set.instSProd Measure.prod	integral Measure.restrict	—	Measure.prod_restrict integral_prod instSFiniteRestrict
setIntegral_prod_mul 📖	mathematical	—	integral NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Prod.instMeasurableSpace Measure.restrict Measure.prod SProd.sprod Set Set.instSProd Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing	—	Measure.prod_restrict integral_prod_mul instSFiniteRestrict
setIntegral_prod_swap 📖	mathematical	—	integral Prod.instMeasurableSpace Measure.restrict Measure.prod SProd.sprod Set Set.instSProd	—	Measure.prod_restrict integral_prod_swap instSFiniteRestrict

MeasureTheory.AEStronglyMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_fst 📖	mathematical	MeasureTheory.AEStronglyMeasurable	Prod.instMeasurableSpace MeasureTheory.Measure.prod	—	comp_quasiMeasurePreserving MeasureTheory.Measure.quasiMeasurePreserving_fst
comp_fst_iff 📖	mathematical	—	MeasureTheory.AEStronglyMeasurable Prod.instMeasurableSpace MeasureTheory.Measure.prod	—	of_comp_fst comp_fst
comp_snd 📖	mathematical	MeasureTheory.AEStronglyMeasurable	Prod.instMeasurableSpace MeasureTheory.Measure.prod	—	comp_quasiMeasurePreserving MeasureTheory.Measure.quasiMeasurePreserving_snd
comp_snd_iff 📖	mathematical	—	MeasureTheory.AEStronglyMeasurable Prod.instMeasurableSpace MeasureTheory.Measure.prod	—	of_comp_snd comp_snd
integral_prod_right' 📖	mathematical	MeasureTheory.AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Prod.instMeasurableSpace MeasureTheory.Measure.prod	MeasureTheory.integral	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.StronglyMeasurable.integral_prod_right' Filter.mp_mem MeasureTheory.Measure.ae_ae_of_ae_prod Filter.univ_mem' MeasureTheory.integral_congr_ae
of_comp_fst 📖	—	MeasureTheory.AEStronglyMeasurable Prod.instMeasurableSpace MeasureTheory.Measure.prod	—	—	of_comp_snd prod_swap
of_comp_snd 📖	—	MeasureTheory.AEStronglyMeasurable Prod.instMeasurableSpace MeasureTheory.Measure.prod	—	—	Filter.Eventually.exists MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.ae.neBot prodMk_left
prodMk_left 📖	mathematical	MeasureTheory.AEStronglyMeasurable Prod.instMeasurableSpace MeasureTheory.Measure.prod	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.ae_ae_of_ae_prod Filter.univ_mem' MeasureTheory.StronglyMeasurable.comp_measurable measurable_prodMk_left
prodMk_right 📖	mathematical	MeasureTheory.AEStronglyMeasurable Prod.instMeasurableSpace MeasureTheory.Measure.prod	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	prodMk_left prod_swap
prod_swap 📖	—	MeasureTheory.AEStronglyMeasurable Prod.instMeasurableSpace MeasureTheory.Measure.prod	—	—	comp_measurable MeasureTheory.Measure.prod_swap measurable_swap

MeasureTheory.Integrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_fst 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	Prod.instMeasurableSpace MeasureTheory.Measure.prod	—	MeasureTheory.memLp_one_iff_integrable MeasureTheory.MemLp.comp_fst
comp_fst_iff 📖	mathematical	—	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace MeasureTheory.Measure.prod	—	of_comp_fst MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite comp_fst
comp_snd 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	Prod.instMeasurableSpace MeasureTheory.Measure.prod	—	MeasureTheory.memLp_one_iff_integrable MeasureTheory.MemLp.comp_snd
comp_snd_iff 📖	mathematical	—	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace MeasureTheory.Measure.prod	—	of_comp_snd comp_snd
integral_norm_prod_left 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace MeasureTheory.Measure.prod	Real Real.pseudoMetricSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Norm.norm NormedAddCommGroup.toNorm	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.integrable_prod_iff aestronglyMeasurable
integral_norm_prod_right 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace MeasureTheory.Measure.prod	Real Real.pseudoMetricSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Norm.norm NormedAddCommGroup.toNorm	—	integral_norm_prod_left swap
integral_prod_left 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace MeasureTheory.Measure.prod	MeasureTheory.integral	—	mono integral_norm_prod_left MeasureTheory.AEStronglyMeasurable.integral_prod_right' aestronglyMeasurable Filter.Eventually.of_forall MeasureTheory.Measure.instOuterMeasureClass LE.le.trans_eq MeasureTheory.norm_integral_le_integral_norm Real.norm_of_nonneg MeasureTheory.integral_nonneg_of_ae Real.instIsOrderedAddMonoid IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal norm_nonneg
integral_prod_right 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace MeasureTheory.Measure.prod	MeasureTheory.integral	—	integral_prod_left swap
mul_prod 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing	Prod.instMeasurableSpace Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing MeasureTheory.Measure.prod	—	smul_prod NonUnitalSeminormedRing.isBoundedSMul
of_comp_fst 📖	—	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace MeasureTheory.Measure.prod	—	—	of_comp_snd swap
of_comp_snd 📖	—	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace MeasureTheory.Measure.prod	—	—	MeasureTheory.AEStronglyMeasurable.of_comp_snd MeasureTheory.AEStronglyMeasurable.enorm MeasureTheory.lintegral_prod MeasureTheory.lintegral_const
op_fst_snd 📖	mathematical	Continuous instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real Real.instLE Norm.norm NormedAddCommGroup.toNorm Real.instMul MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	Prod.instMeasurableSpace MeasureTheory.Measure.prod	—	Continuous.comp_aestronglyMeasurable₂ MeasureTheory.AEStronglyMeasurable.comp_fst MeasureTheory.AEStronglyMeasurable.comp_snd MeasureTheory.lintegral_mono_fn' le_refl LE.le.trans mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing Real.le_coe_toNNReal norm_nonneg MeasureTheory.lintegral_prod_le mul_assoc MeasureTheory.lintegral_const_mul' MeasureTheory.lintegral_mul_const' LT.lt.ne ENNReal.mul_lt_top ENNReal.ofReal_lt_top
prod_left_ae 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace MeasureTheory.Measure.prod	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.integrable_prod_iff' aestronglyMeasurable
prod_right_ae 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace MeasureTheory.Measure.prod	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	prod_left_ae swap
smul_prod 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	Prod.instMeasurableSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid MeasureTheory.Measure.prod	—	op_fst_snd ContinuousSMul.continuous_smul IsBoundedSMul.continuousSMul one_mul norm_smul_le
swap 📖	—	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace MeasureTheory.Measure.prod	—	—	MeasureTheory.integrable_swap_iff

MeasureTheory.IntegrableOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
swap 📖	—	MeasureTheory.IntegrableOn Prod.instMeasurableSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup SProd.sprod Set Set.instSProd MeasureTheory.Measure.prod	—	—	eq_1 MeasureTheory.Measure.prod_restrict MeasureTheory.Integrable.swap MeasureTheory.instSFiniteRestrict

MeasureTheory.Measure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integrable_measure_prodMk_left 📖	mathematical	MeasurableSet Prod.instMeasurableSpace	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing real Set.preimage	—	AEMeasurable.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace BorelSpace.opensMeasurable Real.borelSpace instSecondCountableTopologyReal Measurable.aemeasurable Measurable.ennreal_toReal measurable_measure_prodMk_left Real.enorm_eq_ofReal ENNReal.toReal_nonneg prod_apply MeasureTheory.lintegral_congr_ae Filter.mp_mem instOuterMeasureClass ae_measure_lt_top Filter.univ_mem' ENNReal.ofReal_toReal lt_top_iff_ne_top Ne.lt_top

MeasureTheory.StronglyMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integral_prod_left 📖	mathematical	MeasureTheory.StronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Prod.instMeasurableSpace	MeasureTheory.integral	—	integral_prod_right' comp_measurable measurable_swap
integral_prod_left' 📖	mathematical	MeasureTheory.StronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Prod.instMeasurableSpace	MeasureTheory.integral	—	integral_prod_right' comp_measurable measurable_swap
integral_prod_right 📖	mathematical	MeasureTheory.StronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Prod.instMeasurableSpace	MeasureTheory.integral	—	BorelSpace.opensMeasurable measurable PseudoEMetricSpace.pseudoMetrizableSpace Set.union_singleton separableSpace_range_union_singleton measurable_prodMk_left indicator Finset.Subset.trans Finset.filter_subset MeasureTheory.SimpleFunc.integral_eq_sum_of_subset Finset.stronglyMeasurable_fun_sum IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup smul_const IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Measurable.stronglyMeasurable instSecondCountableTopologyReal Real.borelSpace Measurable.ennreal_toReal measurable_measure_prodMk_left MeasureTheory.SimpleFunc.measurableSet_fiber measurableSet_integrable tendsto_pi_nhds MeasureTheory.Integrable.mono' MeasureTheory.Integrable.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.Integrable.norm MeasureTheory.SimpleFunc.aestronglyMeasurable Filter.univ_mem' MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.SimpleFunc.norm_approxOn_zero_le Set.indicator_of_mem MeasureTheory.SimpleFunc.integral_eq_integral MeasureTheory.tendsto_integral_of_dominated_convergence Filter.Eventually.of_forall MeasureTheory.SimpleFunc.tendsto_approxOn Measurable.of_uncurry_left subset_closure Set.indicator_of_notMem MeasureTheory.integral_undef T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat stronglyMeasurable_of_tendsto instIsCountablyGenerated_atTop OrderTopology.of_linearLocallyFinite instDiscreteTopologyNat TopologicalSpace.SecondCountableTopology.to_separableSpace TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace instCountableNat MeasureTheory.integral_def
integral_prod_right' 📖	mathematical	MeasureTheory.StronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Prod.instMeasurableSpace	MeasureTheory.integral	—	integral_prod_right

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurableSet_integrable 📖	mathematical	MeasureTheory.StronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Prod.instMeasurableSpace	MeasurableSet setOf MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	—	MeasureTheory.StronglyMeasurable.aestronglyMeasurable MeasureTheory.StronglyMeasurable.of_uncurry_left measurableSet_lt BorelSpace.opensMeasurable ENNReal.borelSpace ENNReal.instSecondCountableTopology OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology Measurable.lintegral_prod_right MeasureTheory.StronglyMeasurable.enorm measurable_const

---

← Back to Index