Periodic

📁 Source: Mathlib/Analysis/Complex/Periodic.lean

Statistics

Metric	Count
Definitions cuspFunction, invQParam, qParam	3
Theorems boundedAtFilter_cuspFunction, contDiff_qParam, continuous_qParam, cuspFunction_add, cuspFunction_eq_of_nonzero, cuspFunction_neg, cuspFunction_smul, cuspFunction_sub, cuspFunction_zero_eq_limUnder_nhds_ne, cuspFunction_zero_of_zero_at_inf, differentiableAt_cuspFunction, differentiableAt_cuspFunction_zero, differentiable_qParam, eq_cuspFunction, eventually_differentiableAt_cuspFunction_nhds_ne_zero, exp_decay_of_zero_at_inf, exp_decay_sub_of_bounded_at_inf, im_invQParam, invQParam_tendsto, norm_qParam, norm_qParam_lt_iff, qParam_left_inv_mod_period, qParam_ne_zero, qParam_right_inv, qParam_tendsto, tendsto_at_I_inf, tendsto_nhds_zero	27
Total	30

Function.Periodic

Definitions

Name	Category	Theorems
cuspFunction 📖	CompOp	10 math math: cuspFunction_zero_eq_limUnder_nhds_ne, differentiableAt_cuspFunction, boundedAtFilter_cuspFunction, cuspFunction_zero_of_zero_at_inf, eq_cuspFunction, cuspFunction_eq_of_nonzero, eventually_differentiableAt_cuspFunction_nhds_ne_zero, tendsto_at_I_inf, differentiableAt_cuspFunction_zero, exp_decay_sub_of_bounded_at_inf
invQParam 📖	CompOp	7 math math: tendsto_nhds_zero, im_invQParam, qParam_right_inv, cuspFunction_eq_of_nonzero, invQParam_tendsto, im_invQParam_pos_of_norm_lt_one, qParam_left_inv_mod_period
qParam 📖	CompOp	17 math math: norm_qParam_le_of_one_half_le_im, norm_qParam_lt_iff, SlashInvariantFormClass.eq_cuspFunction, differentiableAt_cuspFunction, continuous_qParam, UpperHalfPlane.norm_qParam_lt_one, qParam_right_inv, UpperHalfPlane.qParam_tendsto_atImInfty, eq_cuspFunction, qParam_tendsto, norm_qParam, qParam_left_inv_mod_period, differentiable_qParam, contDiff_qParam, ModularForm.logDeriv_qParam, ModularFormClass.hasSum_qExpansion, ModularFormClass.qExpansion_coeff_eq_intervalIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
boundedAtFilter_cuspFunction 📖	mathematical	Real Real.instLT Real.instZero Filter.BoundedAtFilter Complex Complex.instNorm Filter.comap Complex.im Filter.atTop Real.instPreorder	nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instZero Compl.compl Set Set.instCompl Set.instSingletonSet cuspFunction	—	Asymptotics.IsBigO.congr' Asymptotics.IsBigO.comp_tendsto invQParam_tendsto eventually_nhdsWithin_of_forall cuspFunction_eq_of_nonzero
contDiff_qParam 📖	mathematical	—	ContDiff Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace qParam	—	ContDiff.cexp ContDiff.div_const ContDiff.mul contDiff_const contDiff_fun_id
continuous_qParam 📖	mathematical	—	Continuous Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField qParam	—	Continuous.cexp Continuous.comp' Continuous.div_const IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing continuous_id' Continuous.fun_mul continuous_const
cuspFunction_add 📖	mathematical	ContinuousAt Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField cuspFunction Complex.instZero	Pi.instAdd Complex.instAdd	—	ne_or_eq Function.update_of_ne Function.update_self Filter.Tendsto.limUnder_eq Complex.instT2Space tendsto_nhds_zero PerfectSpace.not_isolated instPerfectSpace Filter.Tendsto.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing tendsto_nhds_limUnder
cuspFunction_eq_of_nonzero 📖	mathematical	—	cuspFunction invQParam	—	Function.update_of_ne
cuspFunction_neg 📖	mathematical	ContinuousAt Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField cuspFunction Complex.instZero	Pi.instNeg Complex.instNeg	—	neg_smul one_smul cuspFunction_smul
cuspFunction_smul 📖	mathematical	ContinuousAt Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField cuspFunction Complex.instZero	Function.hasSMul Algebra.toSMul Complex.instCommSemiring CommSemiring.toSemiring Algebra.id	—	eq_or_ne Function.update_self Filter.Tendsto.limUnder_eq Complex.instT2Space PerfectSpace.not_isolated instPerfectSpace Filter.Tendsto.const_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Function.update_of_ne
cuspFunction_sub 📖	mathematical	ContinuousAt Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField cuspFunction Complex.instZero	Pi.instSub Complex.instSub	—	sub_eq_add_neg cuspFunction_neg cuspFunction_add IsTopologicalRing.toContinuousNeg IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing
cuspFunction_zero_eq_limUnder_nhds_ne 📖	mathematical	—	cuspFunction Complex Complex.instZero limUnder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instInhabited nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet	—	Function.update_self Filter.map_congr eventuallyEq_nhdsWithin_of_eqOn cuspFunction.eq_1 Function.update_of_ne
cuspFunction_zero_of_zero_at_inf 📖	mathematical	Real Real.instLT Real.instZero Filter.ZeroAtFilter Complex Complex.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Filter.comap Complex.im Filter.atTop Real.instPreorder	cuspFunction	—	Function.update_self Filter.Tendsto.limUnder_eq Complex.instT2Space PerfectSpace.not_isolated instPerfectSpace Filter.Tendsto.comp invQParam_tendsto
differentiableAt_cuspFunction 📖	mathematical	Function.Periodic Complex Complex.instAdd Complex.ofReal DifferentiableAt DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField	cuspFunction qParam	—	IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Nat.instAtLeastTwoHAddOfNat IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul HasStrictDerivAt.congr_simp mul_one HasStrictDerivAt.cexp HasStrictDerivAt.div_const HasStrictDerivAt.const_mul hasStrictDerivAt_id mul_ne_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Complex.exp_ne_zero div_ne_zero Complex.two_pi_I_ne_zero Nat.cast_zero Complex.instCompleteSpace HasStrictFDerivAt.differentiableAt ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul HasStrictDerivAt.to_localInverse HasStrictFDerivAt.eventually_right_inverse RingHomInvPair.ids HasStrictDerivAt.hasStrictFDerivAt_equiv Filter.EventuallyEq.fun_comp eq_cuspFunction DifferentiableAt.congr_of_eventuallyEq DifferentiableAt.comp Filter.EventuallyEq.eq_of_nhds HasStrictFDerivAt.eventually_left_inverse Filter.EventuallyEq.symm
differentiableAt_cuspFunction_zero 📖	mathematical	Real Real.instLT Real.instZero Function.Periodic Complex Complex.instAdd Complex.ofReal Filter.Eventually DifferentiableAt DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Filter.comap Complex.im Filter.atTop Real.instPreorder Filter.BoundedAtFilter Complex.instNorm	cuspFunction Complex.instZero	—	Asymptotics.IsBigO.bound boundedAtFilter_cuspFunction Filter.Eventually.and eventually_differentiableAt_cuspFunction_nhds_ne_zero eventually_nhds_iff eventually_nhdsWithin_iff NormOneClass.norm_one NormedDivisionRing.to_normOneClass mul_one DifferentiableAt.differentiableWithinAt AddTorsor.nonempty Complex.differentiableOn_update_limUnder_of_bddAbove Complex.instCompleteSpace IsOpen.mem_nhds DifferentiableOn.differentiableAt Function.update_eq_self cuspFunction_zero_eq_limUnder_nhds_ne
differentiable_qParam 📖	mathematical	—	Differentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField qParam	—	Differentiable.cexp Differentiable.div_const Differentiable.const_mul differentiable_id
eq_cuspFunction 📖	mathematical	Function.Periodic Complex Complex.instAdd Complex.ofReal	cuspFunction qParam	—	cuspFunction.eq_1 Function.update_of_ne Complex.exp_ne_zero qParam_left_inv_mod_period int_mul
eventually_differentiableAt_cuspFunction_nhds_ne_zero 📖	mathematical	Real Real.instLT Real.instZero Function.Periodic Complex Complex.instAdd Complex.ofReal Filter.Eventually DifferentiableAt DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Filter.comap Complex.im Filter.atTop Real.instPreorder	cuspFunction nhdsWithin Complex.instZero Compl.compl Set Set.instCompl Set.instSingletonSet	—	Filter.Eventually.mp Filter.Tendsto.eventually invQParam_tendsto eventually_nhdsWithin_of_forall qParam_right_inv LT.lt.ne' differentiableAt_cuspFunction
exp_decay_of_zero_at_inf 📖	mathematical	Real Real.instLT Real.instZero Function.Periodic Complex Complex.instAdd Complex.ofReal Filter.Eventually DifferentiableAt DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Filter.comap Complex.im Filter.atTop Real.instPreorder Filter.ZeroAtFilter Complex.instZero	Asymptotics.IsBigO Complex.instNorm Real.norm Real.exp DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul Real.instNeg instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi	—	Nat.instAtLeastTwoHAddOfNat neg_mul cuspFunction_zero_of_zero_at_inf sub_zero exp_decay_sub_of_bounded_at_inf Filter.ZeroAtFilter.boundedAtFilter
exp_decay_sub_of_bounded_at_inf 📖	mathematical	Real Real.instLT Real.instZero Function.Periodic Complex Complex.instAdd Complex.ofReal Filter.Eventually DifferentiableAt DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Filter.comap Complex.im Filter.atTop Real.instPreorder Filter.BoundedAtFilter Complex.instNorm	Asymptotics.IsBigO Real.norm Complex.instSub cuspFunction Complex.instZero Real.exp DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul Real.instNeg instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi	—	Nat.instAtLeastTwoHAddOfNat neg_mul eq_cuspFunction LT.lt.ne' sub_zero norm_qParam Asymptotics.IsBigO.norm_right Asymptotics.IsBigO.comp_tendsto Asymptotics.IsBigO.mono DifferentiableAt.isBigO_sub differentiableAt_cuspFunction_zero nhdsWithin_le_nhds qParam_tendsto
im_invQParam 📖	mathematical	—	Complex.im invQParam Real Real.instMul DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNeg instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi Real.log Norm.norm Complex Complex.instNorm	—	Nat.instAtLeastTwoHAddOfNat Complex.div_I neg_mul Complex.div_ofReal_re Complex.div_ofNat_re MulZeroClass.mul_zero Complex.div_ofReal_im Complex.div_ofNat_im zero_div mul_one sub_self MulZeroClass.zero_mul add_zero Complex.log_re zero_add neg_div
invQParam_tendsto 📖	mathematical	Real Real.instLT Real.instZero	Filter.Tendsto Complex invQParam nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instZero Compl.compl Set Set.instCompl Set.instSingletonSet Filter.comap Complex.im Filter.atTop Real.instPreorder	—	Nat.instAtLeastTwoHAddOfNat im_invQParam Filter.Tendsto.const_mul_atBot_of_neg Real.instIsStrictOrderedRing div_neg_of_neg_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono neg_lt_zero IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mul_pos Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Real.pi_pos Filter.Tendsto.comp Real.tendsto_log_nhdsGT_zero tendsto_norm_nhdsNE_zero
norm_qParam 📖	mathematical	—	Norm.norm Complex Complex.instNorm qParam Real.exp Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul Real.instNeg instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi Complex.im	—	Nat.instAtLeastTwoHAddOfNat Complex.norm_exp Complex.div_ofReal_re MulZeroClass.mul_zero sub_zero MulZeroClass.zero_mul add_zero mul_one sub_self zero_sub neg_mul
norm_qParam_lt_iff 📖	mathematical	Real Real.instLT Real.instZero	Norm.norm Complex Complex.instNorm qParam Real.exp DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul Real.instNeg instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi Complex.im	—	Nat.instAtLeastTwoHAddOfNat norm_qParam Real.exp_lt_exp div_lt_div_iff_of_pos_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing mul_lt_mul_left_of_neg AddGroup.existsAddOfLE IsStrictOrderedRing.toPosMulStrictMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le neg_mul IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Real.instIsOrderedRing Real.instNontrivial Real.pi_pos
qParam_left_inv_mod_period 📖	mathematical	—	invQParam qParam Complex Complex.instAdd Complex.instMul Complex.instIntCast Complex.ofReal	—	Nat.instAtLeastTwoHAddOfNat Complex.log_exp_exists mul_div_assoc mul_comm mul_add Distrib.leftDistribClass mul_assoc div_mul_cancel₀ Complex.two_pi_I_ne_zero mul_div_cancel₀ Nat.cast_zero
qParam_ne_zero 📖	—	—	—	—	—
qParam_right_inv 📖	mathematical	—	qParam invQParam	—	mul_div_cancel₀ Nat.instAtLeastTwoHAddOfNat Complex.two_pi_I_ne_zero mul_div_cancel_left₀ EuclideanDomain.toMulDivCancelClass Complex.ofReal_ne_zero Complex.exp_log
qParam_tendsto 📖	mathematical	Real Real.instLT Real.instZero	Filter.Tendsto Complex qParam Filter.comap Complex.im Filter.atTop Real.instPreorder nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instZero Compl.compl Set Set.instCompl Set.instSingletonSet	—	tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within tendsto_zero_iff_norm_tendsto_zero Nat.instAtLeastTwoHAddOfNat norm_qParam Filter.tendsto_comap'_iff Filter.univ_mem Complex.range_im Filter.Tendsto.comp Real.tendsto_exp_atBot Filter.Tendsto.atBot_div_const Real.instIsStrictOrderedRing Filter.Tendsto.const_mul_atTop_of_neg neg_mul IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsStrictOrderedRing.toPosMulStrictMono PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Real.instIsOrderedRing Real.instNontrivial Real.pi_pos Filter.tendsto_id Filter.Eventually.of_forall Complex.exp_ne_zero
tendsto_at_I_inf 📖	mathematical	Real Real.instLT Real.instZero Function.Periodic Complex Complex.instAdd Complex.ofReal Filter.Eventually DifferentiableAt DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Filter.comap Complex.im Filter.atTop Real.instPreorder Filter.BoundedAtFilter Complex.instNorm	Filter.Tendsto nhds cuspFunction Complex.instZero	—	tendsto_nhdsWithin_of_tendsto_nhds ContinuousAt.tendsto DifferentiableAt.continuousAt IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology differentiableAt_cuspFunction_zero eq_cuspFunction LT.lt.ne' Filter.Tendsto.comp qParam_tendsto
tendsto_nhds_zero 📖	mathematical	ContinuousAt Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField cuspFunction Complex.instZero	Filter.Tendsto invQParam nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet nhds	—	Filter.Tendsto.congr' tendsto_nhdsWithin_of_tendsto_nhds ContinuousAt.tendsto Filter.mp_mem self_mem_nhdsWithin Filter.univ_mem' cuspFunction_eq_of_nonzero

---

← Back to Index