FiniteMeasureProd

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

Statistics

Metric	Count
Definitions prod, prod	2
Theorems map_fst_prod, map_prod_map, map_snd_prod, mass_prod, prod_apply, prod_apply_symm, prod_prod, prod_swap, prod_zero, toMeasure_prod, zero_prod, continuous_prod, map_fst_prod, map_prod_map, map_snd_prod, prod_apply, prod_apply_symm, prod_prod, prod_swap, toMeasure_prod	20
Total	22

MeasureTheory.FiniteMeasure

Definitions

Name	Category	Theorems
prod 📖	CompOp	11 math math: mass_prod, prod_swap, map_fst_prod, prod_apply, prod_apply_symm, prod_prod, map_snd_prod, map_prod_map, zero_prod, toMeasure_prod, prod_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_fst_prod 📖	mathematical	—	map Prod.instMeasurableSpace prod NNReal MeasureTheory.FiniteMeasure instSMul Algebra.toSMul instCommSemiringNNReal CommSemiring.toSemiring Algebra.id ENNReal ENNReal.instCommSemiring ENNReal.instAlgebraNNReal IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiringNNReal ENNReal.instMulActionNNReal DistribMulAction.toMulAction AddCommMonoid.toAddMonoid ENNReal.instAddCommMonoid Module.toDistribMulAction Semiring.toModule IsScalarTower.right DFunLike.coe Set instFunLike Set.univ	—	eq_of_forall_toMeasure_apply_eq IsScalarTower.left IsScalarTower.right MeasureTheory.Measure.map_fst_prod MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite isFiniteMeasure ennreal_coeFn_eq_coeFn_toMeasure
map_prod_map 📖	mathematical	Measurable	prod map Prod.instMeasurableSpace	—	MeasureTheory.Measure.map_prod_map MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite isFiniteMeasure
map_snd_prod 📖	mathematical	—	map Prod.instMeasurableSpace prod NNReal MeasureTheory.FiniteMeasure instSMul Algebra.toSMul instCommSemiringNNReal CommSemiring.toSemiring Algebra.id ENNReal ENNReal.instCommSemiring ENNReal.instAlgebraNNReal IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiringNNReal ENNReal.instMulActionNNReal DistribMulAction.toMulAction AddCommMonoid.toAddMonoid ENNReal.instAddCommMonoid Module.toDistribMulAction Semiring.toModule IsScalarTower.right DFunLike.coe Set instFunLike Set.univ	—	eq_of_forall_toMeasure_apply_eq IsScalarTower.left IsScalarTower.right MeasureTheory.Measure.map_snd_prod MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite isFiniteMeasure ennreal_coeFn_eq_coeFn_toMeasure
mass_prod 📖	mathematical	—	mass Prod.instMeasurableSpace prod NNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal	—	Set.univ_prod_univ ENNReal.toNNReal_mul MeasureTheory.Measure.prod_prod MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite isFiniteMeasure
prod_apply 📖	mathematical	MeasurableSet Prod.instMeasurableSpace	DFunLike.coe MeasureTheory.FiniteMeasure Set NNReal instFunLike prod ENNReal.toNNReal MeasureTheory.lintegral toMeasure MeasureTheory.Measure ENNReal MeasureTheory.Measure.instFunLike Set.preimage	—	MeasureTheory.Measure.prod_apply MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite isFiniteMeasure
prod_apply_symm 📖	mathematical	MeasurableSet Prod.instMeasurableSpace	DFunLike.coe MeasureTheory.FiniteMeasure Set NNReal instFunLike prod ENNReal.toNNReal MeasureTheory.lintegral toMeasure MeasureTheory.Measure ENNReal MeasureTheory.Measure.instFunLike Set.preimage	—	MeasureTheory.Measure.prod_apply_symm MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite isFiniteMeasure
prod_prod 📖	mathematical	—	DFunLike.coe MeasureTheory.FiniteMeasure Prod.instMeasurableSpace Set NNReal instFunLike prod SProd.sprod Set.instSProd Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal	—	MeasureTheory.Measure.prod_prod MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite isFiniteMeasure ENNReal.toNNReal_mul
prod_swap 📖	mathematical	—	map Prod.instMeasurableSpace prod	—	MeasureTheory.Measure.prod_swap MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite isFiniteMeasure
prod_zero 📖	mathematical	—	prod MeasureTheory.FiniteMeasure instZero Prod.instMeasurableSpace	—	mass_zero_iff mass_prod zero_mass MulZeroClass.mul_zero
toMeasure_prod 📖	mathematical	—	toMeasure Prod.instMeasurableSpace prod MeasureTheory.Measure.prod	—	—
zero_prod 📖	mathematical	—	prod MeasureTheory.FiniteMeasure instZero Prod.instMeasurableSpace	—	mass_zero_iff mass_prod zero_mass MulZeroClass.zero_mul

MeasureTheory.ProbabilityMeasure

Definitions

Name	Category	Theorems
prod 📖	CompOp	9 math math: map_prod_map, prod_prod, prod_swap, toMeasure_prod, map_fst_prod, continuous_prod, map_snd_prod, prod_apply_symm, prod_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_prod 📖	mathematical	—	Continuous MeasureTheory.ProbabilityMeasure Prod.instMeasurableSpace instTopologicalSpaceProd instTopologicalSpace Prod.opensMeasurableSpace secondCountableTopologyEither_of_right prod	—	Prod.opensMeasurableSpace secondCountableTopologyEither_of_right continuous_iff_continuousAt MeasurableSet.inter null_iff_toMeasure_null null_frontier_inter Set.prod_inter_prod IsPiSystem.tendsto_probabilityMeasure_of_tendsto_of_mem TopologicalSpace.instSecondCountableTopologyProd FirstCountableTopology.nhds_generated_countable TopologicalSpace.instFirstCountableTopologyProd TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology MeasureTheory.instPseudoMetrizableSpaceProbabilityMeasureOfSeparableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace MeasurableSet.prod Metric.isOpen_iff MeasureTheory.exists_null_frontier_thickening MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.sigmaFinite_of_locallyFinite MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure instIsProbabilityMeasureToMeasure measurableSet_ball Metric.thickening_singleton IsOpen.mem_nhds IsOpen.prod Metric.isOpen_ball dist_self Set.prod_mono Metric.ball_subset_ball LT.lt.le ball_prod_same prod_prod Filter.Tendsto.mul IsTopologicalSemiring.toContinuousMul NNReal.instIsTopologicalSemiring tendsto_measure_of_null_frontier_of_tendsto instHasOuterApproxClosedOfPseudoMetrizableSpace Filter.Tendsto.fst_nhds Filter.tendsto_id Filter.Tendsto.snd_nhds
map_fst_prod 📖	mathematical	—	map Prod.instMeasurableSpace prod Measurable.aemeasurable toMeasure measurable_fst	—	Measurable.aemeasurable measurable_fst IsScalarTower.right MeasureTheory.Measure.map_fst_prod MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure instIsProbabilityMeasureToMeasure MeasureTheory.IsProbabilityMeasure.measure_univ one_smul
map_prod_map 📖	mathematical	Measurable	prod map Measurable.aemeasurable toMeasure Prod.instMeasurableSpace Measurable.prodMap	—	Measurable.aemeasurable Measurable.prodMap MeasureTheory.Measure.map_prod_map MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure instIsProbabilityMeasureToMeasure
map_snd_prod 📖	mathematical	—	map Prod.instMeasurableSpace prod Measurable.aemeasurable toMeasure measurable_snd	—	Measurable.aemeasurable measurable_snd IsScalarTower.right MeasureTheory.Measure.map_snd_prod MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure instIsProbabilityMeasureToMeasure MeasureTheory.IsProbabilityMeasure.measure_univ one_smul
prod_apply 📖	mathematical	MeasurableSet Prod.instMeasurableSpace	DFunLike.coe MeasureTheory.ProbabilityMeasure Set NNReal instFunLike prod ENNReal.toNNReal MeasureTheory.lintegral toMeasure MeasureTheory.Measure ENNReal MeasureTheory.Measure.instFunLike Set.preimage	—	MeasureTheory.Measure.prod_apply MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure instIsProbabilityMeasureToMeasure
prod_apply_symm 📖	mathematical	MeasurableSet Prod.instMeasurableSpace	DFunLike.coe MeasureTheory.ProbabilityMeasure Set NNReal instFunLike prod ENNReal.toNNReal MeasureTheory.lintegral toMeasure MeasureTheory.Measure ENNReal MeasureTheory.Measure.instFunLike Set.preimage	—	MeasureTheory.Measure.prod_apply_symm MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure instIsProbabilityMeasureToMeasure
prod_prod 📖	mathematical	—	DFunLike.coe MeasureTheory.ProbabilityMeasure Prod.instMeasurableSpace Set NNReal instFunLike prod SProd.sprod Set.instSProd Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal	—	MeasureTheory.Measure.prod_prod MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure instIsProbabilityMeasureToMeasure ENNReal.toNNReal_mul
prod_swap 📖	mathematical	—	map Prod.instMeasurableSpace prod Measurable.aemeasurable toMeasure measurable_swap	—	Measurable.aemeasurable measurable_swap MeasureTheory.Measure.prod_swap MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure instIsProbabilityMeasureToMeasure
toMeasure_prod 📖	mathematical	—	toMeasure Prod.instMeasurableSpace prod MeasureTheory.Measure.prod	—	—

---

← Back to Index