FourierTransformDeriv

📁 Source: Mathlib/Analysis/Fourier/FourierTransformDeriv.lean

Statistics

Metric	Count
Definitions `fourierPowSMulRight`, `fourierSMulRight`	2
Theorems `fourierPowSMulRight`, `fourierPowSMulRight`, `fourierPowSMulRight`, `fourierSMulRight`, `contDiff_fourier`, `contDiff_fourierIntegral`, `deriv_fourier`, `deriv_fourierChar`, `deriv_fourierIntegral`, `differentiable_fourier`, `differentiable_fourierChar`, `differentiable_fourierChar_neg_bilinear_left`, `differentiable_fourierChar_neg_bilinear_right`, `differentiable_fourierIntegral`, `fderiv_fourier`, `fderiv_fourierChar_neg_bilinear_left_apply`, `fderiv_fourierChar_neg_bilinear_right_apply`, `fderiv_fourierIntegral`, `fourierIntegral_deriv`, `fourierIntegral_fderiv`, `fourierIntegral_iteratedDeriv`, `fourierIntegral_iteratedFDeriv`, `fourier_deriv`, `fourier_fderiv`, `fourier_iteratedDeriv`, `fourier_iteratedFDeriv`, `hasDerivAt_fourier`, `hasDerivAt_fourierChar`, `hasDerivAt_fourierIntegral`, `hasFDerivAt_fourier`, `hasFDerivAt_fourierChar_neg_bilinear_left`, `hasFDerivAt_fourierChar_neg_bilinear_right`, `hasFDerivAt_fourierIntegral`, `iteratedDeriv_fourier`, `iteratedDeriv_fourierIntegral`, `iteratedFDeriv_fourier`, `iteratedFDeriv_fourierIntegral`, `pow_mul_norm_iteratedFDeriv_fourierIntegral_le`, `pow_mul_norm_iteratedFDeriv_fourier_le`, `contDiff_fourierIntegral`, `differentiable_fourierIntegral`, `fderiv_fourierIntegral`, `fourierIntegral_fderiv`, `fourierIntegral_iteratedFDeriv`, `fourierPowSMulRight_apply`, `fourierPowSMulRight_eq_comp`, `fourierPowSMulRight_iteratedFDeriv_fourierIntegral`, `fourierSMulRight_apply`, `hasFDerivAt_fourierChar_smul`, `hasFDerivAt_fourierIntegral`, `hasFTaylorSeriesUpTo_fourierIntegral`, `hasFTaylorSeriesUpTo_fourierIntegral'`, `integrable_fourierPowSMulRight`, `iteratedFDeriv_fourierIntegral`, `norm_fourierPowSMulRight_iteratedFDeriv_fourierIntegral_le`, `norm_fourierPowSMulRight_le`, `norm_fourierSMulRight`, `norm_fourierSMulRight_le`, `norm_iteratedFDeriv_fourierPowSMulRight`, `pow_mul_norm_iteratedFDeriv_fourierIntegral_le`	60
Total	62

ContDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fourierPowSMulRight` 📖	mathematical	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedSpace.complexToReal` `NormedAddCommGroup.toSeminormedAddCommGroup`	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `ContinuousMultilinearMap` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `NormedSpace.complexToReal` `ContinuousMultilinearMap.normedAddCommGroup'` `Fin.fintype` `ContinuousMultilinearMap.normedSpace'` `NontriviallyNormedField.toNormedField` `smulCommClass_self` `Real.instCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Real.commRing` `VectorFourier.fourierPowSMulRight`	—	`instIsTopologicalAddGroupReal` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `smulCommClass_self` `const_smul` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `SMulCommClass.complexToReal` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousMultilinearMap.instSMulCommClass` `ContinuousMultilinearMap.instContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousMultilinearMap.instIsTopologicalAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `Nat.instAtLeastTwoHAddOfNat` `comp₂` `IsBoundedBilinearMap.contDiff` `ContinuousLinearMap.isBoundedBilinearMap` `comp` `RingHomIsometric.ids` `ContinuousMultilinearMap.contDiff` `contDiff_pi` `ContinuousLinearMap.contDiff`

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fourierPowSMulRight` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`Continuous` `ContinuousMultilinearMap` `Real` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `NormedSpace.complexToReal` `ContinuousMultilinearMap.instTopologicalSpace` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `VectorFourier.fourierPowSMulRight`	—	`instIsTopologicalAddGroupReal` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `const_smul` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `SMulCommClass.complexToReal` `smulCommClass_self` `ContinuousMultilinearMap.instContinuousConstSMul` `IsTopologicalAddGroup.toContinuousAdd` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousMultilinearMap.instIsTopologicalAddGroup` `ContinuousMultilinearMap.instSMulCommClass` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `comp₂` `ContinuousLinearMap.continuous₂` `comp` `ContinuousMapClass.map_continuous` `ContinuousMultilinearMap.continuousMapClass` `continuous_pi` `ContinuousLinearMap.continuous` `Nat.instAtLeastTwoHAddOfNat`

MeasureTheory.AEStronglyMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fourierPowSMulRight` 📖	mathematical	`MeasureTheory.AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`MeasureTheory.AEStronglyMeasurable` `ContinuousMultilinearMap` `Real` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `NormedSpace.complexToReal` `ContinuousMultilinearMap.instTopologicalSpace` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `VectorFourier.fourierPowSMulRight`	—	`instIsTopologicalAddGroupReal` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `const_smul'` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousMultilinearMap.instIsTopologicalAddGroup` `ContinuousMultilinearMap.instSMulCommClass` `ContinuousMultilinearMap.instContinuousConstSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `SMulCommClass.complexToReal` `Continuous.comp_aestronglyMeasurable₂` `ContinuousLinearMap.continuous₂` `Continuous.aestronglyMeasurable` `BorelSpace.opensMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `secondCountableTopologyEither_of_left` `Continuous.comp` `ContinuousMapClass.map_continuous` `ContinuousMultilinearMap.continuousMapClass` `continuous_pi` `ContinuousLinearMap.continuous` `Nat.instAtLeastTwoHAddOfNat`
`fourierSMulRight` 📖	mathematical	`MeasureTheory.AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`MeasureTheory.AEStronglyMeasurable` `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` `NormedSpace.complexToReal` `ContinuousLinearMap.topologicalSpace` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `VectorFourier.fourierSMulRight`	—	`instIsTopologicalAddGroupReal` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `const_smul'` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.continuousConstSMul` `IsScalarTower.left` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.continuous₂` `RingHomIsometric.ids` `smulCommClass_self` `prodMk` `Continuous.aestronglyMeasurable` `BorelSpace.opensMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `ContinuousLinearMap.continuous` `Continuous.comp_aestronglyMeasurable`

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contDiff_fourier` 📖	mathematical	`MeasureTheory.Integrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `instMul` `Monoid.toPow` `instMonoid` `Norm.norm` `NormedAddCommGroup.toNorm` `MeasureTheory.MeasureSpace.volume` `measureSpaceOfInnerProductSpace`	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `InnerProductSpace.toNormedSpace` `instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.complexToReal` `WithTop.some` `ENat` `FourierTransform.fourier` `instFourierTransform`	—	`VectorFourier.contDiff_fourierIntegral` `secondCountable_of_proper` `FiniteDimensional.proper_real`
`contDiff_fourierIntegral` 📖	mathematical	`MeasureTheory.Integrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `instMul` `Monoid.toPow` `instMonoid` `Norm.norm` `NormedAddCommGroup.toNorm` `MeasureTheory.MeasureSpace.volume` `measureSpaceOfInnerProductSpace`	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `InnerProductSpace.toNormedSpace` `instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.complexToReal` `WithTop.some` `ENat` `FourierTransform.fourier` `instFourierTransform`	—	`contDiff_fourier`
`deriv_fourier` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `MeasureTheory.MeasureSpace.volume` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `instMonoid` `Module.toDistribMulAction` `semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `normedField` `NormedSpace.complexToReal`	`deriv` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.complexToReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `FourierTransform.fourier` `instFourierTransform` `normedAddCommGroup` `RCLike.toInnerProductSpaceReal` `instRCLike` `measurableSpace` `borelSpace` `FiniteDimensional.rclike_to_real` `Complex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `Complex.instNormedField` `Complex.instMul` `Complex.instNeg` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `pi` `Complex.I`	—	`borelSpace` `FiniteDimensional.rclike_to_real` `Nat.instAtLeastTwoHAddOfNat` `HasDerivAt.deriv` `hasDerivAt_fourier`
`deriv_fourierChar` 📖	mathematical	—	`deriv` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `Complex` `Complex.addCommGroup` `NormedSpace.toModule` `normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `InnerProductSpace.toNormedSpace` `instRCLike` `instInnerProductSpaceRealComplex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.unitSphere` `DFunLike.coe` `AddChar` `instAddMonoid` `Circle` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `AddChar.instFunLike` `fourierChar` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `pi` `Complex.I`	—	`HasDerivAt.deriv` `Nat.instAtLeastTwoHAddOfNat` `hasDerivAt_fourierChar`
`deriv_fourierIntegral` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `MeasureTheory.MeasureSpace.volume` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `instMonoid` `Module.toDistribMulAction` `semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `normedField` `NormedSpace.complexToReal`	`deriv` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.complexToReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `FourierTransform.fourier` `instFourierTransform` `normedAddCommGroup` `RCLike.toInnerProductSpaceReal` `instRCLike` `measurableSpace` `borelSpace` `FiniteDimensional.rclike_to_real` `Complex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `Complex.instNormedField` `Complex.instMul` `Complex.instNeg` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `pi` `Complex.I`	—	`deriv_fourier`
`differentiable_fourier` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `MeasureTheory.MeasureSpace.volume` `Real` `pseudoMetricSpace` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `instMul` `Norm.norm` `NormedAddCommGroup.toNorm`	`Differentiable` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedSpace.complexToReal` `FourierTransform.fourier` `instFourierTransform`	—	`VectorFourier.differentiable_fourierIntegral` `secondCountable_of_proper` `FiniteDimensional.proper_real`
`differentiable_fourierChar` 📖	mathematical	—	`Differentiable` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `instAddCommGroup` `NormedSpace.toModule` `normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `InnerProductSpace.toNormedSpace` `instRCLike` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `Complex` `Complex.addCommGroup` `NormedField.toNormedCommRing` `Complex.instNormedField` `instInnerProductSpaceRealComplex` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.unitSphere` `DFunLike.coe` `AddChar` `instAddMonoid` `Circle` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `AddChar.instFunLike` `fourierChar`	—	`HasDerivAt.differentiableAt` `Nat.instAtLeastTwoHAddOfNat` `hasDerivAt_fourierChar`
`differentiable_fourierChar_neg_bilinear_left` 📖	mathematical	—	`Differentiable` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Complex` `Complex.addCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `InnerProductSpace.toNormedSpace` `instRCLike` `instInnerProductSpaceRealComplex` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.unitSphere` `DFunLike.coe` `AddChar` `instAddMonoid` `Circle` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `AddChar.instFunLike` `fourierChar` `instNeg` `ContinuousLinearMap` `semiring` `RingHom.id` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `pseudoMetricSpace` `instAddCommMonoid` `normedCommRing` `RCLike.toInnerProductSpaceReal` `ContinuousLinearMap.funLike` `ContinuousLinearMap.topologicalSpace` `instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousLinearMap.addCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `ContinuousLinearMap.module` `Algebra.to_smulCommClass` `instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `SeparatelyContinuousMul.to_continuousSMul` `instMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul`	—	`instIsTopologicalAddGroupReal` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `HasFDerivAt.differentiableAt` `Localization.instSMulCommClassOfIsScalarTower` `IsScalarTower.complexToReal` `IsScalarTower.right` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Nat.instAtLeastTwoHAddOfNat` `RingHomCompTriple.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `RingHomIsometric.ids` `hasFDerivAt_fourierChar_neg_bilinear_left`
`differentiable_fourierChar_neg_bilinear_right` 📖	mathematical	—	`Differentiable` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Complex` `Complex.addCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `InnerProductSpace.toNormedSpace` `instRCLike` `instInnerProductSpaceRealComplex` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.unitSphere` `DFunLike.coe` `AddChar` `instAddMonoid` `Circle` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `AddChar.instFunLike` `fourierChar` `instNeg` `ContinuousLinearMap` `semiring` `RingHom.id` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `pseudoMetricSpace` `instAddCommMonoid` `normedCommRing` `RCLike.toInnerProductSpaceReal` `ContinuousLinearMap.funLike` `ContinuousLinearMap.topologicalSpace` `instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousLinearMap.addCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `ContinuousLinearMap.module` `Algebra.to_smulCommClass` `instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `SeparatelyContinuousMul.to_continuousSMul` `instMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul`	—	`instIsTopologicalAddGroupReal` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `HasFDerivAt.differentiableAt` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Nat.instAtLeastTwoHAddOfNat` `RingHomCompTriple.ids` `hasFDerivAt_fourierChar_neg_bilinear_right`
`differentiable_fourierIntegral` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `MeasureTheory.MeasureSpace.volume` `Real` `pseudoMetricSpace` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `instMul` `Norm.norm` `NormedAddCommGroup.toNorm`	`Differentiable` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedSpace.complexToReal` `FourierTransform.fourier` `instFourierTransform`	—	`differentiable_fourier`
`fderiv_fourier` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `MeasureTheory.MeasureSpace.volume` `Real` `pseudoMetricSpace` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `instMul` `Norm.norm` `NormedAddCommGroup.toNorm`	`fderiv` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedSpace.complexToReal` `FourierTransform.fourier` `instFourierTransform` `ContinuousLinearMap` `semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `ContinuousLinearMap.toNormedSpace` `Complex` `Complex.instNormedField` `SMulCommClass.complexToReal` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `smulCommClass_self` `CommRing.toCommMonoid` `Complex.commRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `VectorFourier.fourierSMulRight` `innerSL`	—	`VectorFourier.fderiv_fourierIntegral` `secondCountable_of_proper` `FiniteDimensional.proper_real`
`fderiv_fourierChar_neg_bilinear_left_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Complex` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Complex.addCommGroup` `NormedSpace.toModule` `normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `InnerProductSpace.toNormedSpace` `instRCLike` `instInnerProductSpaceRealComplex` `ContinuousLinearMap.funLike` `fderiv` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Ring.toSemiring` `SeminormedRing.toRing` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.unitSphere` `AddChar` `instAddMonoid` `Circle` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `AddChar.instFunLike` `fourierChar` `instNeg` `semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `pseudoMetricSpace` `instAddCommMonoid` `normedCommRing` `RCLike.toInnerProductSpaceReal` `ContinuousLinearMap.topologicalSpace` `instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousLinearMap.addCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `ContinuousLinearMap.module` `Algebra.to_smulCommClass` `instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `SeparatelyContinuousMul.to_continuousSMul` `instMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `Complex.instMul` `Complex.instNeg` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `pi` `Complex.I`	—	`instIsTopologicalAddGroupReal` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `Nat.instAtLeastTwoHAddOfNat` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Localization.instSMulCommClassOfIsScalarTower` `IsScalarTower.complexToReal` `IsScalarTower.right` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `RingHomCompTriple.ids` `RingHomIsometric.ids` `HasFDerivAt.fderiv` `IsBoundedSMul.continuousSMul` `Complex.instT2Space` `hasFDerivAt_fourierChar_neg_bilinear_left` `neg_mul` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_left`
`fderiv_fourierChar_neg_bilinear_right_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Complex` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Complex.addCommGroup` `NormedSpace.toModule` `normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `InnerProductSpace.toNormedSpace` `instRCLike` `instInnerProductSpaceRealComplex` `ContinuousLinearMap.funLike` `fderiv` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Ring.toSemiring` `SeminormedRing.toRing` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.unitSphere` `AddChar` `instAddMonoid` `Circle` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `AddChar.instFunLike` `fourierChar` `instNeg` `semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `pseudoMetricSpace` `instAddCommMonoid` `normedCommRing` `RCLike.toInnerProductSpaceReal` `ContinuousLinearMap.topologicalSpace` `instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousLinearMap.addCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `ContinuousLinearMap.module` `Algebra.to_smulCommClass` `instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `SeparatelyContinuousMul.to_continuousSMul` `instMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `Complex.instMul` `Complex.instNeg` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `pi` `Complex.I`	—	`instIsTopologicalAddGroupReal` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `Nat.instAtLeastTwoHAddOfNat` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `RingHomCompTriple.ids` `HasFDerivAt.fderiv` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Complex.instT2Space` `hasFDerivAt_fourierChar_neg_bilinear_right` `neg_mul` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_left`
`fderiv_fourierIntegral` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `MeasureTheory.MeasureSpace.volume` `Real` `pseudoMetricSpace` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `instMul` `Norm.norm` `NormedAddCommGroup.toNorm`	`fderiv` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedSpace.complexToReal` `FourierTransform.fourier` `instFourierTransform` `ContinuousLinearMap` `semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `ContinuousLinearMap.toNormedSpace` `Complex` `Complex.instNormedField` `SMulCommClass.complexToReal` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `smulCommClass_self` `CommRing.toCommMonoid` `Complex.commRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `VectorFourier.fourierSMulRight` `innerSL`	—	`fderiv_fourier`
`fourierIntegral_deriv` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `MeasureTheory.MeasureSpace.volume` `Differentiable` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `instAddCommGroup` `NormedSpace.toModule` `normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `InnerProductSpace.toNormedSpace` `instRCLike` `RCLike.toInnerProductSpaceReal` `pseudoMetricSpace` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.complexToReal` `deriv`	`FourierTransform.fourier` `instFourierTransform` `Real` `normedAddCommGroup` `RCLike.toInnerProductSpaceReal` `instRCLike` `measurableSpace` `borelSpace` `FiniteDimensional.rclike_to_real` `deriv` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.complexToReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Complex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `Complex.instNormedField` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `pi` `Complex.I`	—	`fourier_deriv`
`fourierIntegral_fderiv` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `MeasureTheory.MeasureSpace.volume` `Differentiable` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `normedField` `InnerProductSpace.toNormedSpace` `instRCLike` `NormedSpace.complexToReal` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `fderiv`	`FourierTransform.fourier` `instFourierTransform` `ContinuousLinearMap` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `normedField` `InnerProductSpace.toNormedSpace` `instRCLike` `NormedSpace.complexToReal` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `ContinuousLinearMap.toNormedSpace` `Complex` `Complex.instNormedField` `SMulCommClass.complexToReal` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `SeminormedAddCommGroup.toAddCommGroup` `smulCommClass_self` `CommRing.toCommMonoid` `Complex.commRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Ring.toSemiring` `CommRing.toRing` `fderiv` `VectorFourier.fourierSMulRight` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `starRingEnd` `Semifield.toCommSemiring` `RCLike.toStarRing` `SeminormedRing.toPseudoMetricSpace` `NormedField.toNormedCommRing` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `RCLike.innerProductSpace` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.addCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousLinearMap.module` `Algebra.to_smulCommClass` `CommSemiring.toSemiring` `Algebra.id` `SeparatelyContinuousMul.to_continuousSMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `ContinuousLinearMap.neg` `instRing` `ContinuousLinearMap.addCommGroup` `instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousLinearMap.topologicalAddGroup` `innerSL`	—	`fourier_fderiv`
`fourierIntegral_iteratedDeriv` 📖	mathematical	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `normedAddCommGroup` `InnerProductSpace.toNormedSpace` `instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `NormedSpace.complexToReal` `WithTop.some` `ENat` `MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `measurableSpace` `iteratedDeriv` `MeasureTheory.MeasureSpace.volume` `measureSpace` `instLEENat` `ENat.instNatCast`	`FourierTransform.fourier` `instFourierTransform` `Real` `normedAddCommGroup` `RCLike.toInnerProductSpaceReal` `instRCLike` `measurableSpace` `borelSpace` `FiniteDimensional.rclike_to_real` `iteratedDeriv` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `NormedSpace.complexToReal` `NormedAddCommGroup.toSeminormedAddCommGroup` `Complex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Complex.instNormedField` `Monoid.toPow` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `pi` `Complex.I`	—	`fourier_iteratedDeriv`
`fourierIntegral_iteratedFDeriv` 📖	mathematical	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `InnerProductSpace.toNormedSpace` `instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.complexToReal` `WithTop.some` `ENat` `MeasureTheory.Integrable` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.instTopologicalSpace` `normedField` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `ContinuousMultilinearMap.seminormedAddCommGroup'` `Fin.fintype` `iteratedFDeriv` `MeasureTheory.MeasureSpace.volume` `measureSpaceOfInnerProductSpace` `instLEENat` `ENat.instNatCast`	`FourierTransform.fourier` `instFourierTransform` `ContinuousMultilinearMap` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `instRCLike` `NormedSpace.complexToReal` `ContinuousMultilinearMap.normedAddCommGroup'` `Fin.fintype` `ContinuousMultilinearMap.normedSpace'` `Complex` `Complex.instNormedField` `SMulCommClass.complexToReal` `NormedAddCommGroup.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `smulCommClass_self` `CommRing.toCommMonoid` `Complex.commRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `iteratedFDeriv` `VectorFourier.fourierPowSMulRight` `ContinuousLinearMap` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `starRingEnd` `Semifield.toCommSemiring` `RCLike.toStarRing` `RingHom.id` `Semiring.toNonAssocSemiring` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `RCLike.innerProductSpace` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.addCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousLinearMap.module` `Algebra.to_smulCommClass` `CommSemiring.toSemiring` `Algebra.id` `SeparatelyContinuousMul.to_continuousSMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `ContinuousLinearMap.neg` `instRing` `ContinuousLinearMap.addCommGroup` `instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousLinearMap.topologicalAddGroup` `normedField` `innerSL`	—	`fourier_iteratedFDeriv`
`fourier_deriv` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `MeasureTheory.MeasureSpace.volume` `Differentiable` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `instAddCommGroup` `NormedSpace.toModule` `normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `InnerProductSpace.toNormedSpace` `instRCLike` `RCLike.toInnerProductSpaceReal` `pseudoMetricSpace` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.complexToReal` `deriv`	`FourierTransform.fourier` `instFourierTransform` `Real` `normedAddCommGroup` `RCLike.toInnerProductSpaceReal` `instRCLike` `measurableSpace` `borelSpace` `FiniteDimensional.rclike_to_real` `deriv` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.complexToReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Complex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `Complex.instNormedField` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `pi` `Complex.I`	—	`borelSpace` `FiniteDimensional.rclike_to_real` `Nat.instAtLeastTwoHAddOfNat` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `RingHomIsometric.ids` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.integrable_comp` `smulCommClass_self` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `ContinuousLinearMap.topologicalAddGroup` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `ContinuousLinearMap.smulCommClass` `ContinuousLinearMap.continuousConstSMul` `SMulCommClass.complexToReal` `fourier_continuousLinearMap_apply` `instIsTopologicalAddGroupReal` `fourier_fderiv` `instIsTopologicalRingReal` `RCLike.inner_apply'` `conj_trivial` `instTrivialStarReal` `mul_one` `neg_smul` `smul_neg` `smul_smul` `neg_mul` `neg_neg`
`fourier_fderiv` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `MeasureTheory.MeasureSpace.volume` `Differentiable` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `normedField` `InnerProductSpace.toNormedSpace` `instRCLike` `NormedSpace.complexToReal` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `fderiv`	`FourierTransform.fourier` `instFourierTransform` `ContinuousLinearMap` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `normedField` `InnerProductSpace.toNormedSpace` `instRCLike` `NormedSpace.complexToReal` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `ContinuousLinearMap.toNormedSpace` `Complex` `Complex.instNormedField` `SMulCommClass.complexToReal` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `SeminormedAddCommGroup.toAddCommGroup` `smulCommClass_self` `CommRing.toCommMonoid` `Complex.commRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Ring.toSemiring` `CommRing.toRing` `fderiv` `VectorFourier.fourierSMulRight` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `starRingEnd` `Semifield.toCommSemiring` `RCLike.toStarRing` `SeminormedRing.toPseudoMetricSpace` `NormedField.toNormedCommRing` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `RCLike.innerProductSpace` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.addCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousLinearMap.module` `Algebra.to_smulCommClass` `CommSemiring.toSemiring` `Algebra.id` `SeparatelyContinuousMul.to_continuousSMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `ContinuousLinearMap.neg` `instRing` `ContinuousLinearMap.addCommGroup` `instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousLinearMap.topologicalAddGroup` `innerSL`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `RingHomIsometric.ids` `SMulCommClass.complexToReal` `smulCommClass_self` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `instIsTopologicalAddGroupReal` `ContinuousLinearMap.topologicalAddGroup` `RingHomIsometric.starRingEnd` `CStarRing.to_normedStarGroup` `instCStarRingReal` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `flip_innerSL_real` `VectorFourier.fourierIntegral_fderiv` `instIsAddHaarMeasureVolume`
`fourier_iteratedDeriv` 📖	mathematical	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `normedAddCommGroup` `InnerProductSpace.toNormedSpace` `instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `NormedSpace.complexToReal` `WithTop.some` `ENat` `MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `measurableSpace` `iteratedDeriv` `MeasureTheory.MeasureSpace.volume` `measureSpace` `instLEENat` `ENat.instNatCast`	`FourierTransform.fourier` `instFourierTransform` `Real` `normedAddCommGroup` `RCLike.toInnerProductSpaceReal` `instRCLike` `measurableSpace` `borelSpace` `FiniteDimensional.rclike_to_real` `iteratedDeriv` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `NormedSpace.complexToReal` `NormedAddCommGroup.toSeminormedAddCommGroup` `Complex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Complex.instNormedField` `Monoid.toPow` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `pi` `Complex.I`	—	`borelSpace` `FiniteDimensional.rclike_to_real` `Nat.instAtLeastTwoHAddOfNat` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `RingHomInvPair.ids` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `smulCommClass_self` `iteratedFDeriv_eq_equiv_comp` `LinearIsometryEquiv.integrable_comp_iff` `RingHomIsometric.ids` `SMulCommClass.complexToReal` `fourier_continuousMultilinearMap_apply` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `instIsTopologicalAddGroupReal` `ContinuousLinearMap.topologicalAddGroup` `fourier_iteratedFDeriv` `instIsTopologicalRingReal` `VectorFourier.fourierPowSMulRight_apply` `Finset.prod_congr` `conj_trivial` `instTrivialStarReal` `one_mul` `Finset.prod_const` `Fintype.card_fin` `Complex.ofReal_pow` `Complex.ofReal_neg` `smul_smul` `mul_neg` `neg_mul` `neg_neg`
`fourier_iteratedFDeriv` 📖	mathematical	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `InnerProductSpace.toNormedSpace` `instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.complexToReal` `WithTop.some` `ENat` `MeasureTheory.Integrable` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.instTopologicalSpace` `normedField` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `ContinuousMultilinearMap.seminormedAddCommGroup'` `Fin.fintype` `iteratedFDeriv` `MeasureTheory.MeasureSpace.volume` `measureSpaceOfInnerProductSpace` `instLEENat` `ENat.instNatCast`	`FourierTransform.fourier` `instFourierTransform` `ContinuousMultilinearMap` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `instRCLike` `NormedSpace.complexToReal` `ContinuousMultilinearMap.normedAddCommGroup'` `Fin.fintype` `ContinuousMultilinearMap.normedSpace'` `Complex` `Complex.instNormedField` `SMulCommClass.complexToReal` `NormedAddCommGroup.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `smulCommClass_self` `CommRing.toCommMonoid` `Complex.commRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `iteratedFDeriv` `VectorFourier.fourierPowSMulRight` `ContinuousLinearMap` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `starRingEnd` `Semifield.toCommSemiring` `RCLike.toStarRing` `RingHom.id` `Semiring.toNonAssocSemiring` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `RCLike.innerProductSpace` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.addCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousLinearMap.module` `Algebra.to_smulCommClass` `CommSemiring.toSemiring` `Algebra.id` `SeparatelyContinuousMul.to_continuousSMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `ContinuousLinearMap.neg` `instRing` `ContinuousLinearMap.addCommGroup` `instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousLinearMap.topologicalAddGroup` `normedField` `innerSL`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `SMulCommClass.complexToReal` `smulCommClass_self` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `instIsTopologicalAddGroupReal` `ContinuousLinearMap.topologicalAddGroup` `RingHomIsometric.ids` `RingHomIsometric.starRingEnd` `CStarRing.to_normedStarGroup` `instCStarRingReal` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `flip_innerSL_real` `VectorFourier.fourierIntegral_iteratedFDeriv` `instIsAddHaarMeasureVolume`
`hasDerivAt_fourier` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `MeasureTheory.MeasureSpace.volume` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `instMonoid` `Module.toDistribMulAction` `semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `normedField` `NormedSpace.complexToReal`	`HasDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.complexToReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `IsBoundedSMul.continuousSMul` `pseudoMetricSpace` `instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedSpace.toIsBoundedSMul` `FourierTransform.fourier` `instFourierTransform` `normedAddCommGroup` `RCLike.toInnerProductSpaceReal` `instRCLike` `measurableSpace` `borelSpace` `FiniteDimensional.rclike_to_real` `Complex` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `Complex.instNormedField` `Complex.instMul` `Complex.instNeg` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `pi` `Complex.I`	—	`norm_smul` `NormedSpace.toNormSMulClass` `MeasureTheory.Integrable.norm` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `RingHomIsometric.ids` `IsScalarTower.right` `Algebra.to_smulCommClass` `IsScalarTower.left` `IsBoundedSMul.continuousSMul` `RingHomInvPair.ids` `ContinuousLinearMap.ext_ring` `ContinuousLinearMap.smulRight_apply` `ContinuousLinearMap.flip_apply` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `ContinuousLinearMap.mul_apply'` `one_mul` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `one_smul` `ContinuousLinearMap.integrable_comp` `SMulCommClass.complexToReal` `instIsTopologicalAddGroupReal` `neg_smul` `Nat.instAtLeastTwoHAddOfNat` `neg_mul` `MeasureTheory.Integrable.smul` `borelSpace` `FiniteDimensional.rclike_to_real` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `instIsTopologicalRingReal` `IsScalarTower.to_smulCommClass'` `isScalarTower` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `ContinuousLinearMap.integral_apply` `VectorFourier.fourierIntegral_convergent_iff` `continuous_fourierChar` `ContinuousLinearMap.continuous₂` `SemigroupAction.mul_smul` `HasFDerivAt.hasDerivAt` `VectorFourier.hasFDerivAt_fourierIntegral` `instSecondCountableTopologyReal`
`hasDerivAt_fourierChar` 📖	mathematical	—	`HasDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `Complex` `Complex.addCommGroup` `NormedSpace.toModule` `normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `InnerProductSpace.toNormedSpace` `instRCLike` `instInnerProductSpaceRealComplex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `IsBoundedSMul.continuousSMul` `pseudoMetricSpace` `instZero` `Complex.instZero` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedSpace.toIsBoundedSMul` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.unitSphere` `DFunLike.coe` `AddChar` `instAddMonoid` `Circle` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `AddChar.instFunLike` `fourierChar` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `pi` `Complex.I`	—	`Nat.instAtLeastTwoHAddOfNat` `fourierChar_apply` `fourier_coe_apply` `Complex.ofReal_mul` `Int.cast_one` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.RingNF.mul_assoc_rev` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `add_zero` `Mathlib.Tactic.Ring.div_congr` `Nat.cast_one` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Complex.instCharZero` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `HasDerivAt.congr_simp` `mul_one` `div_one` `hasDerivAt_fourier`
`hasDerivAt_fourierIntegral` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpace` `MeasureTheory.MeasureSpace.volume` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `instMonoid` `Module.toDistribMulAction` `semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `normedField` `NormedSpace.complexToReal`	`HasDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.complexToReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `IsBoundedSMul.continuousSMul` `pseudoMetricSpace` `instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedSpace.toIsBoundedSMul` `FourierTransform.fourier` `instFourierTransform` `normedAddCommGroup` `RCLike.toInnerProductSpaceReal` `instRCLike` `measurableSpace` `borelSpace` `FiniteDimensional.rclike_to_real` `Complex` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `Complex.instNormedField` `Complex.instMul` `Complex.instNeg` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `pi` `Complex.I`	—	`hasDerivAt_fourier`
`hasFDerivAt_fourier` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `MeasureTheory.MeasureSpace.volume` `Real` `pseudoMetricSpace` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `instMul` `Norm.norm` `NormedAddCommGroup.toNorm`	`HasFDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedSpace.complexToReal` `FourierTransform.fourier` `instFourierTransform` `ContinuousLinearMap` `semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `ContinuousLinearMap.toNormedSpace` `Complex` `Complex.instNormedField` `SMulCommClass.complexToReal` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `smulCommClass_self` `CommRing.toCommMonoid` `Complex.commRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `VectorFourier.fourierSMulRight` `innerSL`	—	`VectorFourier.hasFDerivAt_fourierIntegral` `secondCountable_of_proper` `FiniteDimensional.proper_real`
`hasFDerivAt_fourierChar_neg_bilinear_left` 📖	mathematical	—	`HasFDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Complex` `Complex.addCommGroup` `normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `NormedSpace.complexToReal` `NormedField.toNormedSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.unitSphere` `DFunLike.coe` `AddChar` `instAddMonoid` `Circle` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `AddChar.instFunLike` `fourierChar` `instNeg` `ContinuousLinearMap` `semiring` `RingHom.id` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `pseudoMetricSpace` `instAddCommMonoid` `normedCommRing` `InnerProductSpace.toNormedSpace` `instRCLike` `RCLike.toInnerProductSpaceReal` `ContinuousLinearMap.funLike` `ContinuousLinearMap.topologicalSpace` `instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousLinearMap.addCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `ContinuousLinearMap.module` `Algebra.to_smulCommClass` `instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `SeparatelyContinuousMul.to_continuousSMul` `instMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Complex.instNormedAddCommGroup` `ContinuousLinearMap.instSMul` `NonUnitalNonAssocSemiring.toDistribSMul` `Localization.instSMulCommClassOfIsScalarTower` `CommRing.toCommMonoid` `Complex.commRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsScalarTower.complexToReal` `SemigroupAction.toSMul` `Monoid.toSemigroup` `CommMonoid.toMonoid` `MulAction.toSemigroupAction` `Monoid.toMulAction` `IsScalarTower.right` `Complex.instCommSemiring` `Complex.instMul` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Complex.instNeg` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `pi` `Complex.I` `ContinuousLinearMap.comp` `RingHomCompTriple.ids` `Complex.ofRealCLM` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `smulCommClass_self` `Field.toCommRing` `DistribMulAction.toMulAction` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.flip` `RingHomIsometric.ids`	—	`instIsTopologicalAddGroupReal` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `hasFDerivAt_fourierChar_neg_bilinear_right` `RingHomIsometric.ids`
`hasFDerivAt_fourierChar_neg_bilinear_right` 📖	mathematical	—	`HasFDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Complex` `Complex.addCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `NormedSpace.complexToReal` `NormedField.toNormedSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.unitSphere` `DFunLike.coe` `AddChar` `instAddMonoid` `Circle` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `AddChar.instFunLike` `fourierChar` `instNeg` `ContinuousLinearMap` `semiring` `RingHom.id` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `pseudoMetricSpace` `instAddCommMonoid` `normedCommRing` `InnerProductSpace.toNormedSpace` `instRCLike` `RCLike.toInnerProductSpaceReal` `ContinuousLinearMap.funLike` `ContinuousLinearMap.topologicalSpace` `instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousLinearMap.addCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `ContinuousLinearMap.module` `Algebra.to_smulCommClass` `instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `SeparatelyContinuousMul.to_continuousSMul` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Complex.instNormedAddCommGroup` `ContinuousLinearMap.instSMul` `NonUnitalNonAssocSemiring.toDistribSMul` `Semifield.toCommSemiring` `NormedAlgebra.toAlgebra` `RCLike.toNormedAlgebra` `Complex.instRCLike` `NonUnitalNonAssocSemiring.toMulZeroClass` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Complex.instMul` `Complex.instNeg` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `pi` `Complex.I` `ContinuousLinearMap.comp` `RingHomCompTriple.ids` `Complex.ofRealCLM`	—	`instIsTopologicalAddGroupReal` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `ContinuousLinearMap.hasFDerivAt` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Nat.instAtLeastTwoHAddOfNat` `RingHomCompTriple.ids` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.ext` `neg_mul` `ContinuousLinearMap.comp_neg` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `HasFDerivAt.comp` `HasDerivAt.hasFDerivAt` `hasDerivAt_fourierChar` `HasFDerivAt.neg`
`hasFDerivAt_fourierIntegral` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `MeasureTheory.MeasureSpace.volume` `Real` `pseudoMetricSpace` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `instMul` `Norm.norm` `NormedAddCommGroup.toNorm`	`HasFDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedSpace.complexToReal` `FourierTransform.fourier` `instFourierTransform` `ContinuousLinearMap` `semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `ContinuousLinearMap.toNormedSpace` `Complex` `Complex.instNormedField` `SMulCommClass.complexToReal` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `smulCommClass_self` `CommRing.toCommMonoid` `Complex.commRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `VectorFourier.fourierSMulRight` `innerSL`	—	`hasFDerivAt_fourier`
`iteratedDeriv_fourier` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Real` `measurableSpace` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `instMonoid` `Module.toDistribMulAction` `semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `normedField` `NormedSpace.complexToReal` `Monoid.toPow` `MeasureTheory.MeasureSpace.volume` `measureSpace` `ENat` `instLEENat` `ENat.instNatCast`	`iteratedDeriv` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `NormedSpace.complexToReal` `NormedAddCommGroup.toSeminormedAddCommGroup` `FourierTransform.fourier` `instFourierTransform` `normedAddCommGroup` `RCLike.toInnerProductSpaceReal` `instRCLike` `measurableSpace` `borelSpace` `FiniteDimensional.rclike_to_real` `Complex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Complex.instNormedField` `Monoid.toPow` `Complex.instMul` `Complex.instNeg` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `pi` `Complex.I`	—	`borelSpace` `FiniteDimensional.rclike_to_real` `Nat.instAtLeastTwoHAddOfNat` `norm_smul` `NormedSpace.toNormSMulClass` `norm_pow` `NormedDivisionRing.to_normOneClass` `NormedDivisionRing.toNormMulClass` `MeasureTheory.Integrable.norm` `pow_zero` `one_smul` `zero_le` `iteratedDeriv.eq_1` `SMulCommClass.complexToReal` `smulCommClass_self` `iteratedFDeriv_fourier` `fourier_continuousMultilinearMap_apply` `VectorFourier.integrable_fourierPowSMulRight` `instSecondCountableTopologyReal` `fourier_eq` `mul_assoc` `mul_pow` `Complex.ofReal_pow` `smul_smul` `conj_trivial` `instTrivialStarReal` `instIsTopologicalAddGroupReal` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `VectorFourier.fourierPowSMulRight_apply` `Finset.prod_congr` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `innerSL_apply_apply` `one_mul` `Finset.prod_const` `Fintype.card_fin` `neg_mul`
`iteratedDeriv_fourierIntegral` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Real` `measurableSpace` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `instMonoid` `Module.toDistribMulAction` `semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `normedField` `NormedSpace.complexToReal` `Monoid.toPow` `MeasureTheory.MeasureSpace.volume` `measureSpace` `ENat` `instLEENat` `ENat.instNatCast`	`iteratedDeriv` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `NormedSpace.complexToReal` `NormedAddCommGroup.toSeminormedAddCommGroup` `FourierTransform.fourier` `instFourierTransform` `normedAddCommGroup` `RCLike.toInnerProductSpaceReal` `instRCLike` `measurableSpace` `borelSpace` `FiniteDimensional.rclike_to_real` `Complex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Complex.instNormedField` `Monoid.toPow` `Complex.instMul` `Complex.instNeg` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `pi` `Complex.I`	—	`iteratedDeriv_fourier`
`iteratedFDeriv_fourier` 📖	mathematical	`MeasureTheory.Integrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `instMul` `Monoid.toPow` `instMonoid` `Norm.norm` `NormedAddCommGroup.toNorm` `MeasureTheory.MeasureSpace.volume` `measureSpaceOfInnerProductSpace` `MeasureTheory.AEStronglyMeasurable` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasureTheory.MeasureSpace.toMeasurableSpace` `ENat` `instLEENat` `ENat.instNatCast`	`iteratedFDeriv` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `InnerProductSpace.toNormedSpace` `instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.complexToReal` `FourierTransform.fourier` `instFourierTransform` `ContinuousMultilinearMap` `semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `normedField` `ContinuousMultilinearMap.normedAddCommGroup'` `Fin.fintype` `ContinuousMultilinearMap.normedSpace'` `Complex` `Complex.instNormedField` `SMulCommClass.complexToReal` `NormedAddCommGroup.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `smulCommClass_self` `CommRing.toCommMonoid` `Complex.commRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `VectorFourier.fourierPowSMulRight` `innerSL`	—	`VectorFourier.iteratedFDeriv_fourierIntegral` `secondCountable_of_proper` `FiniteDimensional.proper_real`
`iteratedFDeriv_fourierIntegral` 📖	mathematical	`MeasureTheory.Integrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `instMul` `Monoid.toPow` `instMonoid` `Norm.norm` `NormedAddCommGroup.toNorm` `MeasureTheory.MeasureSpace.volume` `measureSpaceOfInnerProductSpace` `MeasureTheory.AEStronglyMeasurable` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasureTheory.MeasureSpace.toMeasurableSpace` `ENat` `instLEENat` `ENat.instNatCast`	`iteratedFDeriv` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `InnerProductSpace.toNormedSpace` `instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.complexToReal` `FourierTransform.fourier` `instFourierTransform` `ContinuousMultilinearMap` `semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `normedField` `ContinuousMultilinearMap.normedAddCommGroup'` `Fin.fintype` `ContinuousMultilinearMap.normedSpace'` `Complex` `Complex.instNormedField` `SMulCommClass.complexToReal` `NormedAddCommGroup.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `smulCommClass_self` `CommRing.toCommMonoid` `Complex.commRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `VectorFourier.fourierPowSMulRight` `innerSL`	—	`iteratedFDeriv_fourier`
`pow_mul_norm_iteratedFDeriv_fourierIntegral_le` 📖	mathematical	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `InnerProductSpace.toNormedSpace` `instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.complexToReal` `WithTop.some` `ENat` `MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `instMul` `Monoid.toPow` `instMonoid` `Norm.norm` `NormedAddCommGroup.toNorm` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.hasOpNorm'` `Fin.fintype` `iteratedFDeriv` `MeasureTheory.MeasureSpace.volume` `measureSpaceOfInnerProductSpace` `instLEENat` `ENat.instNatCast`	`Real` `instLE` `instMul` `Monoid.toPow` `instMonoid` `Norm.norm` `NormedAddCommGroup.toNorm` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `instRCLike` `NormedSpace.complexToReal` `ContinuousMultilinearMap.hasOpNorm'` `Fin.fintype` `iteratedFDeriv` `FourierTransform.fourier` `instFourierTransform` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `pi` `instAdd` `Finset.sum` `instAddCommMonoid` `SProd.sprod` `Finset` `Finset.instSProd` `Finset.range` `MeasureTheory.integral` `normedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `MeasureTheory.MeasureSpace.volume`	—	`pow_mul_norm_iteratedFDeriv_fourier_le`
`pow_mul_norm_iteratedFDeriv_fourier_le` 📖	mathematical	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `InnerProductSpace.toNormedSpace` `instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.complexToReal` `WithTop.some` `ENat` `MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `normedCommRing` `instMul` `Monoid.toPow` `instMonoid` `Norm.norm` `NormedAddCommGroup.toNorm` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.hasOpNorm'` `Fin.fintype` `iteratedFDeriv` `MeasureTheory.MeasureSpace.volume` `measureSpaceOfInnerProductSpace` `instLEENat` `ENat.instNatCast`	`Real` `instLE` `instMul` `Monoid.toPow` `instMonoid` `Norm.norm` `NormedAddCommGroup.toNorm` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `denselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `instRCLike` `NormedSpace.complexToReal` `ContinuousMultilinearMap.hasOpNorm'` `Fin.fintype` `iteratedFDeriv` `FourierTransform.fourier` `instFourierTransform` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `pi` `instAdd` `Finset.sum` `instAddCommMonoid` `SProd.sprod` `Finset` `Finset.instSProd` `Finset.range` `MeasureTheory.integral` `normedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `MeasureTheory.MeasureSpace.volume`	—	`Nat.instAtLeastTwoHAddOfNat` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `RingHomIsometric.ids` `instIsTopologicalAddGroupReal` `instIsTopologicalRingReal` `VectorFourier.pow_mul_norm_iteratedFDeriv_fourierIntegral_le` `instIsAddHaarMeasureVolume` `mul_assoc` `mul_pow` `pow_two` `innerSL_apply_apply` `real_inner_self_eq_norm_sq` `abs_pow` `instIsOrderedRing` `abs_norm` `eq_or_ne` `pow_zero` `one_mul` `mul_one` `Prod.mk_left_injective` `Finset.sum_congr` `zero_add` `Finset.product_singleton` `Finset.sum_map` `norm_iteratedFDeriv_zero` `LE.le.trans` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `pow_le_pow_left₀` `IsOrderedRing.toPosMulMono` `mul_nonneg` `le_of_lt` `Mathlib.Meta.Positivity.pos_of_isNat` `instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `pi_pos` `norm_nonneg` `RingHomIsometric.starRingEnd` `CStarRing.to_normedStarGroup` `instCStarRingReal` `mul_le_mul_of_nonneg_left` `norm_innerSL_le` `Finset.sum_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `MeasureTheory.integral_nonneg` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `instIsStrictOrderedRing` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `norm_zero` `zero_pow` `MulZeroClass.zero_mul` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `Right.add_pos_of_nonneg_of_pos` `covariant_swap_add_of_covariant_add` `Nat.cast_nonneg'` `instZeroLEOneClass` `mul_le_mul_iff_right₀` `PosMulStrictMono.toPosMulReflectLE`

VectorFourier

Definitions

Name	Category	Theorems
`fourierPowSMulRight` 📖	CompOp	18 math math: `fourierPowSMulRight_eq_comp`, `Real.fourier_iteratedFDeriv`, `fourierIntegral_iteratedFDeriv`, `norm_iteratedFDeriv_fourierPowSMulRight`, `iteratedFDeriv_fourierIntegral`, `MeasureTheory.AEStronglyMeasurable.fourierPowSMulRight`, `hasFTaylorSeriesUpTo_fourierIntegral'`, `ContDiff.fourierPowSMulRight`, `Real.iteratedFDeriv_fourier`, `fourierPowSMulRight_apply`, `hasFTaylorSeriesUpTo_fourierIntegral`, `Real.iteratedFDeriv_fourierIntegral`, `Continuous.fourierPowSMulRight`, `norm_fourierPowSMulRight_le`, `fourierPowSMulRight_iteratedFDeriv_fourierIntegral`, `integrable_fourierPowSMulRight`, `norm_fourierPowSMulRight_iteratedFDeriv_fourierIntegral_le`, `Real.fourierIntegral_iteratedFDeriv`
`fourierSMulRight` 📖	CompOp	14 math math: `Real.fderiv_fourierIntegral`, `Real.fderiv_fourier`, `hasFDerivAt_fourierIntegral`, `Real.hasFDerivAt_fourier`, `Real.fourier_fderiv`, `fderiv_fourierIntegral`, `fourierSMulRight_apply`, `MeasureTheory.AEStronglyMeasurable.fourierSMulRight`, `Real.fourierIntegral_fderiv`, `Real.hasFDerivAt_fourierIntegral`, `norm_fourierSMulRight_le`, `norm_fourierSMulRight`, `hasFDerivAt_fourierChar_smul`, `fourierIntegral_fderiv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contDiff_fourierIntegral` 📖	mathematical	`MeasureTheory.Integrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.instMul` `Monoid.toPow` `Real.instMonoid` `Norm.norm` `NormedAddCommGroup.toNorm`	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedSpace.complexToReal` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithTop.some` `ENat` `fourierIntegral` `Real.commRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `Real.fourierChar` `ContinuousLinearMap.toLinearMap₁₂` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `instIsTopologicalAddGroupReal` `SeparatelyContinuousMul.to_continuousSMul` `Real.instMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `RingHom.id` `Semiring.toNonAssocSemiring`	—	`instIsTopologicalAddGroupReal` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `HasFTaylorSeriesUpTo.contDiff` `SMulCommClass.complexToReal` `smulCommClass_self` `hasFTaylorSeriesUpTo_fourierIntegral'` `IsTopologicalAddGroup.toContinuousAdd` `MeasureTheory.integral_def` `contDiff_const`
`differentiable_fourierIntegral` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Real` `Real.pseudoMetricSpace` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.instMul` `Norm.norm` `NormedAddCommGroup.toNorm`	`Differentiable` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedSpace.complexToReal` `fourierIntegral` `Real.commRing` `Real.fourierChar` `ContinuousLinearMap.toLinearMap₁₂` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `instIsTopologicalAddGroupReal` `SeparatelyContinuousMul.to_continuousSMul` `Real.instMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `RingHom.id` `Semiring.toNonAssocSemiring`	—	`instIsTopologicalAddGroupReal` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `HasFDerivAt.differentiableAt` `RingHomIsometric.ids` `SMulCommClass.complexToReal` `smulCommClass_self` `hasFDerivAt_fourierIntegral`
`fderiv_fourierIntegral` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Real` `Real.pseudoMetricSpace` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.instMul` `Norm.norm` `NormedAddCommGroup.toNorm`	`fderiv` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedSpace.complexToReal` `fourierIntegral` `Real.commRing` `Real.fourierChar` `ContinuousLinearMap.toLinearMap₁₂` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `instIsTopologicalAddGroupReal` `SeparatelyContinuousMul.to_continuousSMul` `Real.instMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousLinearMap` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `ContinuousLinearMap.toNormedSpace` `Complex` `Complex.instNormedField` `SMulCommClass.complexToReal` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `smulCommClass_self` `CommRing.toCommMonoid` `Complex.commRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `fourierSMulRight`	—	`instIsTopologicalAddGroupReal` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `RingHomIsometric.ids` `SMulCommClass.complexToReal` `smulCommClass_self` `HasFDerivAt.fderiv` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `hasFDerivAt_fourierIntegral`
`fourierIntegral_fderiv` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Differentiable` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedSpace.complexToReal` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `fderiv`	`fourierIntegral` `Real` `Real.commRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `NormedSpace.complexToReal` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `ContinuousLinearMap.toNormedSpace` `Complex` `Complex.instNormedField` `SMulCommClass.complexToReal` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `SeminormedAddCommGroup.toAddCommGroup` `smulCommClass_self` `CommRing.toCommMonoid` `Complex.commRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Ring.toSemiring` `CommRing.toRing` `Real.fourierChar` `ContinuousLinearMap.toLinearMap₁₂` `Real.semiring` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `instIsTopologicalAddGroupReal` `SeparatelyContinuousMul.to_continuousSMul` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `fderiv` `fourierSMulRight` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `ContinuousLinearMap.module` `Field.toCommRing` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.neg` `Real.instRing` `ContinuousLinearMap.addCommGroup` `ContinuousLinearMap.topologicalAddGroup` `ContinuousLinearMap.flip`	—	`instIsTopologicalAddGroupReal` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `RingHomIsometric.ids` `SMulCommClass.complexToReal` `smulCommClass_self` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.topologicalAddGroup` `ContinuousLinearMap.ext` `Nat.instAtLeastTwoHAddOfNat` `Real.fderiv_fourierChar_neg_bilinear_left_apply` `integral_smul_fderiv_eq_neg_fderiv_smul_of_integrable` `IsScalarTower.complexToReal` `IsScalarTower.left` `MeasureTheory.Integrable.smul` `Real.fourierIntegral_convergent_iff'` `neg_mul` `neg_smul` `smul_smul` `MeasureTheory.Integrable.apply_continuousLinearMap` `Differentiable.differentiableAt` `Real.differentiable_fourierChar_neg_bilinear_left` `MeasureTheory.integral_neg` `neg_neg` `Real.fourierIntegral_continuousLinearMap_apply'` `NormedSpace.toNormSMulClass` `smul_neg`
`fourierIntegral_iteratedFDeriv` 📖	mathematical	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedSpace.complexToReal` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithTop.some` `ENat` `MeasureTheory.Integrable` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.instTopologicalSpace` `Real.normedField` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `ContinuousMultilinearMap.seminormedAddCommGroup'` `Fin.fintype` `iteratedFDeriv` `instLEENat` `ENat.instNatCast`	`fourierIntegral` `Real` `Real.commRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.complexToReal` `ContinuousMultilinearMap.normedAddCommGroup'` `Fin.fintype` `ContinuousMultilinearMap.normedSpace'` `Complex` `Complex.instNormedField` `SMulCommClass.complexToReal` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `smulCommClass_self` `CommRing.toCommMonoid` `Complex.commRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `Real.fourierChar` `ContinuousLinearMap.toLinearMap₁₂` `Real.semiring` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `instIsTopologicalAddGroupReal` `SeparatelyContinuousMul.to_continuousSMul` `Real.instMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `RingHom.id` `Semiring.toNonAssocSemiring` `iteratedFDeriv` `fourierPowSMulRight` `ContinuousLinearMap` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `ContinuousLinearMap.module` `Field.toCommRing` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.neg` `Real.instRing` `ContinuousLinearMap.addCommGroup` `ContinuousLinearMap.topologicalAddGroup` `ContinuousLinearMap.flip` `RingHomIsometric.ids`	—	`instIsTopologicalAddGroupReal` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SMulCommClass.complexToReal` `smulCommClass_self` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.topologicalAddGroup` `RingHomIsometric.ids` `ContinuousMultilinearMap.ext` `Real.fourierIntegral_continuousMultilinearMap_apply'` `bot_le` `Nat.instAtLeastTwoHAddOfNat` `fourierPowSMulRight_apply` `pow_zero` `Finset.prod_congr` `Finset.univ_eq_empty` `Fin.isEmpty'` `one_smul` `ContinuousMultilinearMap.instIsTopologicalAddGroup` `RingHomInvPair.ids` `ContinuousMultilinearMap.instSMulCommClass` `ContinuousMultilinearMap.instContinuousConstSMul` `LinearIsometryEquiv.integrable_comp_iff` `iteratedFDeriv_succ_eq_comp_left` `LT.lt.trans_le` `Nat.cast_lt` `IsOrderedAddMonoid.toAddLeftMono` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid` `fourierIntegral_fderiv` `LT.lt.le` `ContDiff.differentiable_iteratedFDeriv` `neg_smul` `smul_neg` `neg_neg` `smul_smul` `Complex.ofReal_prod` `Complex.ofReal_neg` `pow_succ` `mul_neg` `Fin.prod_univ_succ` `neg_mul` `Complex.ofReal_mul` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.neg_congr` `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.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.pow_prod_atom` `Mathlib.Tactic.Ring.pow_zero` `MeasureTheory.Integrable.apply_continuousLinearMap` `Real.fourierIntegral_continuousLinearMap_apply'`
`fourierPowSMulRight_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMultilinearMap` `Real` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `NormedSpace.complexToReal` `ContinuousMultilinearMap.funLike` `fourierPowSMulRight` `Complex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Module.toDistribMulAction` `Complex.instNormedField` `Monoid.toPow` `Complex.instNeg` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `Real.pi` `Complex.I` `Real.instMonoid` `Finset.prod` `Real.instCommMonoid` `Finset.univ` `Fin.fintype` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Real.pseudoMetricSpace` `Real.instAddCommMonoid` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `ContinuousLinearMap.funLike` `ContinuousLinearMap.topologicalSpace` `NormedAddCommGroup.toAddCommGroup` `Real.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousLinearMap.addCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `ContinuousLinearMap.module` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `SeparatelyContinuousMul.to_continuousSMul` `Real.instMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul`	—	`instIsTopologicalAddGroupReal` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul`
`fourierPowSMulRight_eq_comp` 📖	mathematical	—	`fourierPowSMulRight` `Complex` `ContinuousMultilinearMap` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NormedSpace.complexToReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ContinuousMultilinearMap.instSMul` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `Complex.instNormedField` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `SMulCommClass.complexToReal` `smulCommClass_self` `CommRing.toCommMonoid` `Complex.commRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `Monoid.toPow` `Complex.instNeg` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `Real.pi` `Complex.I` `DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousMultilinearMap.instTopologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousMultilinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `ContinuousMultilinearMap.instModule` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Field.toCommRing` `ContinuousLinearMap.funLike` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousLinearMap.topologicalSpace` `ContinuousMultilinearMap.instAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `ContinuousMultilinearMap.instIsTopologicalAddGroup` `ContinuousLinearMap.addCommMonoid` `ContinuousMultilinearMap.seminormedAddCommGroup` `Fin.fintype` `SeparatelyContinuousMul.to_continuousSMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `ContinuousLinearMap.module` `ContinuousMultilinearMap.instSMulCommClass` `ContinuousMultilinearMap.instContinuousConstSMul` `ContinuousMultilinearMap.smulRightL` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `ContinuousMultilinearMap.funLike` `ContinuousMultilinearMap.compContinuousLinearMapLRight` `ContinuousMultilinearMap.mkPiAlgebra` `Real.instCommSemiring` `Real.pseudoMetricSpace` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Real.semiring` `Real.instAddCommMonoid` `Real.normedField` `Real.instAddCommGroup` `instIsTopologicalAddGroupReal` `Real.instMul`	—	`instIsTopologicalAddGroupReal` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul`
`fourierPowSMulRight_iteratedFDeriv_fourierIntegral` 📖	mathematical	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedSpace.complexToReal` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithTop.some` `ENat` `MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.instMul` `Monoid.toPow` `Real.instMonoid` `Norm.norm` `NormedAddCommGroup.toNorm` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.hasOpNorm'` `Fin.fintype` `iteratedFDeriv` `instLEENat` `ENat.instNatCast`	`fourierPowSMulRight` `ContinuousMultilinearMap` `Real` `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` `NormedSpace.toModule` `NormedSpace.complexToReal` `ContinuousMultilinearMap.normedAddCommGroup'` `Fin.fintype` `ContinuousMultilinearMap.normedSpace'` `Complex` `Complex.instNormedField` `SMulCommClass.complexToReal` `NormedAddCommGroup.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `smulCommClass_self` `CommRing.toCommMonoid` `Complex.commRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Real.semiring` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `ContinuousLinearMap.module` `Field.toCommRing` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.neg` `Real.instRing` `ContinuousLinearMap.addCommGroup` `Real.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousLinearMap.topologicalAddGroup` `Real.normedField` `ContinuousLinearMap.flip` `RingHomIsometric.ids` `iteratedFDeriv` `fourierIntegral` `Real.commRing` `Real.fourierChar` `ContinuousLinearMap.toLinearMap₁₂` `Real.pseudoMetricSpace` `SeparatelyContinuousMul.to_continuousSMul` `Real.instMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Real.instCommMonoid` `ContinuousMultilinearMap.seminormedAddCommGroup'` `ContinuousMultilinearMap.instSMulCommClass`	—	`instIsTopologicalAddGroupReal` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `SMulCommClass.complexToReal` `smulCommClass_self` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.topologicalAddGroup` `RingHomIsometric.ids` `ContinuousMultilinearMap.instSMulCommClass` `fourierIntegral_iteratedFDeriv` `ContDiff.fourierPowSMulRight` `MeasureTheory.integrable_finset_sum` `LE.le.trans` `Nat.cast_le` `IsOrderedAddMonoid.toAddLeftMono` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid` `MeasureTheory.Integrable.mono'` `Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.Integrable.const_mul` `Continuous.aestronglyMeasurable` `BorelSpace.opensMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `secondCountableTopologyEither_of_left` `secondCountable_of_proper` `FiniteDimensional.proper_real` `ContDiff.continuous_iteratedFDeriv` `Filter.univ_mem'` `MeasureTheory.Measure.instOuterMeasureClass` `norm_iteratedFDeriv_fourierPowSMulRight` `Finset.single_le_sum` `Real.instIsOrderedAddMonoid` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `norm_nonneg` `iteratedFDeriv_fourierIntegral` `norm_iteratedFDeriv_zero` `bot_le` `ContDiff.continuous`
`fourierSMulRight_apply` 📖	mathematical	—	`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` `NormedSpace.complexToReal` `ContinuousLinearMap.funLike` `fourierSMulRight` `Complex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Module.toDistribMulAction` `Complex.instNormedField` `Complex.instNeg` `Complex.instMul` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Complex.ofReal` `Real.pi` `Complex.I` `Real.instMonoid` `Real.pseudoMetricSpace` `Real.instAddCommMonoid` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `ContinuousLinearMap.topologicalSpace` `NormedAddCommGroup.toAddCommGroup` `Real.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousLinearMap.addCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `ContinuousLinearMap.module` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `SeparatelyContinuousMul.to_continuousSMul` `Real.instMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul`	—	`instIsTopologicalAddGroupReal` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul`
`hasFDerivAt_fourierChar_smul` 📖	mathematical	—	`HasFDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedSpace.complexToReal` `Circle` `Circle.instSMul` `SMulZeroClass.toSMul` `Complex` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `Complex.instNormedField` `DFunLike.coe` `AddChar` `Real.instAddMonoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Circle.instCommGroup` `AddChar.instFunLike` `Real.fourierChar` `Real.instNeg` `ContinuousLinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Real.pseudoMetricSpace` `Real.instAddCommMonoid` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `ContinuousLinearMap.funLike` `ContinuousLinearMap.topologicalSpace` `Real.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousLinearMap.addCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `ContinuousLinearMap.module` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `SeparatelyContinuousMul.to_continuousSMul` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `ContinuousLinearMap.instSMul` `SMulCommClass.complexToReal` `AddCommMonoid.toAddMonoid` `smulCommClass_self` `CommRing.toCommMonoid` `Complex.commRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `Complex.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `fourierSMulRight`	—	`instIsTopologicalAddGroupReal` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `ContinuousLinearMap.hasFDerivAt` `SMulCommClass.complexToReal` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `IsScalarTower.complexToReal` `IsScalarTower.left` `IsBoundedSMul.continuousSMul` `RingHomCompTriple.ids` `Nat.instAtLeastTwoHAddOfNat` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.ext` `ContinuousLinearMap.comp_apply` `ContinuousLinearMap.neg_apply` `ContinuousLinearMap.toSpanSingleton_apply` `smul_assoc` `Circle.instIsScalarTower` `SMulCommClass.smul_comm` `IsScalarTower.to_smulCommClass'` `Complex.real_smul` `Submonoid.smul_def` `smul_eq_mul` `Complex.ofReal_neg` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_left` `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.one_mul` `Mathlib.Tactic.RingNF.mul_assoc_rev` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `Mathlib.Tactic.RingNF.int_rawCast_neg` `Mathlib.Tactic.RingNF.mul_neg` `add_zero` `HasFDerivAt.smul_const` `HasFDerivAt.comp` `HasDerivAt.hasFDerivAt` `Real.hasDerivAt_fourierChar` `HasFDerivAt.neg`
`hasFDerivAt_fourierIntegral` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Real` `Real.pseudoMetricSpace` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.instMul` `Norm.norm` `NormedAddCommGroup.toNorm`	`HasFDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedSpace.complexToReal` `fourierIntegral` `Real.commRing` `Real.fourierChar` `ContinuousLinearMap.toLinearMap₁₂` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `instIsTopologicalAddGroupReal` `SeparatelyContinuousMul.to_continuousSMul` `Real.instMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `ContinuousLinearMap.toNormedSpace` `Complex` `Complex.instNormedField` `SMulCommClass.complexToReal` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `SeminormedAddCommGroup.toAddCommGroup` `smulCommClass_self` `CommRing.toCommMonoid` `Complex.commRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `fourierSMulRight`	—	`instIsTopologicalAddGroupReal` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `SMulCommClass.complexToReal` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Nat.instAtLeastTwoHAddOfNat` `RingHomIsometric.ids` `fourierIntegral_convergent_iff` `Real.continuous_fourierChar` `ContinuousLinearMap.continuous₂` `Filter.Eventually.of_forall` `MeasureTheory.Integrable.aestronglyMeasurable` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.AEStronglyMeasurable.smul` `Circle.instContinuousSMul` `IsBoundedSMul.continuousSMul` `Continuous.aestronglyMeasurable` `BorelSpace.opensMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `secondCountableTopologyEither_of_left` `Continuous.comp` `Continuous.neg` `IsSemitopologicalRing.toContinuousNeg` `Continuous.clm_apply` `continuous_const` `continuous_id'` `MeasureTheory.AEStronglyMeasurable.fourierSMulRight` `MeasureTheory.Measure.instOuterMeasureClass` `Filter.univ_mem'` `Circle.norm_smul` `norm_fourierSMulRight_le` `MeasureTheory.Integrable.const_mul` `MeasureTheory.ae_of_all` `hasFDerivAt_fourierChar_smul` `hasFDerivAt_integral_of_dominated_of_fderiv_le` `Metric.ball_mem_nhds` `one_pos` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike`
`hasFTaylorSeriesUpTo_fourierIntegral` 📖	mathematical	`MeasureTheory.Integrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.instMul` `Monoid.toPow` `Real.instMonoid` `Norm.norm` `NormedAddCommGroup.toNorm` `MeasureTheory.AEStronglyMeasurable` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`HasFTaylorSeriesUpTo` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedSpace.complexToReal` `NormedAddCommGroup.toSeminormedAddCommGroup` `fourierIntegral` `Real.commRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `Real.fourierChar` `ContinuousLinearMap.toLinearMap₁₂` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `instIsTopologicalAddGroupReal` `SeparatelyContinuousMul.to_continuousSMul` `Real.instMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ContinuousMultilinearMap.normedAddCommGroup'` `Fin.fintype` `ContinuousMultilinearMap.normedSpace'` `Complex` `Complex.instNormedField` `SMulCommClass.complexToReal` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `smulCommClass_self` `CommRing.toCommMonoid` `Complex.commRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `fourierPowSMulRight`	—	`instIsTopologicalAddGroupReal` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `SMulCommClass.complexToReal` `smulCommClass_self` `ContinuousMultilinearMap.curry0_apply` `Matrix.zero_empty` `Real.fourierIntegral_continuousMultilinearMap_apply'` `integrable_fourierPowSMulRight` `bot_le` `Nat.instAtLeastTwoHAddOfNat` `fourierPowSMulRight_apply` `pow_zero` `Finset.prod_congr` `Finset.univ_eq_empty` `Fin.isEmpty'` `one_smul` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `LT.lt.le` `MeasureTheory.Integrable.mono'` `RingHomIsometric.ids` `MeasureTheory.Integrable.const_mul` `ENat.add_one_natCast_le_withTop_of_lt` `MeasureTheory.AEStronglyMeasurable.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `Continuous.aestronglyMeasurable` `BorelSpace.opensMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `secondCountableTopologyEither_of_left` `continuous_norm` `MeasureTheory.AEStronglyMeasurable.norm` `MeasureTheory.AEStronglyMeasurable.fourierPowSMulRight` `Filter.univ_mem'` `MeasureTheory.Measure.instOuterMeasureClass` `norm_mul` `NormedDivisionRing.toNormMulClass` `norm_norm` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `norm_fourierPowSMulRight_le` `norm_nonneg` `pow_succ` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.pow_prod_atom` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.one_pow` `ContinuousMultilinearMap.instIsTopologicalAddGroup` `SeminormedAddCommGroup.to_isUniformAddGroup` `MeasureTheory.AEStronglyMeasurable.fourierSMulRight` `LE.le.trans` `norm_fourierSMulRight_le` `le_of_eq` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousMultilinearMap.instSMulCommClass` `ContinuousLinearMap.ext` `ContinuousMultilinearMap.ext` `ContinuousMultilinearMap.curryLeft_apply` `Real.fourierIntegral_continuousLinearMap_apply'` `MeasureTheory.Integrable.apply_continuousLinearMap` `mul_comm` `neg_mul` `Fin.prod_univ_succ` `Fin.cons_zero` `Fin.cons_succ` `neg_smul` `SMulCommClass.smul_comm` `smul_smul` `hasFDerivAt_fourierIntegral` `fourierIntegral_continuous` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `Real.continuous_fourierChar` `ContinuousLinearMap.continuous₂`
`hasFTaylorSeriesUpTo_fourierIntegral'` 📖	mathematical	`MeasureTheory.Integrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.instMul` `Monoid.toPow` `Real.instMonoid` `Norm.norm` `NormedAddCommGroup.toNorm` `MeasureTheory.AEStronglyMeasurable` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`HasFTaylorSeriesUpTo` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedSpace.complexToReal` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithTop.some` `ENat` `fourierIntegral` `Real.commRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `Real.fourierChar` `ContinuousLinearMap.toLinearMap₁₂` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `instIsTopologicalAddGroupReal` `SeparatelyContinuousMul.to_continuousSMul` `Real.instMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ContinuousMultilinearMap.normedAddCommGroup'` `Fin.fintype` `ContinuousMultilinearMap.normedSpace'` `Complex` `Complex.instNormedField` `SMulCommClass.complexToReal` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `smulCommClass_self` `CommRing.toCommMonoid` `Complex.commRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `fourierPowSMulRight`	—	`instIsTopologicalAddGroupReal` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `hasFTaylorSeriesUpTo_fourierIntegral`
`integrable_fourierPowSMulRight` 📖	mathematical	`MeasureTheory.Integrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.instMul` `Monoid.toPow` `Real.instMonoid` `Norm.norm` `NormedAddCommGroup.toNorm` `MeasureTheory.AEStronglyMeasurable` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`MeasureTheory.Integrable` `ContinuousMultilinearMap` `Real` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `NormedSpace.complexToReal` `ContinuousMultilinearMap.instTopologicalSpace` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `ContinuousMultilinearMap.seminormedAddCommGroup'` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Fin.fintype` `fourierPowSMulRight`	—	`instIsTopologicalAddGroupReal` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `MeasureTheory.Integrable.mono'` `Nat.instAtLeastTwoHAddOfNat` `RingHomIsometric.ids` `MeasureTheory.Integrable.const_mul` `MeasureTheory.AEStronglyMeasurable.fourierPowSMulRight` `Filter.univ_mem'` `MeasureTheory.Measure.instOuterMeasureClass` `LE.le.trans` `norm_fourierPowSMulRight_le` `le_of_eq` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.pow_prod_atom` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.one_pow`
`iteratedFDeriv_fourierIntegral` 📖	mathematical	`MeasureTheory.Integrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.instMul` `Monoid.toPow` `Real.instMonoid` `Norm.norm` `NormedAddCommGroup.toNorm` `MeasureTheory.AEStronglyMeasurable` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENat` `instLEENat` `ENat.instNatCast`	`iteratedFDeriv` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedSpace.complexToReal` `NormedAddCommGroup.toSeminormedAddCommGroup` `fourierIntegral` `Real.commRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `Real.fourierChar` `ContinuousLinearMap.toLinearMap₁₂` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Real.pseudoMetricSpace` `instIsTopologicalAddGroupReal` `SeparatelyContinuousMul.to_continuousSMul` `Real.instMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousMultilinearMap` `ContinuousMultilinearMap.normedAddCommGroup'` `Fin.fintype` `ContinuousMultilinearMap.normedSpace'` `Complex` `Complex.instNormedField` `SMulCommClass.complexToReal` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `smulCommClass_self` `CommRing.toCommMonoid` `Complex.commRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `fourierPowSMulRight`	—	`instIsTopologicalAddGroupReal` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `SMulCommClass.complexToReal` `smulCommClass_self` `HasFTaylorSeriesUpTo.eq_iteratedFDeriv` `hasFTaylorSeriesUpTo_fourierIntegral'`
`norm_fourierPowSMulRight_iteratedFDeriv_fourierIntegral_le` 📖	mathematical	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedSpace.complexToReal` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithTop.some` `ENat` `MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.instMul` `Monoid.toPow` `Real.instMonoid` `Norm.norm` `NormedAddCommGroup.toNorm` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.hasOpNorm'` `Fin.fintype` `iteratedFDeriv` `instLEENat` `ENat.instNatCast`	`Real` `Real.instLE` `Norm.norm` `ContinuousMultilinearMap` `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` `NormedSpace.toModule` `NormedSpace.complexToReal` `Real.semiring` `ContinuousMultilinearMap.normedAddCommGroup'` `Fin.fintype` `Real.normedField` `ContinuousMultilinearMap.normedSpace'` `Complex` `Complex.instNormedField` `SMulCommClass.complexToReal` `NormedAddCommGroup.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `smulCommClass_self` `CommRing.toCommMonoid` `Complex.commRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `ContinuousMultilinearMap.hasOpNorm'` `ContinuousMultilinearMap.seminormedAddCommGroup'` `Real.instCommMonoid` `Real.commRing` `fourierPowSMulRight` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `ContinuousLinearMap.module` `Field.toCommRing` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.neg` `Real.instRing` `ContinuousLinearMap.addCommGroup` `Real.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousLinearMap.topologicalAddGroup` `ContinuousLinearMap.flip` `RingHomIsometric.ids` `iteratedFDeriv` `fourierIntegral` `Real.fourierChar` `ContinuousLinearMap.toLinearMap₁₂` `Real.pseudoMetricSpace` `SeparatelyContinuousMul.to_continuousSMul` `Real.instMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Monoid.toPow` `Real.instMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `Real.instAdd` `Real.instAddCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `ContinuousLinearMap.hasOpNorm` `ContinuousLinearMap.toSeminormedAddCommGroup` `ContinuousLinearMap.toNormedSpace` `Finset.sum` `SProd.sprod` `Finset` `Finset.instSProd` `Finset.range` `MeasureTheory.integral` `Real.normedAddCommGroup` `NormedAddCommGroup.toNorm`	—	`instIsTopologicalAddGroupReal` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `SMulCommClass.complexToReal` `smulCommClass_self` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.topologicalAddGroup` `RingHomIsometric.ids` `Nat.instAtLeastTwoHAddOfNat` `ContinuousMultilinearMap.instSMulCommClass` `fourierPowSMulRight_iteratedFDeriv_fourierIntegral` `LE.le.trans` `norm_fourierIntegral_le_integral_norm` `le_trans` `IsOrderedAddMonoid.toAddLeftMono` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid` `MeasureTheory.integral_finset_sum` `MeasureTheory.integral_const_mul` `MeasureTheory.integral_mono_of_nonneg` `Real.instIsOrderedAddMonoid` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Filter.univ_mem'` `MeasureTheory.Measure.instOuterMeasureClass` `norm_nonneg` `MeasureTheory.Integrable.const_mul` `MeasureTheory.integrable_finset_sum` `norm_iteratedFDeriv_fourierPowSMulRight` `Finset.single_le_sum` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass`
`norm_fourierPowSMulRight_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `ContinuousMultilinearMap` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `NormedSpace.complexToReal` `ContinuousMultilinearMap.hasOpNorm'` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Fin.fintype` `fourierPowSMulRight` `Real.instMul` `Monoid.toPow` `Real.instMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Real.pseudoMetricSpace` `Real.instAddCommMonoid` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `ContinuousLinearMap.topologicalSpace` `NormedAddCommGroup.toAddCommGroup` `Real.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousLinearMap.addCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `ContinuousLinearMap.module` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `ContinuousLinearMap.hasOpNorm` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `ContinuousLinearMap.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toNorm`	—	`instIsTopologicalAddGroupReal` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `ContinuousMultilinearMap.opNorm_le_bound` `Nat.instAtLeastTwoHAddOfNat` `RingHomIsometric.ids` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `le_of_lt` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Real.pi_pos` `norm_nonneg` `fourierPowSMulRight_apply` `norm_smul` `NormedSpace.toNormSMulClass` `norm_pow` `NormedDivisionRing.to_normOneClass` `NormedDivisionRing.toNormMulClass` `norm_neg` `Complex.norm_mul` `Complex.norm_ofNat` `Complex.norm_real` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.pi_nonneg` `Complex.norm_I` `mul_one` `norm_prod` `Finset.prod_congr` `mul_le_mul_of_nonneg_left` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Finset.prod_le_prod` `Real.instZeroLEOneClass` `abs_nonneg` `covariant_swap_add_of_covariant_add` `ContinuousLinearMap.le_opNorm₂` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `mul_pow` `Finset.prod_mul_distrib` `Finset.prod_const` `Fintype.card_fin` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.pow_prod_atom` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `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.mul_pow` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_pow`
`norm_fourierSMulRight` 📖	mathematical	—	`Norm.norm` `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` `NormedSpace.complexToReal` `ContinuousLinearMap.hasOpNorm` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `fourierSMulRight` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `Real.pseudoMetricSpace` `Real.instAddCommMonoid` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `DFunLike.coe` `ContinuousLinearMap.topologicalSpace` `NormedAddCommGroup.toAddCommGroup` `Real.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousLinearMap.addCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `ContinuousLinearMap.module` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `ContinuousLinearMap.funLike` `NormedAddCommGroup.toNorm`	—	`instIsTopologicalAddGroupReal` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `Nat.instAtLeastTwoHAddOfNat` `fourierSMulRight.eq_1` `IsScalarTower.left` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `norm_smul` `NormedSpace.toNormSMulClass` `RingHomIsometric.ids` `SMulCommClass.complexToReal` `smulCommClass_self` `norm_neg` `norm_mul` `NormedDivisionRing.toNormMulClass` `Complex.norm_I` `mul_one` `Complex.norm_of_nonneg` `LT.lt.le` `Real.pi_pos` `Complex.norm_two` `ContinuousLinearMap.norm_smulRight_apply` `mul_assoc`
`norm_fourierSMulRight_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `ContinuousLinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `NormedSpace.complexToReal` `ContinuousLinearMap.hasOpNorm` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `fourierSMulRight` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `Real.pseudoMetricSpace` `Real.instAddCommMonoid` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `ContinuousLinearMap.topologicalSpace` `NormedAddCommGroup.toAddCommGroup` `Real.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousLinearMap.addCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `ContinuousLinearMap.module` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `ContinuousLinearMap.toNormedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toNorm`	—	`instIsTopologicalAddGroupReal` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `Nat.instAtLeastTwoHAddOfNat` `RingHomIsometric.ids` `norm_fourierSMulRight` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `ContinuousLinearMap.le_opNorm` `le_of_lt` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Real.pi_pos` `norm_nonneg` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_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_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul`
`norm_iteratedFDeriv_fourierPowSMulRight` 📖	mathematical	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedSpace.complexToReal` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `instPreorderENat` `WithTop.natCast` `ENat.instNatCast` `Real.instLE` `Real.instMul` `Monoid.toPow` `Real.instMonoid` `Norm.norm` `NormedAddCommGroup.toNorm` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.hasOpNorm'` `Fin.fintype` `iteratedFDeriv`	`Real` `Real.instLE` `Norm.norm` `ContinuousMultilinearMap` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `NormedSpace.complexToReal` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `ContinuousMultilinearMap.normedAddCommGroup'` `Fin.fintype` `ContinuousMultilinearMap.normedSpace'` `smulCommClass_self` `Real.instCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Real.commRing` `ContinuousMultilinearMap.hasOpNorm'` `ContinuousMultilinearMap.seminormedAddCommGroup'` `iteratedFDeriv` `fourierPowSMulRight` `Real.instMul` `Monoid.toPow` `Real.instMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `Real.instAdd` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Real.pseudoMetricSpace` `Real.instAddCommMonoid` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `ContinuousLinearMap.topologicalSpace` `NormedAddCommGroup.toAddCommGroup` `Real.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousLinearMap.addCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `ContinuousLinearMap.module` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `ContinuousLinearMap.hasOpNorm` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `ContinuousLinearMap.toNormedSpace`	—	`instIsTopologicalAddGroupReal` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `smulCommClass_self` `Nat.instAtLeastTwoHAddOfNat` `RingHomIsometric.ids` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `LE.le.trans` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousMultilinearMap.norm_compContinuousLinearMapLRight_le` `ContinuousMultilinearMap.norm_mkPiAlgebra` `NormedDivisionRing.to_normOneClass` `ContinuousMultilinearMap.norm_iteratedFDeriv_le` `Fintype.card_fin` `mul_le_mul` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedRing.toMulPosMono` `mul_le_mul_of_nonneg_left` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `pow_le_pow_left₀` `norm_nonneg` `pi_norm_le_iff_of_nonneg` `mul_nonneg` `ContinuousLinearMap.le_opNorm` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `le_of_lt` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `ContinuousLinearMap.iteratedFDeriv_comp_right` `ContinuousMultilinearMap.contDiff` `le_top` `ContinuousMultilinearMap.norm_compContinuousLinearMap_le` `Finset.prod_const` `Finset.card_fin` `ContinuousLinearMap.norm_pi_le_of_le` `le_rfl` `le_of_eq` `le_or_gt` `pow_add` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `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.pow_congr` `Mathlib.Tactic.Ring.mul_pf_right` `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` `Nat.descFactorial_eq_zero_iff_lt` `CharP.cast_eq_zero` `CharP.ofCharZero` `RCLike.charZero_rclike` `mul_one` `MulZeroClass.zero_mul` `ContDiff.comp` `contDiff_pi` `ContinuousLinearMap.contDiff` `SMulCommClass.complexToReal` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousMultilinearMap.instIsTopologicalAddGroup` `ContinuousMultilinearMap.instSMulCommClass` `ContinuousMultilinearMap.instContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `iteratedFDeriv_const_smul_apply'` `ContDiff.contDiffAt` `ContDiff.comp₂` `IsBoundedBilinearMap.contDiff` `ContinuousLinearMap.isBoundedBilinearMap` `ContDiff.of_le` `norm_smul` `NormedSpace.toNormSMulClass` `IsBoundedSMul.continuousSMul` `mul_assoc` `norm_pow` `NormedDivisionRing.toNormMulClass` `norm_neg` `Complex.norm_mul` `Complex.norm_ofNat` `Complex.norm_real` `abs_of_nonneg` `Real.pi_nonneg` `Complex.norm_I` `ContinuousLinearMap.norm_iteratedFDeriv_le_of_bilinear_of_le_one` `ContinuousMultilinearMap.norm_smulRightL_le` `Finset.sum_le_sum` `mul_le_mul_of_nonneg_right` `Nat.cast_pow` `Nat.cast_le` `Nat.descFactorial_le_pow` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `zero_le` `Nat.instCanonicallyOrderedAdd` `pow_le_pow_right₀` `Nat.instZeroLEOneClass` `le_add_self` `Finset.mem_range_succ_iff` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `Nat.cast_pos'` `NeZero.charZero_one` `Right.add_pos_of_nonneg_of_pos` `covariant_swap_add_of_covariant_add` `Nat.instIsOrderedAddMonoid` `Nat.instNontrivial` `Finset.sum_congr` `Nat.cast_add` `Nat.sum_range_choose` `mul_add` `Distrib.leftDistribClass` `mul_pos` `Mathlib.Meta.NormNum.instAtLeastTwo` `Real.pi_pos`
`pow_mul_norm_iteratedFDeriv_fourierIntegral_le` 📖	mathematical	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedSpace.complexToReal` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithTop.some` `ENat` `MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.instMul` `Monoid.toPow` `Real.instMonoid` `Norm.norm` `NormedAddCommGroup.toNorm` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousMultilinearMap.hasOpNorm'` `Fin.fintype` `iteratedFDeriv` `instLEENat` `ENat.instNatCast`	`Real` `Real.instLE` `Real.instMul` `Monoid.toPow` `Real.instMonoid` `abs` `Real.lattice` `Real.instAddGroup` `DFunLike.coe` `ContinuousLinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.pseudoMetricSpace` `Real.instAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `ContinuousLinearMap.funLike` `ContinuousLinearMap.topologicalSpace` `NormedAddCommGroup.toAddCommGroup` `Real.instAddCommGroup` `instIsTopologicalAddGroupReal` `ContinuousLinearMap.addCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `ContinuousLinearMap.module` `Algebra.to_smulCommClass` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `Norm.norm` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedSpace.complexToReal` `ContinuousMultilinearMap.hasOpNorm'` `Fin.fintype` `iteratedFDeriv` `fourierIntegral` `Real.commRing` `Real.fourierChar` `ContinuousLinearMap.toLinearMap₁₂` `NormedAddCommGroup.toNorm` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `ContinuousLinearMap.hasOpNorm` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `ContinuousLinearMap.toNormedSpace` `Real.instAdd` `Finset.sum` `SProd.sprod` `Finset` `Finset.instSProd` `Finset.range` `MeasureTheory.integral` `Real.normedAddCommGroup`	—	`instIsTopologicalAddGroupReal` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `Nat.instAtLeastTwoHAddOfNat` `RingHomIsometric.ids` `SMulCommClass.complexToReal` `smulCommClass_self` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.topologicalAddGroup` `le_mul_of_one_le_left` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `mul_nonneg` `IsOrderedRing.toPosMulMono` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `norm_nonneg` `one_le_pow₀` `Real.instZeroLEOneClass` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.neg_congr` `Nat.cast_one` `Mathlib.Tactic.Ring.neg_add` `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.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.add_neg` `Mathlib.Tactic.Linarith.mul_neg` `neg_neg_of_pos` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Meta.NormNum.isNat_lt_true` `RCLike.charZero_rclike` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Mathlib.Tactic.Linarith.mul_nonpos` `Mathlib.Tactic.CancelDenoms.sub_subst` `Mathlib.Tactic.CancelDenoms.div_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.one_le_pi_div_two` `fourierPowSMulRight_apply` `Finset.prod_congr` `Finset.prod_const` `Fintype.card_fin` `norm_smul` `NormedSpace.toNormSMulClass` `norm_pow` `NormedDivisionRing.to_normOneClass` `NormedDivisionRing.toNormMulClass` `norm_neg` `Complex.norm_mul` `Complex.norm_ofNat` `Complex.norm_real` `abs_of_nonneg` `Real.pi_nonneg` `Complex.norm_I` `mul_one` `ContinuousMultilinearMap.le_opNorm` `mul_le_mul` `norm_fourierPowSMulRight_iteratedFDeriv_fourierIntegral_le` `instReflLe` `Finset.prod_nonneg` `le_of_lt` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Real.pi_pos` `Right.add_pos_of_nonneg_of_pos` `Nat.cast_nonneg'` `Finset.sum_nonneg` `MeasureTheory.integral_nonneg` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `mul_pow` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.pow_prod_atom` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_atom`

---

← Back to Index