Documentation Verification Report

CharacteristicFunction

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

Statistics

Metric	Count
Definitions	0
Theorems `charFunDual_map_add_eq_mul`, `charFunDual_map_fun_add_eq_mul`, `charFun_map_add_eq_mul`, `charFun_map_fun_add_eq_mul`, `charFunDual_map_add_prod_eq_mul`, `charFunDual_map_sum_pi_eq_prod`, `charFun_map_add_prod_eq_mul`, `charFun_map_sum_pi_eq_prod`, `charFunDual_map_finset_sum_eq_prod`, `charFunDual_map_fun_finset_sum_eq_prod`, `charFunDual_map_fun_sum_eq_prod`, `charFunDual_map_sum_eq_prod`, `charFun_map_finset_sum_eq_prod`, `charFun_map_fun_finset_sum_eq_prod`, `charFun_map_fun_sum_eq_prod`, `charFun_map_sum_eq_prod`, `iIndepFun_iff_charFunDual_pi`, `iIndepFun_iff_charFunDual_pi'`, `iIndepFun_iff_charFun_pi`, `indepFun_iff_charFunDual_prod`, `indepFun_iff_charFunDual_prod'`, `indepFun_iff_charFun_prod`	22
Total	22

ProbabilityTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`charFunDual_map_add_prod_eq_mul` 📖	mathematical	—	`MeasureTheory.charFunDual` `MeasureTheory.Measure.map` `Prod.instMeasurableSpace` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `MeasureTheory.Measure.prod` `Pi.instMul` `StrongDual` `Real` `Real.semiring` `Real.pseudoMetricSpace` `NormedSpace.toModule` `Real.normedField` `Complex` `Complex.instMul`	—	`IndepFun.charFunDual_map_fun_add_eq_mul` `MeasureTheory.Measure.prod.instIsFiniteMeasure` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `AEMeasurable.fst` `aemeasurable_id` `AEMeasurable.snd` `indepFun_prod` `measurable_id` `MeasureTheory.MeasurePreserving.map_eq` `MeasureTheory.measurePreserving_fst` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.sigmaFinite_of_locallyFinite` `MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure` `MeasureTheory.measurePreserving_snd`
`charFunDual_map_sum_pi_eq_prod` 📖	mathematical	`MeasureTheory.IsProbabilityMeasure`	`MeasureTheory.charFunDual` `MeasureTheory.Measure.map` `MeasurableSpace.pi` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.univ` `MeasureTheory.Measure.pi` `Finset.prod` `Pi.commMonoid` `StrongDual` `Real` `Real.semiring` `Real.pseudoMetricSpace` `NormedSpace.toModule` `Real.normedField` `Complex` `CommRing.toCommMonoid` `Complex.commRing`	—	`iIndepFun.charFunDual_map_fun_sum_eq_prod` `AEMeasurable.eval` `aemeasurable_id` `iIndepFun_pi` `Finset.prod_congr` `MeasureTheory.MeasurePreserving.map_eq` `MeasureTheory.measurePreserving_eval`
`charFun_map_add_prod_eq_mul` 📖	mathematical	—	`MeasureTheory.charFun` `InnerProductSpace.toInner` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasureTheory.Measure.map` `Prod.instMeasurableSpace` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `MeasureTheory.Measure.prod` `Pi.instMul` `Complex` `Complex.instMul`	—	`IndepFun.charFun_map_fun_add_eq_mul` `MeasureTheory.Measure.prod.instIsFiniteMeasure` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `AEMeasurable.fst` `aemeasurable_id` `AEMeasurable.snd` `indepFun_prod` `measurable_id` `MeasureTheory.MeasurePreserving.map_eq` `MeasureTheory.measurePreserving_fst` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.sigmaFinite_of_locallyFinite` `MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure` `MeasureTheory.measurePreserving_snd`
`charFun_map_sum_pi_eq_prod` 📖	mathematical	`MeasureTheory.IsProbabilityMeasure`	`MeasureTheory.charFun` `InnerProductSpace.toInner` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasureTheory.Measure.map` `MeasurableSpace.pi` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.univ` `MeasureTheory.Measure.pi` `Finset.prod` `Pi.commMonoid` `Complex` `CommRing.toCommMonoid` `Complex.commRing`	—	`RingHomIsometric.ids` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.charFun_eq_charFunDual_toDualMap` `charFunDual_map_sum_pi_eq_prod` `Finset.prod_apply` `Finset.prod_congr`
`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` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasurableSpace.pi` `MeasureTheory.Measure.map` `Finset.prod` `Complex` `CommRing.toCommMonoid` `Complex.commRing` `Finset.univ` `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.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` `NormedAddCommGroup.toSeminormedAddCommGroup` `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` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `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` `NormedAddCommGroup.toSeminormedAddCommGroup` `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`
`charFunDual_map_fun_add_eq_mul` 📖	mathematical	`AEMeasurable` `ProbabilityTheory.IndepFun`	`MeasureTheory.charFunDual` `MeasureTheory.Measure.map` `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`	—	`charFunDual_map_add_eq_mul`
`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`
`charFun_map_fun_add_eq_mul` 📖	mathematical	`AEMeasurable` `ProbabilityTheory.IndepFun`	`MeasureTheory.charFun` `InnerProductSpace.toInner` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasureTheory.Measure.map` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Pi.instMul` `Complex` `Complex.instMul`	—	`charFun_map_add_eq_mul`

ProbabilityTheory.iIndepFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`charFunDual_map_finset_sum_eq_prod` 📖	mathematical	`AEMeasurable` `ProbabilityTheory.iIndepFun` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.restrict`	`MeasureTheory.charFunDual` `MeasureTheory.Measure.map` `Finset.sum` `Pi.addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.prod` `Pi.commMonoid` `StrongDual` `Real` `Real.semiring` `Real.pseudoMetricSpace` `NormedSpace.toModule` `Real.normedField` `Complex` `CommRing.toCommMonoid` `Complex.commRing`	—	`isProbabilityMeasure` `Finset.induction` `IsScalarTower.right` `MeasureTheory.Measure.map_const` `MeasureTheory.IsProbabilityMeasure.measure_univ` `one_smul` `MeasureTheory.charFunDual_dirac` `BorelSpace.opensMeasurable` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `MulZeroClass.zero_mul` `Complex.exp_zero` `Finset.prod_apply` `Finset.sum_insert` `ProbabilityTheory.IndepFun.charFunDual_map_add_eq_mul` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `Finset.mem_insert_self` `Finset.aemeasurable_sum` `ContinuousAdd.measurableMul₂` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Finset.mem_insert_of_mem` `ProbabilityTheory.IndepFun.symm` `Finset.sum_of_injOn` `Finset.filter.congr_simp` `Finset.attach_insert` `Finset.coe_filter` `indepFun_finset_sum_of_notMem₀` `Finset.prod_insert` `precomp`
`charFunDual_map_fun_finset_sum_eq_prod` 📖	mathematical	`AEMeasurable` `ProbabilityTheory.iIndepFun` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.restrict`	`MeasureTheory.charFunDual` `MeasureTheory.Measure.map` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.prod` `Pi.commMonoid` `StrongDual` `Real` `Real.semiring` `Real.pseudoMetricSpace` `NormedSpace.toModule` `Real.normedField` `Complex` `CommRing.toCommMonoid` `Complex.commRing`	—	`Finset.sum_apply` `charFunDual_map_finset_sum_eq_prod`
`charFunDual_map_fun_sum_eq_prod` 📖	mathematical	`AEMeasurable` `ProbabilityTheory.iIndepFun`	`MeasureTheory.charFunDual` `MeasureTheory.Measure.map` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.univ` `Finset.prod` `Pi.commMonoid` `StrongDual` `Real` `Real.semiring` `Real.pseudoMetricSpace` `NormedSpace.toModule` `Real.normedField` `Complex` `CommRing.toCommMonoid` `Complex.commRing`	—	`charFunDual_map_fun_finset_sum_eq_prod` `restrict`
`charFunDual_map_sum_eq_prod` 📖	mathematical	`AEMeasurable` `ProbabilityTheory.iIndepFun`	`MeasureTheory.charFunDual` `MeasureTheory.Measure.map` `Finset.sum` `Pi.addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.univ` `Finset.prod` `Pi.commMonoid` `StrongDual` `Real` `Real.semiring` `Real.pseudoMetricSpace` `NormedSpace.toModule` `Real.normedField` `Complex` `CommRing.toCommMonoid` `Complex.commRing`	—	`charFunDual_map_finset_sum_eq_prod` `restrict`
`charFun_map_finset_sum_eq_prod` 📖	mathematical	`AEMeasurable` `ProbabilityTheory.iIndepFun` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.restrict`	`MeasureTheory.charFun` `InnerProductSpace.toInner` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasureTheory.Measure.map` `Finset.sum` `Pi.addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.prod` `Pi.commMonoid` `Complex` `CommRing.toCommMonoid` `Complex.commRing`	—	`RingHomIsometric.ids` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.charFun_eq_charFunDual_toDualMap` `charFunDual_map_finset_sum_eq_prod` `Finset.prod_apply` `Finset.prod_congr`
`charFun_map_fun_finset_sum_eq_prod` 📖	mathematical	`AEMeasurable` `ProbabilityTheory.iIndepFun` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.restrict`	`MeasureTheory.charFun` `InnerProductSpace.toInner` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasureTheory.Measure.map` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.prod` `Pi.commMonoid` `Complex` `CommRing.toCommMonoid` `Complex.commRing`	—	`Finset.sum_apply` `charFun_map_finset_sum_eq_prod`
`charFun_map_fun_sum_eq_prod` 📖	mathematical	`AEMeasurable` `ProbabilityTheory.iIndepFun`	`MeasureTheory.charFun` `InnerProductSpace.toInner` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasureTheory.Measure.map` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.univ` `Finset.prod` `Pi.commMonoid` `Complex` `CommRing.toCommMonoid` `Complex.commRing`	—	`charFun_map_fun_finset_sum_eq_prod` `restrict`
`charFun_map_sum_eq_prod` 📖	mathematical	`AEMeasurable` `ProbabilityTheory.iIndepFun`	`MeasureTheory.charFun` `InnerProductSpace.toInner` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasureTheory.Measure.map` `Finset.sum` `Pi.addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.univ` `Finset.prod` `Pi.commMonoid` `Complex` `CommRing.toCommMonoid` `Complex.commRing`	—	`charFun_map_finset_sum_eq_prod` `restrict`

---

← Back to Index