Basic

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

Statistics

Metric	Count
Definitions toSchwartzMap, SchwartzMap, bilinLeftCLM, coeHom, compCLM, compCLMOfAntilipschitz, compCLMOfContinuousLinearEquiv, evalCLM, instAdd, instAddCommGroup, instFunLike, instInhabited, instModule, instNSMul, instNeg, instSMul, instSub, instTopologicalSpace, instUniformSpace, instZSMul, instZero, integralCLM, mkCLM, mkCLMtoNormedSpace, mkLM, pairing, seminorm, smulLeftCLM, smulRightCLM, toBoundedContinuousFunction, toBoundedContinuousFunctionCLM, toContinuousMap, toFun, toLp, toLpCLM, toZeroAtInfty, toZeroAtInftyCLM, «term𝓢(_,_)»»), schwartzSeminormFamily	39
Theorems toSchwartzMap_toFun, add_apply, bilinLeftCLM_apply, coeFn_toLp, coeFn_zero, coeHom_injective, coe_coeHom, coe_zero, compCLMOfAntilipschitz_apply, compCLMOfContinuousLinearEquiv_apply, compCLM_apply, contDiffAt, continuous, continuous_toLp, decay, decay', denseRange_toLpCLM, differentiable, differentiableAt, eLpNorm_le_seminorm, eLpNorm_lt_top, evalCLM_apply_apply, ext, ext_iff, hasTemperateGrowth, injective_toLp, inner_toL2_toL2_eq, instBoundedContinuousMapClass, instContinuousMapClass, instContinuousSMul, instFirstCountableTopology, instIsScalarTower, instIsTopologicalAddGroup, instIsUniformAddGroup, instLocallyConvexSpace, instSMulCommClass, instZeroAtInftyContinuousMapClass, integrable, integrable_pow_mul, integrable_pow_mul_iteratedFDeriv, integralCLM_apply, integral_pow_mul_iteratedFDeriv_le, isBigO_cocompact_rpow, isBigO_cocompact_zpow, isBigO_cocompact_zpow_neg_nat, le_seminorm, le_seminorm', memLp, memLp_top, neg_apply, norm_iteratedFDeriv_le_seminorm, norm_le_seminorm, norm_pow_mul_le_seminorm, norm_toLp, norm_toLp_le_seminorm, one_add_le_sup_seminorm_apply, pairing_apply, pairing_apply_apply, pairing_continuous_left, schwartzSeminormFamily_apply, schwartzSeminormFamily_apply_zero, seminorm_apply, seminorm_le_bound, seminorm_le_bound', smooth, smooth', smulLeftCLM_add, smulLeftCLM_apply, smulLeftCLM_apply_apply, smulLeftCLM_compCLMOfContinuousLinearEquiv, smulLeftCLM_compL_smulLeftCLM, smulLeftCLM_const, smulLeftCLM_fun_neg, smulLeftCLM_neg, smulLeftCLM_ofReal, smulLeftCLM_real_smul, smulLeftCLM_smul, smulLeftCLM_smulLeftCLM_apply, smulLeftCLM_sub, smulLeftCLM_sum, smulRightCLM_apply_apply, smul_apply, sub_apply, sum_apply, tendsto_cocompact, toBoundedContinuousFunctionCLM_apply, toBoundedContinuousFunction_apply, toLpCLM_apply, toZeroAtInftyCLM_apply, toZeroAtInfty_apply, toZeroAtInfty_toBCF, tsupport_smulLeftCLM_subset, zero_apply, schwartz_withSeminorms	94
Total	133

HasCompactSupport

Definitions

Name	Category	Theorems
toSchwartzMap 📖	CompOp	1 math math: toSchwartzMap_toFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toSchwartzMap_toFun 📖	mathematical	HasCompactSupport UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup ContDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField WithTop.some ENat Top.top instTopENat	DFunLike.coe SchwartzMap SchwartzMap.instFunLike toSchwartzMap	—	—

SchwartzMap

Definitions

Name	Category	Theorems
bilinLeftCLM 📖	CompOp	1 math math: bilinLeftCLM_apply
coeHom 📖	CompOp	2 math math: coeHom_injective, coe_coeHom
compCLM 📖	CompOp	1 math math: compCLM_apply
compCLMOfAntilipschitz 📖	CompOp	1 math math: compCLMOfAntilipschitz_apply
compCLMOfContinuousLinearEquiv 📖	CompOp	4 math math: compCLMOfContinuousLinearEquiv_apply, smulLeftCLM_compCLMOfContinuousLinearEquiv, lineDerivOp_compCLMOfContinuousLinearEquiv, fourierInv_apply_eq
evalCLM 📖	CompOp	3 math math: lineDerivOpCLM_eq, fourier_evalCLM_eq, evalCLM_apply_apply
instAdd 📖	CompOp	3 math math: add_apply, instFourierInvAdd, instFourierAdd
instAddCommGroup 📖	CompOp	124 math math: norm_toLp_le_seminorm, TemperedDistribution.lineDerivOpCLM_eq, schwartz_withSeminorms, MeasureTheory.Lp.toTemperedDistributionCLM_apply, TemperedDistribution.fourierInv_toTemperedDistributionCLM_eq, lineDerivOpCLM_eq, norm_le_seminorm, pairing_apply_apply, seminorm_le_bound, lineDerivOp_fourier_eq, TemperedDistribution.lineDerivOp_fourier_eq, bilinLeftCLM_apply, TemperedDistribution.smulLeftCLM_compL_smulLeftCLM, laplacianCLM_eq, fderivCLM_apply, instLineDerivAdd, toLpCLM_apply, compCLMOfContinuousLinearEquiv_apply, TemperedDistribution.smulLeftCLM_neg, Function.HasTemperateGrowth.toTemperedDistribution_apply, fourier_lineDerivOp_eq, TemperedDistribution.instLineDerivLeftSMulReal, smulLeftCLM_compCLMOfContinuousLinearEquiv, TemperedDistribution.fourierInv_lineDerivOp_eq, smulLeftCLM_real_smul, TemperedDistribution.instFourierAdd, TemperedDistribution.instFourierSMul, TemperedDistribution.delta_apply, laplacianCLM_eq', TemperedDistribution.instContinuousFourier, smulLeftCLM_sum, toBoundedContinuousFunctionCLM_apply, delta_apply, smulLeftCLM_fun_neg, pairing_apply, lineDerivOp_compCLMOfContinuousLinearEquiv, norm_iteratedFDeriv_le_seminorm, seminorm_le_bound', TemperedDistribution.fourier_toTemperedDistributionCLM_eq, convolution_apply, TemperedDistribution.fourierTransformInv_toTemperedDistributionCLM_eq, compCLMOfAntilipschitz_apply, fourierInv_apply_eq, smulRightCLM_apply_apply, toTemperedDistributionCLM_apply_apply, TemperedDistribution.smulLeftCLM_sub, smulLeftCLM_const, coeHom_injective, fourierInv_lineDerivOp_eq, smulLeftCLM_smulLeftCLM_apply, fourier_evalCLM_eq, TemperedDistribution.instLineDerivSMulReal, evalCLM_apply_apply, MeasureTheory.Measure.toTemperedDistribution_apply, TemperedDistribution.fourier_lineDerivOp_eq, integral_pow_mul_iteratedFDeriv_le, TemperedDistribution.lineDerivOp_toTemperedDistributionCLM_eq, smulLeftCLM_add, TemperedDistribution.laplacian_eq_sum, TemperedDistribution.instContinuousLineDeriv, le_seminorm, eLpNorm_le_seminorm, TemperedDistribution.smulLeftCLM_add, TemperedDistribution.fourierTransform_apply, tsupport_smulLeftCLM_subset, tsupport_fderivCLM_subset, smulLeftCLM_neg, convolution_continuous_left, pairing_continuous_left, integralCLM_apply, lineDerivOp_fourierInv_eq, sum_apply, instLocallyConvexSpace, compCLM_apply, coe_coeHom, TemperedDistribution.instFourierInvSMul, TemperedDistribution.instFourierInvAdd, TemperedDistribution.fourierInv_apply, fourierTransformCLM_apply, TemperedDistribution.fourierTransform_toTemperedDistributionCLM_eq, fderivCLM_fourier_eq, TemperedDistribution.instLineDerivAdd, derivCLM_apply, TemperedDistribution.instLineDerivSMulComplex, TemperedDistribution.laplacian_toTemperedDistributionCLM_eq, convolution_flip, laplacian_eq_sum, TemperedDistribution.derivCLM_toTemperedDistributionCLM_eq, MeasureTheory.Lp.ker_toTemperedDistributionCLM_eq_bot, seminorm_apply, MeasureTheory.Lp.toTemperedDistribution_toLp_eq, TemperedDistribution.laplacian_apply_apply, TemperedDistribution.smulLeftCLM_smulLeftCLM_apply, tsupport_derivCLM_subset, le_seminorm', TemperedDistribution.lineDerivOp_apply_apply, TemperedDistribution.lineDerivOp_fourierInv_eq, MeasureTheory.Lp.toTemperedDistribution_apply, smulLeftCLM_sub, TemperedDistribution.smulLeftCLM_const, smulLeftCLM_apply_apply, fourier_fderivCLM_eq, fourier_convolution_apply, TemperedDistribution.smulLeftCLM_sum, TemperedDistribution.instContinuousFourierInv, TemperedDistribution.fourier_apply, coe_apply, smulLeftCLM_ofReal, TemperedDistribution.smulLeftCLM_smul, smulLeftCLM_apply, smulLeftCLM_compL_smulLeftCLM, TemperedDistribution.derivCLM_apply_apply, instIsTopologicalAddGroup, TemperedDistribution.fourierTransformInv_apply, fourier_convolution, one_add_le_sup_seminorm_apply, denseRange_toLpCLM, toZeroAtInftyCLM_apply, TemperedDistribution.laplacianCLM_apply, smulLeftCLM_smul, MeasureTheory.Lp.toTemperedDistribution_smul_eq, TemperedDistribution.smulLeftCLM_apply_apply, norm_pow_mul_le_seminorm, instIsUniformAddGroup
instFunLike 📖	CompOp	108 math math: neg_apply, integral_sesq_fourier_fourier, coe_zero, norm_le_seminorm, add_apply, sub_apply, pairing_apply_apply, coeFn_zero, integral_clm_comp_lineDerivOp_right_eq_neg_left, integral_bilin_fourierInv_eq, bilinLeftCLM_apply, fderivCLM_apply, compCLMOfContinuousLinearEquiv_apply, integral_fourierInv_smul_eq, inner_toL2_toL2_eq, integral_bilin_fourierIntegral_eq, eLpNorm_lt_top, Function.HasTemperateGrowth.toTemperedDistribution_apply, integral_sesq_fourier_eq, memLp, integral_norm_sq_fourier, differentiable, TemperedDistribution.delta_apply, continuous, toBoundedContinuousFunctionCLM_apply, delta_apply, pairing_apply, integral_bilinear_deriv_right_eq_neg_left, norm_iteratedFDeriv_le_seminorm, integral_mul_laplacian_right_eq_left, convolution_apply, integral_bilin_fourier_eq, zero_apply, compCLMOfAntilipschitz_apply, tsupport_lineDerivOp_subset, smulRightCLM_apply_apply, toTemperedDistributionCLM_apply_apply, coeFn_toLp, norm_toLp, toBoundedContinuousFunction_apply, contDiffAt, hasFDerivAt, evalCLM_apply_apply, MeasureTheory.Measure.toTemperedDistribution_apply, tsupport_iteratedLineDerivOp_subset, integral_pow_mul_iteratedFDeriv_le, instContinuousMapClass, tendsto_cocompact, instBoundedContinuousMapClass, integral_sesq_fourierIntegral_eq, integral_bilinear_laplacian_right_eq_left, ext_iff, le_seminorm, eLpNorm_le_seminorm, hasDerivAt, tsupport_smulLeftCLM_subset, tsupport_fderivCLM_subset, iteratedPDeriv_eq_iteratedFDeriv, integral_fourier_mul_eq, integralCLM_apply, fourier_coe, iteratedLineDerivOp_eq_iteratedFDeriv, sum_apply, fourierInv_coe, integral_smul_lineDerivOp_right_eq_neg_left, compCLM_apply, coe_coeHom, integral_mul_deriv_eq_neg_deriv_mul, derivCLM_apply, isBigO_cocompact_zpow_neg_nat, integral_clm_comp_deriv_right_eq_neg_left, memLp_top, smul_apply, integral_fourierInv_mul_eq, instZeroAtInftyContinuousMapClass, decay, lineDerivOp_apply_eq_fderiv, integral_fourier_smul_eq, integral_bilinear_lineDerivOp_right_eq_neg_left, tsupport_derivCLM_subset, integral_smul_laplacian_right_eq_left, le_seminorm', integral_inner_fourier_fourier, MeasureTheory.Lp.toTemperedDistribution_apply, smulLeftCLM_apply_apply, fourier_convolution_apply, integrable, lineDerivOp_apply, coe_apply, integrable_pow_mul, isBigO_cocompact_zpow, smulLeftCLM_apply, tsum_eq_tsum_fourierIntegral, toZeroAtInfty_apply, integral_clm_comp_laplacian_right_eq_left, differentiableAt, integral_smul_deriv_right_eq_neg_left, one_add_le_sup_seminorm_apply, smooth, toZeroAtInftyCLM_apply, integrable_pow_mul_iteratedFDeriv, laplacian_apply, hasTemperateGrowth, HasCompactSupport.toSchwartzMap_toFun, integral_mul_lineDerivOp_right_eq_neg_left, isBigO_cocompact_rpow, norm_pow_mul_le_seminorm, tsum_eq_tsum_fourier
instInhabited 📖	CompOp	—
instModule 📖	CompOp	108 math math: norm_toLp_le_seminorm, TemperedDistribution.lineDerivOpCLM_eq, schwartz_withSeminorms, MeasureTheory.Lp.toTemperedDistributionCLM_apply, TemperedDistribution.fourierInv_toTemperedDistributionCLM_eq, lineDerivOpCLM_eq, pairing_apply_apply, lineDerivOp_fourier_eq, TemperedDistribution.lineDerivOp_fourier_eq, bilinLeftCLM_apply, TemperedDistribution.smulLeftCLM_compL_smulLeftCLM, laplacianCLM_eq, fderivCLM_apply, toLpCLM_apply, compCLMOfContinuousLinearEquiv_apply, TemperedDistribution.smulLeftCLM_neg, Function.HasTemperateGrowth.toTemperedDistribution_apply, fourier_lineDerivOp_eq, TemperedDistribution.instLineDerivLeftSMulReal, smulLeftCLM_compCLMOfContinuousLinearEquiv, TemperedDistribution.fourierInv_lineDerivOp_eq, smulLeftCLM_real_smul, TemperedDistribution.instFourierAdd, TemperedDistribution.instFourierSMul, TemperedDistribution.delta_apply, laplacianCLM_eq', TemperedDistribution.instContinuousFourier, smulLeftCLM_sum, toBoundedContinuousFunctionCLM_apply, delta_apply, smulLeftCLM_fun_neg, pairing_apply, lineDerivOp_compCLMOfContinuousLinearEquiv, TemperedDistribution.fourier_toTemperedDistributionCLM_eq, convolution_apply, TemperedDistribution.fourierTransformInv_toTemperedDistributionCLM_eq, compCLMOfAntilipschitz_apply, fourierInv_apply_eq, smulRightCLM_apply_apply, toTemperedDistributionCLM_apply_apply, TemperedDistribution.smulLeftCLM_sub, smulLeftCLM_const, fourierInv_lineDerivOp_eq, smulLeftCLM_smulLeftCLM_apply, fourier_evalCLM_eq, TemperedDistribution.instLineDerivSMulReal, evalCLM_apply_apply, MeasureTheory.Measure.toTemperedDistribution_apply, TemperedDistribution.fourier_lineDerivOp_eq, TemperedDistribution.lineDerivOp_toTemperedDistributionCLM_eq, smulLeftCLM_add, TemperedDistribution.laplacian_eq_sum, TemperedDistribution.instContinuousLineDeriv, eLpNorm_le_seminorm, TemperedDistribution.smulLeftCLM_add, TemperedDistribution.fourierTransform_apply, tsupport_smulLeftCLM_subset, tsupport_fderivCLM_subset, smulLeftCLM_neg, convolution_continuous_left, pairing_continuous_left, integralCLM_apply, lineDerivOp_fourierInv_eq, instLocallyConvexSpace, compCLM_apply, TemperedDistribution.instFourierInvSMul, TemperedDistribution.instFourierInvAdd, TemperedDistribution.fourierInv_apply, fourierTransformCLM_apply, TemperedDistribution.fourierTransform_toTemperedDistributionCLM_eq, fderivCLM_fourier_eq, TemperedDistribution.instLineDerivAdd, derivCLM_apply, TemperedDistribution.instLineDerivSMulComplex, TemperedDistribution.laplacian_toTemperedDistributionCLM_eq, convolution_flip, TemperedDistribution.derivCLM_toTemperedDistributionCLM_eq, MeasureTheory.Lp.ker_toTemperedDistributionCLM_eq_bot, MeasureTheory.Lp.toTemperedDistribution_toLp_eq, TemperedDistribution.laplacian_apply_apply, TemperedDistribution.smulLeftCLM_smulLeftCLM_apply, tsupport_derivCLM_subset, TemperedDistribution.lineDerivOp_apply_apply, TemperedDistribution.lineDerivOp_fourierInv_eq, MeasureTheory.Lp.toTemperedDistribution_apply, smulLeftCLM_sub, TemperedDistribution.smulLeftCLM_const, smulLeftCLM_apply_apply, fourier_fderivCLM_eq, fourier_convolution_apply, TemperedDistribution.smulLeftCLM_sum, TemperedDistribution.instContinuousFourierInv, TemperedDistribution.fourier_apply, coe_apply, smulLeftCLM_ofReal, TemperedDistribution.smulLeftCLM_smul, smulLeftCLM_apply, smulLeftCLM_compL_smulLeftCLM, TemperedDistribution.derivCLM_apply_apply, TemperedDistribution.fourierTransformInv_apply, fourier_convolution, one_add_le_sup_seminorm_apply, denseRange_toLpCLM, toZeroAtInftyCLM_apply, TemperedDistribution.laplacianCLM_apply, smulLeftCLM_smul, MeasureTheory.Lp.toTemperedDistribution_smul_eq, TemperedDistribution.smulLeftCLM_apply_apply
instNSMul 📖	CompOp	—
instNeg 📖	CompOp	3 math math: neg_apply, TemperedDistribution.lineDerivOp_apply_apply, TemperedDistribution.derivCLM_apply_apply
instSMul 📖	CompOp	24 math math: instLineDerivLeftSMulReal, norm_le_seminorm, seminorm_le_bound, lineDerivOp_fourier_eq, instContinuousSMul, fourier_lineDerivOp_eq, norm_iteratedFDeriv_le_seminorm, seminorm_le_bound', instLineDerivSMul, fourierInv_lineDerivOp_eq, integral_pow_mul_iteratedFDeriv_le, le_seminorm, lineDerivOp_fourierInv_eq, instFourierSMul, fderivCLM_fourier_eq, smul_apply, seminorm_apply, le_seminorm', fourier_fderivCLM_eq, instFourierInvSMul, instSMulCommClass, instIsScalarTower, one_add_le_sup_seminorm_apply, norm_pow_mul_le_seminorm
instSub 📖	CompOp	1 math math: sub_apply
instTopologicalSpace 📖	CompOp	112 math math: TemperedDistribution.lineDerivOpCLM_eq, schwartz_withSeminorms, MeasureTheory.Lp.toTemperedDistributionCLM_apply, TemperedDistribution.fourierInv_toTemperedDistributionCLM_eq, lineDerivOpCLM_eq, pairing_apply_apply, lineDerivOp_fourier_eq, instContinuousSMul, TemperedDistribution.lineDerivOp_fourier_eq, bilinLeftCLM_apply, TemperedDistribution.smulLeftCLM_compL_smulLeftCLM, laplacianCLM_eq, fderivCLM_apply, toLpCLM_apply, compCLMOfContinuousLinearEquiv_apply, TemperedDistribution.smulLeftCLM_neg, Function.HasTemperateGrowth.toTemperedDistribution_apply, fourier_lineDerivOp_eq, TemperedDistribution.instLineDerivLeftSMulReal, smulLeftCLM_compCLMOfContinuousLinearEquiv, TemperedDistribution.fourierInv_lineDerivOp_eq, smulLeftCLM_real_smul, TemperedDistribution.instFourierAdd, TemperedDistribution.instFourierSMul, TemperedDistribution.delta_apply, laplacianCLM_eq', TemperedDistribution.instContinuousFourier, smulLeftCLM_sum, toBoundedContinuousFunctionCLM_apply, instFirstCountableTopology, delta_apply, smulLeftCLM_fun_neg, pairing_apply, lineDerivOp_compCLMOfContinuousLinearEquiv, TemperedDistribution.fourier_toTemperedDistributionCLM_eq, convolution_apply, TemperedDistribution.fourierTransformInv_toTemperedDistributionCLM_eq, compCLMOfAntilipschitz_apply, fourierInv_apply_eq, smulRightCLM_apply_apply, toTemperedDistributionCLM_apply_apply, TemperedDistribution.smulLeftCLM_sub, smulLeftCLM_const, fourierInv_lineDerivOp_eq, smulLeftCLM_smulLeftCLM_apply, fourier_evalCLM_eq, TemperedDistribution.instLineDerivSMulReal, evalCLM_apply_apply, MeasureTheory.Measure.toTemperedDistribution_apply, instContinuousFourierInv, TemperedDistribution.fourier_lineDerivOp_eq, TemperedDistribution.lineDerivOp_toTemperedDistributionCLM_eq, smulLeftCLM_add, TemperedDistribution.laplacian_eq_sum, TemperedDistribution.instContinuousLineDeriv, TemperedDistribution.smulLeftCLM_add, TemperedDistribution.fourierTransform_apply, tsupport_smulLeftCLM_subset, tsupport_fderivCLM_subset, smulLeftCLM_neg, convolution_continuous_left, pairing_continuous_left, integralCLM_apply, lineDerivOp_fourierInv_eq, instLocallyConvexSpace, compCLM_apply, continuous_toLp, TemperedDistribution.instFourierInvSMul, TemperedDistribution.instFourierInvAdd, TemperedDistribution.fourierInv_apply, fourierTransformCLM_apply, TemperedDistribution.fourierTransform_toTemperedDistributionCLM_eq, fderivCLM_fourier_eq, TemperedDistribution.instLineDerivAdd, derivCLM_apply, TemperedDistribution.instLineDerivSMulComplex, TemperedDistribution.laplacian_toTemperedDistributionCLM_eq, convolution_flip, TemperedDistribution.derivCLM_toTemperedDistributionCLM_eq, MeasureTheory.Lp.ker_toTemperedDistributionCLM_eq_bot, MeasureTheory.Lp.toTemperedDistribution_toLp_eq, TemperedDistribution.laplacian_apply_apply, TemperedDistribution.smulLeftCLM_smulLeftCLM_apply, tsupport_derivCLM_subset, TemperedDistribution.lineDerivOp_apply_apply, TemperedDistribution.lineDerivOp_fourierInv_eq, MeasureTheory.Lp.toTemperedDistribution_apply, smulLeftCLM_sub, TemperedDistribution.smulLeftCLM_const, smulLeftCLM_apply_apply, fourier_fderivCLM_eq, fourier_convolution_apply, instContinuousFourier, TemperedDistribution.smulLeftCLM_sum, TemperedDistribution.instContinuousFourierInv, TemperedDistribution.fourier_apply, coe_apply, smulLeftCLM_ofReal, TemperedDistribution.smulLeftCLM_smul, smulLeftCLM_apply, smulLeftCLM_compL_smulLeftCLM, TemperedDistribution.derivCLM_apply_apply, instIsTopologicalAddGroup, TemperedDistribution.fourierTransformInv_apply, instContinuousLineDeriv, fourier_convolution, denseRange_toLpCLM, toZeroAtInftyCLM_apply, TemperedDistribution.laplacianCLM_apply, smulLeftCLM_smul, MeasureTheory.Lp.toTemperedDistribution_smul_eq, TemperedDistribution.smulLeftCLM_apply_apply
instUniformSpace 📖	CompOp	1 math math: instIsUniformAddGroup
instZSMul 📖	CompOp	—
instZero 📖	CompOp	3 math math: coe_zero, coeFn_zero, zero_apply
integralCLM 📖	CompOp	1 math math: integralCLM_apply
mkCLM 📖	CompOp	—
mkCLMtoNormedSpace 📖	CompOp	—
mkLM 📖	CompOp	—
pairing 📖	CompOp	4 math math: pairing_apply_apply, pairing_apply, pairing_continuous_left, fourier_convolution
seminorm 📖	CompOp	12 math math: norm_le_seminorm, seminorm_le_bound, norm_iteratedFDeriv_le_seminorm, seminorm_le_bound', integral_pow_mul_iteratedFDeriv_le, le_seminorm, schwartzSeminormFamily_apply_zero, seminorm_apply, le_seminorm', schwartzSeminormFamily_apply, one_add_le_sup_seminorm_apply, norm_pow_mul_le_seminorm
smulLeftCLM 📖	CompOp	20 math math: lineDerivOp_fourier_eq, fourier_lineDerivOp_eq, smulLeftCLM_compCLMOfContinuousLinearEquiv, smulLeftCLM_real_smul, smulLeftCLM_sum, smulLeftCLM_fun_neg, smulLeftCLM_const, fourierInv_lineDerivOp_eq, smulLeftCLM_smulLeftCLM_apply, smulLeftCLM_add, tsupport_smulLeftCLM_subset, smulLeftCLM_neg, lineDerivOp_fourierInv_eq, smulLeftCLM_sub, smulLeftCLM_apply_apply, smulLeftCLM_ofReal, smulLeftCLM_apply, smulLeftCLM_compL_smulLeftCLM, smulLeftCLM_smul, TemperedDistribution.smulLeftCLM_apply_apply
smulRightCLM 📖	CompOp	3 math math: smulRightCLM_apply_apply, fderivCLM_fourier_eq, fourier_fderivCLM_eq
toBoundedContinuousFunction 📖	CompOp	2 math math: toBoundedContinuousFunction_apply, toZeroAtInfty_toBCF
toBoundedContinuousFunctionCLM 📖	CompOp	1 math math: toBoundedContinuousFunctionCLM_apply
toContinuousMap 📖	CompOp	—
toFun 📖	CompOp	2 math math: decay', smooth'
toLp 📖	CompOp	16 math math: norm_toLp_le_seminorm, inner_fourier_toL2_eq, toLp_fourierTransformInv_eq, toLpCLM_apply, inner_toL2_toL2_eq, toLp_fourierInv_eq, injective_toLp, norm_fourier_toL2_eq, norm_fourierTransformCLM_toL2_eq, coeFn_toLp, norm_toLp, inner_fourierTransformCLM_toL2_eq, continuous_toLp, toLp_fourierTransform_eq, MeasureTheory.Lp.toTemperedDistribution_toLp_eq, toLp_fourier_eq
toLpCLM 📖	CompOp	2 math math: toLpCLM_apply, denseRange_toLpCLM
toZeroAtInfty 📖	CompOp	2 math math: toZeroAtInfty_toBCF, toZeroAtInfty_apply
toZeroAtInftyCLM 📖	CompOp	1 math math: toZeroAtInftyCLM_apply
«term𝓢(_,_)» 📖» "API Documentation")	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_apply 📖	mathematical	—	DFunLike.coe SchwartzMap instFunLike instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	—
bilinLeftCLM_apply 📖	mathematical	Function.HasTemperateGrowth	DFunLike.coe SchwartzMap instFunLike ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule IsScalarTower.to_smulCommClass Real Real.instCommSemiring NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.isScalarTower NormedAddCommGroup.toAddCommGroup IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace MonoidWithZero.toMonoid Semiring.toMonoidWithZero ContinuousLinearMap.funLike bilinLeftCLM ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
coeFn_toLp 📖	mathematical	—	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.AEEqFun.cast UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.AEEqFun AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp toLp DFunLike.coe SchwartzMap instFunLike	—	MeasureTheory.MemLp.coeFn_toLp memLp
coeFn_zero 📖	mathematical	—	DFunLike.coe SchwartzMap instFunLike instZero Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	—
coeHom_injective 📖	mathematical	—	SchwartzMap DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup Pi.addZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddMonoidHom.instFunLike coeHom	—	coe_coeHom DFunLike.coe_injective
coe_coeHom 📖	mathematical	—	DFunLike.coe AddMonoidHom SchwartzMap AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup Pi.addZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddMonoidHom.instFunLike coeHom instFunLike	—	—
coe_zero 📖	mathematical	—	DFunLike.coe SchwartzMap instFunLike instZero Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	—
compCLMOfAntilipschitz_apply 📖	mathematical	Function.HasTemperateGrowth AntilipschitzWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace	DFunLike.coe SchwartzMap instFunLike ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule ContinuousLinearMap.funLike compCLMOfAntilipschitz	—	—
compCLMOfContinuousLinearEquiv_apply 📖	mathematical	—	DFunLike.coe SchwartzMap instFunLike ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule ContinuousLinearMap.funLike compCLMOfContinuousLinearEquiv ContinuousLinearEquiv Real Real.semiring RingHomInvPair.ids UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField EquivLike.toFunLike ContinuousLinearEquiv.equivLike	—	RingHomInvPair.ids
compCLM_apply 📖	mathematical	Function.HasTemperateGrowth Real Real.instLE Norm.norm NormedAddCommGroup.toNorm Real.instMul Monoid.toNatPow Real.instMonoid Real.instAdd Real.instOne	DFunLike.coe SchwartzMap instFunLike ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule ContinuousLinearMap.funLike compCLM	—	—
contDiffAt 📖	mathematical	—	ContDiffAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField WithTop.some ENat DFunLike.coe SchwartzMap instFunLike	—	ContDiff.contDiffAt smooth
continuous 📖	mathematical	—	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe SchwartzMap instFunLike	—	ContDiff.continuous smooth
continuous_toLp 📖	mathematical	—	Continuous SchwartzMap 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 instTopologicalSpace MeasureTheory.Lp.instNormedAddCommGroup toLp	—	ContinuousLinearMap.continuous SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self NormedSpace.toIsBoundedSMul
decay 📖	mathematical	—	Real Real.instLT Real.instZero Real.instLE Real.instMul Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.hasOpNorm' Fin.fintype iteratedFDeriv DFunLike.coe SchwartzMap instFunLike	—	decay' lt_max_of_lt_right Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one LE.le.trans le_max_left
decay' 📖	mathematical	—	Real Real.instLE Real.instMul Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.hasOpNorm' Fin.fintype iteratedFDeriv toFun	—	—
denseRange_toLpCLM 📖	mathematical	—	DenseRange 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 MeasureTheory.Lp.instNormedAddCommGroup SchwartzMap DFunLike.coe ContinuousLinearMap Real DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Real.normedField RingHom.id Semiring.toNonAssocSemiring instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instModule smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing NormedSpace.toModule MeasureTheory.Lp.instModule NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedSpace.toIsBoundedSMul ContinuousLinearMap.funLike toLpCLM	—	SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self NormedSpace.toIsBoundedSMul mem_closure_iff_nhds_basis Metric.nhds_basis_closedBall MeasureTheory.MemLp.exist_eLpNorm_sub_le Fact.out MeasureTheory.Lp.memLp MeasureTheory.Measure.instOuterMeasureClass Filter.mp_mem coeFn_toLp Filter.univ_mem' MeasureTheory.Lp.dist_def MeasureTheory.eLpNorm_congr_ae le_imp_le_of_le_of_le ENNReal.toReal_mono le_refl ENNReal.toReal_ofReal LT.lt.le
differentiable 📖	mathematical	—	Differentiable Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe SchwartzMap instFunLike	—	ContDiff.differentiable smooth one_ne_zero NeZero.charZero_one WithTop.charZero
differentiableAt 📖	mathematical	—	DifferentiableAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe SchwartzMap instFunLike	—	Differentiable.differentiableAt differentiable
eLpNorm_le_seminorm 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.eLpNorm ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm DFunLike.coe SchwartzMap instFunLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofNNReal ENNReal.ofReal Seminorm SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddGroup instAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid instModule Real Seminorm.instFunLike Finset.sup Seminorm.instSemilatticeSup Seminorm.instOrderBot Finset.Iic Prod.instPreorder Nat.instPreorder Prod.instLocallyFiniteOrderBot LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder Prod.instDecidableLE schwartzSeminormFamily	—	MeasureTheory.Measure.HasTemperateGrowth.exists_eLpNorm_lt_top Nat.instAtLeastTwoHAddOfNat lt_add_of_pos_of_le IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike norm_nonneg Real.rpow_neg_natCast zpow_neg zpow_natCast inv_smul_smul₀ isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Real.instNontrivial LT.lt.ne' MeasureTheory.eLpNorm_smul_le_eLpNorm_mul_eLpNorm_top NormedSpace.toIsBoundedSMul Continuous.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace secondCountableTopologyEither_of_right instSecondCountableTopologyReal Continuous.rpow_const Continuous.fun_add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal continuous_const Continuous.norm continuous_id' mul_le_mul_right IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid MeasureTheory.eLpNormEssSup_le_of_ae_nnnorm_bound MeasureTheory.ae_of_all MeasureTheory.Measure.instOuterMeasureClass norm_toNNReal Real.toNNReal_le_iff_le_coe norm_smul NormedSpace.toNormSMulClass norm_pow NormedDivisionRing.to_normOneClass abs_of_nonneg LT.lt.le sup_of_le_left AddGroupSeminormClass.toNonnegHomClass SeminormClass.toAddGroupSeminormClass Seminorm.instSeminormClass norm_iteratedFDeriv_zero one_add_le_sup_seminorm_apply le_refl ENNReal.coe_mul ENNReal.coe_toNNReal LT.lt.ne Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right
eLpNorm_lt_top 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.eLpNorm ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm DFunLike.coe SchwartzMap instFunLike Top.top instTopENNReal	—	smulCommClass_self eLpNorm_le_seminorm lt_of_le_of_lt ENNReal.mul_lt_top ENNReal.coe_lt_top ENNReal.ofReal_lt_top
evalCLM_apply_apply 📖	mathematical	—	DFunLike.coe SchwartzMap instFunLike ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring Real Real.semiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.toNormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule ContinuousLinearMap.smulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SeminormedAddCommGroup.toAddCommGroup ContinuousLinearMap.funLike evalCLM	—	RingHomIsometric.ids smulCommClass_self ContinuousLinearMap.smulCommClass
ext 📖	—	DFunLike.coe SchwartzMap instFunLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe SchwartzMap instFunLike	—	ext
hasTemperateGrowth 📖	mathematical	—	Function.HasTemperateGrowth DFunLike.coe SchwartzMap instFunLike	—	smooth decay pow_zero mul_one one_mul
injective_toLp 📖	mathematical	—	SchwartzMap 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 toLp	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Measure.instOuterMeasureClass memLp Continuous.ae_eq_iff_eq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace continuous
inner_toL2_toL2_eq 📖	mathematical	—	Inner.inner 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 ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat MeasureTheory.L2.instInnerSubtypeAEEqFunMemAddSubgroupLpOfNatENNReal Complex.instRCLike toLp NormedSpace.complexToReal InnerProductSpace.toNormedSpace BorelSpace.opensMeasurable secondCountableTopologyEither_of_left secondCountable_of_proper FiniteDimensional.proper_real MeasureTheory.integral Complex.instNormedAddCommGroup Real Real.instRCLike instInnerProductSpaceRealComplex InnerProductSpace.toInner DFunLike.coe SchwartzMap instFunLike	—	MeasureTheory.integral_congr_ae BorelSpace.opensMeasurable secondCountableTopologyEither_of_left secondCountable_of_proper FiniteDimensional.proper_real Nat.instAtLeastTwoHAddOfNat MeasureTheory.Measure.instOuterMeasureClass coeFn_toLp Filter.mp_mem Filter.univ_mem'
instBoundedContinuousMapClass 📖	mathematical	—	BoundedContinuousMapClass SchwartzMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instFunLike	—	instContinuousMapClass Nat.instAtLeastTwoHAddOfNat smulCommClass_self BoundedContinuousFunction.dist_le_two_norm' norm_le_seminorm
instContinuousMapClass 📖	mathematical	—	ContinuousMapClass SchwartzMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instFunLike	—	continuous
instContinuousSMul 📖	mathematical	—	ContinuousSMul SchwartzMap instSMul UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instTopologicalSpace	—	WithSeminorms.withSeminorms_eq schwartz_withSeminorms ModuleFilterBasis.continuousSMul IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing
instFirstCountableTopology 📖	mathematical	—	FirstCountableTopology SchwartzMap instTopologicalSpace	—	WithSeminorms.firstCountableTopology smulCommClass_self instCountableProd instCountableNat schwartz_withSeminorms
instIsScalarTower 📖	mathematical	—	IsScalarTower SchwartzMap instSMul	—	ext smul_assoc
instIsTopologicalAddGroup 📖	mathematical	—	IsTopologicalAddGroup SchwartzMap instTopologicalSpace AddCommGroup.toAddGroup instAddCommGroup	—	AddGroupFilterBasis.isTopologicalAddGroup smulCommClass_self
instIsUniformAddGroup 📖	mathematical	—	IsUniformAddGroup SchwartzMap instUniformSpace AddCommGroup.toAddGroup instAddCommGroup	—	AddGroupFilterBasis.isUniformAddGroup smulCommClass_self
instLocallyConvexSpace 📖	mathematical	—	LocallyConvexSpace Real SchwartzMap Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid instAddCommGroup instModule Real.normedField smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing NormedSpace.toModule instTopologicalSpace	—	WithSeminorms.toLocallyConvexSpace smulCommClass_self instIsScalarTower IsScalarTower.left schwartz_withSeminorms
instSMulCommClass 📖	mathematical	—	SMulCommClass SchwartzMap instSMul	—	ext SMulCommClass.smul_comm
instZeroAtInftyContinuousMapClass 📖	mathematical	—	ZeroAtInftyContinuousMapClass SchwartzMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup instFunLike	—	instContinuousMapClass tendsto_cocompact
integrable 📖	mathematical	—	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe SchwartzMap instFunLike	—	MeasureTheory.Integrable.mono integrable_pow_mul Continuous.aestronglyMeasurable BorelSpace.opensMeasurable PseudoEMetricSpace.pseudoMetrizableSpace secondCountableTopologyEither_of_left continuous Filter.Eventually.of_forall MeasureTheory.Measure.instOuterMeasureClass pow_zero one_mul norm_norm
integrable_pow_mul 📖	mathematical	—	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.instMul Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm DFunLike.coe SchwartzMap instFunLike	—	norm_iteratedFDeriv_zero integrable_pow_mul_iteratedFDeriv
integrable_pow_mul_iteratedFDeriv 📖	mathematical	—	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.instMul Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.hasOpNorm' Fin.fintype iteratedFDeriv DFunLike.coe SchwartzMap instFunLike	—	integrable_of_le_of_pow_mul_le smulCommClass_self norm_iteratedFDeriv_le_seminorm le_seminorm Continuous.aestronglyMeasurable SeminormedAddCommGroup.toIsTopologicalAddGroup BorelSpace.opensMeasurable PseudoEMetricSpace.pseudoMetrizableSpace secondCountableTopologyEither_of_left ContDiff.continuous_iteratedFDeriv le_top smooth
integralCLM_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring SchwartzMap instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instModule IsScalarTower.to_smulCommClass Real Real.instCommSemiring NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing RCLike.toNormedAlgebra NormedSpace.toModule Real.isScalarTower NormedAddCommGroup.toAddCommGroup IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal MonoidWithZero.toMonoid Semiring.toMonoidWithZero ContinuousLinearMap.funLike integralCLM MeasureTheory.integral instFunLike	—	IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
integral_pow_mul_iteratedFDeriv_le 📖	mathematical	—	Real Real.instLE MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instMul Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.hasOpNorm' Fin.fintype iteratedFDeriv DFunLike.coe SchwartzMap instFunLike instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat MeasureTheory.Measure.integrablePower Real.instPow Real.instAdd Real.instOne Real.instNeg Seminorm SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddGroup instAddCommGroup instSMul IsScalarTower.to_smulCommClass Real.instCommSemiring NormedAlgebra.toAlgebra Real.normedField RCLike.toNormedAlgebra Real.isScalarTower NormedAddCommGroup.toAddCommGroup IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero Seminorm.instFunLike seminorm	—	integral_pow_mul_le_of_le_of_pow_mul_le IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace norm_iteratedFDeriv_le_seminorm smulCommClass_self le_seminorm
isBigO_cocompact_rpow 📖	mathematical	—	Asymptotics.IsBigO Real NormedAddCommGroup.toNorm Real.norm Filter.cocompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe SchwartzMap instFunLike Real.instPow Norm.norm	—	Real.instIsStrictOrderedRing neg_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Nat.le_ceil Asymptotics.IsBigO.trans isBigO_cocompact_zpow_neg_nat Asymptotics.IsBigO_def Asymptotics.IsBigOWith_def Filter.Eventually.mono Filter.eventually_ge_atTop one_mul Real.norm_of_nonneg le_of_lt zpow_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono IsStrictOrderedRing.toZeroLEOneClass lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Real.rpow_pos_of_pos Real.rpow_intCast Int.cast_neg Int.cast_natCast Real.rpow_le_rpow_of_exponent_le Asymptotics.IsBigO.comp_tendsto tendsto_norm_cocompact_atTop
isBigO_cocompact_zpow 📖	mathematical	—	Asymptotics.IsBigO Real NormedAddCommGroup.toNorm Real.norm Filter.cocompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe SchwartzMap instFunLike DivInvMonoid.toZPow Real.instDivInvMonoid Norm.norm	—	Real.rpow_intCast isBigO_cocompact_rpow
isBigO_cocompact_zpow_neg_nat 📖	mathematical	—	Asymptotics.IsBigO Real NormedAddCommGroup.toNorm Real.norm Filter.cocompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe SchwartzMap instFunLike DivInvMonoid.toZPow Real.instDivInvMonoid Norm.norm	—	decay Asymptotics.IsBigO_def Asymptotics.IsBigOWith_def Filter.Eventually.filter_mono Filter.cocompact_le_cofinite Filter.Eventually.mono Filter.eventually_cofinite_ne Real.norm_of_nonneg le_of_lt zpow_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsStrictOrderedRing.toZeroLEOneClass norm_pos_iff zpow_neg div_eq_mul_inv le_div_iff₀' norm_iteratedFDeriv_zero
le_seminorm 📖	mathematical	—	Real Real.instLE Real.instMul Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.hasOpNorm' Fin.fintype iteratedFDeriv DFunLike.coe SchwartzMap instFunLike Seminorm SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddGroup instAddCommGroup instSMul Seminorm.instFunLike seminorm	—	—
le_seminorm' 📖	mathematical	—	Real Real.instLE Real.instMul Monoid.toNatPow Real.instMonoid abs Real.lattice Real.instAddGroup Norm.norm NormedAddCommGroup.toNorm iteratedDeriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField DFunLike.coe SchwartzMap Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal instFunLike Seminorm SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddGroup instAddCommGroup instSMul Seminorm.instFunLike seminorm	—	le_seminorm Real.norm_eq_abs norm_iteratedFDeriv_eq_norm_iteratedDeriv
memLp 📖	mathematical	—	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe SchwartzMap instFunLike	—	Continuous.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace continuous eLpNorm_lt_top
memLp_top 📖	mathematical	—	MeasureTheory.MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe SchwartzMap instFunLike Top.top ENNReal instTopENNReal	—	decay MeasureTheory.memLp_top_of_bound Continuous.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace continuous MeasureTheory.ae_of_all MeasureTheory.Measure.instOuterMeasureClass pow_zero norm_iteratedFDeriv_zero one_mul
neg_apply 📖	mathematical	—	DFunLike.coe SchwartzMap instFunLike instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	—
norm_iteratedFDeriv_le_seminorm 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.hasOpNorm' Fin.fintype iteratedFDeriv DFunLike.coe SchwartzMap instFunLike Seminorm SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddGroup instAddCommGroup instSMul Seminorm.instFunLike seminorm	—	le_seminorm one_mul pow_zero
norm_le_seminorm 📖	mathematical	—	Real Real.instLE Norm.norm NormedAddCommGroup.toNorm DFunLike.coe SchwartzMap instFunLike Seminorm SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddGroup instAddCommGroup instSMul Seminorm.instFunLike seminorm	—	norm_pow_mul_le_seminorm one_mul pow_zero
norm_pow_mul_le_seminorm 📖	mathematical	—	Real Real.instLE Real.instMul Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm DFunLike.coe SchwartzMap instFunLike Seminorm SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddGroup instAddCommGroup instSMul Seminorm.instFunLike seminorm	—	le_seminorm norm_iteratedFDeriv_zero
norm_toLp 📖	mathematical	—	Norm.norm 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 MeasureTheory.Lp.instNorm toLp ENNReal.toReal MeasureTheory.eLpNorm ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddGroup.toContinuousENorm DFunLike.coe SchwartzMap instFunLike	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Lp.norm_def MeasureTheory.eLpNorm_congr_ae coeFn_toLp
norm_toLp_le_seminorm 📖	mathematical	—	Real Real.instLE Real.instZero Norm.norm 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 MeasureTheory.Lp.instNorm toLp Real.instMul DFunLike.coe Seminorm SchwartzMap SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddGroup instAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid instModule Seminorm.instFunLike Finset.sup Seminorm.instSemilatticeSup Seminorm.instOrderBot Finset.Iic Prod.instPreorder Nat.instPreorder Prod.instLocallyFiniteOrderBot LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder Prod.instDecidableLE schwartzSeminormFamily	—	SeminormedAddCommGroup.toIsTopologicalAddGroup eLpNorm_le_seminorm NNReal.coe_nonneg norm_toLp ENNReal.toReal_le_of_le_ofReal IsOrderedRing.toPosMulMono Real.instIsOrderedRing AddGroupSeminormClass.toNonnegHomClass Real.instIsOrderedAddMonoid SeminormClass.toAddGroupSeminormClass Seminorm.instSeminormClass ENNReal.ofReal_mul NNReal.zero_le_coe ENNReal.ofReal_coe_nnreal
one_add_le_sup_seminorm_apply 📖	mathematical	—	Real Real.instLE Real.instMul Monoid.toNatPow Real.instMonoid Real.instAdd Real.instOne Norm.norm NormedAddCommGroup.toNorm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.hasOpNorm' Fin.fintype iteratedFDeriv DFunLike.coe SchwartzMap instFunLike instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Seminorm SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddGroup instAddCommGroup instSMul Seminorm.instFunLike Finset.sup Seminorm.instSemilatticeSup Seminorm.instOrderBot instModule Finset.Iic Prod.instPreorder Nat.instPreorder Prod.instLocallyFiniteOrderBot LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder Prod.instDecidableLE seminorm	—	Nat.instAtLeastTwoHAddOfNat add_comm add_pow Finset.sum_congr one_pow mul_one Finset.sum_mul Nat.sum_range_choose Nat.cast_sum le_imp_le_of_le_of_le Finset.sum_le_sum_of_subset_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing pow_nonneg IsOrderedRing.toZeroLEOneClass norm_nonneg Nat.cast_nonneg' Real.instZeroLEOneClass le_refl Finset.sum_le_sum mul_comm mul_assoc mul_le_mul IsOrderedRing.toMulPosMono le_seminorm Seminorm.le_def Finset.le_sup_of_le Finset.mem_Iic Finset.mem_range_succ_iff le_rfl Nat.mono_cast Nat.choose_le_choose NonnegHomClass.apply_nonneg AddGroupSeminormClass.toNonnegHomClass SeminormClass.toAddGroupSeminormClass Seminorm.instSeminormClass
pairing_apply 📖	mathematical	—	DFunLike.coe SchwartzMap instFunLike ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule IsScalarTower.to_smulCommClass Real Real.instCommSemiring NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.isScalarTower NormedAddCommGroup.toAddCommGroup IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace MonoidWithZero.toMonoid Semiring.toMonoidWithZero ContinuousLinearMap.funLike LinearMap ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd instIsTopologicalAddGroup ContinuousLinearMap.module instSMulCommClass smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid CommRing.toRing ContinuousSMul.continuousConstSMul instContinuousSMul LinearMap.instFunLike pairing ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace instIsTopologicalAddGroup instSMulCommClass ContinuousSMul.continuousConstSMul instContinuousSMul
pairing_apply_apply 📖	mathematical	—	DFunLike.coe SchwartzMap instFunLike ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule IsScalarTower.to_smulCommClass Real Real.instCommSemiring NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.isScalarTower NormedAddCommGroup.toAddCommGroup IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace MonoidWithZero.toMonoid Semiring.toMonoidWithZero ContinuousLinearMap.funLike LinearMap ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd instIsTopologicalAddGroup ContinuousLinearMap.module instSMulCommClass smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid CommRing.toRing ContinuousSMul.continuousConstSMul instContinuousSMul LinearMap.instFunLike pairing ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace instIsTopologicalAddGroup instSMulCommClass ContinuousSMul.continuousConstSMul instContinuousSMul
pairing_continuous_left 📖	mathematical	—	Continuous SchwartzMap instTopologicalSpace DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instAddCommGroup instModule IsScalarTower.to_smulCommClass Real Real.instCommSemiring NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.isScalarTower NormedAddCommGroup.toAddCommGroup IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace MonoidWithZero.toMonoid Semiring.toMonoidWithZero ContinuousLinearMap.funLike LinearMap ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd instIsTopologicalAddGroup ContinuousLinearMap.module instSMulCommClass smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid CommRing.toRing ContinuousSMul.continuousConstSMul instContinuousSMul LinearMap.instFunLike pairing	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ContinuousLinearMap.continuous IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace instIsTopologicalAddGroup instSMulCommClass ContinuousSMul.continuousConstSMul instContinuousSMul RingHomIsometric.ids
schwartzSeminormFamily_apply 📖	mathematical	—	schwartzSeminormFamily seminorm	—	—
schwartzSeminormFamily_apply_zero 📖	mathematical	—	schwartzSeminormFamily Prod.instZero MulZeroClass.toZero Nat.instMulZeroClass seminorm	—	—
seminorm_apply 📖	mathematical	—	DFunLike.coe Seminorm SchwartzMap SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddGroup instAddCommGroup instSMul Real Seminorm.instFunLike seminorm InfSet.sInf Real.instInfSet setOf Real.instLE Real.instZero	—	—
seminorm_le_bound 📖	mathematical	Real Real.instLE Real.instZero Real.instMul Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm ContinuousMultilinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousMultilinearMap.hasOpNorm' Fin.fintype iteratedFDeriv DFunLike.coe SchwartzMap instFunLike	Seminorm SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddGroup instAddCommGroup instSMul Seminorm.instFunLike seminorm	—	—
seminorm_le_bound' 📖	mathematical	Real Real.instLE Real.instZero Real.instMul Monoid.toNatPow Real.instMonoid abs Real.lattice Real.instAddGroup Norm.norm NormedAddCommGroup.toNorm iteratedDeriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField DFunLike.coe SchwartzMap Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal instFunLike	Seminorm SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AddCommGroup.toAddGroup instAddCommGroup instSMul Seminorm.instFunLike seminorm	—	seminorm_le_bound norm_iteratedFDeriv_eq_norm_iteratedDeriv
smooth 📖	mathematical	—	ContDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField WithTop.some ENat DFunLike.coe SchwartzMap instFunLike	—	ContDiff.of_le smooth' le_top
smooth' 📖	mathematical	—	ContDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField WithTop.some ENat Top.top instTopENat toFun	—	—
smulLeftCLM_add 📖	mathematical	Function.HasTemperateGrowth NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedAlgebra.toNormedSpace Real Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing	smulLeftCLM Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring SchwartzMap instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule IsScalarTower.to_smulCommClass Real.instCommSemiring NormedAlgebra.toAlgebra ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.isScalarTower NormedAddCommGroup.toAddCommGroup IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Algebra.toSMul Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero ContinuousLinearMap.add IsTopologicalAddGroup.toContinuousAdd instIsTopologicalAddGroup	—	ContinuousLinearMap.ext IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace IsTopologicalAddGroup.toContinuousAdd instIsTopologicalAddGroup ext smulLeftCLM_apply_apply Function.HasTemperateGrowth.add add_smul
smulLeftCLM_apply 📖	mathematical	Function.HasTemperateGrowth NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedAlgebra.toNormedSpace Real Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing	DFunLike.coe SchwartzMap instFunLike ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule IsScalarTower.to_smulCommClass Real.instCommSemiring NormedAlgebra.toAlgebra ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.isScalarTower NormedAddCommGroup.toAddCommGroup IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Algebra.toSMul Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero ContinuousLinearMap.funLike smulLeftCLM ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid	—	IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
smulLeftCLM_apply_apply 📖	mathematical	Function.HasTemperateGrowth NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedAlgebra.toNormedSpace Real Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing	DFunLike.coe SchwartzMap instFunLike ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule IsScalarTower.to_smulCommClass Real.instCommSemiring NormedAlgebra.toAlgebra ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.isScalarTower NormedAddCommGroup.toAddCommGroup IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Algebra.toSMul Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero ContinuousLinearMap.funLike smulLeftCLM ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid	—	IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace smulLeftCLM_apply
smulLeftCLM_compCLMOfContinuousLinearEquiv 📖	mathematical	Function.HasTemperateGrowth NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedAlgebra.toNormedSpace Real Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring SchwartzMap instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule IsScalarTower.to_smulCommClass Real.instCommSemiring NormedAlgebra.toAlgebra ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.isScalarTower NormedAddCommGroup.toAddCommGroup IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Algebra.toSMul Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero ContinuousLinearMap.funLike smulLeftCLM DenselyNormedField.toNormedField RCLike.toDenselyNormedField compCLMOfContinuousLinearEquiv ContinuousLinearEquiv RingHomInvPair.ids EquivLike.toFunLike ContinuousLinearEquiv.equivLike ContinuousLinearEquiv.symm	—	RingHomInvPair.ids ext IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Function.HasTemperateGrowth.comp ContinuousLinearEquiv.hasTemperateGrowth smulLeftCLM_apply_apply ContinuousLinearEquiv.symm_apply_apply
smulLeftCLM_compL_smulLeftCLM 📖	mathematical	Function.HasTemperateGrowth NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedAlgebra.toNormedSpace Real Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing	ContinuousLinearMap.comp DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring SchwartzMap instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule IsScalarTower.to_smulCommClass Real.instCommSemiring NormedAlgebra.toAlgebra ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.isScalarTower NormedAddCommGroup.toAddCommGroup IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Algebra.toSMul Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHomCompTriple.ids smulLeftCLM Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	ContinuousLinearMap.ext IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace RingHomCompTriple.ids smulLeftCLM_smulLeftCLM_apply
smulLeftCLM_const 📖	mathematical	—	smulLeftCLM ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring SchwartzMap instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule IsScalarTower.to_smulCommClass Real Real.instCommSemiring NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.isScalarTower NormedAddCommGroup.toAddCommGroup IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace MonoidWithZero.toMonoid Semiring.toMonoidWithZero ContinuousLinearMap.instSMul AddCommMonoid.toAddMonoid instSMulCommClass smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid CommRing.toRing ContinuousSMul.continuousConstSMul instContinuousSMul ContinuousLinearMap.id	—	ContinuousLinearMap.ext IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace instSMulCommClass smulCommClass_self ContinuousSMul.continuousConstSMul instContinuousSMul ext Function.HasTemperateGrowth.const smulLeftCLM_apply_apply
smulLeftCLM_fun_neg 📖	mathematical	Function.HasTemperateGrowth NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedAlgebra.toNormedSpace Real Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing	smulLeftCLM NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring SchwartzMap instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule IsScalarTower.to_smulCommClass Real.instCommSemiring NormedAlgebra.toAlgebra ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.isScalarTower IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Algebra.toSMul Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero ContinuousLinearMap.neg instIsTopologicalAddGroup	—	smulLeftCLM_neg
smulLeftCLM_neg 📖	mathematical	Function.HasTemperateGrowth NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedAlgebra.toNormedSpace Real Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing	smulLeftCLM Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring SchwartzMap instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule IsScalarTower.to_smulCommClass Real.instCommSemiring NormedAlgebra.toAlgebra ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.isScalarTower IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Algebra.toSMul Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero ContinuousLinearMap.neg instIsTopologicalAddGroup	—	ContinuousLinearMap.ext IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace instIsTopologicalAddGroup ext smulLeftCLM_apply_apply Function.HasTemperateGrowth.neg neg_smul
smulLeftCLM_ofReal 📖	mathematical	Function.HasTemperateGrowth Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring SchwartzMap instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule IsScalarTower.to_smulCommClass Real.instCommSemiring NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing RCLike.toNormedAlgebra ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.isScalarTower NormedAddCommGroup.toAddCommGroup IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace MonoidWithZero.toMonoid Semiring.toMonoidWithZero ContinuousLinearMap.funLike smulLeftCLM RCLike.ofReal Real.denselyNormedField	—	ext IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace smulLeftCLM_apply_apply Function.HasTemperateGrowth.comp Function.RCLike.hasTemperateGrowth_ofReal algebraMap_smul
smulLeftCLM_real_smul 📖	mathematical	Function.HasTemperateGrowth NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal	smulLeftCLM DenselyNormedField.toNontriviallyNormedField RCLike.toNormedAlgebra Function.hasSMul Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedAlgebra.toAlgebra ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring SchwartzMap instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule IsScalarTower.to_smulCommClass Real.instCommSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.isScalarTower NormedAddCommGroup.toAddCommGroup IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace MonoidWithZero.toMonoid Semiring.toMonoidWithZero ContinuousLinearMap.instSMul AddCommMonoid.toAddMonoid smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid CommRing.toRing Real.commRing instSMulCommClass IsScalarTower.to_smulCommClass' ContinuousSMul.continuousConstSMul instContinuousSMul	—	IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace smulCommClass_self instSMulCommClass IsScalarTower.to_smulCommClass' ContinuousSMul.continuousConstSMul instContinuousSMul RCLike.real_smul_eq_coe_smul Pi.isScalarTower IsScalarTower.right smulLeftCLM_smul instIsTopologicalAddGroup ContinuousLinearMap.isScalarTower instIsScalarTower
smulLeftCLM_smul 📖	mathematical	Function.HasTemperateGrowth NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedAlgebra.toNormedSpace Real Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing	smulLeftCLM Function.hasSMul Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField CommSemiring.toSemiring Algebra.id ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.id Semiring.toNonAssocSemiring SchwartzMap instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule IsScalarTower.to_smulCommClass Real.instCommSemiring NormedAlgebra.toAlgebra ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.isScalarTower NormedAddCommGroup.toAddCommGroup IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero ContinuousLinearMap.instSMul AddCommMonoid.toAddMonoid instSMulCommClass smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid CommRing.toRing ContinuousSMul.continuousConstSMul instContinuousSMul	—	Function.HasTemperateGrowth.const IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace instSMulCommClass smulCommClass_self ContinuousSMul.continuousConstSMul instContinuousSMul RingHomCompTriple.ids ContinuousLinearMap.comp.congr_simp smulLeftCLM_const ContinuousLinearMap.id_comp smulLeftCLM_compL_smulLeftCLM
smulLeftCLM_smulLeftCLM_apply 📖	mathematical	Function.HasTemperateGrowth NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedAlgebra.toNormedSpace Real Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring SchwartzMap instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule IsScalarTower.to_smulCommClass Real.instCommSemiring NormedAlgebra.toAlgebra ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.isScalarTower NormedAddCommGroup.toAddCommGroup IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Algebra.toSMul Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero ContinuousLinearMap.funLike smulLeftCLM Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	ext IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace smulLeftCLM_apply_apply smul_smul Function.HasTemperateGrowth.mul
smulLeftCLM_sub 📖	mathematical	Function.HasTemperateGrowth NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedAlgebra.toNormedSpace Real Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing	smulLeftCLM Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring SchwartzMap instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule IsScalarTower.to_smulCommClass Real.instCommSemiring NormedAlgebra.toAlgebra ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.isScalarTower NormedAddCommGroup.toAddCommGroup IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Algebra.toSMul Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero ContinuousLinearMap.sub instIsTopologicalAddGroup	—	ContinuousLinearMap.ext IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace instIsTopologicalAddGroup ext smulLeftCLM_apply_apply Function.HasTemperateGrowth.sub sub_smul
smulLeftCLM_sum 📖	mathematical	Function.HasTemperateGrowth NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedAlgebra.toNormedSpace Real Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing	smulLeftCLM Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring SchwartzMap instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule IsScalarTower.to_smulCommClass Real.instCommSemiring NormedAlgebra.toAlgebra SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.isScalarTower NormedAddCommGroup.toAddCommGroup IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toIsBoundedSMul 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 Algebra.toSMul Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd instIsTopologicalAddGroup	—	ContinuousLinearMap.ext IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace IsTopologicalAddGroup.toContinuousAdd instIsTopologicalAddGroup ext smulLeftCLM_apply_apply Function.HasTemperateGrowth.sum Finset.sum_smul ContinuousLinearMap.coe_sum' Finset.sum_apply sum_apply Finset.sum_congr
smulRightCLM_apply_apply 📖	mathematical	—	DFunLike.coe SchwartzMap ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.toNormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing instFunLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule IsScalarTower.to_smulCommClass Real.instCommSemiring NormedAlgebra.toAlgebra NormedField.toNormedCommRing Real.isScalarTower NormedAddCommGroup.toAddCommGroup IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace MonoidWithZero.toMonoid Semiring.toMonoidWithZero ContinuousLinearMap.smulCommClass SeminormedAddCommGroup.toAddCommGroup ContinuousLinearMap.funLike smulRightCLM ContinuousLinearMap.smulRight InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal IsScalarTower.left Real.instAddCommMonoid ContinuousLinearMap.topologicalSpace instIsTopologicalAddGroupReal ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousLinearMap.module Algebra.to_smulCommClass CommSemiring.toSemiring Algebra.id UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul Real.instRing instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	instIsTopologicalAddGroupReal IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul RingHomIsometric.ids smulCommClass_self IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace ContinuousLinearMap.smulCommClass
smul_apply 📖	mathematical	—	DFunLike.coe SchwartzMap instFunLike instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule	—	—
sub_apply 📖	mathematical	—	DFunLike.coe SchwartzMap instFunLike instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	—
sum_apply 📖	mathematical	—	DFunLike.coe SchwartzMap instFunLike Finset.sum AddCommGroup.toAddCommMonoid instAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	Finset.induction_on Finset.sum_insert
tendsto_cocompact 📖	mathematical	—	Filter.Tendsto DFunLike.coe SchwartzMap instFunLike Filter.cocompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	Asymptotics.IsBigO.trans_tendsto isBigO_cocompact_rpow Real.rpow_neg_one Filter.Tendsto.inv_tendsto_atTop Real.instIsStrictOrderedRing instOrderTopologyReal tendsto_norm_cocompact_atTop
toBoundedContinuousFunctionCLM_apply 📖	mathematical	—	DFunLike.coe BoundedContinuousFunction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup BoundedContinuousFunction.instFunLike ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring SchwartzMap instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup BoundedContinuousFunction.instPseudoMetricSpace BoundedContinuousFunction.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instBoundedAddOfLipschitzAdd AddCommMonoid.toAddMonoid SeminormedAddCommGroup.to_lipschitzAdd IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup instModule BoundedContinuousFunction.instModule SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NormedSpace.toModule NormedSpace.toIsBoundedSMul ContinuousLinearMap.funLike toBoundedContinuousFunctionCLM instFunLike	—	instBoundedAddOfLipschitzAdd SeminormedAddCommGroup.to_lipschitzAdd IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup NormedSpace.toIsBoundedSMul
toBoundedContinuousFunction_apply 📖	mathematical	—	DFunLike.coe BoundedContinuousFunction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup BoundedContinuousFunction.instFunLike toBoundedContinuousFunction SchwartzMap instFunLike	—	—
toLpCLM_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring SchwartzMap instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup 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 MeasureTheory.Lp.instNormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instModule MeasureTheory.Lp.instModule NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedSpace.toModule NormedSpace.toIsBoundedSMul ContinuousLinearMap.funLike toLpCLM toLp	—	SeminormedAddCommGroup.toIsTopologicalAddGroup NormedSpace.toIsBoundedSMul
toZeroAtInftyCLM_apply 📖	mathematical	—	DFunLike.coe ZeroAtInftyContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup ZeroAtInftyContinuousMap.instFunLike ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring SchwartzMap instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup ZeroAtInftyContinuousMap.instPseudoMetricSpace ZeroAtInftyContinuousMap.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup instModule ZeroAtInftyContinuousMap.instModule NormedSpace.toModule UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toIsBoundedSMul ContinuousLinearMap.funLike toZeroAtInftyCLM instFunLike	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul
toZeroAtInfty_apply 📖	mathematical	—	DFunLike.coe ZeroAtInftyContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup ZeroAtInftyContinuousMap.instFunLike toZeroAtInfty SchwartzMap instFunLike	—	—
toZeroAtInfty_toBCF 📖	mathematical	—	ZeroAtInftyContinuousMap.toBCF UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup toZeroAtInfty toBoundedContinuousFunction	—	—
tsupport_smulLeftCLM_subset 📖	mathematical	—	Set Set.instHasSubset tsupport NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe SchwartzMap instFunLike ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring instTopologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModule IsScalarTower.to_smulCommClass Real Real.instCommSemiring NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.isScalarTower IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace SeminormedRing.toPseudoMetricSpace NormedRing.toRing NormedCommRing.toNormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Algebra.toSMul Ring.toSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedAlgebra.toNormedSpace MonoidWithZero.toMonoid Semiring.toMonoidWithZero ContinuousLinearMap.funLike smulLeftCLM Set.instInter	—	IsScalarTower.to_smulCommClass Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace smulLeftCLM_apply tsupport_smul_subset_right tsupport_smul_subset_left tsupport_zero
zero_apply 📖	mathematical	—	DFunLike.coe SchwartzMap instFunLike instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	—

(root)

Definitions

Name	Category	Theorems
SchwartzMap 📖	CompData	218 math math: SchwartzMap.norm_toLp_le_seminorm, TemperedDistribution.lineDerivOpCLM_eq, schwartz_withSeminorms, MeasureTheory.Lp.toTemperedDistributionCLM_apply, TemperedDistribution.fourierInv_toTemperedDistributionCLM_eq, SchwartzMap.lineDerivOpCLM_eq, SchwartzMap.neg_apply, SchwartzMap.instLineDerivLeftSMulReal, SchwartzMap.integral_sesq_fourier_fourier, SchwartzMap.coe_zero, SchwartzMap.norm_le_seminorm, SchwartzMap.inner_fourier_toL2_eq, SchwartzMap.toLp_fourierTransformInv_eq, SchwartzMap.add_apply, SchwartzMap.sub_apply, SchwartzMap.pairing_apply_apply, SchwartzMap.coeFn_zero, SchwartzMap.integral_clm_comp_lineDerivOp_right_eq_neg_left, SchwartzMap.lineDerivOp_fourier_eq, SchwartzMap.integral_bilin_fourierInv_eq, SchwartzMap.instContinuousSMul, TemperedDistribution.lineDerivOp_fourier_eq, SchwartzMap.bilinLeftCLM_apply, TemperedDistribution.smulLeftCLM_compL_smulLeftCLM, SchwartzMap.laplacianCLM_eq, SchwartzMap.fderivCLM_apply, SchwartzMap.instLineDerivAdd, SchwartzMap.toLpCLM_apply, SchwartzMap.compCLMOfContinuousLinearEquiv_apply, SchwartzMap.integral_fourierInv_smul_eq, SchwartzMap.inner_toL2_toL2_eq, SchwartzMap.integral_bilin_fourierIntegral_eq, SchwartzMap.toLp_fourierInv_eq, TemperedDistribution.smulLeftCLM_neg, SchwartzMap.eLpNorm_lt_top, Function.HasTemperateGrowth.toTemperedDistribution_apply, SchwartzMap.integral_sesq_fourier_eq, SchwartzMap.memLp, SchwartzMap.fourier_lineDerivOp_eq, TemperedDistribution.instLineDerivLeftSMulReal, SchwartzMap.smulLeftCLM_compCLMOfContinuousLinearEquiv, TemperedDistribution.fourierInv_lineDerivOp_eq, SchwartzMap.injective_toLp, SchwartzMap.smulLeftCLM_real_smul, SchwartzMap.integral_norm_sq_fourier, SchwartzMap.differentiable, TemperedDistribution.instFourierAdd, TemperedDistribution.instFourierSMul, TemperedDistribution.delta_apply, SchwartzMap.continuous, SchwartzMap.laplacianCLM_eq', TemperedDistribution.instContinuousFourier, SchwartzMap.smulLeftCLM_sum, SchwartzMap.toBoundedContinuousFunctionCLM_apply, SchwartzMap.instFirstCountableTopology, SchwartzMap.delta_apply, SchwartzMap.norm_fourier_toL2_eq, SchwartzMap.instFourierPair, SchwartzMap.smulLeftCLM_fun_neg, SchwartzMap.pairing_apply, SchwartzMap.norm_fourierTransformCLM_toL2_eq, SchwartzMap.lineDerivOp_compCLMOfContinuousLinearEquiv, SchwartzMap.integral_bilinear_deriv_right_eq_neg_left, SchwartzMap.norm_iteratedFDeriv_le_seminorm, TemperedDistribution.fourier_toTemperedDistributionCLM_eq, SchwartzMap.integral_mul_laplacian_right_eq_left, SchwartzMap.convolution_apply, TemperedDistribution.fourierTransformInv_toTemperedDistributionCLM_eq, SchwartzMap.integral_bilin_fourier_eq, SchwartzMap.zero_apply, SchwartzMap.compCLMOfAntilipschitz_apply, SchwartzMap.tsupport_lineDerivOp_subset, SchwartzMap.fourierInv_apply_eq, SchwartzMap.smulRightCLM_apply_apply, SchwartzMap.toTemperedDistributionCLM_apply_apply, TemperedDistribution.smulLeftCLM_sub, SchwartzMap.coeFn_toLp, SchwartzMap.smulLeftCLM_const, SchwartzMap.coeHom_injective, SchwartzMap.norm_toLp, SchwartzMap.instLineDerivSMul, SchwartzMap.fourierInv_lineDerivOp_eq, SchwartzMap.smulLeftCLM_smulLeftCLM_apply, SchwartzMap.toBoundedContinuousFunction_apply, SchwartzMap.fourier_evalCLM_eq, SchwartzMap.contDiffAt, SchwartzMap.hasFDerivAt, TemperedDistribution.instLineDerivSMulReal, SchwartzMap.evalCLM_apply_apply, MeasureTheory.Measure.toTemperedDistribution_apply, SchwartzMap.instContinuousFourierInv, TemperedDistribution.fourier_lineDerivOp_eq, SchwartzMap.tsupport_iteratedLineDerivOp_subset, SchwartzMap.integral_pow_mul_iteratedFDeriv_le, TemperedDistribution.lineDerivOp_toTemperedDistributionCLM_eq, SchwartzMap.instContinuousMapClass, SchwartzMap.smulLeftCLM_add, TemperedDistribution.laplacian_eq_sum, TemperedDistribution.instContinuousLineDeriv, SchwartzMap.tendsto_cocompact, SchwartzMap.instBoundedContinuousMapClass, SchwartzMap.integral_sesq_fourierIntegral_eq, SchwartzMap.integral_bilinear_laplacian_right_eq_left, SchwartzMap.ext_iff, SchwartzMap.le_seminorm, SchwartzMap.eLpNorm_le_seminorm, TemperedDistribution.smulLeftCLM_add, SchwartzMap.hasDerivAt, TemperedDistribution.fourierTransform_apply, SchwartzMap.tsupport_smulLeftCLM_subset, SchwartzMap.tsupport_fderivCLM_subset, SchwartzMap.smulLeftCLM_neg, SchwartzMap.iteratedPDeriv_eq_iteratedFDeriv, SchwartzMap.inner_fourierTransformCLM_toL2_eq, SchwartzMap.convolution_continuous_left, SchwartzMap.integral_fourier_mul_eq, SchwartzMap.pairing_continuous_left, SchwartzMap.integralCLM_apply, SchwartzMap.fourier_coe, SchwartzMap.iteratedLineDerivOp_eq_iteratedFDeriv, SchwartzMap.lineDerivOp_fourierInv_eq, SchwartzMap.sum_apply, SchwartzMap.fourierInv_coe, SchwartzMap.integral_smul_lineDerivOp_right_eq_neg_left, SchwartzMap.instLocallyConvexSpace, SchwartzMap.compCLM_apply, SchwartzMap.continuous_toLp, SchwartzMap.coe_coeHom, TemperedDistribution.instFourierInvSMul, SchwartzMap.toLp_fourierTransform_eq, TemperedDistribution.instFourierInvAdd, SchwartzMap.integral_mul_deriv_eq_neg_deriv_mul, TemperedDistribution.fourierInv_apply, SchwartzMap.instFourierSMul, SchwartzMap.fourierTransformCLM_apply, TemperedDistribution.fourierTransform_toTemperedDistributionCLM_eq, SchwartzMap.fderivCLM_fourier_eq, TemperedDistribution.instLineDerivAdd, SchwartzMap.derivCLM_apply, SchwartzMap.isBigO_cocompact_zpow_neg_nat, SchwartzMap.integral_clm_comp_deriv_right_eq_neg_left, SchwartzMap.memLp_top, TemperedDistribution.instLineDerivSMulComplex, SchwartzMap.smul_apply, SchwartzMap.integral_fourierInv_mul_eq, TemperedDistribution.laplacian_toTemperedDistributionCLM_eq, SchwartzMap.instZeroAtInftyContinuousMapClass, SchwartzMap.decay, SchwartzMap.convolution_flip, SchwartzMap.laplacian_eq_sum, SchwartzMap.lineDerivOp_apply_eq_fderiv, SchwartzMap.integral_fourier_smul_eq, SchwartzMap.instFourierInvAdd, SchwartzMap.integral_bilinear_lineDerivOp_right_eq_neg_left, TemperedDistribution.derivCLM_toTemperedDistributionCLM_eq, MeasureTheory.Lp.ker_toTemperedDistributionCLM_eq_bot, SchwartzMap.seminorm_apply, MeasureTheory.Lp.toTemperedDistribution_toLp_eq, TemperedDistribution.laplacian_apply_apply, TemperedDistribution.smulLeftCLM_smulLeftCLM_apply, SchwartzMap.tsupport_derivCLM_subset, SchwartzMap.integral_smul_laplacian_right_eq_left, SchwartzMap.le_seminorm', SchwartzMap.instFourierInvPair, TemperedDistribution.lineDerivOp_apply_apply, TemperedDistribution.lineDerivOp_fourierInv_eq, SchwartzMap.integral_inner_fourier_fourier, MeasureTheory.Lp.toTemperedDistribution_apply, SchwartzMap.smulLeftCLM_sub, TemperedDistribution.smulLeftCLM_const, SchwartzMap.smulLeftCLM_apply_apply, SchwartzMap.fourier_fderivCLM_eq, SchwartzMap.fourier_convolution_apply, SchwartzMap.instContinuousFourier, TemperedDistribution.smulLeftCLM_sum, TemperedDistribution.instContinuousFourierInv, SchwartzMap.integrable, TemperedDistribution.fourier_apply, SchwartzMap.lineDerivOp_apply, SchwartzMap.coe_apply, SchwartzMap.smulLeftCLM_ofReal, SchwartzMap.integrable_pow_mul, TemperedDistribution.smulLeftCLM_smul, SchwartzMap.isBigO_cocompact_zpow, SchwartzMap.smulLeftCLM_apply, SchwartzMap.tsum_eq_tsum_fourierIntegral, SchwartzMap.smulLeftCLM_compL_smulLeftCLM, SchwartzMap.instFourierInvSMul, TemperedDistribution.derivCLM_apply_apply, SchwartzMap.instSMulCommClass, SchwartzMap.instIsTopologicalAddGroup, SchwartzMap.toZeroAtInfty_apply, TemperedDistribution.fourierTransformInv_apply, SchwartzMap.integral_clm_comp_laplacian_right_eq_left, SchwartzMap.instIsScalarTower, SchwartzMap.instContinuousLineDeriv, SchwartzMap.differentiableAt, SchwartzMap.integral_smul_deriv_right_eq_neg_left, SchwartzMap.fourier_convolution, SchwartzMap.one_add_le_sup_seminorm_apply, SchwartzMap.smooth, SchwartzMap.denseRange_toLpCLM, SchwartzMap.toZeroAtInftyCLM_apply, SchwartzMap.toLp_fourier_eq, SchwartzMap.integrable_pow_mul_iteratedFDeriv, SchwartzMap.laplacian_apply, SchwartzMap.hasTemperateGrowth, TemperedDistribution.laplacianCLM_apply, SchwartzMap.instFourierAdd, SchwartzMap.smulLeftCLM_smul, HasCompactSupport.toSchwartzMap_toFun, MeasureTheory.Lp.toTemperedDistribution_smul_eq, SchwartzMap.integral_mul_lineDerivOp_right_eq_neg_left, SchwartzMap.isBigO_cocompact_rpow, TemperedDistribution.smulLeftCLM_apply_apply, SchwartzMap.norm_pow_mul_le_seminorm, SchwartzMap.tsum_eq_tsum_fourier, SchwartzMap.instIsUniformAddGroup
schwartzSeminormFamily 📖	CompOp	5 math math: SchwartzMap.norm_toLp_le_seminorm, schwartz_withSeminorms, SchwartzMap.eLpNorm_le_seminorm, SchwartzMap.schwartzSeminormFamily_apply_zero, SchwartzMap.schwartzSeminormFamily_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
schwartz_withSeminorms 📖	mathematical	—	WithSeminorms SchwartzMap SchwartzMap.instAddCommGroup SchwartzMap.instModule schwartzSeminormFamily SchwartzMap.instTopologicalSpace	—	smulCommClass_self SeminormFamily.withSeminorms_iff_nhds_eq_iInf AddGroupFilterBasis.isTopologicalAddGroup

---

← Back to Index