CharacteristicFunction

📁 Source: Mathlib/Probability/Independence/CharacteristicFunction.lean

Statistics

Metric	Count
Definitions	0
Theorems charFunDual_map_add_eq_mul, charFun_map_add_eq_mul, iIndepFun_iff_charFunDual_pi, iIndepFun_iff_charFunDual_pi', iIndepFun_iff_charFun_pi, indepFun_iff_charFunDual_prod, indepFun_iff_charFunDual_prod', indepFun_iff_charFun_prod	8
Total	8

ProbabilityTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iIndepFun_iff_charFunDual_pi 📖	mathematical	CompleteSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup BorelSpace UniformSpace.toTopologicalSpace SecondCountableTopology AEMeasurable	iIndepFun MeasureTheory.charFunDual Pi.normedAddCommGroup Pi.normedSpace Real Real.normedField MeasurableSpace.pi MeasureTheory.Measure.map Finset.prod Complex CommRing.toCommMonoid Complex.commRing Finset.univ ContinuousLinearMap.comp Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.pseudoMetricSpace NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring NormedSpace.toModule Semiring.toModule RingHomCompTriple.ids ContinuousLinearMap.single	—	RingHomCompTriple.ids iIndepFun_iff_map_fun_eq_pi_map MeasureTheory.charFunDual_eq_pi_iff MeasureTheory.Measure.isFiniteMeasure_map MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure
iIndepFun_iff_charFunDual_pi' 📖	mathematical	CompleteSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup BorelSpace UniformSpace.toTopologicalSpace SecondCountableTopology AEMeasurable	iIndepFun MeasureTheory.charFunDual WithLp PiLp.normedAddCommGroup PiLp.normedSpace Real Real.normedField WithLp.measurableSpace MeasurableSpace.pi MeasureTheory.Measure.map WithLp.toLp Finset.prod Complex CommRing.toCommMonoid Complex.commRing Finset.univ ContinuousLinearMap.comp Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.pseudoMetricSpace NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring NormedSpace.toModule Semiring.toModule RingHomCompTriple.ids Pi.topologicalSpace Pi.addCommMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup PiLp PiLp.topologicalSpace WithLp.instAddCommGroup Pi.addCommGroup Pi.module WithLp.instModule ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids ContinuousLinearEquiv.symm PiLp.continuousLinearEquiv ContinuousLinearMap.single	—	RingHomCompTriple.ids RingHomInvPair.ids iIndepFun_iff_map_fun_eq_pi_map MeasureTheory.charFunDual_eq_pi_iff' MeasureTheory.Measure.isFiniteMeasure_map MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure AEMeasurable.map_map_of_aemeasurable Measurable.aemeasurable WithLp.measurable_toLp aemeasurable_pi_lambda Finite.to_countable Finite.of_fintype
iIndepFun_iff_charFun_pi 📖	mathematical	CompleteSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup BorelSpace UniformSpace.toTopologicalSpace SecondCountableTopology AEMeasurable	iIndepFun MeasureTheory.charFun WithLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat WithLp.measurableSpace MeasurableSpace.pi InnerProductSpace.toInner Real Real.instRCLike PiLp.seminormedAddCommGroup fact_one_le_two_ennreal PiLp.innerProductSpace MeasureTheory.Measure.map WithLp.toLp Finset.prod Complex CommRing.toCommMonoid Complex.commRing Finset.univ WithLp.ofLp	—	Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal iIndepFun_iff_map_fun_eq_pi_map MeasureTheory.charFun_eq_pi_iff MeasureTheory.Measure.isFiniteMeasure_map MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure AEMeasurable.map_map_of_aemeasurable Measurable.aemeasurable WithLp.measurable_toLp aemeasurable_pi_lambda Finite.to_countable Finite.of_fintype
indepFun_iff_charFunDual_prod 📖	mathematical	AEMeasurable	IndepFun MeasureTheory.charFunDual Prod.normedAddCommGroup Prod.normedSpace Real Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup Prod.instMeasurableSpace MeasureTheory.Measure.map Complex Complex.instMul ContinuousLinearMap.comp Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.pseudoMetricSpace NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring NormedSpace.toModule Semiring.toModule RingHomCompTriple.ids ContinuousLinearMap.inl ContinuousLinearMap.inr	—	RingHomCompTriple.ids indepFun_iff_map_prod_eq_prod_map_map MeasureTheory.charFunDual_eq_prod_iff MeasureTheory.Measure.isFiniteMeasure_map
indepFun_iff_charFunDual_prod' 📖	mathematical	AEMeasurable	IndepFun MeasureTheory.charFunDual WithLp WithLp.instProdNormedAddCommGroup WithLp.instProdNormedSpace Real NormedAddCommGroup.toSeminormedAddCommGroup Real.normedField WithLp.measurableSpace Prod.instMeasurableSpace MeasureTheory.Measure.map WithLp.toLp Complex Complex.instMul ContinuousLinearMap.comp Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.pseudoMetricSpace NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring NormedSpace.toModule Semiring.toModule RingHomCompTriple.ids instTopologicalSpaceProd Prod.instAddCommMonoid AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup WithLp.instProdTopologicalSpace WithLp.instAddCommGroup Prod.instAddCommGroup Prod.instModule WithLp.instModule ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids ContinuousLinearEquiv.symm WithLp.prodContinuousLinearEquiv ContinuousLinearMap.inl ContinuousLinearMap.inr	—	RingHomCompTriple.ids RingHomInvPair.ids indepFun_iff_map_prod_eq_prod_map_map MeasureTheory.charFunDual_eq_prod_iff' MeasureTheory.Measure.isFiniteMeasure_map AEMeasurable.map_map_of_aemeasurable Measurable.aemeasurable WithLp.measurable_toLp AEMeasurable.prodMk
indepFun_iff_charFun_prod 📖	mathematical	AEMeasurable	IndepFun MeasureTheory.charFun WithLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat WithLp.measurableSpace Prod.instMeasurableSpace InnerProductSpace.toInner Real Real.instRCLike WithLp.instProdSeminormedAddCommGroup fact_one_le_two_ennreal NormedAddCommGroup.toSeminormedAddCommGroup WithLp.instProdInnerProductSpace MeasureTheory.Measure.map WithLp.toLp Complex Complex.instMul WithLp.ofLp	—	Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal indepFun_iff_map_prod_eq_prod_map_map MeasureTheory.charFun_eq_prod_iff MeasureTheory.Measure.isFiniteMeasure_map AEMeasurable.map_map_of_aemeasurable Measurable.aemeasurable WithLp.measurable_toLp AEMeasurable.prodMk

ProbabilityTheory.IndepFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
charFunDual_map_add_eq_mul 📖	mathematical	AEMeasurable ProbabilityTheory.IndepFun	MeasureTheory.charFunDual MeasureTheory.Measure.map Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Pi.instMul StrongDual Real Real.semiring Real.pseudoMetricSpace NormedSpace.toModule Real.normedField Complex Complex.instMul	—	map_add_eq_map_conv_map₀ ContinuousAdd.measurableMul₂ IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.charFunDual_conv MeasureTheory.Measure.isFiniteMeasure_map Pi.mul_apply
charFun_map_add_eq_mul 📖	mathematical	AEMeasurable ProbabilityTheory.IndepFun	MeasureTheory.charFun InnerProductSpace.toInner Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.Measure.map Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Pi.instMul Complex Complex.instMul	—	map_add_eq_map_conv_map₀ ContinuousAdd.measurableMul₂ IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.charFun_conv MeasureTheory.Measure.isFiniteMeasure_map Pi.mul_apply

---

← Back to Index