FourierTransform

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

Statistics

Metric	Count
Definitions fourierIntegral, fourierTransform, fourierTransformCLM, fourierIntegral, fourierIntegralInv, instFourierTransform, instFourierTransformInv, fourierIntegral	8
Theorems fourierIntegral_comp_add_right, fourierIntegral_const_smul, fourierIntegral_def, norm_fourierIntegral_le_integral_norm, coe_fourierTransform, fourierTransformCLM_apply, fourierTransform_apply, 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, fourierTransform_toLp, fourier_comp_linearIsometry, fourier_congr_ae, 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_congr_ae, 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	54
Total	62

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	84 math math: hasDerivAt_fourier, fourierInv_eq_fourier_neg, mellin_eq_fourier, fourierCoeff_tsum_comp_add, fourierIntegral_comp_linearIsometry, fderiv_fourierIntegral, tsum_eq_tsum_fourier, fourierIntegral_eq, fourier_continuousLinearMap_apply, MeasureTheory.Integrable.fourierInv_fourier_eq, tsum_eq_tsum_fourierIntegral_of_rpow_decay_of_summable, 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, tsum_eq_tsum_fourier_of_rpow_decay_of_summable, pow_mul_norm_iteratedFDeriv_fourier_le, zero_at_infty_fourierIntegral, fourierIntegral_real_eq_integral_exp_smul, deriv_fourierIntegral, Lp.fourierTransform_apply, Continuous.fourierInv_fourier_eq, 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, tsum_eq_tsum_fourier_of_rpow_decay, Continuous.fourier_inversion_inv, pow_mul_norm_iteratedFDeriv_fourierIntegral_le, fourierInv_comm, MeasureTheory.Integrable.fourier_inversion, Continuous.fourier_inversion, iteratedFDeriv_fourierIntegral, tendsto_integral_gaussian_smul, MeasureTheory.Integrable.fourier_inversion_inv, fourierTransform_toLp, Continuous.fourier_fourierInv_eq, fourier_continuousMultilinearMap_apply, SchwartzMap.fourier_convolution_apply, iteratedDeriv_fourierIntegral, hasDerivAt_fourierIntegral, fourier_congr_ae, tsum_eq_tsum_fourierIntegral, Lp.coe_fourierTransform, fourierIntegral_deriv, fourierIntegral_real_eq, tsum_eq_tsum_fourierIntegral_of_rpow_decay, fourier_eq', differentiable_fourier, fourierIntegral_iteratedFDeriv, fourier_gaussian_pi, fourier_smul_convolution_eq, deriv_fourier, fourierIntegral_gaussian_pi', MeasureTheory.Integrable.fourier_fourierInv_eq
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 NormedAddCommGroup.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 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.funLike FourierTransform.fourier instFourierTransform ContinuousLinearMap.toNormedAddCommGroup DenselyNormedField.toNontriviallyNormedField denselyNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing normedCommRing ContinuousLinearMap.toNormedSpace 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	—	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 NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.toSeminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField denselyNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing normedCommRing	DFunLike.coe 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.funLike VectorFourier.fourierIntegral commRing NormedAddCommGroup.toAddCommGroup ContinuousLinearMap.toNormedAddCommGroup DenselyNormedField.toNontriviallyNormedField denselyNormedField 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 fourierChar ContinuousLinearMap.toLinearMap₁₂ instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace instRCLike RCLike.toInnerProductSpaceReal pseudoMetricSpace instIsTopologicalAddGroupReal SeparatelyContinuousMul.to_continuousSMul instMul IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal	—	instIsTopologicalAddGroupReal IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul 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.toIsTopologicalAddGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousMultilinearMap.seminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField denselyNormedField MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace MeasureTheory.MeasureSpace.volume	DFunLike.coe ContinuousMultilinearMap Real semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule normedField NormedSpace.complexToReal ContinuousMultilinearMap.funLike FourierTransform.fourier instFourierTransform ContinuousMultilinearMap.normedAddCommGroup DenselyNormedField.toNontriviallyNormedField denselyNormedField 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	—	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.toIsTopologicalAddGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousMultilinearMap.seminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField denselyNormedField	DFunLike.coe ContinuousMultilinearMap Real semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule normedField NormedSpace.complexToReal ContinuousMultilinearMap.funLike VectorFourier.fourierIntegral commRing NormedAddCommGroup.toAddCommGroup ContinuousMultilinearMap.normedAddCommGroup DenselyNormedField.toNontriviallyNormedField denselyNormedField 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 fourierChar ContinuousLinearMap.toLinearMap₁₂ instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing InnerProductSpace.toNormedSpace instRCLike RCLike.toInnerProductSpaceReal pseudoMetricSpace instIsTopologicalAddGroupReal SeparatelyContinuousMul.to_continuousSMul 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 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 NormedAddCommGroup.toAddCommGroup 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 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
fourierTransform_toLp 📖	mathematical	MeasureTheory.MemLp MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal MeasureTheory.MeasureSpace.volume	DFunLike.coe BoundedContinuousFunction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup BoundedContinuousFunction.instFunLike Lp.fourierTransform MeasureTheory.MemLp.toLp MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal MeasureTheory.MeasureSpace.volume FourierTransform.fourier instFourierTransform	—	fourier_congr_ae SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.MemLp.coeFn_toLp
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_congr_ae 📖	mathematical	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.MeasureSpace.volume	FourierTransform.fourier instFourierTransform	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.integral_congr_ae Filter.mp_mem Filter.univ_mem'
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 NormedAddCommGroup.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 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.funLike FourierTransform.fourier instFourierTransform ContinuousLinearMap.toNormedAddCommGroup DenselyNormedField.toNontriviallyNormedField denselyNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing normedCommRing ContinuousLinearMap.toNormedSpace 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	—	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.toIsTopologicalAddGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousMultilinearMap.seminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField denselyNormedField MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace MeasureTheory.MeasureSpace.volume	DFunLike.coe ContinuousMultilinearMap Real semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule normedField NormedSpace.complexToReal ContinuousMultilinearMap.funLike FourierTransform.fourier instFourierTransform ContinuousMultilinearMap.normedAddCommGroup DenselyNormedField.toNontriviallyNormedField denselyNormedField 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	—	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

Real.Lp

Definitions

Name	Category	Theorems
fourierTransform 📖	CompOp	4 math math: fourierTransform_apply, fourierTransformCLM_apply, Real.fourierTransform_toLp, coe_fourierTransform
fourierTransformCLM 📖	CompOp	1 math math: fourierTransformCLM_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_fourierTransform 📖	mathematical	—	DFunLike.coe BoundedContinuousFunction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup BoundedContinuousFunction.instFunLike fourierTransform FourierTransform.fourier Real.instFourierTransform MeasureTheory.AEEqFun.cast MeasureTheory.MeasureSpace.volume measureSpaceOfInnerProductSpace MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	SeminormedAddCommGroup.toIsTopologicalAddGroup
fourierTransformCLM_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.MeasureSpace.volume measureSpaceOfInnerProductSpace AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal MeasureTheory.Lp.instNormedAddCommGroup fact_one_le_one_ennreal ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid BoundedContinuousFunction BoundedContinuousFunction.instPseudoMetricSpace BoundedContinuousFunction.instAddCommMonoid instBoundedAddOfLipschitzAdd ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid SeminormedAddCommGroup.to_lipschitzAdd IsTopologicalAddGroup.toContinuousAdd MeasureTheory.Lp.instModule NormedCommRing.toNormedRing NormedField.toNormedCommRing Complex.instNormedField NormedSpace.toModule NormedSpace.toIsBoundedSMul BoundedContinuousFunction.instModule SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ContinuousLinearMap.funLike fourierTransformCLM fourierTransform	—	SeminormedAddCommGroup.toIsTopologicalAddGroup fact_one_le_one_ennreal instBoundedAddOfLipschitzAdd SeminormedAddCommGroup.to_lipschitzAdd IsTopologicalAddGroup.toContinuousAdd NormedSpace.toIsBoundedSMul
fourierTransform_apply 📖	mathematical	—	DFunLike.coe BoundedContinuousFunction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup BoundedContinuousFunction.instFunLike fourierTransform FourierTransform.fourier Real.instFourierTransform MeasureTheory.AEEqFun.cast MeasureTheory.MeasureSpace.volume measureSpaceOfInnerProductSpace MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	SeminormedAddCommGroup.toIsTopologicalAddGroup

VectorFourier

Definitions

Name	Category	Theorems
fourierIntegral 📖	CompOp	30 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, fourierIntegral_congr_ae, 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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup 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_congr_ae 📖	mathematical	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	fourierIntegral	—	Algebra.to_smulCommClass MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.integral_congr_ae Filter.mp_mem Filter.univ_mem'
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	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup 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 IsSemitopologicalRing.toContinuousNeg IsTopologicalRing.toIsSemitopologicalRing 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 NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.toSeminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHomIsometric.ids Real.normedCommRing	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 fourierIntegral EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup ContinuousLinearMap.toNormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField 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 DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing ContinuousLinearMap.toLinearMap₁₂ NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace SeminormedRing.toPseudoMetricSpace SeminormedAddCommGroup.toIsTopologicalAddGroup SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul 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.toIsTopologicalAddGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousMultilinearMap.seminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField	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 fourierIntegral EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup ContinuousMultilinearMap.normedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField 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 Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing ContinuousLinearMap.toLinearMap₁₂ NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing SeminormedAddCommGroup.toIsTopologicalAddGroup SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing RingHom.id Semiring.toNonAssocSemiring	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul 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 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 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 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	—	Algebra.to_smulCommClass Continuous.comp Continuous.neg IsSemitopologicalRing.toContinuousNeg IsTopologicalRing.toIsSemitopologicalRing 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 NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe ContinuousLinearMap Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Complex.instNormedField ContinuousLinearMap.funLike ContinuousLinearMap.topologicalSpace NormedAddCommGroup.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 CommRing.toRing 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 NormedSpace.toIsBoundedSMul fourierIntegral LinearMap.flip CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule Algebra.to_smulCommClass Algebra.id	—	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 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 fourierIntegral Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike RCLike.innerProductSpace LinearMap.flip CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule Algebra.to_smulCommClass Algebra.id RingHom.id Semiring.toNonAssocSemiring	—	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 NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe ContinuousLinearMap Complex Complex.instSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Complex.instNormedField ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.topologicalSpace NormedAddCommGroup.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 CommRing.toRing 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 NormedSpace.toIsBoundedSMul Circle Circle.instSMul ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid AddChar AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup AddChar.instFunLike NegZeroClass.toNeg Ring.toAddCommGroup LinearMap CommSemiring.toSemiring CommRing.toCommSemiring 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	—	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 IsSemitopologicalRing.toContinuousNeg IsTopologicalRing.toIsSemitopologicalRing 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 NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe ContinuousLinearMap Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Complex.instNormedField ContinuousLinearMap.funLike starRingEnd Complex.instCommSemiring Complex.instStarRing ContinuousLinearMap.topologicalSpace NormedAddCommGroup.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 CommRing.toRing 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 NormedSpace.toIsBoundedSMul fourierIntegral LinearMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule LinearMap.addCommMonoid LinearMap.module SMulCommClass.symm Algebra.to_smulCommClass Algebra.id 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 IsSemitopologicalRing.toContinuousNeg IsTopologicalRing.toIsSemitopologicalRing 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