Fourier

📁 Source: Mathlib/Analysis/Distribution/SchwartzSpace/Fourier.lean

Statistics

Metric	Count
Definitions fourierTransformCLE, fourierTransformCLM, instFourierTransform, instFourierTransformInv	4
Theorems fderivCLM_fourier_eq, fourierInv_apply_eq, fourierInv_coe, fourierInv_lineDerivOp_eq, fourierTransformCLE_apply, fourierTransformCLE_symm_apply, fourierTransformCLM_apply, fourier_coe, fourier_evalCLM_eq, fourier_fderivCLM_eq, fourier_inversion, fourier_inversion_inv, fourier_lineDerivOp_eq, inner_fourierTransformCLM_toL2_eq, inner_fourier_toL2_eq, instContinuousFourier, instContinuousFourierInv, instFourierAdd, instFourierInvAdd, instFourierInvPair, instFourierInvSMul, instFourierPair, instFourierSMul, integral_bilin_fourierIntegral_eq, integral_bilin_fourierInv_eq, integral_bilin_fourier_eq, integral_fourierInv_mul_eq, integral_fourierInv_smul_eq, integral_fourier_mul_eq, integral_fourier_smul_eq, integral_inner_fourier_fourier, integral_norm_sq_fourier, integral_sesq_fourierIntegral_eq, integral_sesq_fourier_eq, integral_sesq_fourier_fourier, lineDerivOp_fourierInv_eq, lineDerivOp_fourier_eq, norm_fourierTransformCLM_toL2_eq, norm_fourier_toL2_eq	39
Total	43

SchwartzMap

Definitions

Name	Category	Theorems
fourierTransformCLE 📖	CompOp	—
fourierTransformCLM 📖	CompOp	1 math math: fourierTransformCLM_apply
instFourierTransform 📖	CompOp	36 math math: integral_sesq_fourier_fourier, inner_fourier_toL2_eq, lineDerivOp_fourier_eq, integral_bilin_fourierIntegral_eq, integral_sesq_fourier_eq, fourier_lineDerivOp_eq, integral_norm_sq_fourier, norm_fourier_toL2_eq, instFourierPair, norm_fourierTransformCLM_toL2_eq, TemperedDistribution.fourier_toTemperedDistributionCLM_eq, integral_bilin_fourier_eq, fourierInv_apply_eq, fourier_evalCLM_eq, integral_sesq_fourierIntegral_eq, TemperedDistribution.fourierTransform_apply, inner_fourierTransformCLM_toL2_eq, integral_fourier_mul_eq, fourier_coe, toLp_fourierTransform_eq, instFourierSMul, fourierTransformCLM_apply, TemperedDistribution.fourierTransform_toTemperedDistributionCLM_eq, fderivCLM_fourier_eq, integral_fourier_smul_eq, instFourierInvPair, integral_inner_fourier_fourier, fourier_fderivCLM_eq, fourier_convolution_apply, instContinuousFourier, TemperedDistribution.fourier_apply, tsum_eq_tsum_fourierIntegral, fourier_convolution, toLp_fourier_eq, instFourierAdd, tsum_eq_tsum_fourier
instFourierTransformInv 📖	CompOp	20 math math: TemperedDistribution.fourierInv_toTemperedDistributionCLM_eq, toLp_fourierTransformInv_eq, integral_bilin_fourierInv_eq, integral_fourierInv_smul_eq, toLp_fourierInv_eq, integral_sesq_fourier_eq, instFourierPair, TemperedDistribution.fourierTransformInv_toTemperedDistributionCLM_eq, fourierInv_apply_eq, fourierInv_lineDerivOp_eq, instContinuousFourierInv, integral_sesq_fourierIntegral_eq, lineDerivOp_fourierInv_eq, fourierInv_coe, TemperedDistribution.fourierInv_apply, integral_fourierInv_mul_eq, instFourierInvAdd, instFourierInvPair, instFourierInvSMul, TemperedDistribution.fourierTransformInv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fderivCLM_fourier_eq 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.complexToReal instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup Real.semiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.toNormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing instModule SMulCommClass.complexToReal NormedAddCommGroup.toAddCommGroup Complex Complex.instNormedField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero ContinuousLinearMap.smulCommClass SeminormedAddCommGroup.toAddCommGroup ContinuousLinearMap.funLike fderivCLM FourierTransform.fourier instFourierTransform SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup CommRing.toCommMonoid Complex.commRing instSMul Complex.instNeg Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I NontriviallyNormedField.toNormedField Complex.instDenselyNormedField IsScalarTower.to_smulCommClass Real.instCommSemiring NormedAlgebra.toAlgebra NormedField.toNormedCommRing RCLike.toNormedAlgebra Complex.instRCLike Real.isScalarTower IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddCommGroup.toAddGroup Real.instMonoid NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace smulRightCLM innerSL	—	ext RingHomIsometric.ids smulCommClass_self SMulCommClass.complexToReal ContinuousLinearMap.smulCommClass Nat.instAtLeastTwoHAddOfNat IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Real.fderiv_fourier integrable MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth instIsAddHaarMeasureVolume secondCountable_of_proper FiniteDimensional.proper_real pow_one integrable_pow_mul
fourierInv_apply_eq 📖	mathematical	—	FourierTransformInv.fourierInv SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.complexToReal instFourierTransformInv DFunLike.coe ContinuousLinearMap Complex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Complex.instRCLike RingHom.id Semiring.toNonAssocSemiring instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule SMulCommClass.complexToReal NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Complex.instNormedField 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 Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing ContinuousLinearMap.funLike compCLMOfContinuousLinearEquiv LinearIsometryEquiv.toContinuousLinearEquiv Real.semiring RingHomInvPair.ids Real.normedField LinearIsometryEquiv.neg FourierTransform.fourier instFourierTransform	—	—
fourierInv_coe 📖	mathematical	—	DFunLike.coe SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.complexToReal instFunLike FourierTransformInv.fourierInv instFourierTransformInv Real.instFourierTransformInv	—	Real.fourierInv_eq_fourier_neg
fourierInv_lineDerivOp_eq 📖	mathematical	—	FourierTransformInv.fourierInv SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.complexToReal instFourierTransformInv LineDeriv.lineDerivOp instLineDeriv Complex instSMul Complex.instNormedField SMulCommClass.complexToReal NormedAddCommGroup.toAddCommGroup NormedSpace.toModule 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 DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing Complex.instNeg Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I DFunLike.coe ContinuousLinearMap NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHom.id Semiring.toNonAssocSemiring instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule IsScalarTower.to_smulCommClass Real.instCommSemiring NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing RCLike.toNormedAlgebra Real.isScalarTower IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Real.instMonoid Real.semiring NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace ContinuousLinearMap.funLike smulLeftCLM Inner.inner InnerProductSpace.toInner	—	Function.hasTemperateGrowth_inner_left SMulCommClass.complexToReal smulCommClass_self Nat.instAtLeastTwoHAddOfNat IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace RingHomInvPair.ids fourierInv_apply_eq fourier_lineDerivOp_eq map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass smulLeftCLM_compCLMOfContinuousLinearEquiv instIsTopologicalAddGroup inner_neg_left smulLeftCLM_fun_neg map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass smul_neg neg_smul neg_neg
fourierTransformCLE_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike ContinuousLinearEquiv.equivLike FourierTransform.fourierCLE FourierTransform.fourier	—	FourierTransform.fourierCLE_apply
fourierTransformCLE_symm_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike ContinuousLinearEquiv.equivLike ContinuousLinearEquiv.symm FourierTransform.fourierCLE FourierTransformInv.fourierInv	—	FourierTransform.fourierCLE_symm_apply
fourierTransformCLM_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.complexToReal instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule SMulCommClass.complexToReal NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Complex Complex.instNormedField 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 Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid ContinuousLinearMap.funLike fourierTransformCLM FourierTransform.fourier instFourierTransform	—	SMulCommClass.complexToReal
fourier_coe 📖	mathematical	—	DFunLike.coe SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.complexToReal instFunLike FourierTransform.fourier instFourierTransform Real.instFourierTransform	—	—
fourier_evalCLM_eq 📖	mathematical	—	FourierTransform.fourier SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.complexToReal instFourierTransform DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring Real.semiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.toNormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule ContinuousLinearMap.smulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SeminormedAddCommGroup.toAddCommGroup ContinuousLinearMap.funLike evalCLM 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 CommRing.toCommMonoid Complex.commRing	—	RingHomIsometric.ids smulCommClass_self ext ContinuousLinearMap.smulCommClass SMulCommClass.complexToReal Real.fourier_continuousLinearMap_apply integrable MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth instIsAddHaarMeasureVolume secondCountable_of_proper FiniteDimensional.proper_real
fourier_fderivCLM_eq 📖	mathematical	—	FourierTransform.fourier SchwartzMap 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 InnerProductSpace.toNormedSpace Real.instRCLike NormedSpace.complexToReal ContinuousLinearMap.toNormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing 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 AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup CommRing.toCommMonoid Complex.commRing instFourierTransform DFunLike.coe DenselyNormedField.toNormedField RCLike.toDenselyNormedField instTopologicalSpace instAddCommGroup instModule ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ContinuousLinearMap.smulCommClass ContinuousLinearMap.funLike fderivCLM instSMul Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I NontriviallyNormedField.toNormedField Complex.instDenselyNormedField IsScalarTower.to_smulCommClass Real.instCommSemiring NormedAlgebra.toAlgebra NormedField.toNormedCommRing RCLike.toNormedAlgebra Complex.instRCLike Real.isScalarTower IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddCommGroup.toAddGroup Real.instMonoid NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace smulRightCLM innerSL	—	ext RingHomIsometric.ids SMulCommClass.complexToReal smulCommClass_self ContinuousLinearMap.smulCommClass Nat.instAtLeastTwoHAddOfNat IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace ContinuousLinearMap.ext SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul instIsTopologicalAddGroupReal ContinuousLinearMap.topologicalAddGroup Real.fourier_fderiv integrable MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth instIsAddHaarMeasureVolume secondCountable_of_proper FiniteDimensional.proper_real differentiable instIsTopologicalRingReal instIsUniformAddGroupReal innerSL_apply_apply neg_smul smul_neg neg_neg IsScalarTower.left
fourier_inversion 📖	mathematical	—	FourierTransformInv.fourierInv FourierTransform.fourier	—	FourierPair.fourierInv_fourier_eq
fourier_inversion_inv 📖	mathematical	—	FourierTransform.fourier FourierTransformInv.fourierInv	—	FourierInvPair.fourier_fourierInv_eq
fourier_lineDerivOp_eq 📖	mathematical	—	FourierTransform.fourier SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.complexToReal instFourierTransform LineDeriv.lineDerivOp instLineDeriv Complex instSMul Complex.instNormedField SMulCommClass.complexToReal NormedAddCommGroup.toAddCommGroup NormedSpace.toModule 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 DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I DFunLike.coe ContinuousLinearMap NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHom.id Semiring.toNonAssocSemiring instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule IsScalarTower.to_smulCommClass Real.instCommSemiring NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing RCLike.toNormedAlgebra Real.isScalarTower IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Real.instMonoid Real.semiring NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace ContinuousLinearMap.funLike smulLeftCLM Inner.inner InnerProductSpace.toInner	—	SMulCommClass.complexToReal smulCommClass_self Nat.instAtLeastTwoHAddOfNat IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace ext RingHomIsometric.ids ContinuousLinearMap.smulCommClass ContinuousLinearMap.hasTemperateGrowth SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul RingHomIsometric.starRingEnd CStarRing.to_normedStarGroup instCStarRingReal fourier_evalCLM_eq fourier_fderivCLM_eq IsScalarTower.to_smulCommClass' IsScalarTower.complexToReal IsScalarTower.left instIsTopologicalAddGroupReal IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Algebra.to_smulCommClass Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul innerSL_apply_apply smulLeftCLM_apply_apply
inner_fourierTransformCLM_toL2_eq 📖	mathematical	—	Inner.inner Complex 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 instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat MeasureTheory.L2.instInnerSubtypeAEEqFunMemAddSubgroupLpOfNatENNReal Complex.instRCLike toLp InnerProductSpace.toNormedSpace Real Real.instRCLike NormedSpace.complexToReal BorelSpace.opensMeasurable secondCountableTopologyEither_of_left secondCountable_of_proper FiniteDimensional.proper_real FourierTransform.fourier SchwartzMap instFourierTransform MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth instIsAddHaarMeasureVolume	—	inner_fourier_toL2_eq
inner_fourier_toL2_eq 📖	mathematical	—	Inner.inner Complex 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 instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat MeasureTheory.L2.instInnerSubtypeAEEqFunMemAddSubgroupLpOfNatENNReal Complex.instRCLike toLp InnerProductSpace.toNormedSpace Real Real.instRCLike NormedSpace.complexToReal BorelSpace.opensMeasurable secondCountableTopologyEither_of_left secondCountable_of_proper FiniteDimensional.proper_real FourierTransform.fourier SchwartzMap instFourierTransform MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth instIsAddHaarMeasureVolume	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat BorelSpace.opensMeasurable secondCountableTopologyEither_of_left secondCountable_of_proper FiniteDimensional.proper_real MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth instIsAddHaarMeasureVolume inner_toL2_toL2_eq integral_inner_fourier_fourier
instContinuousFourier 📖	mathematical	—	ContinuousFourier SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.complexToReal instTopologicalSpace instFourierTransform	—	ContinuousLinearMap.continuous
instContinuousFourierInv 📖	mathematical	—	ContinuousFourierInv SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.complexToReal instTopologicalSpace instFourierTransformInv	—	ContinuousLinearMap.continuous RingHomInvPair.ids
instFourierAdd 📖	mathematical	—	FourierAdd SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.complexToReal instAdd instFourierTransform	—	ContinuousLinearMap.map_add SMulCommClass.complexToReal
instFourierInvAdd 📖	mathematical	—	FourierInvAdd SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.complexToReal instAdd instFourierTransformInv	—	ContinuousLinearMap.map_add RingHomInvPair.ids
instFourierInvPair 📖	mathematical	—	FourierInvPair SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.complexToReal instFourierTransform instFourierTransformInv	—	ext fourier_coe fourierInv_coe Continuous.fourier_fourierInv_eq continuous integrable MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth instIsAddHaarMeasureVolume secondCountable_of_proper FiniteDimensional.proper_real
instFourierInvSMul 📖	mathematical	—	FourierInvSMul SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.complexToReal instSMul DenselyNormedField.toNormedField RCLike.toDenselyNormedField SMulCommClass.complexToReal NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Complex Complex.instNormedField 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 DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid instFourierTransformInv	—	SMulCommClass.complexToReal ContinuousLinearMap.map_smul RingHomCompTriple.ids RingHomInvPair.ids
instFourierPair 📖	mathematical	—	FourierPair SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.complexToReal instFourierTransform instFourierTransformInv	—	ext fourierInv_coe fourier_coe Continuous.fourierInv_fourier_eq continuous integrable MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth instIsAddHaarMeasureVolume secondCountable_of_proper FiniteDimensional.proper_real
instFourierSMul 📖	mathematical	—	FourierSMul SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.complexToReal instSMul DenselyNormedField.toNormedField RCLike.toDenselyNormedField SMulCommClass.complexToReal NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Complex Complex.instNormedField 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 DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid instFourierTransform	—	SMulCommClass.complexToReal ContinuousLinearMap.map_smul
integral_bilin_fourierIntegral_eq 📖	mathematical	—	MeasureTheory.integral NormedSpace.complexToReal NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace MeasureTheory.MeasureSpace.volume 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 SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring 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 NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike instFunLike FourierTransform.fourier instFourierTransform	—	integral_bilin_fourier_eq
integral_bilin_fourierInv_eq 📖	mathematical	—	MeasureTheory.integral NormedSpace.complexToReal NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace MeasureTheory.MeasureSpace.volume 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 SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring 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 NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike instFunLike FourierTransformInv.fourierInv instFourierTransformInv	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul FourierInvPair.fourier_fourierInv_eq instFourierInvPair integral_bilin_fourier_eq
integral_bilin_fourier_eq 📖	mathematical	—	MeasureTheory.integral NormedSpace.complexToReal NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace MeasureTheory.MeasureSpace.volume 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 SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring 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 NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike instFunLike FourierTransform.fourier instFourierTransform	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul Algebra.to_smulCommClass SMulCommClass.symm flip_innerₗ VectorFourier.integral_bilin_fourierIntegral_eq_flip instIsTopologicalRingReal MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper FiniteDimensional.proper_real instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper Real.continuous_fourierChar continuous_inner integrable MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth
integral_fourierInv_mul_eq 📖	mathematical	—	MeasureTheory.integral Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace MeasureTheory.MeasureSpace.volume Complex.instMul DFunLike.coe SchwartzMap NormedSpace.complexToReal Complex.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField RCLike.innerProductSpace instFunLike FourierTransformInv.fourierInv instFourierTransformInv	—	integral_bilin_fourierInv_eq Complex.instCompleteSpace IsScalarTower.right Algebra.to_smulCommClass
integral_fourierInv_smul_eq 📖	mathematical	—	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 DFunLike.coe SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike Complex.instNormedAddCommGroup Complex.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing RCLike.innerProductSpace instFunLike FourierTransformInv.fourierInv instInnerProductSpaceRealComplex instFourierTransformInv	—	integral_bilin_fourierInv_eq Complex.instCompleteSpace NormedSpace.toIsBoundedSMul IsScalarTower.left
integral_fourier_mul_eq 📖	mathematical	—	MeasureTheory.integral Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace MeasureTheory.MeasureSpace.volume Complex.instMul DFunLike.coe SchwartzMap NormedSpace.complexToReal Complex.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField RCLike.innerProductSpace instFunLike FourierTransform.fourier instFourierTransform	—	integral_bilin_fourier_eq Complex.instCompleteSpace IsScalarTower.right Algebra.to_smulCommClass
integral_fourier_smul_eq 📖	mathematical	—	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 DFunLike.coe SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike Complex.instNormedAddCommGroup Complex.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing RCLike.innerProductSpace instFunLike FourierTransform.fourier instInnerProductSpaceRealComplex instFourierTransform	—	integral_bilin_fourier_eq Complex.instCompleteSpace NormedSpace.toIsBoundedSMul IsScalarTower.left
integral_inner_fourier_fourier 📖	mathematical	—	MeasureTheory.integral Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace MeasureTheory.MeasureSpace.volume Inner.inner InnerProductSpace.toInner Complex.instRCLike DFunLike.coe SchwartzMap NormedSpace.complexToReal instFunLike FourierTransform.fourier instFourierTransform	—	integral_sesq_fourier_fourier
integral_norm_sq_fourier 📖	mathematical	—	MeasureTheory.integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace MeasureTheory.MeasureSpace.volume Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm DFunLike.coe SchwartzMap NormedSpace.complexToReal Complex Complex.instRCLike instFunLike FourierTransform.fourier instFourierTransform	—	LinearIsometry.injective Complex.instCompleteSpace Real.instCompleteSpace Complex.ofReal_pow inner_self_eq_norm_sq_to_K integral_inner_fourier_fourier
integral_sesq_fourierIntegral_eq 📖	mathematical	—	MeasureTheory.integral NormedSpace.complexToReal NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace MeasureTheory.MeasureSpace.volume 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 CommSemiring.toSemiring Complex.instCommSemiring starRingEnd Complex.instStarRing ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring 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 NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike instFunLike FourierTransform.fourier instFourierTransform FourierTransformInv.fourierInv instFourierTransformInv	—	integral_sesq_fourier_eq
integral_sesq_fourier_eq 📖	mathematical	—	MeasureTheory.integral NormedSpace.complexToReal NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace MeasureTheory.MeasureSpace.volume 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 CommSemiring.toSemiring Complex.instCommSemiring starRingEnd Complex.instStarRing ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring 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 NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike instFunLike FourierTransform.fourier instFourierTransform FourierTransformInv.fourierInv instFourierTransformInv	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul fourierInv_coe SMulCommClass.symm Algebra.to_smulCommClass flip_innerₗ VectorFourier.integral_sesq_fourierIntegral_eq_neg_flip instIsTopologicalRingReal MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper FiniteDimensional.proper_real instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper Real.continuous_fourierChar continuous_inner integrable MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth
integral_sesq_fourier_fourier 📖	mathematical	—	MeasureTheory.integral NormedSpace.complexToReal NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace MeasureTheory.MeasureSpace.volume 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 CommSemiring.toSemiring Complex.instCommSemiring starRingEnd Complex.instStarRing ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring 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 NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike instFunLike FourierTransform.fourier instFourierTransform	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul FourierPair.fourierInv_fourier_eq instFourierPair integral_sesq_fourier_eq
lineDerivOp_fourierInv_eq 📖	mathematical	—	LineDeriv.lineDerivOp SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.complexToReal instLineDeriv FourierTransformInv.fourierInv instFourierTransformInv Complex instSMul Complex.instNormedField SMulCommClass.complexToReal NormedAddCommGroup.toAddCommGroup NormedSpace.toModule 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 DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I DFunLike.coe ContinuousLinearMap NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHom.id Semiring.toNonAssocSemiring instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule IsScalarTower.to_smulCommClass Real.instCommSemiring NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing RCLike.toNormedAlgebra Real.isScalarTower IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Real.instMonoid Real.semiring NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace ContinuousLinearMap.funLike smulLeftCLM Inner.inner InnerProductSpace.toInner	—	SMulCommClass.complexToReal smulCommClass_self Nat.instAtLeastTwoHAddOfNat IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace RingHomInvPair.ids fourierInv_apply_eq lineDerivOp_compCLMOfContinuousLinearEquiv LineDeriv.lineDerivOp_left_neg instLineDerivAdd lineDerivOp_fourier_eq neg_smul FourierTransform.fourier_neg instFourierAdd FourierSMul.fourier_smul instFourierSMul neg_neg map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass FourierInvSMul.fourierInv_smul instFourierInvSMul
lineDerivOp_fourier_eq 📖	mathematical	—	LineDeriv.lineDerivOp SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.complexToReal instLineDeriv FourierTransform.fourier instFourierTransform Complex instSMul Complex.instNormedField SMulCommClass.complexToReal NormedAddCommGroup.toAddCommGroup NormedSpace.toModule 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 DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing Complex.instNeg Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I DFunLike.coe ContinuousLinearMap NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHom.id Semiring.toNonAssocSemiring instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule IsScalarTower.to_smulCommClass Real.instCommSemiring NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing RCLike.toNormedAlgebra Real.isScalarTower IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Real.instMonoid Real.semiring NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace ContinuousLinearMap.funLike smulLeftCLM Inner.inner InnerProductSpace.toInner	—	SMulCommClass.complexToReal smulCommClass_self Nat.instAtLeastTwoHAddOfNat IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace RingHomIsometric.ids ContinuousLinearMap.smulCommClass IsScalarTower.to_smulCommClass' IsScalarTower.complexToReal IsScalarTower.left fderivCLM_fourier_eq fourier_evalCLM_eq ext ContinuousLinearMap.hasTemperateGrowth SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul RingHomIsometric.starRingEnd CStarRing.to_normedStarGroup instCStarRingReal neg_smul map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass instIsTopologicalAddGroupReal IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Algebra.to_smulCommClass Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul innerSL_apply_apply smulLeftCLM_apply_apply
norm_fourierTransformCLM_toL2_eq 📖	mathematical	—	Norm.norm 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 instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat MeasureTheory.Lp.instNorm toLp InnerProductSpace.toNormedSpace Real Real.instRCLike NormedSpace.complexToReal Complex Complex.instRCLike BorelSpace.opensMeasurable secondCountableTopologyEither_of_left secondCountable_of_proper FiniteDimensional.proper_real FourierTransform.fourier SchwartzMap instFourierTransform MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth instIsAddHaarMeasureVolume	—	norm_fourier_toL2_eq
norm_fourier_toL2_eq 📖	mathematical	—	Norm.norm 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 instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat MeasureTheory.Lp.instNorm toLp InnerProductSpace.toNormedSpace Real Real.instRCLike NormedSpace.complexToReal Complex Complex.instRCLike BorelSpace.opensMeasurable secondCountableTopologyEither_of_left secondCountable_of_proper FiniteDimensional.proper_real FourierTransform.fourier SchwartzMap instFourierTransform MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth instIsAddHaarMeasureVolume	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat BorelSpace.opensMeasurable secondCountableTopologyEither_of_left secondCountable_of_proper FiniteDimensional.proper_real MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth instIsAddHaarMeasureVolume fact_one_le_two_ennreal norm_eq_sqrt_re_inner inner_fourier_toL2_eq

---

← Back to Index