FourierMultiplier

📁 Source: Mathlib/Analysis/Distribution/FourierMultiplier.lean

Statistics

Metric	Count
Definitions fourierMultiplierCLM, fourierMultiplierCLM	2
Theorems fourierMultiplierCLM_apply, fourierMultiplierCLM_compL_fourierMultiplierCLM, fourierMultiplierCLM_const, fourierMultiplierCLM_fourierMultiplierCLM_apply, fourierMultiplierCLM_ofReal, fourierMultiplierCLM_smul, fourierMultiplierCLM_sum, laplacian_eq_fourierMultiplierCLM, lineDeriv_eq_fourierMultiplierCLM, fourierMultiplierCLM_apply, fourierMultiplierCLM_apply_apply, fourierMultiplierCLM_compL_fourierMultiplierCLM, fourierMultiplierCLM_const, fourierMultiplierCLM_fourierMultiplierCLM_apply, fourierMultiplierCLM_smul, fourierMultiplierCLM_sum, fourierMultiplierCLM_toTemperedDistributionCLM_eq, laplacian_eq_fourierMultiplierCLM, lineDeriv_eq_fourierMultiplierCLM	19
Total	21

SchwartzMap

Definitions

Name	Category	Theorems
fourierMultiplierCLM 📖	CompOp	10 math math: fourierMultiplierCLM_compL_fourierMultiplierCLM, fourierMultiplierCLM_sum, lineDeriv_eq_fourierMultiplierCLM, fourierMultiplierCLM_apply, TemperedDistribution.fourierMultiplierCLM_toTemperedDistributionCLM_eq, fourierMultiplierCLM_ofReal, fourierMultiplierCLM_const, fourierMultiplierCLM_fourierMultiplierCLM_apply, fourierMultiplierCLM_smul, laplacian_eq_fourierMultiplierCLM

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fourierMultiplierCLM_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 fourierMultiplierCLM FourierTransformInv.fourierInv instFourierTransformInv NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField 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 Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace smulLeftCLM FourierTransform.fourier instFourierTransform	—	SMulCommClass.complexToReal
fourierMultiplierCLM_compL_fourierMultiplierCLM 📖	mathematical	Function.HasTemperateGrowth InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField RCLike.toInnerProductSpaceReal	ContinuousLinearMap.comp 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 RingHomCompTriple.ids fourierMultiplierCLM Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing	—	ContinuousLinearMap.ext SMulCommClass.complexToReal RingHomCompTriple.ids fourierMultiplierCLM_fourierMultiplierCLM_apply
fourierMultiplierCLM_const 📖	mathematical	—	fourierMultiplierCLM 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.instSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instSMulCommClass smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing ContinuousSMul.continuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instContinuousSMul ContinuousLinearMap.id	—	ContinuousLinearMap.ext SMulCommClass.complexToReal instSMulCommClass smulCommClass_self ContinuousSMul.continuousConstSMul instContinuousSMul ext IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace fourierMultiplierCLM_apply smulLeftCLM_const FourierInvSMul.fourierInv_smul instFourierInvSMul FourierPair.fourierInv_fourier_eq instFourierPair
fourierMultiplierCLM_fourierMultiplierCLM_apply 📖	mathematical	Function.HasTemperateGrowth InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField RCLike.toInnerProductSpaceReal	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 fourierMultiplierCLM Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing	—	SMulCommClass.complexToReal IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace fourierMultiplierCLM_apply FourierInvPair.fourier_fourierInv_eq instFourierInvPair smulLeftCLM_smulLeftCLM_apply
fourierMultiplierCLM_ofReal 📖	mathematical	Function.HasTemperateGrowth Real InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Real.normedAddCommGroup RCLike.toInnerProductSpaceReal	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 fourierMultiplierCLM RCLike.ofReal IsScalarTower.to_smulCommClass' Real.instCommSemiring Complex.instSemiring NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing RCLike.toNormedAlgebra Complex.instRCLike IsScalarTower.complexToReal Complex.addCommGroup Complex.instModuleSelf AddCommMonoid.toAddMonoid IsScalarTower.left DistribMulAction.toMulAction	—	SMulCommClass.complexToReal IsScalarTower.to_smulCommClass' IsScalarTower.complexToReal IsScalarTower.left IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace fourierMultiplierCLM_apply smulLeftCLM_ofReal
fourierMultiplierCLM_smul 📖	mathematical	Function.HasTemperateGrowth InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField RCLike.toInnerProductSpaceReal	fourierMultiplierCLM Function.hasSMul Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField CommSemiring.toSemiring Algebra.id ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring 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.instSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instSMulCommClass smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing ContinuousSMul.continuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instContinuousSMul	—	ContinuousLinearMap.ext SMulCommClass.complexToReal instSMulCommClass smulCommClass_self ContinuousSMul.continuousConstSMul instContinuousSMul IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace fourierMultiplierCLM_apply smulLeftCLM_smul FourierInvSMul.fourierInv_smul instFourierInvSMul
fourierMultiplierCLM_sum 📖	mathematical	Function.HasTemperateGrowth InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField RCLike.toInnerProductSpaceReal	fourierMultiplierCLM Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField 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 SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup instIsTopologicalAddGroup	—	ContinuousLinearMap.ext SMulCommClass.complexToReal IsTopologicalAddGroup.toContinuousAdd instIsTopologicalAddGroup IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace fourierMultiplierCLM_apply smulLeftCLM_sum ContinuousLinearMap.coe_sum' Finset.sum_apply FourierTransform.fourierInv_sum instFourierInvAdd Finset.sum_congr
laplacian_eq_fourierMultiplierCLM 📖	mathematical	—	Laplacian.laplacian SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.complexToReal instLaplacian instSMul Real.normedField smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing NormedSpace.toModule Real.instNeg Monoid.toPow Real.instMonoid Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup 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 IsScalarTower.to_smulCommClass' Real.instCommSemiring Complex.instSemiring NormedAlgebra.toAlgebra SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing RCLike.toNormedAlgebra Complex.instRCLike IsScalarTower.complexToReal Complex.addCommGroup Complex.instModuleSelf IsScalarTower.left ContinuousLinearMap.funLike fourierMultiplierCLM Norm.norm NormedAddCommGroup.toNorm	—	Function.HasTemperateGrowth.fun_pow Function.hasTemperateGrowth_inner_left smulCommClass_self Nat.instAtLeastTwoHAddOfNat SMulCommClass.complexToReal IsScalarTower.to_smulCommClass' IsScalarTower.complexToReal IsScalarTower.left laplacian_eq_sum fourierMultiplierCLM.congr_simp OrthonormalBasis.sum_sq_inner_left IsTopologicalAddGroup.toContinuousAdd instIsTopologicalAddGroup fourierMultiplierCLM_sum ContinuousLinearMap.coe_sum' Finset.sum_apply Finset.smul_sum ext lineDeriv_eq_fourierMultiplierCLM fourierMultiplierCLM_ofReal map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass smul_smul RingHom.map_zero' Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.RingNF.mul_assoc_rev add_zero Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg Complex.I_sq mul_neg mul_one neg_mul Complex.ofReal_neg Complex.ofReal_mul Complex.ofReal_pow fourierMultiplierCLM_fourierMultiplierCLM_apply sq
lineDeriv_eq_fourierMultiplierCLM 📖	mathematical	—	LineDeriv.lineDerivOp SchwartzMap InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.complexToReal 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 DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule IsScalarTower.to_smulCommClass' Real.instCommSemiring Complex.instSemiring NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing RCLike.toNormedAlgebra Complex.instRCLike IsScalarTower.complexToReal Complex.addCommGroup Complex.instModuleSelf IsScalarTower.left ContinuousLinearMap.funLike fourierMultiplierCLM Inner.inner InnerProductSpace.toInner	—	SMulCommClass.complexToReal smulCommClass_self Nat.instAtLeastTwoHAddOfNat IsScalarTower.to_smulCommClass' IsScalarTower.complexToReal IsScalarTower.left IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace fourierMultiplierCLM_apply FourierInvSMul.fourierInv_smul instFourierInvSMul fourier_lineDerivOp_eq FourierPair.fourierInv_fourier_eq instFourierPair

TemperedDistribution

Definitions

Name	Category	Theorems
fourierMultiplierCLM 📖	CompOp	10 math math: fourierMultiplierCLM_smul, fourierMultiplierCLM_compL_fourierMultiplierCLM, laplacian_eq_fourierMultiplierCLM, fourierMultiplierCLM_fourierMultiplierCLM_apply, fourierMultiplierCLM_apply, fourierMultiplierCLM_const, fourierMultiplierCLM_toTemperedDistributionCLM_eq, fourierMultiplierCLM_apply_apply, fourierMultiplierCLM_sum, lineDeriv_eq_fourierMultiplierCLM

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fourierMultiplierCLM_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring TemperedDistribution InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup UniformConvergenceCLM.instTopologicalSpace Complex.instNormedField SchwartzMap Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex SchwartzMap.instAddCommGroup SchwartzMap.instModule Complex.instRCLike RCLike.innerProductSpace SchwartzMap.instTopologicalSpace NormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toIsTopologicalAddGroup setOf Set Finite Set.Elem AddCommGroup.toAddCommMonoid UniformConvergenceCLM.instAddCommGroup UniformConvergenceCLM.instModule smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup 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 ContinuousLinearMap.funLike fourierMultiplierCLM FourierTransformInv.fourierInv instFourierTransformInv smulLeftCLM FourierTransform.fourier instFourierTransform	—	SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul
fourierMultiplierCLM_apply_apply 📖	mathematical	—	DFunLike.coe TemperedDistribution InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup SchwartzMap Complex Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex UniformConvergenceCLM.instFunLike Complex.instNormedField RingHom.id Semiring.toNonAssocSemiring Complex.instSemiring SchwartzMap.instAddCommGroup SchwartzMap.instModule Complex.instRCLike RCLike.innerProductSpace SchwartzMap.instTopologicalSpace NormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace setOf Set Finite Set.Elem ContinuousLinearMap UniformConvergenceCLM.instTopologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup AddCommGroup.toAddCommMonoid UniformConvergenceCLM.instAddCommGroup UniformConvergenceCLM.instModule smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup 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 ContinuousLinearMap.funLike fourierMultiplierCLM FourierTransform.fourier SchwartzMap.instFourierTransform NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField IsScalarTower.to_smulCommClass Real.instCommSemiring NormedAlgebra.toAlgebra Real.normedField RCLike.toNormedAlgebra Real.isScalarTower IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero Real.instMonoid Real.semiring TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul NormedAlgebra.toNormedSpace SchwartzMap.smulLeftCLM FourierTransformInv.fourierInv SchwartzMap.instFourierTransformInv	—	SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul
fourierMultiplierCLM_compL_fourierMultiplierCLM 📖	mathematical	Function.HasTemperateGrowth Complex InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex	ContinuousLinearMap.comp Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring TemperedDistribution InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup UniformConvergenceCLM.instTopologicalSpace Complex.instNormedField SchwartzMap Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex SchwartzMap.instAddCommGroup SchwartzMap.instModule Complex.instRCLike RCLike.innerProductSpace SchwartzMap.instTopologicalSpace NormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toIsTopologicalAddGroup setOf Set Finite Set.Elem AddCommGroup.toAddCommMonoid UniformConvergenceCLM.instAddCommGroup UniformConvergenceCLM.instModule smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup 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 RingHomCompTriple.ids fourierMultiplierCLM Pi.instMul Complex.instMul	—	ContinuousLinearMap.ext SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomCompTriple.ids fourierMultiplierCLM_fourierMultiplierCLM_apply
fourierMultiplierCLM_const 📖	mathematical	—	fourierMultiplierCLM Complex ContinuousLinearMap Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring TemperedDistribution InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup UniformConvergenceCLM.instTopologicalSpace Complex.instNormedField SchwartzMap Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex SchwartzMap.instAddCommGroup SchwartzMap.instModule Complex.instRCLike RCLike.innerProductSpace SchwartzMap.instTopologicalSpace NormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toIsTopologicalAddGroup setOf Set Finite Set.Elem AddCommGroup.toAddCommMonoid UniformConvergenceCLM.instAddCommGroup UniformConvergenceCLM.instModule smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup 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 ContinuousLinearMap.instSMul UniformConvergenceCLM.instDistribMulAction UniformConvergenceCLM UniformConvergenceCLM.instContinuousConstSMul ContinuousLinearMap.id	—	ContinuousLinearMap.ext SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul UniformConvergenceCLM.instContinuousConstSMul UniformConvergenceCLM.ext IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace fourierMultiplierCLM_apply_apply Localization.instSMulCommClassOfIsScalarTower IsScalarTower.complexToReal IsScalarTower.right SchwartzMap.instSMulCommClass ContinuousSMul.continuousConstSMul SchwartzMap.instContinuousSMul SchwartzMap.smulLeftCLM_const FourierSMul.fourier_smul SchwartzMap.instFourierSMul Algebra.to_smulCommClass FourierInvPair.fourier_fourierInv_eq SchwartzMap.instFourierInvPair Complex.instCompleteSpace map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass UniformConvergenceCLM.instContinuousSemilinearMapClass
fourierMultiplierCLM_fourierMultiplierCLM_apply 📖	mathematical	Function.HasTemperateGrowth Complex InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex	DFunLike.coe ContinuousLinearMap Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring TemperedDistribution InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup UniformConvergenceCLM.instTopologicalSpace Complex.instNormedField SchwartzMap Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex SchwartzMap.instAddCommGroup SchwartzMap.instModule Complex.instRCLike RCLike.innerProductSpace SchwartzMap.instTopologicalSpace NormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toIsTopologicalAddGroup setOf Set Finite Set.Elem AddCommGroup.toAddCommMonoid UniformConvergenceCLM.instAddCommGroup UniformConvergenceCLM.instModule smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup 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 ContinuousLinearMap.funLike fourierMultiplierCLM Pi.instMul Complex.instMul	—	SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul fourierMultiplierCLM_apply FourierInvPair.fourier_fourierInv_eq instFourierPairInv smulLeftCLM_smulLeftCLM_apply
fourierMultiplierCLM_smul 📖	mathematical	Function.HasTemperateGrowth Complex InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex	fourierMultiplierCLM Complex Function.hasSMul Algebra.toSMul Complex.instCommSemiring CommSemiring.toSemiring Algebra.id ContinuousLinearMap Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring TemperedDistribution InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup UniformConvergenceCLM.instTopologicalSpace Complex.instNormedField SchwartzMap Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex SchwartzMap.instAddCommGroup SchwartzMap.instModule Complex.instRCLike RCLike.innerProductSpace SchwartzMap.instTopologicalSpace NormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toIsTopologicalAddGroup setOf Set Finite Set.Elem AddCommGroup.toAddCommMonoid UniformConvergenceCLM.instAddCommGroup UniformConvergenceCLM.instModule smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup 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 ContinuousLinearMap.instSMul UniformConvergenceCLM.instDistribMulAction UniformConvergenceCLM UniformConvergenceCLM.instContinuousConstSMul	—	ContinuousLinearMap.ext SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul UniformConvergenceCLM.instContinuousConstSMul fourierMultiplierCLM_apply smulLeftCLM_smul FourierInvSMul.fourierInv_smul instFourierInvSMul
fourierMultiplierCLM_sum 📖	mathematical	Function.HasTemperateGrowth Complex InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex	fourierMultiplierCLM Finset.sum Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup ContinuousLinearMap Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring TemperedDistribution InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup UniformConvergenceCLM.instTopologicalSpace SchwartzMap instInnerProductSpaceRealComplex SchwartzMap.instAddCommGroup SchwartzMap.instModule Complex.instRCLike RCLike.innerProductSpace SchwartzMap.instTopologicalSpace NormedAddCommGroup.toAddCommGroup NormedSpace.toModule SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toIsTopologicalAddGroup setOf Set Finite Set.Elem AddCommGroup.toAddCommMonoid UniformConvergenceCLM.instAddCommGroup UniformConvergenceCLM.instModule 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 SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsBoundedSMul.toUniformContinuousConstSMul Complex.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd UniformConvergenceCLM.instIsTopologicalAddGroup	—	ContinuousLinearMap.ext SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul IsTopologicalAddGroup.toContinuousAdd UniformConvergenceCLM.instIsTopologicalAddGroup UniformConvergenceCLM.ext IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace fourierMultiplierCLM_apply_apply SchwartzMap.instIsTopologicalAddGroup SchwartzMap.smulLeftCLM_sum ContinuousLinearMap.coe_sum' Finset.sum_apply FourierTransform.fourier_sum SchwartzMap.instFourierAdd map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass UniformConvergenceCLM.instContinuousSemilinearMapClass UniformConvergenceCLM.sum_apply Finset.sum_congr
fourierMultiplierCLM_toTemperedDistributionCLM_eq 📖	mathematical	Function.HasTemperateGrowth Complex InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex	DFunLike.coe ContinuousLinearMap Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring TemperedDistribution InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup UniformConvergenceCLM.instTopologicalSpace Complex.instNormedField SchwartzMap Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex SchwartzMap.instAddCommGroup SchwartzMap.instModule Complex.instRCLike RCLike.innerProductSpace SchwartzMap.instTopologicalSpace NormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toIsTopologicalAddGroup setOf Set Finite Set.Elem AddCommGroup.toAddCommMonoid UniformConvergenceCLM.instAddCommGroup UniformConvergenceCLM.instModule smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup 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 ContinuousLinearMap.funLike fourierMultiplierCLM NormedSpace.complexToReal SchwartzMap.toTemperedDistributionCLM MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace secondCountable_of_proper FiniteDimensional.proper_real MeasureTheory.MeasureSpace.volume MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth instIsAddHaarMeasureVolume DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField SMulCommClass.complexToReal ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid SchwartzMap.fourierMultiplierCLM	—	UniformConvergenceCLM.ext SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul secondCountable_of_proper FiniteDimensional.proper_real MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth instIsAddHaarMeasureVolume SMulCommClass.complexToReal IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace fourierMultiplierCLM_apply_apply SchwartzMap.toTemperedDistributionCLM_apply_apply SchwartzMap.integral_fourier_smul_eq SchwartzMap.smulLeftCLM_apply_apply SchwartzMap.fourierMultiplierCLM_apply smul_smul mul_comm
laplacian_eq_fourierMultiplierCLM 📖	mathematical	—	Laplacian.laplacian TemperedDistribution InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instLaplacian SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup UniformConvergenceCLM.instAddCommGroup Complex Complex.instNormedField RingHom.id Semiring.toNonAssocSemiring Complex.instSemiring SchwartzMap Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex SchwartzMap.instAddCommGroup SchwartzMap.instModule Complex.instRCLike RCLike.innerProductSpace SchwartzMap.instTopologicalSpace NormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toIsTopologicalAddGroup setOf Set Finite Set.Elem DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid Module.complexToReal UniformConvergenceCLM.instModule smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul 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 Real.instNeg Monoid.toPow Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi DFunLike.coe ContinuousLinearMap UniformConvergenceCLM.instTopologicalSpace ContinuousLinearMap.funLike fourierMultiplierCLM Complex.ofReal Norm.norm NormedAddCommGroup.toNorm	—	Function.HasTemperateGrowth.fun_pow Function.HasTemperateGrowth.comp Function.Complex.hasTemperateGrowth_ofReal Function.hasTemperateGrowth_inner_left SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul Nat.instAtLeastTwoHAddOfNat laplacian_eq_sum fourierMultiplierCLM.congr_simp OrthonormalBasis.sum_sq_inner_left Complex.ofReal_sum Finset.sum_congr Complex.ofReal_pow IsTopologicalAddGroup.toContinuousAdd UniformConvergenceCLM.instIsTopologicalAddGroup fourierMultiplierCLM_sum ContinuousLinearMap.coe_sum' Finset.sum_apply Finset.smul_sum UniformConvergenceCLM.ext lineDeriv_eq_fourierMultiplierCLM map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass smul_smul fourierMultiplierCLM_fourierMultiplierCLM_apply Complex.coe_smul Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.RingNF.mul_assoc_rev add_zero Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg Complex.I_sq mul_neg mul_one neg_mul Complex.ofReal_neg Complex.ofReal_mul sq
lineDeriv_eq_fourierMultiplierCLM 📖	mathematical	—	LineDeriv.lineDerivOp TemperedDistribution InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instLineDeriv Complex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup UniformConvergenceCLM.instAddCommGroup Complex.instNormedField RingHom.id Semiring.toNonAssocSemiring Complex.instSemiring SchwartzMap Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex SchwartzMap.instAddCommGroup SchwartzMap.instModule Complex.instRCLike RCLike.innerProductSpace SchwartzMap.instTopologicalSpace NormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toIsTopologicalAddGroup setOf Set Finite Set.Elem DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero UniformConvergenceCLM.instDistribMulAction Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I DFunLike.coe ContinuousLinearMap UniformConvergenceCLM.instTopologicalSpace AddCommGroup.toAddCommMonoid UniformConvergenceCLM.instModule ContinuousLinearMap.funLike fourierMultiplierCLM Inner.inner InnerProductSpace.toInner	—	SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul Nat.instAtLeastTwoHAddOfNat fourierMultiplierCLM_apply FourierInvSMul.fourierInv_smul instFourierInvSMul fourier_lineDerivOp_eq FourierPair.fourierInv_fourier_eq instFourierPair

---

← Back to Index