Documentation Verification Report

TaylorExpansion

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

Statistics

Metric	Count
Definitions	0
Theorems `contDiff_charFun`, `contDiff_charFun'`, `continuous_charFun`, `iteratedDeriv_charFun`, `iteratedDeriv_charFun_zero`, `iteratedFDeriv_charFun`, `taylorWithinEval_charFun_two_zero`, `taylorWithinEval_charFun_two_zero'`, `taylorWithinEval_charFun_zero`, `taylor_charFun_two`	10
Total	10

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contDiff_charFun` 📖	mathematical	`MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENNReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Complex` `Complex.instNormedAddCommGroup` `instInnerProductSpaceRealComplex` `WithTop` `ENat` `WithTop.natCast` `ENat.instNatCast` `charFun` `InnerProductSpace.toInner`	—	`Nat.instAtLeastTwoHAddOfNat` `charFun_eq_fourierIntegral'` `ContDiff.comp` `instIsTopologicalAddGroupReal` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `VectorFourier.contDiff_fourierIntegral` `CStarRing.norm_of_mem_unitary` `RCLike.instCStarRing` `Complex.instNontrivial` `SubmonoidClass.toOneMemClass` `Submonoid.instSubmonoidClass` `mul_one` `MemLp.integrable_norm_pow'` `MemLp.mono_exponent` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `ENNReal.instIsOrderedRing` `ENNReal.instCharZero` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid` `contDiff_const_smul` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul`
`contDiff_charFun'` 📖	mathematical	`MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENNReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Complex` `Complex.instNormedAddCommGroup` `instInnerProductSpaceRealComplex` `WithTop.some` `ENat` `charFun` `InnerProductSpace.toInner`	—	`Nat.instAtLeastTwoHAddOfNat` `charFun_eq_fourierIntegral'` `ContDiff.comp` `instIsTopologicalAddGroupReal` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `VectorFourier.contDiff_fourierIntegral` `CStarRing.norm_of_mem_unitary` `RCLike.instCStarRing` `Complex.instNontrivial` `SubmonoidClass.toOneMemClass` `Submonoid.instSubmonoidClass` `mul_one` `MemLp.integrable_norm_pow'` `MemLp.mono_exponent` `instReflLe` `contDiff_const_smul` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul`
`continuous_charFun` 📖	mathematical	—	`Continuous` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `charFun` `InnerProductSpace.toInner` `Real` `Real.instRCLike`	—	`contDiff_zero` `contDiff_charFun` `CharP.cast_eq_zero` `CharP.ofCharZero` `ENNReal.instCharZero` `aestronglyMeasurable_id` `PseudoEMetricSpace.pseudoMetrizableSpace` `BorelSpace.opensMeasurable`
`iteratedDeriv_charFun` 📖	mathematical	`MemLp` `Real` `Real.measurableSpace` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `SeminormedAddGroup.toContinuousENorm` `Real.pseudoMetricSpace` `ENNReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`iteratedDeriv` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Complex` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex` `charFun` `Real.measurableSpace` `InnerProductSpace.toInner` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toInnerProductSpaceReal` `Complex.instMul` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Complex.I` `integral` `Complex.ofReal` `Complex.exp`	—	`iteratedDeriv.eq_1` `iteratedFDeriv_charFun` `Real.borelSpace` `instSecondCountableTopologyReal` `Finset.prod_congr` `conj_trivial` `instTrivialStarReal` `one_mul` `Finset.prod_const` `Fintype.card_fin` `Complex.ofReal_pow` `Complex.ofReal_mul`
`iteratedDeriv_charFun_zero` 📖	mathematical	`MemLp` `Real` `Real.measurableSpace` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `SeminormedAddGroup.toContinuousENorm` `Real.pseudoMetricSpace` `ENNReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`iteratedDeriv` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Complex` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex` `charFun` `Real.measurableSpace` `InnerProductSpace.toInner` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toInnerProductSpaceReal` `Real.instZero` `Complex.instMul` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Complex.I` `Complex.ofReal` `integral` `Real.normedAddCommGroup` `Real.instMonoid`	—	`iteratedDeriv_charFun` `MulZeroClass.zero_mul` `Complex.exp_zero` `mul_one` `IsCancelMulZero.toIsLeftCancelMulZero` `IsDomain.toIsCancelMulZero` `instIsDomain` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Complex.instNontrivial` `integral_complex_ofReal`
`iteratedFDeriv_charFun` 📖	mathematical	`MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENNReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`DFunLike.coe` `ContinuousMultilinearMap` `Real` `Complex` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `instInnerProductSpaceRealComplex` `ContinuousMultilinearMap.funLike` `iteratedFDeriv` `charFun` `InnerProductSpace.toInner` `Complex.instMul` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Complex.I` `integral` `Complex.ofReal` `Finset.prod` `Real.instCommMonoid` `Finset.univ` `Fin.fintype` `Inner.inner` `Complex.exp`	—	`Algebra.to_smulCommClass` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `CStarRing.norm_of_mem_unitary` `RCLike.instCStarRing` `Complex.instNontrivial` `SubmonoidClass.toOneMemClass` `Submonoid.instSubmonoidClass` `mul_one` `MemLp.integrable_norm_pow'` `MemLp.mono_exponent` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `ENNReal.instIsOrderedRing` `ENNReal.instCharZero` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid` `Nat.instAtLeastTwoHAddOfNat` `charFun_eq_fourierIntegral'` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `iteratedFDeriv_comp_const_smul` `VectorFourier.contDiff_fourierIntegral` `mul_inv_rev` `neg_smul` `SMulCommClass.complexToReal` `instIsTopologicalAddGroupReal` `instIsTopologicalRingReal` `VectorFourier.iteratedFDeriv_fourierIntegral` `aestronglyMeasurable_one` `le_rfl` `Complex.ofReal_pow` `Complex.ofReal_neg` `Complex.ofReal_mul` `Complex.ofReal_inv` `Complex.ofReal_prod` `VectorFourier.fourierIntegral_continuousMultilinearMap_apply` `Real.continuous_fourierChar` `VectorFourier.integrable_fourierPowSMulRight` `map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `neg_neg` `IsSemitopologicalSemiring.toContinuousAdd` `VectorFourier.fourierPowSMulRight_apply` `Finset.prod_congr` `mul_left_comm` `integral_const_mul` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `neg_mul_neg` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `one_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `Mathlib.Meta.NormNum.isNat_eq_false` `Complex.instCharZero` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_zero` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `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`
`taylorWithinEval_charFun_two_zero` 📖	mathematical	`AEMeasurable` `Real` `Real.measurableSpace` `MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `SeminormedAddGroup.toContinuousENorm` `Real.pseudoMetricSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `Measure.map`	`taylorWithinEval` `Complex` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex` `charFun` `Real.measurableSpace` `InnerProductSpace.toInner` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toInnerProductSpaceReal` `Measure.map` `Set.univ` `Real.instZero` `Complex.instSub` `Complex.instAdd` `Complex.instOne` `Complex.instMul` `Complex.ofReal` `integral` `Real.normedAddCommGroup` `Complex.I` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Monoid.toPow` `Pi.monoid` `Real.instMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `Measure.isProbabilityMeasure_map` `Finset.sum_range_succ` `Finset.sum_singleton` `Nat.cast_one` `inv_one` `pow_zero` `mul_one` `integral_const` `Real.instCompleteSpace` `probReal_univ` `pow_one` `one_mul` `integral_map` `aestronglyMeasurable_id` `PseudoEMetricSpace.pseudoMetrizableSpace` `BorelSpace.opensMeasurable` `Real.borelSpace` `instSecondCountableTopologyReal` `Continuous.aestronglyMeasurable` `secondCountableTopologyEither_of_right` `Continuous.pow` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `continuous_id'` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `div_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `Mathlib.Meta.NormNum.isNat_eq_false` `Complex.instCharZero` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_zero` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.pow_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.zpow'_ofNat` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Complex.I_sq` `mul_neg` `neg_mul` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.atom_pf` `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` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.neg_congr` `taylorWithinEval_charFun_zero` `Measure.isFiniteMeasure_map` `IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure`
`taylorWithinEval_charFun_two_zero'` 📖	mathematical	`AEMeasurable` `Real` `Real.measurableSpace` `integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.instZero` `Monoid.toPow` `Pi.monoid` `Real.instMonoid` `Real.instOne`	`taylorWithinEval` `Complex` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex` `charFun` `Real.measurableSpace` `InnerProductSpace.toInner` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toInnerProductSpaceReal` `Measure.map` `Set.univ` `Real.instZero` `Complex.instSub` `Complex.instOne` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Complex.ofReal` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `taylorWithinEval_charFun_two_zero` `memLp_two_iff_integrable_sq` `aestronglyMeasurable_id` `PseudoEMetricSpace.pseudoMetrizableSpace` `BorelSpace.opensMeasurable` `Real.borelSpace` `instSecondCountableTopologyReal` `Integrable.of_integral_ne_zero` `integral_map` `Continuous.comp_aestronglyMeasurable` `Continuous.pow` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `continuous_id'` `NeZero.charZero_one` `RCLike.charZero_rclike` `MulZeroClass.zero_mul` `add_zero` `one_mul`
`taylorWithinEval_charFun_zero` 📖	mathematical	`MemLp` `Real` `Real.measurableSpace` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `SeminormedAddGroup.toContinuousENorm` `Real.pseudoMetricSpace` `ENNReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`taylorWithinEval` `Complex` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex` `charFun` `Real.measurableSpace` `InnerProductSpace.toInner` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toInnerProductSpaceReal` `Set.univ` `Real.instZero` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.range` `Complex.instMul` `Complex.instInv` `Complex.instNatCast` `Nat.factorial` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Complex.ofReal` `Complex.I` `integral` `Real.normedAddCommGroup` `Real.instMonoid`	—	`taylor_within_apply` `Finset.sum_congr` `sub_zero` `RCLike.real_smul_eq_coe_mul` `algebraMap.coe_mul` `RCLike.ofReal_inv` `algebraMap.coe_natCast` `algebraMap.coe_pow` `MemLp.mono_exponent` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `ENNReal.instIsOrderedRing` `ENNReal.instCharZero` `Nat.instNoMaxOrder` `mul_comm` `iteratedDerivWithin_univ` `iteratedDeriv_charFun_zero` `mul_left_comm` `mul_assoc` `mul_pow`
`taylor_charFun_two` 📖	mathematical	`AEMeasurable` `Real` `Real.measurableSpace` `integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.instZero` `Monoid.toPow` `Pi.monoid` `Real.instMonoid` `Real.instOne`	`Asymptotics.IsLittleO` `Real` `Complex` `Complex.instNorm` `Real.norm` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero` `Complex.instSub` `charFun` `Real.measurableSpace` `InnerProductSpace.toInner` `Real.instRCLike` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toInnerProductSpaceReal` `Measure.map` `Complex.instOne` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Complex.ofReal` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.instMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `taylorWithinEval_charFun_two_zero'` `sub_zero` `taylor_isLittleO_univ` `contDiff_charFun` `Real.borelSpace` `instSecondCountableTopologyReal` `Measure.isFiniteMeasure_map` `IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `memLp_two_iff_integrable_sq` `aestronglyMeasurable_id` `PseudoEMetricSpace.pseudoMetrizableSpace` `BorelSpace.opensMeasurable` `Integrable.of_integral_ne_zero` `integral_map` `Continuous.comp_aestronglyMeasurable` `Continuous.pow` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `continuous_id'` `NeZero.charZero_one` `RCLike.charZero_rclike`

---

← Back to Index