TemperedDistribution

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

Statistics

Metric	Count
Definitions toTemperedDistribution, instCoeDep, toTemperedDistribution, toTemperedDistributionCLM, toTemperedDistribution, delta, instCoeToTemperedDistribution, toTemperedDistributionCLM, «term𝓢'(_,_)»»), TemperedDistribution, delta, derivCLM, fourierTransformCLM, fourierTransformInvCLM, instFourierTransform, instFourierTransformInv, instLaplacian, instLineDeriv, smulLeftCLM	19
Theorems toTemperedDistribution_apply, ker_toTemperedDistributionCLM_eq_bot, toTemperedDistributionCLM_apply, toTemperedDistribution_apply, toTemperedDistribution_smul_eq, toTemperedDistribution_toLp_eq, toTemperedDistribution_apply, coe_apply, delta_apply, integralCLM_dirac_eq_delta, toTemperedDistributionCLM_apply_apply, delta_apply, derivCLM_apply_apply, derivCLM_toTemperedDistributionCLM_eq, fourierInv_apply, fourierInv_lineDerivOp_eq, fourierInv_toTemperedDistributionCLM_eq, fourierTransformCLM_apply, fourierTransformInvCLM_apply, fourierTransformInv_apply, fourierTransformInv_toTemperedDistributionCLM_eq, fourierTransform_apply, fourierTransform_toTemperedDistributionCLM_eq, fourier_apply, fourier_delta_zero, fourier_lineDerivOp_eq, fourier_toTemperedDistributionCLM_eq, instContinuousFourier, instContinuousFourierInv, instContinuousLineDeriv, instFourierAdd, instFourierInvAdd, instFourierInvSMul, instFourierPair, instFourierPairInv, instFourierSMul, instLineDerivAdd, instLineDerivLeftSMulReal, instLineDerivSMulComplex, instLineDerivSMulReal, laplacianCLM_apply, laplacian_apply_apply, laplacian_eq_sum, laplacian_toTemperedDistributionCLM_eq, lineDerivOpCLM_eq, lineDerivOp_apply_apply, lineDerivOp_fourierInv_eq, lineDerivOp_fourier_eq, lineDerivOp_toTemperedDistributionCLM_eq, smulLeftCLM_add, smulLeftCLM_apply_apply, smulLeftCLM_compL_smulLeftCLM, smulLeftCLM_const, smulLeftCLM_neg, smulLeftCLM_smul, smulLeftCLM_smulLeftCLM_apply, smulLeftCLM_sub, smulLeftCLM_sum, toTemperedDistribution_dirac_eq_delta	59
Total	78

Function.HasTemperateGrowth

Definitions

Name	Category	Theorems
toTemperedDistribution 📖	CompOp	1 math math: toTemperedDistribution_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toTemperedDistribution_apply 📖	mathematical	Function.HasTemperateGrowth NormedSpace.complexToReal NormedAddCommGroup.toSeminormedAddCommGroup	DFunLike.coe TemperedDistribution SchwartzMap Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike 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 toTemperedDistribution MeasureTheory.integral SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid SchwartzMap.instFunLike	—	—

MeasureTheory.Lp

Definitions

Name	Category	Theorems
instCoeDep 📖	CompOp	—
toTemperedDistribution 📖	CompOp	6 math math: toTemperedDistributionCLM_apply, fourierInv_toTemperedDistribution_eq, toTemperedDistribution_toLp_eq, toTemperedDistribution_apply, fourier_toTemperedDistribution_eq, toTemperedDistribution_smul_eq
toTemperedDistributionCLM 📖	CompOp	2 math math: toTemperedDistributionCLM_apply, ker_toTemperedDistributionCLM_eq_bot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ker_toTemperedDistributionCLM_eq_bot 📖	mathematical	—	LinearMap.ker Complex MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp TemperedDistribution Complex.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid instNormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCommGroup.toAddCommMonoid UniformConvergenceCLM.instAddCommGroup Complex.instNormedField RingHom.id Semiring.toNonAssocSemiring SchwartzMap Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike instInnerProductSpaceRealComplex SchwartzMap.instAddCommGroup SchwartzMap.instModule Complex.instRCLike RCLike.innerProductSpace SchwartzMap.instTopologicalSpace NormedAddCommGroup.toAddCommGroup NormedSpace.toModule setOf Set Finite Set.Elem instModule NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedSpace.toIsBoundedSMul 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 SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Complex.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid ContinuousLinearMap.toLinearMap UniformConvergenceCLM.instTopologicalSpace toTemperedDistributionCLM Bot.bot Submodule Submodule.instBot	—	SeminormedAddCommGroup.toIsTopologicalAddGroup NormedSpace.toIsBoundedSMul smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul LinearMap.ker_eq_bot' ContinuousLinearMap.coe_coe MeasureTheory.Measure.instOuterMeasureClass eq_zero_iff_ae_eq_zero ae_eq_zero_of_integral_contDiff_smul_eq_zero MeasureTheory.MemLp.locallyIntegrable memLp Fact.elim HasCompactSupport.comp_left ContDiff.clm_apply contDiff_const RingHomIsometric.ids toTemperedDistribution_apply
toTemperedDistributionCLM_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp instNormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid TemperedDistribution UniformConvergenceCLM.instTopologicalSpace Complex.instNormedField SchwartzMap Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike instInnerProductSpaceRealComplex SchwartzMap.instAddCommGroup SchwartzMap.instModule Complex.instRCLike RCLike.innerProductSpace SchwartzMap.instTopologicalSpace NormedAddCommGroup.toAddCommGroup NormedSpace.toModule setOf Set Finite Set.Elem AddCommGroup.toAddCommMonoid UniformConvergenceCLM.instAddCommGroup instModule NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedSpace.toIsBoundedSMul 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 SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Complex.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid ContinuousLinearMap.funLike toTemperedDistributionCLM toTemperedDistribution	—	SeminormedAddCommGroup.toIsTopologicalAddGroup NormedSpace.toIsBoundedSMul smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul
toTemperedDistribution_apply 📖	mathematical	—	DFunLike.coe TemperedDistribution SchwartzMap Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup 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 toTemperedDistribution MeasureTheory.integral NormedSpace.complexToReal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid SchwartzMap.instFunLike MeasureTheory.AEEqFun.cast MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ContinuousLinearMap.comp_apply ContinuousLinearMap.lpPairing_eq_integral MeasureTheory.integral_congr_ae Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass BorelSpace.opensMeasurable secondCountableTopologyEither_of_right UniformSpace.secondCountable_of_separable EMetric.instIsCountablyGeneratedUniformity TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper Complex.instProperSpace SchwartzMap.coeFn_toLp Filter.univ_mem'
toTemperedDistribution_smul_eq 📖	mathematical	Function.HasTemperateGrowth Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SeminormedAddGroup.toContinuousENorm SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing	toTemperedDistribution MeasureTheory.AEEqFun SeminormedAddCommGroup.toPseudoMetricSpace AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp instHSMulSubtypeAEEqFunMemAddSubgroup NormedCommRing.toNormedRing Module.toMulActionWithZero Ring.toSemiring NormedRing.toRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule NormedSpace.toIsBoundedSMul MeasureTheory.MemLp.toLp DFunLike.coe ContinuousLinearMap Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring TemperedDistribution UniformConvergenceCLM.instTopologicalSpace SchwartzMap SchwartzMap.instAddCommGroup SchwartzMap.instModule Complex.instRCLike RCLike.innerProductSpace SchwartzMap.instTopologicalSpace NormedAddCommGroup.toAddCommGroup 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 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 ContinuousLinearMap.funLike TemperedDistribution.smulLeftCLM	—	SeminormedAddCommGroup.toIsTopologicalAddGroup UniformConvergenceCLM.ext NormedSpace.toIsBoundedSMul smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace toTemperedDistribution_apply TemperedDistribution.smulLeftCLM_apply_apply MeasureTheory.integral_congr_ae Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.MemLp.coeFn_toLp coeFn_lpSMul Filter.univ_mem' smul_smul mul_comm SchwartzMap.smulLeftCLM_apply_apply
toTemperedDistribution_toLp_eq 📖	mathematical	—	toTemperedDistribution SchwartzMap.toLp NormedSpace.complexToReal NormedAddCommGroup.toSeminormedAddCommGroup BorelSpace.opensMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace secondCountableTopologyEither_of_left DFunLike.coe ContinuousLinearMap Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring SchwartzMap SchwartzMap.instTopologicalSpace AddCommGroup.toAddCommMonoid SchwartzMap.instAddCommGroup TemperedDistribution UniformConvergenceCLM.instTopologicalSpace Complex.instNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike instInnerProductSpaceRealComplex SchwartzMap.instModule Complex.instRCLike RCLike.innerProductSpace NormedAddCommGroup.toAddCommGroup NormedSpace.toModule SeminormedAddCommGroup.toIsTopologicalAddGroup setOf Set Finite Set.Elem UniformConvergenceCLM.instAddCommGroup SMulCommClass.complexToReal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero 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 UniformConvergenceCLM.instModule UniformContinuousConstSMul.to_continuousConstSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup 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 SchwartzMap.toTemperedDistributionCLM	—	UniformConvergenceCLM.ext BorelSpace.opensMeasurable secondCountableTopologyEither_of_left SeminormedAddCommGroup.toIsTopologicalAddGroup SMulCommClass.complexToReal smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul toTemperedDistribution_apply SchwartzMap.toTemperedDistributionCLM_apply_apply MeasureTheory.integral_congr_ae Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass SchwartzMap.coeFn_toLp Filter.univ_mem'

MeasureTheory.Measure

Definitions

Name	Category	Theorems
toTemperedDistribution 📖	CompOp	4 math math: toTemperedDistribution_apply, TemperedDistribution.fourier_delta_zero, SchwartzMap.integralCLM_dirac_eq_delta, TemperedDistribution.toTemperedDistribution_dirac_eq_delta

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toTemperedDistribution_apply 📖	mathematical	—	DFunLike.coe TemperedDistribution Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace SchwartzMap Real Real.instRCLike instInnerProductSpaceRealComplex UniformConvergenceCLM.instFunLike Complex.instNormedField RingHom.id Semiring.toNonAssocSemiring Complex.instSemiring SchwartzMap.instAddCommGroup SchwartzMap.instModule SchwartzMap.instTopologicalSpace NormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace setOf Set Finite Set.Elem toTemperedDistribution MeasureTheory.integral SchwartzMap.instFunLike	—	—

SchwartzMap

Definitions

Name	Category	Theorems
delta 📖	CompOp	—
instCoeToTemperedDistribution 📖	CompOp	—
toTemperedDistributionCLM 📖	CompOp	10 math math: TemperedDistribution.fourierInv_toTemperedDistributionCLM_eq, TemperedDistribution.fourier_toTemperedDistributionCLM_eq, TemperedDistribution.fourierTransformInv_toTemperedDistributionCLM_eq, toTemperedDistributionCLM_apply_apply, TemperedDistribution.lineDerivOp_toTemperedDistributionCLM_eq, TemperedDistribution.fourierTransform_toTemperedDistributionCLM_eq, TemperedDistribution.laplacian_toTemperedDistributionCLM_eq, TemperedDistribution.derivCLM_toTemperedDistributionCLM_eq, MeasureTheory.Lp.toTemperedDistribution_toLp_eq, coe_apply
«term𝓢'(_,_)» 📖» "API Documentation")	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_apply 📖	mathematical	—	DFunLike.coe TemperedDistribution SchwartzMap Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex UniformConvergenceCLM.instFunLike Complex.instNormedField RingHom.id Semiring.toNonAssocSemiring Complex.instSemiring instAddCommGroup instModule Complex.instRCLike RCLike.innerProductSpace instTopologicalSpace NormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace setOf Set Finite Set.Elem ContinuousLinearMap NormedSpace.complexToReal AddCommGroup.toAddCommMonoid UniformConvergenceCLM.instTopologicalSpace UniformConvergenceCLM.instAddCommGroup UniformConvergenceCLM.instModule ContinuousLinearMap.funLike toTemperedDistributionCLM MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.MeasureSpace.volume MeasureTheory.integral SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid instFunLike	—	toTemperedDistributionCLM_apply_apply
delta_apply 📖	mathematical	—	DFunLike.coe TemperedDistribution Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace SchwartzMap Real Real.instRCLike instInnerProductSpaceRealComplex UniformConvergenceCLM.instFunLike Complex.instNormedField RingHom.id Semiring.toNonAssocSemiring Complex.instSemiring instAddCommGroup instModule instTopologicalSpace NormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace setOf Set Finite Set.Elem TemperedDistribution.delta instFunLike	—	TemperedDistribution.delta_apply
integralCLM_dirac_eq_delta 📖	mathematical	—	MeasureTheory.Measure.toTemperedDistribution MeasureTheory.Measure.dirac MeasureTheory.IsFiniteMeasure.instHasTemperateGrowth MeasureTheory.Measure.dirac.instIsFiniteMeasure TemperedDistribution.delta	—	TemperedDistribution.toTemperedDistribution_dirac_eq_delta
toTemperedDistributionCLM_apply_apply 📖	mathematical	—	DFunLike.coe TemperedDistribution SchwartzMap Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex UniformConvergenceCLM.instFunLike Complex.instNormedField RingHom.id Semiring.toNonAssocSemiring Complex.instSemiring instAddCommGroup instModule Complex.instRCLike RCLike.innerProductSpace instTopologicalSpace NormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace setOf Set Finite Set.Elem ContinuousLinearMap NormedSpace.complexToReal AddCommGroup.toAddCommMonoid UniformConvergenceCLM.instTopologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup UniformConvergenceCLM.instAddCommGroup SMulCommClass.complexToReal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero 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 UniformConvergenceCLM.instModule UniformContinuousConstSMul.to_continuousConstSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup 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 toTemperedDistributionCLM MeasureTheory.integral instFunLike	—	SeminormedAddCommGroup.toIsTopologicalAddGroup SMulCommClass.complexToReal smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ContinuousLinearMap.comp_apply integralCLM_apply

TemperedDistribution

Definitions

Name	Category	Theorems
delta 📖	CompOp	5 math math: delta_apply, SchwartzMap.delta_apply, fourier_delta_zero, SchwartzMap.integralCLM_dirac_eq_delta, toTemperedDistribution_dirac_eq_delta
derivCLM 📖	CompOp	2 math math: derivCLM_toTemperedDistributionCLM_eq, derivCLM_apply_apply
fourierTransformCLM 📖	CompOp	—
fourierTransformInvCLM 📖	CompOp	—
instFourierTransform 📖	CompOp	13 math math: lineDerivOp_fourier_eq, instFourierAdd, instFourierSMul, instFourierPairInv, instFourierPair, instContinuousFourier, fourier_toTemperedDistributionCLM_eq, fourier_lineDerivOp_eq, fourier_delta_zero, fourierTransform_apply, fourierTransform_toTemperedDistributionCLM_eq, fourier_apply, MeasureTheory.Lp.fourier_toTemperedDistribution_eq
instFourierTransformInv 📖	CompOp	12 math math: fourierInv_toTemperedDistributionCLM_eq, fourierInv_lineDerivOp_eq, instFourierPairInv, instFourierPair, fourierTransformInv_toTemperedDistributionCLM_eq, instFourierInvSMul, instFourierInvAdd, MeasureTheory.Lp.fourierInv_toTemperedDistribution_eq, fourierInv_apply, lineDerivOp_fourierInv_eq, instContinuousFourierInv, fourierTransformInv_apply
instLaplacian 📖	CompOp	4 math math: laplacian_eq_sum, laplacian_toTemperedDistributionCLM_eq, laplacian_apply_apply, laplacianCLM_apply
instLineDeriv 📖	CompOp	14 math math: lineDerivOpCLM_eq, lineDerivOp_fourier_eq, instLineDerivLeftSMulReal, fourierInv_lineDerivOp_eq, instLineDerivSMulReal, fourier_lineDerivOp_eq, lineDerivOp_toTemperedDistributionCLM_eq, laplacian_eq_sum, instContinuousLineDeriv, instLineDerivAdd, instLineDerivSMulComplex, lineDerivOp_apply_apply, lineDerivOp_fourierInv_eq, laplacianCLM_apply
smulLeftCLM 📖	CompOp	14 math math: lineDerivOp_fourier_eq, smulLeftCLM_compL_smulLeftCLM, smulLeftCLM_neg, fourierInv_lineDerivOp_eq, smulLeftCLM_sub, fourier_lineDerivOp_eq, smulLeftCLM_add, smulLeftCLM_smulLeftCLM_apply, lineDerivOp_fourierInv_eq, smulLeftCLM_const, smulLeftCLM_sum, smulLeftCLM_smul, MeasureTheory.Lp.toTemperedDistribution_smul_eq, smulLeftCLM_apply_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
delta_apply 📖	mathematical	—	DFunLike.coe TemperedDistribution Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace SchwartzMap Real Real.instRCLike instInnerProductSpaceRealComplex UniformConvergenceCLM.instFunLike Complex.instNormedField RingHom.id Semiring.toNonAssocSemiring Complex.instSemiring SchwartzMap.instAddCommGroup SchwartzMap.instModule SchwartzMap.instTopologicalSpace NormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace setOf Set Finite Set.Elem delta SchwartzMap.instFunLike	—	—
derivCLM_apply_apply 📖	mathematical	—	DFunLike.coe TemperedDistribution Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal 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 derivCLM SchwartzMap.instNeg DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField 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 NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing SchwartzMap.derivCLM	—	SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul
derivCLM_toTemperedDistributionCLM_eq 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring TemperedDistribution Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal 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 derivCLM NormedSpace.complexToReal SchwartzMap.toTemperedDistributionCLM MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace Real.borelSpace instSecondCountableTopologyReal MeasureTheory.MeasureSpace.volume MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth FiniteDimensional.rclike_to_real instIsAddHaarMeasureVolume Real.measurableSpace DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField 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 NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing SchwartzMap.derivCLM	—	UniformConvergenceCLM.ext SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul Real.borelSpace instSecondCountableTopologyReal MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth FiniteDimensional.rclike_to_real instIsAddHaarMeasureVolume IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SMulCommClass.complexToReal SchwartzMap.toTemperedDistributionCLM_apply_apply neg_smul MeasureTheory.integral_neg SchwartzMap.integral_smul_deriv_right_eq_neg_left
fourierInv_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 FourierTransformInv.fourierInv instFourierTransformInv SchwartzMap.instFourierTransformInv NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing	—	—
fourierInv_lineDerivOp_eq 📖	mathematical	—	FourierTransformInv.fourierInv TemperedDistribution InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instFourierTransformInv LineDeriv.lineDerivOp 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.instNeg Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I DFunLike.coe ContinuousLinearMap UniformConvergenceCLM.instTopologicalSpace AddCommGroup.toAddCommMonoid UniformConvergenceCLM.instModule ContinuousLinearMap.funLike smulLeftCLM Inner.inner InnerProductSpace.toInner	—	UniformConvergenceCLM.ext SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul Nat.instAtLeastTwoHAddOfNat Function.hasTemperateGrowth_inner_left IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Algebra.to_smulCommClass SMulCommClass.complexToReal SchwartzMap.lineDerivOp_fourierInv_eq SchwartzMap.smulLeftCLM_ofReal FourierInvSMul.fourierInv_smul SchwartzMap.instFourierInvSMul map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass UniformConvergenceCLM.instContinuousSemilinearMapClass map_smul SemilinearMapClass.toMulActionSemiHomClass neg_smul smulLeftCLM_apply_apply
fourierInv_toTemperedDistributionCLM_eq 📖	mathematical	—	FourierTransformInv.fourierInv TemperedDistribution InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instFourierTransformInv DFunLike.coe ContinuousLinearMap Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring SchwartzMap NormedSpace.complexToReal SchwartzMap.instTopologicalSpace AddCommGroup.toAddCommMonoid SchwartzMap.instAddCommGroup UniformConvergenceCLM.instTopologicalSpace Complex.instNormedField Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex SchwartzMap.instModule Complex.instRCLike RCLike.innerProductSpace NormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace setOf Set Finite Set.Elem UniformConvergenceCLM.instAddCommGroup UniformConvergenceCLM.instModule ContinuousLinearMap.funLike SchwartzMap.toTemperedDistributionCLM MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace secondCountable_of_proper FiniteDimensional.proper_real MeasureTheory.MeasureSpace.volume MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth instIsAddHaarMeasureVolume SchwartzMap.instFourierTransformInv	—	secondCountable_of_proper FiniteDimensional.proper_real MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth instIsAddHaarMeasureVolume SeminormedAddCommGroup.toIsTopologicalAddGroup SMulCommClass.complexToReal smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul FourierInvPair.fourier_fourierInv_eq SchwartzMap.instFourierInvPair fourier_toTemperedDistributionCLM_eq FourierPair.fourierInv_fourier_eq instFourierPair
fourierTransformCLM_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike FourierTransform.fourierCLM FourierTransform.fourier	—	FourierTransform.fourierCLM_apply
fourierTransformInvCLM_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike FourierTransform.fourierInvCLM FourierTransformInv.fourierInv	—	FourierTransform.fourierInvCLM_apply
fourierTransformInv_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 FourierTransformInv.fourierInv instFourierTransformInv SchwartzMap.instFourierTransformInv NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing	—	fourierInv_apply
fourierTransformInv_toTemperedDistributionCLM_eq 📖	mathematical	—	FourierTransformInv.fourierInv TemperedDistribution InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instFourierTransformInv DFunLike.coe ContinuousLinearMap Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring SchwartzMap NormedSpace.complexToReal SchwartzMap.instTopologicalSpace AddCommGroup.toAddCommMonoid SchwartzMap.instAddCommGroup UniformConvergenceCLM.instTopologicalSpace Complex.instNormedField Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex SchwartzMap.instModule Complex.instRCLike RCLike.innerProductSpace NormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace setOf Set Finite Set.Elem UniformConvergenceCLM.instAddCommGroup UniformConvergenceCLM.instModule ContinuousLinearMap.funLike SchwartzMap.toTemperedDistributionCLM MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace secondCountable_of_proper FiniteDimensional.proper_real MeasureTheory.MeasureSpace.volume MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth instIsAddHaarMeasureVolume SchwartzMap.instFourierTransformInv	—	fourierInv_toTemperedDistributionCLM_eq
fourierTransform_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 FourierTransform.fourier instFourierTransform SchwartzMap.instFourierTransform NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing	—	fourier_apply
fourierTransform_toTemperedDistributionCLM_eq 📖	mathematical	—	FourierTransform.fourier TemperedDistribution InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instFourierTransform DFunLike.coe ContinuousLinearMap Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring SchwartzMap NormedSpace.complexToReal SchwartzMap.instTopologicalSpace AddCommGroup.toAddCommMonoid SchwartzMap.instAddCommGroup UniformConvergenceCLM.instTopologicalSpace Complex.instNormedField Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex SchwartzMap.instModule Complex.instRCLike RCLike.innerProductSpace NormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace setOf Set Finite Set.Elem UniformConvergenceCLM.instAddCommGroup UniformConvergenceCLM.instModule ContinuousLinearMap.funLike SchwartzMap.toTemperedDistributionCLM MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace secondCountable_of_proper FiniteDimensional.proper_real MeasureTheory.MeasureSpace.volume MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth instIsAddHaarMeasureVolume SchwartzMap.instFourierTransform	—	fourier_toTemperedDistributionCLM_eq
fourier_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 FourierTransform.fourier instFourierTransform SchwartzMap.instFourierTransform NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing	—	—
fourier_delta_zero 📖	mathematical	—	FourierTransform.fourier TemperedDistribution Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Complex.instRCLike RCLike.innerProductSpace instFourierTransform delta NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup MeasureTheory.Measure.toTemperedDistribution MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace secondCountable_of_proper SeminormedAddCommGroup.toPseudoMetricSpace FiniteDimensional.proper_real MeasureTheory.MeasureSpace.volume MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth instIsAddHaarMeasureVolume	—	UniformConvergenceCLM.ext secondCountable_of_proper FiniteDimensional.proper_real MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth instIsAddHaarMeasureVolume inner_zero_right neg_zero AddChar.map_zero_eq_one one_smul MeasureTheory.Measure.toTemperedDistribution_apply
fourier_lineDerivOp_eq 📖	mathematical	—	FourierTransform.fourier TemperedDistribution InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instFourierTransform LineDeriv.lineDerivOp 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 smulLeftCLM Inner.inner InnerProductSpace.toInner	—	UniformConvergenceCLM.ext SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul Nat.instAtLeastTwoHAddOfNat Function.hasTemperateGrowth_inner_left IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Algebra.to_smulCommClass SMulCommClass.complexToReal SchwartzMap.lineDerivOp_fourier_eq SchwartzMap.smulLeftCLM_ofReal neg_smul FourierTransform.fourier_neg SchwartzMap.instFourierAdd FourierSMul.fourier_smul SchwartzMap.instFourierSMul neg_neg map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass UniformConvergenceCLM.instContinuousSemilinearMapClass smulLeftCLM_apply_apply
fourier_toTemperedDistributionCLM_eq 📖	mathematical	—	FourierTransform.fourier TemperedDistribution InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instFourierTransform DFunLike.coe ContinuousLinearMap Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring SchwartzMap NormedSpace.complexToReal SchwartzMap.instTopologicalSpace AddCommGroup.toAddCommMonoid SchwartzMap.instAddCommGroup UniformConvergenceCLM.instTopologicalSpace Complex.instNormedField Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex SchwartzMap.instModule Complex.instRCLike RCLike.innerProductSpace NormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace setOf Set Finite Set.Elem UniformConvergenceCLM.instAddCommGroup UniformConvergenceCLM.instModule ContinuousLinearMap.funLike SchwartzMap.toTemperedDistributionCLM MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace secondCountable_of_proper FiniteDimensional.proper_real MeasureTheory.MeasureSpace.volume MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth instIsAddHaarMeasureVolume SchwartzMap.instFourierTransform	—	UniformConvergenceCLM.ext secondCountable_of_proper FiniteDimensional.proper_real MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth instIsAddHaarMeasureVolume SchwartzMap.toTemperedDistributionCLM_apply_apply SchwartzMap.integral_fourier_smul_eq
instContinuousFourier 📖	mathematical	—	ContinuousFourier TemperedDistribution InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup UniformConvergenceCLM.instTopologicalSpace 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 instFourierTransform	—	SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.cont Algebra.to_smulCommClass smulCommClass_self RingHomCompTriple.ids SchwartzMap.instFourierAdd SchwartzMap.instFourierSMul SchwartzMap.instContinuousFourier
instContinuousFourierInv 📖	mathematical	—	ContinuousFourierInv TemperedDistribution InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup UniformConvergenceCLM.instTopologicalSpace 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 instFourierTransformInv	—	SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.cont Algebra.to_smulCommClass smulCommClass_self RingHomCompTriple.ids SchwartzMap.instFourierInvAdd SchwartzMap.instFourierInvSMul SchwartzMap.instContinuousFourierInv
instContinuousLineDeriv 📖	mathematical	—	ContinuousLineDeriv TemperedDistribution UniformConvergenceCLM.instTopologicalSpace Complex Complex.instNormedField RingHom.id Semiring.toNonAssocSemiring Complex.instSemiring SchwartzMap Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup 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 instLineDeriv	—	SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.continuous Algebra.to_smulCommClass smulCommClass_self RingHomCompTriple.ids SchwartzMap.instIsTopologicalAddGroup SchwartzMap.instLineDerivAdd SchwartzMap.instLineDerivSMul SchwartzMap.instContinuousLineDeriv
instFourierAdd 📖	mathematical	—	FourierAdd TemperedDistribution InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid 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 instFourierTransform	—	SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.map_add Algebra.to_smulCommClass smulCommClass_self RingHomCompTriple.ids SchwartzMap.instFourierAdd SchwartzMap.instFourierSMul SchwartzMap.instContinuousFourier
instFourierInvAdd 📖	mathematical	—	FourierInvAdd TemperedDistribution InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid 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 instFourierTransformInv	—	SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.map_add Algebra.to_smulCommClass smulCommClass_self RingHomCompTriple.ids SchwartzMap.instFourierInvAdd SchwartzMap.instFourierInvSMul SchwartzMap.instContinuousFourierInv
instFourierInvSMul 📖	mathematical	—	FourierInvSMul Complex TemperedDistribution InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup 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 instFourierTransformInv	—	SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ContinuousLinearMap.map_smul Algebra.to_smulCommClass RingHomCompTriple.ids SchwartzMap.instFourierInvAdd SchwartzMap.instFourierInvSMul SchwartzMap.instContinuousFourierInv
instFourierPair 📖	mathematical	—	FourierPair TemperedDistribution InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instFourierTransform instFourierTransformInv	—	UniformConvergenceCLM.ext FourierInvPair.fourier_fourierInv_eq SchwartzMap.instFourierInvPair Complex.instCompleteSpace
instFourierPairInv 📖	mathematical	—	FourierInvPair TemperedDistribution InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instFourierTransform instFourierTransformInv	—	UniformConvergenceCLM.ext FourierPair.fourierInv_fourier_eq SchwartzMap.instFourierPair Complex.instCompleteSpace
instFourierSMul 📖	mathematical	—	FourierSMul Complex TemperedDistribution InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup 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 instFourierTransform	—	SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ContinuousLinearMap.map_smul Algebra.to_smulCommClass RingHomCompTriple.ids SchwartzMap.instFourierAdd SchwartzMap.instFourierSMul SchwartzMap.instContinuousFourier
instLineDerivAdd 📖	mathematical	—	LineDerivAdd TemperedDistribution NormedAddCommGroup.toAddCommGroup UniformConvergenceCLM.instAddCommGroup Complex Complex.instNormedField RingHom.id Semiring.toNonAssocSemiring Complex.instSemiring SchwartzMap Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex SchwartzMap.instAddCommGroup SchwartzMap.instModule Complex.instRCLike RCLike.innerProductSpace SchwartzMap.instTopologicalSpace NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toIsTopologicalAddGroup setOf Set Finite Set.Elem instLineDeriv	—	SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.map_add Algebra.to_smulCommClass smulCommClass_self RingHomCompTriple.ids SchwartzMap.instIsTopologicalAddGroup SchwartzMap.instLineDerivAdd SchwartzMap.instLineDerivSMul SchwartzMap.instContinuousLineDeriv UniformConvergenceCLM.ext LineDerivAdd.lineDerivOp_left_add neg_add_rev add_comm map_add SemilinearMapClass.toAddHomClass ContinuousSemilinearMapClass.toSemilinearMapClass UniformConvergenceCLM.instContinuousSemilinearMapClass map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass
instLineDerivLeftSMulReal 📖	mathematical	—	LineDerivLeftSMul Real TemperedDistribution SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup UniformConvergenceCLM.instAddCommGroup Complex Complex.instNormedField RingHom.id Semiring.toNonAssocSemiring Complex.instSemiring SchwartzMap Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike instInnerProductSpaceRealComplex SchwartzMap.instAddCommGroup SchwartzMap.instModule Complex.instRCLike RCLike.innerProductSpace SchwartzMap.instTopologicalSpace NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup setOf Set Finite Set.Elem UniformConvergenceCLM.instDistribMulAction NormedSpace.complexToReal IsScalarTower.to_smulCommClass' Real.instCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NormedAlgebra.toAlgebra SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing RCLike.toNormedAlgebra IsScalarTower.complexToReal Complex.addCommGroup Complex.instModuleSelf AddCommMonoid.toAddMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsScalarTower.left DistribMulAction.toMulAction UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul instLineDeriv	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsScalarTower.to_smulCommClass' IsScalarTower.complexToReal IsScalarTower.left UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul UniformConvergenceCLM.ext smulCommClass_self LineDerivLeftSMul.lineDerivOp_left_smul SchwartzMap.instLineDerivLeftSMulReal map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass UniformConvergenceCLM.instContinuousSemilinearMapClass ContinuousLinearMap.map_smul_of_tower LinearMap.IsScalarTower.compatibleSMul Algebra.to_smulCommClass SchwartzMap.instIsScalarTower IsScalarTower.right smul_neg
instLineDerivSMulComplex 📖	mathematical	—	LineDerivSMul Complex TemperedDistribution 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 InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup 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 instLineDeriv	—	SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ContinuousLinearMap.map_smul Algebra.to_smulCommClass RingHomCompTriple.ids SchwartzMap.instIsTopologicalAddGroup SchwartzMap.instLineDerivAdd SchwartzMap.instLineDerivSMul SchwartzMap.instContinuousLineDeriv
instLineDerivSMulReal 📖	mathematical	—	LineDerivSMul Real TemperedDistribution 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 InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup 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 UniformConvergenceCLM.instDistribMulAction Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.normedField NormedSpace.complexToReal IsScalarTower.to_smulCommClass' Real.instCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NormedAlgebra.toAlgebra SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing RCLike.toNormedAlgebra IsScalarTower.complexToReal Complex.addCommGroup Complex.instModuleSelf AddCommMonoid.toAddMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsScalarTower.left DistribMulAction.toMulAction UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul instLineDeriv	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsScalarTower.to_smulCommClass' IsScalarTower.complexToReal IsScalarTower.left UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ContinuousLinearMap.map_smul_of_tower Algebra.to_smulCommClass smulCommClass_self LinearMap.IsScalarTower.compatibleSMul RingHomCompTriple.ids SchwartzMap.instIsTopologicalAddGroup SchwartzMap.instLineDerivAdd SchwartzMap.instLineDerivSMul SchwartzMap.instContinuousLineDeriv
laplacianCLM_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Complex CommSemiring.toSemiring CommRing.toCommSemiring Complex.commRing RingHom.id Semiring.toNonAssocSemiring TemperedDistribution InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup UniformConvergenceCLM.instTopologicalSpace Complex.instNormedField 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 AddCommGroup.toAddCommMonoid UniformConvergenceCLM.instAddCommGroup UniformConvergenceCLM.instModule smulCommClass_self CommRing.toCommMonoid 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 LineDeriv.laplacianCLM instLineDeriv UniformConvergenceCLM.instIsTopologicalAddGroup instLineDerivAdd instLineDerivSMulComplex instContinuousLineDeriv Laplacian.laplacian instLaplacian	—	SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul UniformConvergenceCLM.instIsTopologicalAddGroup instLineDerivAdd instLineDerivSMulComplex instContinuousLineDeriv ContinuousLinearMap.coe_sum' Finset.sum_congr Finset.sum_apply
laplacian_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 Laplacian.laplacian instLaplacian SchwartzMap.instLaplacian	—	SeminormedAddCommGroup.toIsTopologicalAddGroup laplacian_eq_sum UniformConvergenceCLM.sum_apply Finset.sum_congr map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass UniformConvergenceCLM.instContinuousSemilinearMapClass neg_neg SchwartzMap.laplacian_eq_sum map_sum
laplacian_eq_sum 📖	mathematical	—	Laplacian.laplacian TemperedDistribution InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instLaplacian Finset.sum AddCommGroup.toAddCommMonoid 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 Finset.univ LineDeriv.lineDerivOp instLineDeriv DFunLike.coe OrthonormalBasis OrthonormalBasis.instFunLike	—	LineDeriv.laplacianCLM_eq_sum SeminormedAddCommGroup.toIsTopologicalAddGroup IsScalarTower.to_smulCommClass' IsScalarTower.complexToReal IsScalarTower.left UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul UniformConvergenceCLM.instIsTopologicalAddGroup instLineDerivAdd instLineDerivSMulReal instContinuousLineDeriv instLineDerivLeftSMulReal
laplacian_toTemperedDistributionCLM_eq 📖	mathematical	—	Laplacian.laplacian TemperedDistribution InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instLaplacian DFunLike.coe ContinuousLinearMap Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring SchwartzMap NormedSpace.complexToReal SchwartzMap.instTopologicalSpace AddCommGroup.toAddCommMonoid SchwartzMap.instAddCommGroup UniformConvergenceCLM.instTopologicalSpace Complex.instNormedField Complex.instNormedAddCommGroup instInnerProductSpaceRealComplex SchwartzMap.instModule Complex.instRCLike RCLike.innerProductSpace NormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace setOf Set Finite Set.Elem UniformConvergenceCLM.instAddCommGroup UniformConvergenceCLM.instModule ContinuousLinearMap.funLike SchwartzMap.toTemperedDistributionCLM MeasureTheory.MeasureSpace.toMeasurableSpace measureSpaceOfInnerProductSpace secondCountable_of_proper FiniteDimensional.proper_real MeasureTheory.MeasureSpace.volume MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth instIsAddHaarMeasureVolume SchwartzMap.instLaplacian	—	UniformConvergenceCLM.ext secondCountable_of_proper FiniteDimensional.proper_real MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth instIsAddHaarMeasureVolume laplacian_apply_apply SchwartzMap.toTemperedDistributionCLM_apply_apply SeminormedAddCommGroup.toIsTopologicalAddGroup SMulCommClass.complexToReal smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul SchwartzMap.integral_smul_laplacian_right_eq_left
lineDerivOpCLM_eq 📖	mathematical	—	LineDeriv.lineDerivOpCLM Complex TemperedDistribution Complex.instRing UniformConvergenceCLM.instAddCommGroup Complex.instNormedField RingHom.id Semiring.toNonAssocSemiring Complex.instSemiring SchwartzMap Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup 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 UniformConvergenceCLM.instModule Ring.toSemiring smulCommClass_self CommRing.toCommMonoid Complex.commRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction 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 AddCommGroup.toAddCommMonoid IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul UniformConvergenceCLM.instTopologicalSpace instLineDeriv instLineDerivAdd instLineDerivSMulComplex instContinuousLineDeriv PointwiseConvergenceCLM.precomp RingHomCompTriple.ids DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Algebra.to_smulCommClass Semifield.toCommSemiring Real.normedField SeminormedRing.toRing NormedAlgebra.toAlgebra RCLike.toNormedAlgebra ContinuousLinearMap ContinuousLinearMap.neg SchwartzMap.instIsTopologicalAddGroup SchwartzMap.instLineDeriv SchwartzMap.instLineDerivAdd SchwartzMap.instLineDerivSMul SchwartzMap.instContinuousLineDeriv	—	SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul instLineDerivAdd instLineDerivSMulComplex instContinuousLineDeriv
lineDerivOp_apply_apply 📖	mathematical	—	DFunLike.coe TemperedDistribution SchwartzMap Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup 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 LineDeriv.lineDerivOp instLineDeriv SchwartzMap.instNeg SchwartzMap.instLineDeriv	—	—
lineDerivOp_fourierInv_eq 📖	mathematical	—	LineDeriv.lineDerivOp TemperedDistribution InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instLineDeriv FourierTransformInv.fourierInv instFourierTransformInv 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 smulLeftCLM Inner.inner InnerProductSpace.toInner	—	UniformConvergenceCLM.ext SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul Nat.instAtLeastTwoHAddOfNat Function.hasTemperateGrowth_inner_left IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Algebra.to_smulCommClass FourierTransform.fourierInv_neg SchwartzMap.instFourierInvAdd SMulCommClass.complexToReal SchwartzMap.fourierInv_lineDerivOp_eq SchwartzMap.smulLeftCLM_ofReal neg_smul neg_neg map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass UniformConvergenceCLM.instContinuousSemilinearMapClass FourierInvSMul.fourierInv_smul instFourierInvSMul smulLeftCLM_apply_apply
lineDerivOp_fourier_eq 📖	mathematical	—	LineDeriv.lineDerivOp TemperedDistribution InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instLineDeriv FourierTransform.fourier instFourierTransform 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.instNeg Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I DFunLike.coe ContinuousLinearMap UniformConvergenceCLM.instTopologicalSpace AddCommGroup.toAddCommMonoid UniformConvergenceCLM.instModule ContinuousLinearMap.funLike smulLeftCLM Inner.inner InnerProductSpace.toInner	—	UniformConvergenceCLM.ext SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul Nat.instAtLeastTwoHAddOfNat Function.hasTemperateGrowth_inner_left IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SMulCommClass.complexToReal FourierTransform.fourier_neg SchwartzMap.instFourierAdd SchwartzMap.fourier_lineDerivOp_eq SchwartzMap.smulLeftCLM_ofReal map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass UniformConvergenceCLM.instContinuousSemilinearMapClass map_smul SemilinearMapClass.toMulActionSemiHomClass neg_smul instFourierAdd FourierSMul.fourier_smul instFourierSMul smulLeftCLM_apply_apply
lineDerivOp_toTemperedDistributionCLM_eq 📖	mathematical	—	LineDeriv.lineDerivOp TemperedDistribution instLineDeriv DFunLike.coe ContinuousLinearMap Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring SchwartzMap NormedSpace.complexToReal NormedAddCommGroup.toSeminormedAddCommGroup SchwartzMap.instTopologicalSpace AddCommGroup.toAddCommMonoid SchwartzMap.instAddCommGroup UniformConvergenceCLM.instTopologicalSpace Complex.instNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike instInnerProductSpaceRealComplex SchwartzMap.instModule Complex.instRCLike RCLike.innerProductSpace NormedAddCommGroup.toAddCommGroup NormedSpace.toModule UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toIsTopologicalAddGroup setOf Set Finite Set.Elem UniformConvergenceCLM.instAddCommGroup SMulCommClass.complexToReal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero 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 UniformConvergenceCLM.instModule UniformContinuousConstSMul.to_continuousConstSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup 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 SchwartzMap.toTemperedDistributionCLM MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth SchwartzMap.instLineDeriv	—	UniformConvergenceCLM.ext SeminormedAddCommGroup.toIsTopologicalAddGroup SMulCommClass.complexToReal smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul MeasureTheory.Measure.IsAddHaarMeasure.instHasTemperateGrowth SchwartzMap.toTemperedDistributionCLM_apply_apply neg_smul MeasureTheory.integral_neg SchwartzMap.integral_smul_lineDerivOp_right_eq_neg_left
smulLeftCLM_add 📖	mathematical	Function.HasTemperateGrowth Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex	smulLeftCLM Pi.instAdd Complex.instAdd ContinuousLinearMap Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring TemperedDistribution UniformConvergenceCLM.instTopologicalSpace Complex.instNormedField SchwartzMap 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.add 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 smulLeftCLM_apply_apply SchwartzMap.instIsTopologicalAddGroup SchwartzMap.smulLeftCLM_add map_add SemilinearMapClass.toAddHomClass ContinuousSemilinearMapClass.toSemilinearMapClass UniformConvergenceCLM.instContinuousSemilinearMapClass
smulLeftCLM_apply_apply 📖	mathematical	—	DFunLike.coe TemperedDistribution SchwartzMap Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup 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 smulLeftCLM 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 NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace SchwartzMap.smulLeftCLM	—	SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul
smulLeftCLM_compL_smulLeftCLM 📖	mathematical	Function.HasTemperateGrowth Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex	ContinuousLinearMap.comp Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring TemperedDistribution UniformConvergenceCLM.instTopologicalSpace Complex.instNormedField SchwartzMap 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 smulLeftCLM Pi.instMul Complex.instMul	—	ContinuousLinearMap.ext SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomCompTriple.ids smulLeftCLM_smulLeftCLM_apply
smulLeftCLM_const 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring TemperedDistribution UniformConvergenceCLM.instTopologicalSpace Complex.instNormedField SchwartzMap Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup 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 smulLeftCLM UniformConvergenceCLM.instDistribMulAction	—	UniformConvergenceCLM.ext SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace smulLeftCLM_apply_apply SchwartzMap.instSMulCommClass ContinuousSMul.continuousConstSMul SchwartzMap.instContinuousSMul SchwartzMap.smulLeftCLM_const map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass UniformConvergenceCLM.instContinuousSemilinearMapClass
smulLeftCLM_neg 📖	mathematical	Function.HasTemperateGrowth Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex	smulLeftCLM Pi.instNeg Complex.instNeg ContinuousLinearMap Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring TemperedDistribution UniformConvergenceCLM.instTopologicalSpace Complex.instNormedField SchwartzMap 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.neg Complex.instRing UniformConvergenceCLM.instIsTopologicalAddGroup	—	ContinuousLinearMap.ext SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul UniformConvergenceCLM.instIsTopologicalAddGroup UniformConvergenceCLM.ext IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace smulLeftCLM_apply_apply SchwartzMap.instIsTopologicalAddGroup SchwartzMap.smulLeftCLM_neg map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass UniformConvergenceCLM.instContinuousSemilinearMapClass
smulLeftCLM_smul 📖	mathematical	Function.HasTemperateGrowth Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex	smulLeftCLM Function.hasSMul Algebra.toSMul Complex.instCommSemiring CommSemiring.toSemiring Algebra.id ContinuousLinearMap Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring TemperedDistribution UniformConvergenceCLM.instTopologicalSpace Complex.instNormedField SchwartzMap 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 UniformConvergenceCLM.ext IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace smulLeftCLM_apply_apply SchwartzMap.instSMulCommClass ContinuousSMul.continuousConstSMul SchwartzMap.instContinuousSMul SchwartzMap.smulLeftCLM_smul map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass UniformConvergenceCLM.instContinuousSemilinearMapClass
smulLeftCLM_smulLeftCLM_apply 📖	mathematical	Function.HasTemperateGrowth Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex	DFunLike.coe ContinuousLinearMap Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring TemperedDistribution UniformConvergenceCLM.instTopologicalSpace Complex.instNormedField SchwartzMap 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 smulLeftCLM Pi.instMul Complex.instMul	—	UniformConvergenceCLM.ext SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace smulLeftCLM_apply_apply SchwartzMap.smulLeftCLM_smulLeftCLM_apply
smulLeftCLM_sub 📖	mathematical	Function.HasTemperateGrowth Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex	smulLeftCLM Pi.instSub Complex.instSub ContinuousLinearMap Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring TemperedDistribution UniformConvergenceCLM.instTopologicalSpace Complex.instNormedField SchwartzMap 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.sub Complex.instRing UniformConvergenceCLM.instIsTopologicalAddGroup	—	ContinuousLinearMap.ext SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul UniformConvergenceCLM.instIsTopologicalAddGroup UniformConvergenceCLM.ext IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace smulLeftCLM_apply_apply SchwartzMap.instIsTopologicalAddGroup SchwartzMap.smulLeftCLM_sub map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass UniformConvergenceCLM.instContinuousSemilinearMapClass
smulLeftCLM_sum 📖	mathematical	Function.HasTemperateGrowth Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex	smulLeftCLM Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring TemperedDistribution UniformConvergenceCLM.instTopologicalSpace SchwartzMap 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 smulLeftCLM_apply_apply SchwartzMap.instIsTopologicalAddGroup SchwartzMap.smulLeftCLM_sum ContinuousLinearMap.coe_sum' Finset.sum_apply map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass UniformConvergenceCLM.instContinuousSemilinearMapClass UniformConvergenceCLM.sum_apply Finset.sum_congr
toTemperedDistribution_dirac_eq_delta 📖	mathematical	—	MeasureTheory.Measure.toTemperedDistribution MeasureTheory.Measure.dirac MeasureTheory.IsFiniteMeasure.instHasTemperateGrowth MeasureTheory.Measure.dirac.instIsFiniteMeasure delta	—	UniformConvergenceCLM.ext MeasureTheory.IsFiniteMeasure.instHasTemperateGrowth MeasureTheory.Measure.dirac.instIsFiniteMeasure MeasureTheory.Measure.toTemperedDistribution_apply MeasureTheory.integral_dirac Complex.instCompleteSpace instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace

(root)

Definitions

Name	Category	Theorems
TemperedDistribution 📖	CompOp	57 math math: TemperedDistribution.lineDerivOpCLM_eq, MeasureTheory.Lp.toTemperedDistributionCLM_apply, TemperedDistribution.fourierInv_toTemperedDistributionCLM_eq, TemperedDistribution.lineDerivOp_fourier_eq, TemperedDistribution.smulLeftCLM_compL_smulLeftCLM, TemperedDistribution.smulLeftCLM_neg, Function.HasTemperateGrowth.toTemperedDistribution_apply, TemperedDistribution.instLineDerivLeftSMulReal, TemperedDistribution.fourierInv_lineDerivOp_eq, TemperedDistribution.instFourierAdd, TemperedDistribution.instFourierSMul, TemperedDistribution.instFourierPairInv, TemperedDistribution.instFourierPair, TemperedDistribution.delta_apply, TemperedDistribution.instContinuousFourier, SchwartzMap.delta_apply, TemperedDistribution.fourier_toTemperedDistributionCLM_eq, TemperedDistribution.fourierTransformInv_toTemperedDistributionCLM_eq, SchwartzMap.toTemperedDistributionCLM_apply_apply, TemperedDistribution.smulLeftCLM_sub, TemperedDistribution.instLineDerivSMulReal, MeasureTheory.Measure.toTemperedDistribution_apply, TemperedDistribution.fourier_lineDerivOp_eq, TemperedDistribution.fourier_delta_zero, TemperedDistribution.lineDerivOp_toTemperedDistributionCLM_eq, TemperedDistribution.laplacian_eq_sum, TemperedDistribution.instContinuousLineDeriv, TemperedDistribution.smulLeftCLM_add, TemperedDistribution.fourierTransform_apply, TemperedDistribution.instFourierInvSMul, TemperedDistribution.instFourierInvAdd, MeasureTheory.Lp.fourierInv_toTemperedDistribution_eq, TemperedDistribution.fourierInv_apply, TemperedDistribution.fourierTransform_toTemperedDistributionCLM_eq, TemperedDistribution.instLineDerivAdd, TemperedDistribution.instLineDerivSMulComplex, TemperedDistribution.laplacian_toTemperedDistributionCLM_eq, TemperedDistribution.derivCLM_toTemperedDistributionCLM_eq, MeasureTheory.Lp.ker_toTemperedDistributionCLM_eq_bot, MeasureTheory.Lp.toTemperedDistribution_toLp_eq, TemperedDistribution.laplacian_apply_apply, TemperedDistribution.smulLeftCLM_smulLeftCLM_apply, TemperedDistribution.lineDerivOp_apply_apply, TemperedDistribution.lineDerivOp_fourierInv_eq, MeasureTheory.Lp.toTemperedDistribution_apply, TemperedDistribution.smulLeftCLM_const, TemperedDistribution.smulLeftCLM_sum, TemperedDistribution.instContinuousFourierInv, TemperedDistribution.fourier_apply, SchwartzMap.coe_apply, TemperedDistribution.smulLeftCLM_smul, TemperedDistribution.derivCLM_apply_apply, TemperedDistribution.fourierTransformInv_apply, MeasureTheory.Lp.fourier_toTemperedDistribution_eq, TemperedDistribution.laplacianCLM_apply, MeasureTheory.Lp.toTemperedDistribution_smul_eq, TemperedDistribution.smulLeftCLM_apply_apply

---

← Back to Index