FourierTransform

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

Statistics

Metric	Count
Definitions fourierIntegral, fourierIntegral, fourierIntegralInv, instFourierTransform, instFourierTransformInv, fourierIntegral	6
Theorems fourierIntegral_comp_add_right, fourierIntegral_const_smul, fourierIntegral_def, norm_fourierIntegral_le_integral_norm, fourierIntegralInv_comm, fourierIntegralInv_comp_linearIsometry, fourierIntegralInv_eq, fourierIntegralInv_eq', fourierIntegralInv_eq_fourierIntegral_comp_neg, fourierIntegralInv_eq_fourierIntegral_neg, fourierIntegral_comp_linearIsometry, fourierIntegral_continuousLinearMap_apply, fourierIntegral_continuousLinearMap_apply', fourierIntegral_continuousMultilinearMap_apply, fourierIntegral_continuousMultilinearMap_apply', fourierIntegral_convergent_iff, fourierIntegral_convergent_iff', fourierIntegral_eq, fourierIntegral_eq', fourierIntegral_real_eq, fourierIntegral_real_eq_integral_exp_smul, fourierInv_comm, fourierInv_comp_linearIsometry, fourierInv_eq, fourierInv_eq', fourierInv_eq_fourier_comp_neg, fourierInv_eq_fourier_neg, fourier_comp_linearIsometry, fourier_continuousLinearMap_apply, fourier_continuousMultilinearMap_apply, fourier_eq, fourier_eq', fourier_real_eq, fourier_real_eq_integral_exp_smul, vector_fourierIntegral_eq_integral_exp_smul, fourierIntegral_add, fourierIntegral_comp_add_right, fourierIntegral_const_smul, fourierIntegral_continuous, fourierIntegral_continuousLinearMap_apply, fourierIntegral_continuousMultilinearMap_apply, fourierIntegral_convergent_iff, fourierIntegral_probChar, integral_bilin_fourierIntegral_eq_flip, integral_fourierIntegral_smul_eq_flip, integral_fourierIntegral_swap, integral_sesq_fourierIntegral_eq_neg_flip, norm_fourierIntegral_le_integral_norm	48
Total	54

Fourier

Definitions

Name	Category	Theorems
fourierIntegral 📖	CompOp	5 math math: fourierIntegral_const_smul, norm_fourierIntegral_le_integral_norm, fourierIntegral_def, ZMod.dft_eq_fourier, fourierIntegral_comp_add_right

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fourierIntegral_comp_add_right 📖	mathematical	—	fourierIntegral Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Circle Circle.instSMul SMulZeroClass.toSMul Complex AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Complex.instNormedField DFunLike.coe AddChar AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup AddChar.instFunLike Distrib.toMul	—	VectorFourier.fourierIntegral_comp_add_right
fourierIntegral_const_smul 📖	mathematical	—	fourierIntegral Complex Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Complex.instNormedField	—	VectorFourier.fourierIntegral_const_smul
fourierIntegral_def 📖	mathematical	—	fourierIntegral MeasureTheory.integral NormedSpace.complexToReal NormedAddCommGroup.toSeminormedAddCommGroup Circle Circle.instSMul SMulZeroClass.toSMul Complex 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 DFunLike.coe AddChar AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup AddChar.instFunLike NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—
norm_fourierIntegral_le_integral_norm 📖	mathematical	—	Real Real.instLE Norm.norm NormedAddCommGroup.toNorm fourierIntegral MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal	—	VectorFourier.norm_fourierIntegral_le_integral_norm

Real

Definitions

Name	Category	Theorems
fourierIntegral 📖	CompOp	—
fourierIntegralInv 📖	CompOp	—
instFourierTransform 📖	CompOp	65 math math: hasDerivAt_fourier, fourierInv_eq_fourier_neg, mellin_eq_fourier, fourierCoeff_tsum_comp_add, fourierIntegral_comp_linearIsometry, fderiv_fourierIntegral, fourierIntegral_eq, fourier_continuousLinearMap_apply, fourierIntegral_gaussian_innerProductSpace', fourier_gaussian_pi', fourier_real_eq_integral_exp_smul, fourier_deriv, fourier_gaussian_innerProductSpace, fourierIntegral_continuousMultilinearMap_apply, fderiv_fourier, fourier_iteratedFDeriv, fourierIntegral_gaussian_pi, fourierIntegralInv_eq_fourierIntegral_neg, fourierIntegral_continuousLinearMap_apply, fourier_gaussian_innerProductSpace', fourier_real_eq, hasFDerivAt_fourier, fourier_comp_linearIsometry, fourier_mul_convolution_eq, differentiable_fourierIntegral, fourierIntegral_iteratedDeriv, pow_mul_norm_iteratedFDeriv_fourier_le, zero_at_infty_fourierIntegral, fourierIntegral_real_eq_integral_exp_smul, deriv_fourierIntegral, contDiff_fourierIntegral, fourier_fderiv, fourier_eq, fourier_iteratedDeriv, fourierInv_eq_fourier_comp_neg, fourier_bilin_convolution_eq, fourierIntegralInv_comm, mellin_eq_fourierIntegral, fourierIntegral_eq', contDiff_fourier, fourierIntegral_gaussian_innerProductSpace, iteratedDeriv_fourier, fourierIntegral_fderiv, zero_at_infty_fourier, iteratedFDeriv_fourier, hasFDerivAt_fourierIntegral, SchwartzMap.fourier_coe, fourier_bilin_convolution_eq_integral, fourierIntegralInv_eq_fourierIntegral_comp_neg, pow_mul_norm_iteratedFDeriv_fourierIntegral_le, fourierInv_comm, iteratedFDeriv_fourierIntegral, fourier_continuousMultilinearMap_apply, SchwartzMap.fourier_convolution_apply, iteratedDeriv_fourierIntegral, hasDerivAt_fourierIntegral, fourierIntegral_deriv, fourierIntegral_real_eq, fourier_eq', differentiable_fourier, fourierIntegral_iteratedFDeriv, fourier_gaussian_pi, fourier_smul_convolution_eq, deriv_fourier, fourierIntegral_gaussian_pi'
instFourierTransformInv 📖	CompOp	24 math math: fourierInv_eq_fourier_neg, fourierIntegralInv_eq', MeasureTheory.Integrable.fourierInv_fourier_eq, fourierIntegralInv_eq_fourierIntegral_neg, mellinInv_eq_fourierIntegralInv, fourierIntegralInv_comp_linearIsometry, mellinInv_eq_fourierInv, fourierInv_comp_linearIsometry, Continuous.fourierInv_fourier_eq, fourierInv_eq_fourier_comp_neg, fourierIntegralInv_comm, SchwartzMap.fourierInv_coe, fourierIntegralInv_eq_fourierIntegral_comp_neg, Continuous.fourier_inversion_inv, fourierInv_comm, MeasureTheory.Integrable.fourier_inversion, Continuous.fourier_inversion, tendsto_integral_gaussian_smul, MeasureTheory.Integrable.fourier_inversion_inv, Continuous.fourier_fourierInv_eq, fourierInv_eq, fourierInv_eq', fourierIntegralInv_eq, MeasureTheory.Integrable.fourier_fourierInv_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fourierIntegralInv_comm 📖	mathematical	—	FourierTransform.fourier instFourierTransform FourierTransformInv.fourierInv instFourierTransformInv	—	fourierInv_comm
fourierIntegralInv_comp_linearIsometry 📖	mathematical	—	FourierTransformInv.fourierInv instFourierTransformInv DFunLike.coe LinearIsometryEquiv Real semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule normedField InnerProductSpace.toNormedSpace instRCLike EquivLike.toFunLike LinearIsometryEquiv.instEquivLike	—	fourierInv_comp_linearIsometry
fourierIntegralInv_eq 📖	mathematical	—	FourierTransformInv.fourierInv instFourierTransformInv MeasureTheory.integral NormedSpace.complexToReal NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace MeasureTheory.MeasureSpace.volume Circle Circle.instSMul SMulZeroClass.toSMul Complex 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 DFunLike.coe AddChar Real instAddMonoid DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup AddChar.instFunLike fourierChar Inner.inner InnerProductSpace.toInner instRCLike	—	fourierInv_eq
fourierIntegralInv_eq' 📖	mathematical	—	FourierTransformInv.fourierInv instFourierTransformInv MeasureTheory.integral NormedSpace.complexToReal NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace MeasureTheory.MeasureSpace.volume 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 Complex.exp Complex.instMul Complex.ofReal Real instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat pi Inner.inner InnerProductSpace.toInner instRCLike Complex.I	—	fourierInv_eq'
fourierIntegralInv_eq_fourierIntegral_comp_neg 📖	mathematical	—	FourierTransformInv.fourierInv instFourierTransformInv FourierTransform.fourier instFourierTransform NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	fourierInv_eq_fourier_comp_neg
fourierIntegralInv_eq_fourierIntegral_neg 📖	mathematical	—	FourierTransformInv.fourierInv instFourierTransformInv FourierTransform.fourier instFourierTransform NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	fourierInv_eq_fourier_neg
fourierIntegral_comp_linearIsometry 📖	mathematical	—	FourierTransform.fourier instFourierTransform DFunLike.coe LinearIsometryEquiv Real semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule normedField InnerProductSpace.toNormedSpace instRCLike EquivLike.toFunLike LinearIsometryEquiv.instEquivLike	—	fourier_comp_linearIsometry
fourierIntegral_continuousLinearMap_apply 📖	mathematical	MeasureTheory.Integrable ContinuousLinearMap Real semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule normedField NormedSpace.complexToReal ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.toSeminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField denselyNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing normedCommRing MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace MeasureTheory.MeasureSpace.volume	DFunLike.coe ContinuousLinearMap.funLike FourierTransform.fourier instFourierTransform ContinuousLinearMap.toNormedAddCommGroup ContinuousLinearMap.toNormedSpace Complex Complex.instNormedField SMulCommClass.complexToReal NormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing	—	fourier_continuousLinearMap_apply
fourierIntegral_continuousLinearMap_apply' 📖	mathematical	MeasureTheory.Integrable ContinuousLinearMap Real semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule normedField NormedSpace.complexToReal ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.toSeminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField denselyNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing normedCommRing	DFunLike.coe ContinuousLinearMap.funLike VectorFourier.fourierIntegral commRing ContinuousLinearMap.toNormedAddCommGroup ContinuousLinearMap.toNormedSpace Complex Complex.instNormedField SMulCommClass.complexToReal NormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing fourierChar ContinuousLinearMap.toLinearMap₁₂ NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace instRCLike RCLike.toInnerProductSpaceReal pseudoMetricSpace instIsTopologicalAddGroupReal UniformContinuousConstSMul.to_continuousConstSMul instAddCommMonoid Ring.uniformContinuousConstSMul instRing instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal	—	instIsTopologicalAddGroupReal IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul SeminormedAddCommGroup.toIsTopologicalAddGroup RingHomIsometric.ids VectorFourier.fourierIntegral_continuousLinearMap_apply continuous_fourierChar
fourierIntegral_continuousMultilinearMap_apply 📖	mathematical	MeasureTheory.Integrable ContinuousMultilinearMap Real semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule normedField NormedSpace.complexToReal ContinuousMultilinearMap.instTopologicalSpace NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousMultilinearMap.seminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField denselyNormedField MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace MeasureTheory.MeasureSpace.volume	DFunLike.coe ContinuousMultilinearMap.funLike FourierTransform.fourier instFourierTransform ContinuousMultilinearMap.normedAddCommGroup ContinuousMultilinearMap.normedSpace Complex Complex.instNormedField SMulCommClass.complexToReal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing	—	fourier_continuousMultilinearMap_apply
fourierIntegral_continuousMultilinearMap_apply' 📖	mathematical	MeasureTheory.Integrable ContinuousMultilinearMap Real semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule normedField NormedSpace.complexToReal ContinuousMultilinearMap.instTopologicalSpace NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousMultilinearMap.seminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField denselyNormedField	DFunLike.coe ContinuousMultilinearMap.funLike VectorFourier.fourierIntegral commRing ContinuousMultilinearMap.normedAddCommGroup ContinuousMultilinearMap.normedSpace Complex Complex.instNormedField SMulCommClass.complexToReal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing fourierChar ContinuousLinearMap.toLinearMap₁₂ NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing InnerProductSpace.toNormedSpace instRCLike RCLike.toInnerProductSpaceReal pseudoMetricSpace instIsTopologicalAddGroupReal UniformContinuousConstSMul.to_continuousConstSMul instAddCommMonoid Ring.uniformContinuousConstSMul instRing instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal RingHom.id Semiring.toNonAssocSemiring	—	instIsTopologicalAddGroupReal IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul SeminormedAddCommGroup.toIsTopologicalAddGroup VectorFourier.fourierIntegral_continuousMultilinearMap_apply continuous_fourierChar
fourierIntegral_convergent_iff 📖	mathematical	—	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup 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 NormedSpace.toModule Complex.instNormedField DFunLike.coe AddChar Real instAddMonoid DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup AddChar.instFunLike fourierChar instNeg Inner.inner InnerProductSpace.toInner instRCLike	—	fourierIntegral_convergent_iff'
fourierIntegral_convergent_iff' 📖	mathematical	—	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup 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 NormedSpace.toModule Complex.instNormedField DFunLike.coe AddChar Real instAddMonoid DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup AddChar.instFunLike fourierChar instNeg ContinuousLinearMap semiring RingHom.id Semiring.toNonAssocSemiring pseudoMetricSpace instAddCommMonoid normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing InnerProductSpace.toNormedSpace instRCLike RCLike.toInnerProductSpaceReal ContinuousLinearMap.funLike ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup instIsTopologicalAddGroupReal ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousLinearMap.module Algebra.to_smulCommClass instCommSemiring CommSemiring.toSemiring Algebra.id UniformContinuousConstSMul.to_continuousConstSMul AddCommMonoid.toAddMonoid Ring.uniformContinuousConstSMul instRing instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	instIsTopologicalAddGroupReal IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul VectorFourier.fourierIntegral_convergent_iff continuous_fourierChar ContinuousLinearMap.continuous₂
fourierIntegral_eq 📖	mathematical	—	FourierTransform.fourier instFourierTransform MeasureTheory.integral NormedSpace.complexToReal NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace MeasureTheory.MeasureSpace.volume Circle Circle.instSMul SMulZeroClass.toSMul Complex 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 DFunLike.coe AddChar Real instAddMonoid DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup AddChar.instFunLike fourierChar instNeg Inner.inner InnerProductSpace.toInner instRCLike	—	fourier_eq
fourierIntegral_eq' 📖	mathematical	—	FourierTransform.fourier instFourierTransform MeasureTheory.integral NormedSpace.complexToReal NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace MeasureTheory.MeasureSpace.volume 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 Complex.exp Complex.instMul Complex.ofReal Real instMul instNeg instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat pi Inner.inner InnerProductSpace.toInner instRCLike Complex.I	—	fourier_eq'
fourierIntegral_real_eq 📖	mathematical	—	FourierTransform.fourier instFourierTransform Real normedAddCommGroup RCLike.toInnerProductSpaceReal instRCLike measurableSpace borelSpace FiniteDimensional.rclike_to_real MeasureTheory.integral NormedSpace.complexToReal NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.MeasureSpace.toMeasurableSpace measureSpace MeasureTheory.MeasureSpace.volume Circle Circle.instSMul SMulZeroClass.toSMul Complex 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 DFunLike.coe AddChar instAddMonoid DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup AddChar.instFunLike fourierChar instNeg instMul	—	fourier_real_eq
fourierIntegral_real_eq_integral_exp_smul 📖	mathematical	—	FourierTransform.fourier instFourierTransform Real normedAddCommGroup RCLike.toInnerProductSpaceReal instRCLike measurableSpace borelSpace FiniteDimensional.rclike_to_real MeasureTheory.integral NormedSpace.complexToReal NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.MeasureSpace.toMeasurableSpace measureSpace MeasureTheory.MeasureSpace.volume 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 Complex.exp Complex.instMul Complex.ofReal instMul instNeg instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat pi Complex.I	—	fourier_real_eq_integral_exp_smul
fourierInv_comm 📖	mathematical	—	FourierTransform.fourier instFourierTransform FourierTransformInv.fourierInv instFourierTransformInv	—	fourierInv_eq_fourier_comp_neg
fourierInv_comp_linearIsometry 📖	mathematical	—	FourierTransformInv.fourierInv instFourierTransformInv DFunLike.coe LinearIsometryEquiv Real semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule normedField InnerProductSpace.toNormedSpace instRCLike EquivLike.toFunLike LinearIsometryEquiv.instEquivLike	—	RingHomInvPair.ids fourierInv_eq_fourier_neg fourier_comp_linearIsometry map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearIsometryClass.toSemilinearMapClass SemilinearIsometryEquivClass.toSemilinearIsometryClass LinearIsometryEquiv.instSemilinearIsometryEquivClass
fourierInv_eq 📖	mathematical	—	FourierTransformInv.fourierInv instFourierTransformInv MeasureTheory.integral NormedSpace.complexToReal NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace MeasureTheory.MeasureSpace.volume Circle Circle.instSMul SMulZeroClass.toSMul Complex 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 DFunLike.coe AddChar Real instAddMonoid DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup AddChar.instFunLike fourierChar Inner.inner InnerProductSpace.toInner instRCLike	—	neg_neg
fourierInv_eq' 📖	mathematical	—	FourierTransformInv.fourierInv instFourierTransformInv MeasureTheory.integral NormedSpace.complexToReal NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace MeasureTheory.MeasureSpace.volume 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 Complex.exp Complex.instMul Complex.ofReal Real instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat pi Inner.inner InnerProductSpace.toInner instRCLike Complex.I	—	Nat.instAtLeastTwoHAddOfNat fourierInv_eq
fourierInv_eq_fourier_comp_neg 📖	mathematical	—	FourierTransformInv.fourierInv instFourierTransformInv FourierTransform.fourier instFourierTransform NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	fourierInv_eq_fourier_neg RingHomInvPair.ids fourier_comp_linearIsometry
fourierInv_eq_fourier_neg 📖	mathematical	—	FourierTransformInv.fourierInv instFourierTransformInv FourierTransform.fourier instFourierTransform NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	fourierInv_eq inner_neg_right neg_neg
fourier_comp_linearIsometry 📖	mathematical	—	FourierTransform.fourier instFourierTransform DFunLike.coe LinearIsometryEquiv Real semiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule normedField InnerProductSpace.toNormedSpace instRCLike EquivLike.toFunLike LinearIsometryEquiv.instEquivLike	—	RingHomInvPair.ids LinearIsometryEquiv.inner_map_map MeasureTheory.MeasurePreserving.integral_comp LinearIsometryEquiv.measurePreserving Homeomorph.measurableEmbedding
fourier_continuousLinearMap_apply 📖	mathematical	MeasureTheory.Integrable ContinuousLinearMap Real semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule normedField NormedSpace.complexToReal ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.toSeminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField denselyNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing normedCommRing MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace MeasureTheory.MeasureSpace.volume	DFunLike.coe ContinuousLinearMap.funLike FourierTransform.fourier instFourierTransform ContinuousLinearMap.toNormedAddCommGroup ContinuousLinearMap.toNormedSpace Complex Complex.instNormedField SMulCommClass.complexToReal NormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing	—	SeminormedAddCommGroup.toIsTopologicalAddGroup RingHomIsometric.ids fourierIntegral_continuousLinearMap_apply'
fourier_continuousMultilinearMap_apply 📖	mathematical	MeasureTheory.Integrable ContinuousMultilinearMap Real semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule normedField NormedSpace.complexToReal ContinuousMultilinearMap.instTopologicalSpace NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousMultilinearMap.seminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField denselyNormedField MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace MeasureTheory.MeasureSpace.volume	DFunLike.coe ContinuousMultilinearMap.funLike FourierTransform.fourier instFourierTransform ContinuousMultilinearMap.normedAddCommGroup ContinuousMultilinearMap.normedSpace Complex Complex.instNormedField SMulCommClass.complexToReal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing	—	SeminormedAddCommGroup.toIsTopologicalAddGroup fourierIntegral_continuousMultilinearMap_apply'
fourier_eq 📖	mathematical	—	FourierTransform.fourier instFourierTransform MeasureTheory.integral NormedSpace.complexToReal NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace MeasureTheory.MeasureSpace.volume Circle Circle.instSMul SMulZeroClass.toSMul Complex 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 DFunLike.coe AddChar Real instAddMonoid DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup AddChar.instFunLike fourierChar instNeg Inner.inner InnerProductSpace.toInner instRCLike	—	—
fourier_eq' 📖	mathematical	—	FourierTransform.fourier instFourierTransform MeasureTheory.integral NormedSpace.complexToReal NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace MeasureTheory.MeasureSpace.volume 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 Complex.exp Complex.instMul Complex.ofReal Real instMul instNeg instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat pi Inner.inner InnerProductSpace.toInner instRCLike Complex.I	—	Nat.instAtLeastTwoHAddOfNat mul_neg neg_mul
fourier_real_eq 📖	mathematical	—	FourierTransform.fourier instFourierTransform Real normedAddCommGroup RCLike.toInnerProductSpaceReal instRCLike measurableSpace borelSpace FiniteDimensional.rclike_to_real MeasureTheory.integral NormedSpace.complexToReal NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.MeasureSpace.toMeasurableSpace measureSpace MeasureTheory.MeasureSpace.volume Circle Circle.instSMul SMulZeroClass.toSMul Complex 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 DFunLike.coe AddChar instAddMonoid DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup AddChar.instFunLike fourierChar instNeg instMul	—	borelSpace FiniteDimensional.rclike_to_real mul_comm
fourier_real_eq_integral_exp_smul 📖	mathematical	—	FourierTransform.fourier instFourierTransform Real normedAddCommGroup RCLike.toInnerProductSpaceReal instRCLike measurableSpace borelSpace FiniteDimensional.rclike_to_real MeasureTheory.integral NormedSpace.complexToReal NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.MeasureSpace.toMeasurableSpace measureSpace MeasureTheory.MeasureSpace.volume 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 Complex.exp Complex.instMul Complex.ofReal instMul instNeg instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat pi Complex.I	—	borelSpace FiniteDimensional.rclike_to_real Nat.instAtLeastTwoHAddOfNat fourier_real_eq mul_neg neg_mul mul_assoc
vector_fourierIntegral_eq_integral_exp_smul 📖	mathematical	—	VectorFourier.fourierIntegral Real commRing fourierChar MeasureTheory.integral 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 Complex.exp Complex.instMul Complex.ofReal instMul instNeg instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat pi DFunLike.coe LinearMap semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instAddCommMonoid normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing InnerProductSpace.toNormedSpace instRCLike RCLike.toInnerProductSpaceReal LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass instCommSemiring CommSemiring.toSemiring Algebra.id Complex.I	—	Algebra.to_smulCommClass Nat.instAtLeastTwoHAddOfNat mul_neg neg_mul

VectorFourier

Definitions

Name	Category	Theorems
fourierIntegral 📖	CompOp	29 math math: MeasureTheory.charFun_eq_fourierIntegral', fourierIntegral_continuous, MeasureTheory.charFun_eq_fourierIntegral, Real.vector_fourierIntegral_eq_integral_exp_smul, fourierIntegral_continuousLinearMap_apply, hasFDerivAt_fourierIntegral, fourierIntegral_iteratedFDeriv, fourierIntegral_const_smul, differentiable_fourierIntegral, iteratedFDeriv_fourierIntegral, fourierIntegral_add, integral_sesq_fourierIntegral_eq_neg_flip, fderiv_fourierIntegral, pow_mul_norm_iteratedFDeriv_fourierIntegral_le, hasFTaylorSeriesUpTo_fourierIntegral', contDiff_fourierIntegral, integral_bilin_fourierIntegral_eq_flip, Real.fourierIntegral_continuousLinearMap_apply', hasFTaylorSeriesUpTo_fourierIntegral, fourierIntegral_continuousMultilinearMap_apply, fourierIntegral_comp_add_right, fourierIntegral_probChar, fourierPowSMulRight_iteratedFDeriv_fourierIntegral, integral_fourierIntegral_smul_eq_flip, Real.zero_at_infty_vector_fourierIntegral, norm_fourierIntegral_le_integral_norm, fourierIntegral_fderiv, norm_fourierPowSMulRight_iteratedFDeriv_fourierIntegral_le, Real.fourierIntegral_continuousMultilinearMap_apply'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fourierIntegral_add 📖	mathematical	Continuous Circle instTopologicalSpaceCircle DFunLike.coe AddChar AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup AddChar.instFunLike instTopologicalSpaceProd LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	fourierIntegral Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	Algebra.to_smulCommClass smul_add MeasureTheory.integral_add fourierIntegral_convergent_iff
fourierIntegral_comp_add_right 📖	mathematical	—	fourierIntegral AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid Circle Circle.instSMul SMulZeroClass.toSMul Complex AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Complex.instNormedField DFunLike.coe AddChar AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup AddChar.instFunLike LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id	—	Algebra.to_smulCommClass add_sub_cancel_right MeasureTheory.integral_add_right_eq_self MeasureTheory.integral_smul NormedSpace.toNormSMulClass SMulCommClass.complexToReal smulCommClass_self smul_assoc IsScalarTower.left smul_eq_mul Circle.coe_mul AddChar.map_add_eq_mul LinearMap.neg_apply sub_eq_add_neg LinearMap.sub_apply map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass neg_sub
fourierIntegral_const_smul 📖	mathematical	—	fourierIntegral Complex Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Complex.instNormedField	—	Algebra.to_smulCommClass SMulCommClass.smul_comm Circle.instSMulCommClass_left smulCommClass_self MeasureTheory.integral_smul NormedSpace.toNormSMulClass SMulCommClass.complexToReal
fourierIntegral_continuous 📖	mathematical	Continuous Circle instTopologicalSpaceCircle DFunLike.coe AddChar AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup AddChar.instFunLike instTopologicalSpaceProd LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	fourierIntegral	—	Algebra.to_smulCommClass MeasureTheory.continuous_of_dominated fourierIntegral_convergent_iff MeasureTheory.ae_of_all MeasureTheory.Measure.instOuterMeasureClass le_of_eq Circle.norm_smul MeasureTheory.Integrable.norm Filter.univ_mem' Continuous.smul Circle.instContinuousSMul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Continuous.comp' Continuous.neg IsTopologicalRing.toContinuousNeg Continuous.prodMk continuous_const continuous_id'
fourierIntegral_continuousLinearMap_apply 📖	mathematical	Continuous Circle UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField instTopologicalSpaceCircle DFunLike.coe AddChar ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup AddChar.instFunLike MeasureTheory.Integrable ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField NormedSpace.complexToReal ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.toSeminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHomIsometric.ids Real.normedCommRing	ContinuousLinearMap.funLike fourierIntegral EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField ContinuousLinearMap.toNormedAddCommGroup ContinuousLinearMap.toNormedSpace Complex Complex.instNormedField SMulCommClass.complexToReal NormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction AddCommGroup.toAddCommMonoid smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing ContinuousLinearMap.toLinearMap₁₂ NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul RingHomIsometric.ids SMulCommClass.complexToReal smulCommClass_self fourierIntegral.eq_1 IsScalarTower.to_smulCommClass' Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace ContinuousLinearMap.integral_apply fourierIntegral_convergent_iff ContinuousLinearMap.continuous₂
fourierIntegral_continuousMultilinearMap_apply 📖	mathematical	Continuous Circle UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField instTopologicalSpaceCircle DFunLike.coe AddChar ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup AddChar.instFunLike MeasureTheory.Integrable ContinuousMultilinearMap Real Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField NormedSpace.complexToReal ContinuousMultilinearMap.instTopologicalSpace NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousMultilinearMap.seminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField	ContinuousMultilinearMap.funLike fourierIntegral EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField ContinuousMultilinearMap.normedAddCommGroup ContinuousMultilinearMap.normedSpace Complex Complex.instNormedField SMulCommClass.complexToReal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction AddCommGroup.toAddCommMonoid smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing ContinuousLinearMap.toLinearMap₁₂ NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RingHom.id Semiring.toNonAssocSemiring	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul SMulCommClass.complexToReal smulCommClass_self fourierIntegral.eq_1 IsScalarTower.to_smulCommClass' Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace ContinuousMultilinearMap.integral_apply fourierIntegral_convergent_iff ContinuousLinearMap.continuous₂
fourierIntegral_convergent_iff 📖	mathematical	Continuous Circle instTopologicalSpaceCircle DFunLike.coe AddChar AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup AddChar.instFunLike instTopologicalSpaceProd LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup 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 NormedSpace.toModule Complex.instNormedField NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	Algebra.to_smulCommClass Continuous.comp Continuous.neg IsTopologicalRing.toContinuousNeg Continuous.prodMk_left MeasureTheory.integrable_norm_iff MeasureTheory.AEStronglyMeasurable.smul Circle.instContinuousSMul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Continuous.aestronglyMeasurable BorelSpace.opensMeasurable PseudoEMetricSpace.pseudoMetrizableSpace secondCountableTopologyEither_of_right TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace instLindelofSpaceOfSigmaCompactSpace CompactSpace.sigmaCompact Circle.instCompactSpace Circle.norm_smul MeasureTheory.Integrable.norm one_smul AddChar.map_zero_eq_one neg_add_cancel map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass AddChar.map_add_eq_mul SemigroupAction.mul_smul
fourierIntegral_probChar 📖	mathematical	—	fourierIntegral Real Real.commRing Real.probChar MeasureTheory.integral 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 Complex.exp Complex.instMul Complex.instNeg Complex.ofReal DFunLike.coe LinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Real.instAddCommMonoid Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id Complex.I	—	Algebra.to_smulCommClass Complex.ofReal_neg
integral_bilin_fourierIntegral_eq_flip 📖	mathematical	Continuous Circle instTopologicalSpaceCircle DFunLike.coe AddChar AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup AddChar.instFunLike instTopologicalSpaceProd LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	MeasureTheory.integral NormedSpace.complexToReal ContinuousLinearMap Complex Complex.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Complex.instNormedField ContinuousLinearMap.funLike ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero 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 fourierIntegral LinearMap.flip	—	Algebra.to_smulCommClass SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomIsometric.ids SMulCommClass.symm ContinuousLinearMap.integral_comp_comm fourierIntegral_convergent_iff integral_fourierIntegral_swap ContinuousLinearMap.map_smul_of_tower LinearMap.IsScalarTower.compatibleSMul Circle.instIsScalarTower IsScalarTower.left ContinuousLinearMap.isScalarTower Continuous.comp continuous_swap MeasureTheory.integral_def
integral_fourierIntegral_smul_eq_flip 📖	mathematical	Continuous Circle instTopologicalSpaceCircle DFunLike.coe AddChar AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup AddChar.instFunLike instTopologicalSpaceProd LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id MeasureTheory.Integrable Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	MeasureTheory.integral NormedSpace.complexToReal 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 NormedSpace.toModule fourierIntegral Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike RCLike.innerProductSpace LinearMap.flip	—	Algebra.to_smulCommClass integral_bilin_fourierIntegral_eq_flip Complex.instCompleteSpace NormedSpace.toIsBoundedSMul IsScalarTower.left
integral_fourierIntegral_swap 📖	mathematical	Continuous Circle instTopologicalSpaceCircle DFunLike.coe AddChar AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup AddChar.instFunLike instTopologicalSpaceProd LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	MeasureTheory.integral NormedSpace.complexToReal ContinuousLinearMap Complex Complex.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Complex.instNormedField ContinuousLinearMap.funLike ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero 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 Circle.instSMul ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid NegZeroClass.toNeg Ring.toAddCommGroup	—	Algebra.to_smulCommClass SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul MeasureTheory.integral_integral_swap MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.Integrable.const_mul MeasureTheory.Integrable.mul_prod MeasureTheory.Integrable.norm MeasureTheory.Integrable.mono MeasureTheory.AEStronglyMeasurable.smul Circle.instContinuousSMul IsBoundedSMul.continuousSMul Continuous.aestronglyMeasurable Prod.opensMeasurableSpace BorelSpace.opensMeasurable secondCountableTopologyEither_of_right PseudoEMetricSpace.pseudoMetrizableSpace TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace instLindelofSpaceOfSigmaCompactSpace CompactSpace.sigmaCompact Circle.instCompactSpace Continuous.comp Continuous.neg IsTopologicalRing.toContinuousNeg continuous_swap MeasureTheory.AEStronglyMeasurable.comp_snd MeasureTheory.AEStronglyMeasurable.prodMk MeasureTheory.AEStronglyMeasurable.comp_fst Continuous.clm_apply RingHomIsometric.ids ContinuousLinearMap.cont continuous_snd continuous_fst Continuous.comp_aestronglyMeasurable Filter.univ_mem' MeasureTheory.Measure.instOuterMeasureClass norm_mul NormedDivisionRing.toNormMulClass norm_norm Circle.norm_smul ContinuousLinearMap.le_opNorm₂
integral_sesq_fourierIntegral_eq_neg_flip 📖	mathematical	Continuous Circle instTopologicalSpaceCircle DFunLike.coe AddChar AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup AddChar.instFunLike instTopologicalSpaceProd LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	MeasureTheory.integral NormedSpace.complexToReal ContinuousLinearMap Complex Complex.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Complex.instNormedField ContinuousLinearMap.funLike Complex.instCommSemiring starRingEnd Complex.instStarRing ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero 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 fourierIntegral SMulCommClass.symm LinearMap.instNeg LinearMap.addCommGroup Ring.toAddCommGroup LinearMap.flip	—	Algebra.to_smulCommClass SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul SMulCommClass.symm RingHomIsometric.ids RingHomIsometric.starRingEnd CStarRing.to_normedStarGroup RCLike.instCStarRing ContinuousLinearMap.integral_comp_commSL RCLike.conj_smul fourierIntegral_convergent_iff integral_fourierIntegral_swap smul_one_smul Circle.instIsScalarTower IsScalarTower.left AddChar.map_neg_eq_inv mul_one MulActionSemiHomClass.map_smulₛₗ SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass inv_inv ContinuousLinearMap.map_smul_of_tower LinearMap.IsScalarTower.compatibleSMul neg_neg ContinuousLinearMap.integral_comp_comm Continuous.comp ContinuousNeg.continuous_neg IsTopologicalRing.toContinuousNeg continuous_swap MeasureTheory.integral_def
norm_fourierIntegral_le_integral_norm 📖	mathematical	—	Real Real.instLE Norm.norm NormedAddCommGroup.toNorm fourierIntegral MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal	—	Algebra.to_smulCommClass LE.le.trans MeasureTheory.norm_integral_le_integral_norm le_of_eq Circle.norm_smul

---

← Back to Index