CharacteristicFunction

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

Statistics

Metric	Count
Definitions `innerProbChar`, `probCharDual`, `charFun`, `charFunDual`	4
Theorems `innerProbChar_apply`, `innerProbChar_zero`, `probCharDual_apply`, `probCharDual_zero`, `ext_of_charFun`, `ext_of_charFunDual`, `charFunDual_apply`, `charFunDual_conv`, `charFunDual_dirac`, `charFunDual_eq_charFun_map_one`, `charFunDual_eq_pi_iff`, `charFunDual_eq_pi_iff'`, `charFunDual_eq_prod_iff`, `charFunDual_eq_prod_iff'`, `charFunDual_map`, `charFunDual_map_add_const`, `charFunDual_map_const_add`, `charFunDual_pi`, `charFunDual_pi'`, `charFunDual_prod`, `charFunDual_prod'`, `charFun_apply`, `charFun_apply_real`, `charFun_conv`, `charFun_dirac`, `charFun_eq_charFunDual_toDualMap`, `charFun_eq_fourierIntegral`, `charFun_eq_fourierIntegral'`, `charFun_eq_integral_innerProbChar`, `charFun_eq_integral_probChar`, `charFun_eq_pi_iff`, `charFun_eq_prod_iff`, `charFun_map_add_const`, `charFun_map_const_add`, `charFun_map_eq_charFunDual_smul`, `charFun_map_mul`, `charFun_map_smul`, `charFun_neg`, `charFun_pi`, `charFun_prod`, `charFun_toDual_symm_eq_charFunDual`, `charFun_zero`, `charFun_zero_measure`, `ext_of_integral_char_eq`, `intervalIntegrable_charFun`, `measurable_charFun`, `norm_charFun_le`, `norm_charFun_le_one`, `norm_one_sub_charFun_le_two`, `stronglyMeasurable_charFun`	50
Total	54

BoundedContinuousFunction

Definitions

Name	Category	Theorems
`innerProbChar` 📖	CompOp	3 math math: `innerProbChar_zero`, `innerProbChar_apply`, `MeasureTheory.charFun_eq_integral_innerProbChar`
`probCharDual` 📖	CompOp	2 math math: `probCharDual_zero`, `probCharDual_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`innerProbChar_apply` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `instFunLike` `innerProbChar` `Complex.exp` `Complex.instMul` `Complex.ofReal` `Inner.inner` `Real` `InnerProductSpace.toInner` `Real.instRCLike` `Complex.I`	—	—
`innerProbChar_zero` 📖	mathematical	—	`innerProbChar` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `BoundedContinuousFunction` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `instOne` `Complex.instOne`	—	`char_zero_eq_one` `Real.continuous_probChar` `continuous_inner`
`probCharDual_apply` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `instFunLike` `probCharDual` `Complex.exp` `Complex.instMul` `Complex.ofReal` `StrongDual` `Real` `Real.semiring` `Real.pseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `ContinuousLinearMap.funLike` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Complex.I`	—	—
`probCharDual_zero` 📖	mathematical	—	`probCharDual` `StrongDual` `Real` `Real.semiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `ContinuousLinearMap.zero` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `BoundedContinuousFunction` `Complex` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `instOne` `Complex.instOne`	—	`char_zero_eq_one` `instIsTopologicalAddGroupReal` `Real.continuous_probChar`

MeasureTheory

Definitions

Name	Category	Theorems
`charFun` 📖	CompOp	44 math math: `ProbabilityTheory.isGaussian_iff_gaussian_charFun`, `charFun_eq_fourierIntegral'`, `charFun_neg`, `charFun_toDual_symm_eq_charFunDual`, `charFun_eq_fourierIntegral`, `ProbabilityTheory.hasGaussianLaw_iff_charFun_map_eq`, `charFunDual_eq_charFun_map_one`, `charFun_apply`, `charFun_apply_real`, `ProbabilityTheory.complexMGF_mul_I`, `charFun_eq_prod_iff`, `ProbabilityTheory.IsGaussian.charFun_eq'`, `ProbabilityTheory.complexMGF_id_mul_I`, `charFun_pi`, `ProbabilityTheory.isGaussian_iff_charFun_eq`, `charFun_conv`, `integral_charFun_Icc`, `ProbabilityTheory.indepFun_iff_charFun_prod`, `norm_charFun_le_one`, `ProbabilityTheory.HasGaussianLaw.charFun_map_eq`, `measureReal_abs_gt_le_integral_charFun`, `norm_one_sub_charFun_le_two`, `charFun_eq_charFunDual_toDualMap`, `charFun_zero_measure`, `stronglyMeasurable_charFun`, `measureReal_abs_inner_gt_le_integral_charFun`, `ProbabilityTheory.iIndepFun_iff_charFun_pi`, `charFun_map_mul`, `charFun_dirac`, `ProbabilityTheory.IsGaussian.charFun_eq`, `charFun_map_eq_charFunDual_smul`, `intervalIntegrable_charFun`, `charFun_eq_integral_innerProbChar`, `ProbabilityTheory.charFun_gaussianReal`, `ProbabilityTheory.IndepFun.charFun_map_add_eq_mul`, `charFun_zero`, `norm_charFun_le`, `measurable_charFun`, `charFun_map_const_add`, `charFun_eq_pi_iff`, `charFun_prod`, `charFun_map_smul`, `charFun_eq_integral_probChar`, `charFun_map_add_const`
`charFunDual` 📖	CompOp	33 math math: `charFunDual_apply`, `ProbabilityTheory.hasGaussianLaw_iff_charFunDual_map_eq`, `charFun_toDual_symm_eq_charFunDual`, `charFunDual_eq_charFun_map_one`, `charFunDual_pi'`, `charFunDual_prod`, `charFunDual_eq_prod_iff`, `ProbabilityTheory.IsGaussian.charFunDual_eq_of_forall_strongDual_eq_zero`, `ProbabilityTheory.IsGaussian.charFunDual_eq`, `ProbabilityTheory.indepFun_iff_charFunDual_prod'`, `charFunDual_map_const_add`, `charFunDual_map_add_const`, `ProbabilityTheory.isGaussian_iff_gaussian_charFunDual`, `ProbabilityTheory.iIndepFun_iff_charFunDual_pi`, `ProbabilityTheory.IndepFun.charFunDual_map_add_eq_mul`, `measureReal_abs_dual_gt_le_integral_charFunDual`, `charFunDual_eq_pi_iff`, `ProbabilityTheory.iIndepFun_iff_charFunDual_pi'`, `ProbabilityTheory.isGaussian_iff_charFunDual_eq`, `charFun_eq_charFunDual_toDualMap`, `charFunDual_prod'`, `ProbabilityTheory.HasGaussianLaw.charFunDual_map_eq_fun`, `charFunDual_eq_pi_iff'`, `charFunDual_dirac`, `charFunDual_map`, `ProbabilityTheory.IsGaussian.charFunDual_eq_of_integral_eq_zero`, `charFunDual_pi`, `charFun_map_eq_charFunDual_smul`, `ProbabilityTheory.IsGaussian.charFunDual_eq'`, `ProbabilityTheory.HasGaussianLaw.charFunDual_map_eq`, `charFunDual_eq_prod_iff'`, `ProbabilityTheory.indepFun_iff_charFunDual_prod`, `charFunDual_conv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`charFunDual_apply` 📖	mathematical	—	`charFunDual` `integral` `Complex` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex` `Complex.exp` `Complex.instMul` `Complex.ofReal` `DFunLike.coe` `StrongDual` `Real.semiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `ContinuousLinearMap.funLike` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Complex.I`	—	—
`charFunDual_conv` 📖	mathematical	—	`charFunDual` `Measure.conv` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex` `Complex.instMul`	—	`integral_conv` `ContinuousAdd.measurableMul₂` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `instSFiniteOfSigmaFinite` `sigmaFinite_of_locallyFinite` `IsFiniteMeasure.toIsLocallyFiniteMeasure` `Integrable.mono` `integrable_const` `Measure.finite_of_finite_conv` `Continuous.comp_aestronglyMeasurable` `Continuous.cexp` `continuous_id'` `AEStronglyMeasurable.mul_const` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Complex.continuous_ofReal` `Continuous.aestronglyMeasurable` `BorelSpace.opensMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `secondCountableTopologyEither_of_right` `instSecondCountableTopologyReal` `Continuous.clm_apply` `continuous_const` `Measure.instOuterMeasureClass` `Complex.norm_exp_ofReal_mul_I` `CStarRing.norm_of_mem_unitary` `instCStarRingReal` `Real.instNontrivial` `SubmonoidClass.toOneMemClass` `Submonoid.instSubmonoidClass` `map_add` `SemilinearMapClass.toAddHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `Complex.ofReal_add` `add_mul` `Distrib.rightDistribClass` `Complex.exp_add` `integral_const_mul` `integral_mul_const`
`charFunDual_dirac` 📖	mathematical	—	`charFunDual` `Measure.dirac` `Complex.exp` `Complex` `Complex.instMul` `Complex.ofReal` `DFunLike.coe` `StrongDual` `Real` `Real.semiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `ContinuousLinearMap.funLike` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Complex.I`	—	`charFunDual_apply` `integral_dirac` `Complex.instCompleteSpace` `OpensMeasurableSpace.toMeasurableSingletonClass` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace`
`charFunDual_eq_charFun_map_one` 📖	mathematical	—	`charFunDual` `charFun` `Real` `Real.measurableSpace` `InnerProductSpace.toInner` `Real.instRCLike` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toInnerProductSpaceReal` `Measure.map` `DFunLike.coe` `StrongDual` `Real.semiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `ContinuousLinearMap.funLike` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Real.instOne`	—	`charFunDual_apply` `integral_map` `Measurable.aemeasurable` `ContinuousLinearMap.measurable` `Real.borelSpace` `Measurable.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `UniformSpace.secondCountable_of_separable` `EMetric.instIsCountablyGeneratedUniformity` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `secondCountable_of_proper` `Complex.instProperSpace` `BorelSpace.opensMeasurable` `Complex.borelSpace` `Measurable.cexp` `Measurable.mul_const` `ContinuousMul.measurableMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Measurable.complex_ofReal` `measurable_id'` `charFun_apply` `conj_trivial` `instTrivialStarReal` `one_mul`
`charFunDual_eq_pi_iff` 📖	mathematical	`BorelSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SecondCountableTopology` `CompleteSpace` `IsFiniteMeasure`	`charFunDual` `Pi.normedAddCommGroup` `Pi.normedSpace` `Real` `Real.normedField` `MeasurableSpace.pi` `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` `Measure.pi`	—	`RingHomCompTriple.ids` `Measure.ext_of_charFunDual` `Pi.borelSpace` `Finite.to_countable` `Finite.of_fintype` `TopologicalSpace.instSecondCountableTopologyForallOfCountable` `Pi.complete` `Measure.pi.instIsFiniteMeasure` `charFunDual_pi` `sigmaFinite_of_locallyFinite` `IsFiniteMeasure.toIsLocallyFiniteMeasure`
`charFunDual_eq_pi_iff'` 📖	mathematical	`BorelSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SecondCountableTopology` `CompleteSpace` `IsFiniteMeasure`	`charFunDual` `WithLp` `PiLp.normedAddCommGroup` `PiLp.normedSpace` `Real` `Real.normedField` `WithLp.measurableSpace` `MeasurableSpace.pi` `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` `Measure.pi`	—	`RingHomCompTriple.ids` `RingHomInvPair.ids` `MeasurableEquiv.map_measurableEquiv_injective` `Measure.ext_of_charFunDual` `PiLp.borelSpace` `Finite.to_countable` `Finite.of_fintype` `PiLp.secondCountableTopology` `PiLp.completeSpace` `Measure.isFiniteMeasure_map` `Measure.pi.instIsFiniteMeasure` `MeasurableEquiv.coe_toLp` `charFunDual_pi'` `sigmaFinite_of_locallyFinite` `IsFiniteMeasure.toIsLocallyFiniteMeasure`
`charFunDual_eq_prod_iff` 📖	mathematical	—	`charFunDual` `Prod.normedAddCommGroup` `Prod.normedSpace` `Real` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `Prod.instMeasurableSpace` `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` `Measure.prod`	—	`RingHomCompTriple.ids` `Measure.ext_of_charFunDual` `Prod.borelSpace` `secondCountableTopologyEither_of_right` `TopologicalSpace.instSecondCountableTopologyProd` `CompleteSpace.prod` `Measure.prod.instIsFiniteMeasure` `charFunDual_prod` `instSFiniteOfSigmaFinite` `sigmaFinite_of_locallyFinite` `IsFiniteMeasure.toIsLocallyFiniteMeasure`
`charFunDual_eq_prod_iff'` 📖	mathematical	—	`charFunDual` `WithLp` `WithLp.instProdNormedAddCommGroup` `WithLp.instProdNormedSpace` `Real` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.normedField` `WithLp.measurableSpace` `Prod.instMeasurableSpace` `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` `Measure.prod`	—	`RingHomCompTriple.ids` `RingHomInvPair.ids` `MeasurableEquiv.map_measurableEquiv_injective` `Measure.ext_of_charFunDual` `WithLp.borelSpace` `secondCountableTopologyEither_of_right` `WithLp.secondCountableTopology` `WithLp.instProdCompleteSpace` `Measure.isFiniteMeasure_map` `Measure.prod.instIsFiniteMeasure` `MeasurableEquiv.coe_toLp` `charFunDual_prod'` `instSFiniteOfSigmaFinite` `sigmaFinite_of_locallyFinite` `IsFiniteMeasure.toIsLocallyFiniteMeasure`
`charFunDual_map` 📖	mathematical	—	`charFunDual` `Measure.map` `DFunLike.coe` `ContinuousLinearMap` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `ContinuousLinearMap.funLike` `ContinuousLinearMap.comp` `Real.pseudoMetricSpace` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `RingHomCompTriple.ids`	—	`RingHomCompTriple.ids` `charFunDual_eq_charFun_map_one` `BorelSpace.opensMeasurable` `Measure.map_map` `ContinuousLinearMap.measurable` `Real.borelSpace`
`charFunDual_map_add_const` 📖	mathematical	—	`charFunDual` `Measure.map` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex` `Complex.instMul` `Complex.exp` `Complex.ofReal` `DFunLike.coe` `StrongDual` `Real` `Real.semiring` `Real.pseudoMetricSpace` `NormedSpace.toModule` `Real.normedField` `ContinuousLinearMap.funLike` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Complex.I`	—	`charFunDual_apply` `integral_map` `AEMeasurable.add_const` `ContinuousAdd.measurableAdd` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `aemeasurable_id` `Continuous.comp_aestronglyMeasurable` `Continuous.cexp` `continuous_id'` `AEStronglyMeasurable.mul_const` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Complex.continuous_ofReal` `Continuous.aestronglyMeasurable` `BorelSpace.opensMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `secondCountableTopologyEither_of_right` `instSecondCountableTopologyReal` `Continuous.clm_apply` `continuous_const` `integral_mul_const` `Complex.exp_add` `map_add` `SemilinearMapClass.toAddHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `Complex.ofReal_add` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul`
`charFunDual_map_const_add` 📖	mathematical	—	`charFunDual` `Measure.map` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex` `Complex.instMul` `Complex.exp` `Complex.ofReal` `DFunLike.coe` `StrongDual` `Real` `Real.semiring` `Real.pseudoMetricSpace` `NormedSpace.toModule` `Real.normedField` `ContinuousLinearMap.funLike` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Complex.I`	—	`add_comm` `charFunDual_map_add_const`
`charFunDual_pi` 📖	mathematical	`SigmaFinite`	`charFunDual` `Pi.normedAddCommGroup` `Pi.normedSpace` `Real` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasurableSpace.pi` `Measure.pi` `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` `Pi.topologicalSpace` `Pi.addCommMonoid` `Real.pseudoMetricSpace` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `NormedSpace.toModule` `Pi.module` `Semiring.toModule` `RingHomCompTriple.ids` `ContinuousLinearMap.single`	—	`RingHomCompTriple.ids` `Finset.prod_congr` `ContinuousLinearMap.sum_comp_single` `Complex.ofReal_sum` `Finset.sum_mul` `Complex.exp_sum`
`charFunDual_pi'` 📖	mathematical	`SigmaFinite`	`charFunDual` `WithLp` `PiLp.normedAddCommGroup` `PiLp.normedSpace` `Real` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithLp.measurableSpace` `MeasurableSpace.pi` `Measure.map` `WithLp.toLp` `Measure.pi` `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` `PiLp` `PiLp.topologicalSpace` `Real.pseudoMetricSpace` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `NormedSpace.toModule` `WithLp.instModule` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.module` `Semiring.toModule` `RingHomCompTriple.ids` `Pi.topologicalSpace` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid` `WithLp.instAddCommGroup` `ContinuousLinearEquiv.toContinuousLinearMap` `RingHomInvPair.ids` `ContinuousLinearEquiv.symm` `PiLp.continuousLinearEquiv` `ContinuousLinearMap.single`	—	`RingHomCompTriple.ids` `RingHomInvPair.ids` `Finset.prod_congr` `Finset.sum_congr` `ContinuousLinearMap.comp_apply` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `ContinuousLinearMap.sum_comp_single` `MeasurableEquiv.coe_toLp` `integral_map_equiv`
`charFunDual_prod` 📖	mathematical	—	`charFunDual` `Prod.normedAddCommGroup` `Prod.normedSpace` `Real` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `Prod.instMeasurableSpace` `Measure.prod` `Complex` `Complex.instMul` `ContinuousLinearMap.comp` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Real.pseudoMetricSpace` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `NormedSpace.toModule` `Prod.instModule` `Semiring.toModule` `RingHomCompTriple.ids` `ContinuousLinearMap.inl` `ContinuousLinearMap.inr`	—	`RingHomCompTriple.ids` `ContinuousLinearMap.comp_inl_add_comp_inr` `Complex.ofReal_add` `add_mul` `Distrib.rightDistribClass` `Complex.exp_add`
`charFunDual_prod'` 📖	mathematical	—	`charFunDual` `WithLp` `WithLp.instProdNormedAddCommGroup` `WithLp.instProdNormedSpace` `Real` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.normedField` `WithLp.measurableSpace` `Prod.instMeasurableSpace` `Measure.map` `WithLp.toLp` `Measure.prod` `Complex` `Complex.instMul` `ContinuousLinearMap.comp` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `WithLp.instProdTopologicalSpace` `Real.pseudoMetricSpace` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `NormedSpace.toModule` `WithLp.instModule` `Prod.instAddCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Prod.instModule` `Semiring.toModule` `RingHomCompTriple.ids` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `WithLp.instAddCommGroup` `ContinuousLinearEquiv.toContinuousLinearMap` `RingHomInvPair.ids` `ContinuousLinearEquiv.symm` `WithLp.prodContinuousLinearEquiv` `ContinuousLinearMap.inl` `ContinuousLinearMap.inr`	—	`RingHomCompTriple.ids` `RingHomInvPair.ids` `Distrib.rightDistribClass` `ContinuousLinearMap.comp_apply` `SemilinearMapClass.toAddHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `ContinuousLinearMap.comp_inl_add_comp_inr` `MeasurableEquiv.coe_toLp` `integral_map_equiv`
`charFun_apply` 📖	mathematical	—	`charFun` `integral` `Complex` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex` `Complex.exp` `Complex.instMul` `Complex.ofReal` `Inner.inner` `Complex.I`	—	—
`charFun_apply_real` 📖	mathematical	—	`charFun` `Real` `Real.measurableSpace` `InnerProductSpace.toInner` `Real.instRCLike` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toInnerProductSpaceReal` `integral` `Complex` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex` `Complex.exp` `Complex.instMul` `Complex.ofReal` `Complex.I`	—	`conj_trivial` `instTrivialStarReal` `Complex.ofReal_mul`
`charFun_conv` 📖	mathematical	—	`charFun` `InnerProductSpace.toInner` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Measure.conv` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex` `Complex.instMul`	—	`integral_conv` `ContinuousAdd.measurableMul₂` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `instSFiniteOfSigmaFinite` `sigmaFinite_of_locallyFinite` `IsFiniteMeasure.toIsLocallyFiniteMeasure` `Integrable.mono` `integrable_const` `Measure.finite_of_finite_conv` `Continuous.comp_aestronglyMeasurable` `Continuous.cexp` `continuous_id'` `AEStronglyMeasurable.mul_const` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Complex.continuous_ofReal` `Continuous.aestronglyMeasurable` `BorelSpace.opensMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `secondCountableTopologyEither_of_right` `instSecondCountableTopologyReal` `Continuous.inner` `continuous_const` `Measure.instOuterMeasureClass` `Complex.norm_exp_ofReal_mul_I` `CStarRing.norm_of_mem_unitary` `instCStarRingReal` `Real.instNontrivial` `SubmonoidClass.toOneMemClass` `Submonoid.instSubmonoidClass` `inner_add_left` `Complex.ofReal_add` `add_mul` `Distrib.rightDistribClass` `Complex.exp_add` `integral_const_mul` `integral_mul_const`
`charFun_dirac` 📖	mathematical	—	`charFun` `InnerProductSpace.toInner` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Measure.dirac` `Complex.exp` `Complex` `Complex.instMul` `Complex.ofReal` `Inner.inner` `Complex.I`	—	`charFun_apply` `integral_dirac` `Complex.instCompleteSpace` `OpensMeasurableSpace.toMeasurableSingletonClass` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace`
`charFun_eq_charFunDual_toDualMap` 📖	mathematical	—	`charFun` `InnerProductSpace.toInner` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `charFunDual` `InnerProductSpace.toNormedSpace` `DFunLike.coe` `LinearIsometry` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `starRingEnd` `RCLike.toStarRing` `StrongDual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.toSeminormedAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `DenselyNormedField.toNontriviallyNormedField` `RCLike.innerProductSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomIsometric.ids` `ContinuousLinearMap.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Algebra.to_smulCommClass` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `LinearIsometry.instFunLike` `InnerProductSpace.toDualMap`	—	`real_inner_comm`
`charFun_eq_fourierIntegral` 📖	mathematical	—	`charFun` `InnerProductSpace.toInner` `Real` `Real.instRCLike` `VectorFourier.fourierIntegral` `Real.commRing` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Complex` `Complex.instNormedAddCommGroup` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Real.probChar` `innerₗ` `Pi.instOne` `Complex.instOne` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`Algebra.to_smulCommClass` `VectorFourier.fourierIntegral_probChar` `inner_neg_right` `Complex.ofReal_neg` `neg_neg` `mul_one`
`charFun_eq_fourierIntegral'` 📖	mathematical	—	`charFun` `InnerProductSpace.toInner` `Real` `Real.instRCLike` `VectorFourier.fourierIntegral` `Real.commRing` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Complex` `Complex.instNormedAddCommGroup` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `Real.fourierChar` `innerₗ` `Pi.instOne` `Complex.instOne` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `AddCommGroup.toAddCommMonoid` `Real.instNeg` `Real.instInv` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi`	—	`Nat.instAtLeastTwoHAddOfNat` `neg_smul` `inner_neg_right` `inner_smul_right` `neg_neg` `Complex.ofReal_mul` `Complex.ofReal_inv` `mul_one` `mul_assoc` `mul_inv_cancel₀` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Complex.instCharZero` `one_mul`
`charFun_eq_integral_innerProbChar` 📖	mathematical	—	`charFun` `InnerProductSpace.toInner` `Real` `Real.instRCLike` `integral` `Complex` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex` `DFunLike.coe` `BoundedContinuousFunction` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `BoundedContinuousFunction.instFunLike` `BoundedContinuousFunction.innerProbChar`	—	—
`charFun_eq_integral_probChar` 📖	mathematical	—	`charFun` `InnerProductSpace.toInner` `Real` `Real.instRCLike` `integral` `Complex` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.unitSphere` `DFunLike.coe` `AddChar` `Real.instAddMonoid` `Circle` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `AddChar.instFunLike` `Real.probChar` `Inner.inner`	—	—
`charFun_eq_pi_iff` 📖	mathematical	`CompleteSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SecondCountableTopology` `UniformSpace.toTopologicalSpace` `BorelSpace` `IsFiniteMeasure`	`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` `Measure.map` `WithLp.toLp` `Finset.prod` `Complex` `CommRing.toCommMonoid` `Complex.commRing` `Finset.univ` `WithLp.ofLp` `Measure.pi`	—	`Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `MeasurableEquiv.map_measurableEquiv_injective` `Measure.ext_of_charFun` `PiLp.borelSpace` `Finite.to_countable` `Finite.of_fintype` `PiLp.secondCountableTopology` `PiLp.completeSpace` `Measure.isFiniteMeasure_map` `Measure.pi.instIsFiniteMeasure` `MeasurableEquiv.coe_toLp` `charFun_pi` `sigmaFinite_of_locallyFinite` `IsFiniteMeasure.toIsLocallyFiniteMeasure`
`charFun_eq_prod_iff` 📖	mathematical	—	`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` `Measure.map` `WithLp.toLp` `Complex` `Complex.instMul` `WithLp.ofLp` `Measure.prod`	—	`Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `MeasurableEquiv.map_measurableEquiv_injective` `Measure.ext_of_charFun` `WithLp.borelSpace` `secondCountableTopologyEither_of_right` `WithLp.secondCountableTopology` `WithLp.instProdCompleteSpace` `Measure.isFiniteMeasure_map` `Measure.prod.instIsFiniteMeasure` `MeasurableEquiv.coe_toLp` `charFun_prod` `instSFiniteOfSigmaFinite` `sigmaFinite_of_locallyFinite` `IsFiniteMeasure.toIsLocallyFiniteMeasure`
`charFun_map_add_const` 📖	mathematical	—	`charFun` `InnerProductSpace.toInner` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Measure.map` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex` `Complex.instMul` `Complex.exp` `Complex.ofReal` `Inner.inner` `Complex.I`	—	`charFun_apply` `integral_map` `AEMeasurable.add_const` `ContinuousAdd.measurableAdd` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `aemeasurable_id` `Continuous.comp_aestronglyMeasurable` `Continuous.cexp` `continuous_id'` `AEStronglyMeasurable.mul_const` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Complex.continuous_ofReal` `Continuous.aestronglyMeasurable` `BorelSpace.opensMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `secondCountableTopologyEither_of_right` `instSecondCountableTopologyReal` `Continuous.inner` `continuous_const` `integral_mul_const` `Complex.exp_add` `inner_add_left` `Complex.ofReal_add` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul`
`charFun_map_const_add` 📖	mathematical	—	`charFun` `InnerProductSpace.toInner` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Measure.map` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex` `Complex.instMul` `Complex.exp` `Complex.ofReal` `Inner.inner` `Complex.I`	—	`add_comm` `charFun_map_add_const`
`charFun_map_eq_charFunDual_smul` 📖	mathematical	—	`charFun` `Real` `Real.measurableSpace` `InnerProductSpace.toInner` `Real.instRCLike` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toInnerProductSpaceReal` `Measure.map` `DFunLike.coe` `StrongDual` `Real.semiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `ContinuousLinearMap.funLike` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `charFunDual` `ContinuousLinearMap.instSMul` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real.normedCommRing` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `Ring.uniformContinuousConstSMul` `Real.instRing` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal`	—	`Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `charFunDual_apply` `integral_map` `Measurable.aemeasurable` `ContinuousLinearMap.measurable` `Real.borelSpace` `Measurable.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `UniformSpace.secondCountable_of_separable` `EMetric.instIsCountablyGeneratedUniformity` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `secondCountable_of_proper` `Complex.instProperSpace` `BorelSpace.opensMeasurable` `Complex.borelSpace` `Measurable.cexp` `Measurable.mul_const` `ContinuousMul.measurableMul` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Measurable.const_mul` `Measurable.complex_ofReal` `measurable_id'` `Complex.ofReal_mul` `charFun_apply` `conj_trivial` `instTrivialStarReal`
`charFun_map_mul` 📖	mathematical	—	`charFun` `Real` `Real.measurableSpace` `InnerProductSpace.toInner` `Real.instRCLike` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toInnerProductSpaceReal` `Measure.map` `Real.instMul`	—	`charFun_map_smul` `Real.borelSpace`
`charFun_map_smul` 📖	mathematical	—	`charFun` `InnerProductSpace.toInner` `Real` `Real.instRCLike` `Measure.map` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace`	—	`charFun_apply` `integral_map` `AEMeasurable.fun_const_smul` `MeasurableSMul.toMeasurableConstSMul` `ContinuousSMul.toMeasurableSMul` `BorelSpace.opensMeasurable` `Real.borelSpace` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `aemeasurable_id` `Continuous.comp_aestronglyMeasurable` `Continuous.cexp` `continuous_id'` `AEStronglyMeasurable.mul_const` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Complex.continuous_ofReal` `Continuous.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `secondCountableTopologyEither_of_right` `instSecondCountableTopologyReal` `Continuous.inner` `continuous_const` `inner_smul_right`
`charFun_neg` 📖	mathematical	—	`charFun` `InnerProductSpace.toInner` `Real` `Real.instRCLike` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `DFunLike.coe` `RingHom` `Complex` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Complex.instCommSemiring` `RingHom.instFunLike` `starRingEnd` `Complex.instStarRing`	—	`inner_neg_right` `Complex.ofReal_neg` `neg_mul` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `Complex.conj_ofReal` `Complex.conj_I` `mul_neg`
`charFun_pi` 📖	mathematical	`SigmaFinite`	`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` `Measure.map` `WithLp.toLp` `Measure.pi` `Finset.prod` `Complex` `CommRing.toCommMonoid` `Complex.commRing` `Finset.univ` `WithLp.ofLp`	—	`Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `Finset.prod_congr` `integral_map_equiv` `Finset.sum_congr` `Complex.ofReal_sum` `Finset.sum_mul` `Complex.exp_sum`
`charFun_prod` 📖	mathematical	—	`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` `Measure.map` `WithLp.toLp` `Measure.prod` `Complex` `Complex.instMul` `WithLp.ofLp`	—	`Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `integral_map_equiv` `Complex.ofReal_add` `add_mul` `Distrib.rightDistribClass` `Complex.exp_add`
`charFun_toDual_symm_eq_charFunDual` 📖	mathematical	—	`charFun` `InnerProductSpace.toInner` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `LinearIsometryEquiv` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `starRingEnd` `RCLike.toStarRing` `RingHomInvPair.instStarRingEnd` `StrongDual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `ContinuousLinearMap.toSeminormedAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `DenselyNormedField.toNontriviallyNormedField` `RCLike.innerProductSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomIsometric.ids` `ContinuousLinearMap.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Algebra.to_smulCommClass` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `LinearIsometryEquiv.symm` `InnerProductSpace.toDual` `charFunDual`	—	`RingHomInvPair.instStarRingEnd` `RingHomIsometric.ids` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `charFun_eq_charFunDual_toDualMap` `InnerProductSpace.toDual_apply_eq_toDualMap_apply` `LinearIsometryEquiv.apply_symm_apply`
`charFun_zero` 📖	mathematical	—	`charFun` `InnerProductSpace.toInner` `Real` `Real.instRCLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Complex.ofReal` `Measure.real` `Set.univ`	—	`inner_zero_right` `MulZeroClass.zero_mul` `Complex.exp_zero` `integral_const` `Complex.instCompleteSpace` `mul_one`
`charFun_zero_measure` 📖	mathematical	—	`charFun` `InnerProductSpace.toInner` `Real` `Real.instRCLike` `Measure` `Measure.instZero` `Complex` `Complex.instZero`	—	`integral_zero_measure`
`ext_of_integral_char_eq` 📖	—	`Continuous` `Real` `Circle` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpaceCircle` `DFunLike.coe` `AddChar` `Real.instAddMonoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `AddChar.instFunLike` `instTopologicalSpaceProd` `PseudoEMetricSpace.toUniformSpace` `LinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Real.instAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `integral` `Complex` `Complex.instNormedAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex` `BoundedContinuousFunction` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `BoundedContinuousFunction.instFunLike` `BoundedContinuousFunction.char`	—	—	`Algebra.to_smulCommClass` `ext_of_forall_mem_subalgebra_integral_eq_of_pseudoEMetric_complete_countable` `BoundedContinuousFunction.separatesPoints_charPoly` `instBoundedMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalSemiring.toContinuousAdd` `CStarRing.to_normedStarGroup` `RCLike.instCStarRing` `BoundedContinuousFunction.instStarModule` `StarMul.toStarModule` `integral_finset_sum` `Integrable.const_mul` `BoundedContinuousFunction.integrable` `BorelSpace.opensMeasurable` `UniformSpace.secondCountable_of_separable` `EMetric.instIsCountablyGeneratedUniformity` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `secondCountable_of_proper` `Complex.instProperSpace` `Complex.borelSpace` `Finset.sum_congr` `integral_const_mul` `IsCancelMulZero.toIsLeftCancelMulZero` `IsDomain.toIsCancelMulZero` `instIsDomain`
`intervalIntegrable_charFun` 📖	mathematical	—	`IntervalIntegrable` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `NormedAddGroup.toENormedAddMonoid` `NormedAddCommGroup.toNormedAddGroup` `Complex.instNormedAddCommGroup` `charFun` `Real` `Real.measurableSpace` `InnerProductSpace.toInner` `Real.instRCLike` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toInnerProductSpaceReal` `MeasureSpace.volume` `Real.measureSpace`	—	`IntervalIntegrable.mono_fun'` `Real.locallyFinite_volume` `StronglyMeasurable.aestronglyMeasurable` `stronglyMeasurable_charFun` `BorelSpace.opensMeasurable` `Real.borelSpace` `instSecondCountableTopologyReal` `instSFiniteOfSigmaFinite` `sigmaFinite_of_locallyFinite` `isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `instProperSpaceReal` `Measure.Regular.toIsFiniteMeasureOnCompacts` `Measure.InnerRegularCompactLTTop.instRegularOfBorelSpaceOfR1SpaceOfIsFiniteMeasure` `instR1Space` `TopologicalSpace.PseudoMetrizableSpace.regularSpace` `PseudoEMetricSpace.pseudoMetrizableSpace` `instInnerRegularCompactLTTopOfIsCompletelyPseudoMetrizableSpace` `TopologicalSpace.IsCompletelyMetrizableSpace.toIsCompletelyPseudoMetrizableSpace` `TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable` `Real.instCompleteSpace` `EMetric.instIsCountablyGeneratedUniformity` `T6Space.toT0Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `ae_of_all` `Measure.instOuterMeasureClass` `norm_charFun_le`
`measurable_charFun` 📖	mathematical	—	`Measurable` `Complex` `Complex.measurableSpace` `charFun` `InnerProductSpace.toInner` `Real` `Real.instRCLike`	—	`StronglyMeasurable.measurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `Complex.borelSpace` `stronglyMeasurable_charFun`
`norm_charFun_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `Complex` `Complex.instNorm` `charFun` `InnerProductSpace.toInner` `Real.instRCLike` `Measure.real` `Set.univ`	—	`charFun_eq_fourierIntegral` `LE.le.trans_eq` `VectorFourier.norm_fourierIntegral_le_integral_norm` `CStarRing.norm_of_mem_unitary` `RCLike.instCStarRing` `Complex.instNontrivial` `SubmonoidClass.toOneMemClass` `Submonoid.instSubmonoidClass` `integral_const` `Real.instCompleteSpace` `mul_one`
`norm_charFun_le_one` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `Complex` `Complex.instNorm` `charFun` `InnerProductSpace.toInner` `Real.instRCLike` `Real.instOne`	—	`LE.le.trans_eq` `norm_charFun_le` `probReal_univ`
`norm_one_sub_charFun_le_two` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `Complex` `Complex.instNorm` `Complex.instSub` `Complex.instOne` `charFun` `InnerProductSpace.toInner` `Real.instRCLike` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `norm_sub_le` `CStarRing.norm_of_mem_unitary` `RCLike.instCStarRing` `Complex.instNontrivial` `SubmonoidClass.toOneMemClass` `Submonoid.instSubmonoidClass` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Meta.NormNum.instAtLeastTwo`
`stronglyMeasurable_charFun` 📖	mathematical	—	`StronglyMeasurable` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `charFun` `InnerProductSpace.toInner` `Real` `Real.instRCLike`	—	`StronglyMeasurable.integral_prod_left` `Measurable.stronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `UniformSpace.secondCountable_of_separable` `EMetric.instIsCountablyGeneratedUniformity` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `secondCountable_of_proper` `Complex.instProperSpace` `BorelSpace.opensMeasurable` `Complex.borelSpace` `Measurable.cexp` `Measurable.mul_const` `ContinuousMul.measurableMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Measurable.complex_ofReal` `Continuous.measurable` `Prod.opensMeasurableSpace` `secondCountableTopologyEither_of_right` `Real.borelSpace` `Continuous.inner` `Continuous.fst` `continuous_id'` `Continuous.snd`

MeasureTheory.Measure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext_of_charFun` 📖	—	`MeasureTheory.charFun` `InnerProductSpace.toInner` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	—	`MeasureTheory.ext_of_integral_char_eq` `Real.continuous_probChar` `Real.probChar_ne_one` `Algebra.to_smulCommClass` `DFunLike.ne_iff` `inner_self_ne_zero` `continuous_inner` `MeasureTheory.charFun_eq_integral_innerProbChar`
`ext_of_charFunDual` 📖	—	`MeasureTheory.charFunDual`	—	—	`MeasureTheory.ext_of_integral_char_eq` `instIsTopologicalAddGroupReal` `Real.continuous_probChar` `Real.probChar_ne_one` `Algebra.to_smulCommClass` `LinearMap.ext_iff` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `NormedSpace.eq_zero_of_forall_dual_eq_zero` `IsBoundedBilinearMap.continuous` `RingHomIsometric.ids` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedBilinearMap.symm` `isBoundedBilinearMap_apply`

---

← Back to Index