AbstractFuncEq

📁 Source: Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean

Statistics

Metric	Count
Definitions StrongFEPair, toWeakFEPair, Λ, WeakFEPair, f, f_modif, f₀, g, g_modif, g₀, k, toStrongFEPair, Λ, Λ₀, ε	15
Theorems differentiable_Λ, functional_equation, hasMellin, hf_top', hf_zero', hf₀, hg₀, symm_Λ_eq, Λ_eq, differentiableAt_Λ, differentiable_Λ₀, f_modif_aux1, f_modif_aux2, functional_equation, functional_equation₀, h_feq, h_feq', hasMellin, hf_int, hf_modif_FE, hf_modif_int, hf_top, hf_zero, hf_zero', hg_int, hg_top, hk, hε, symm_Λ₀_eq, Λ_residue_k, Λ_residue_zero, Λ₀_eq	32
Total	47

StrongFEPair

Definitions

Name	Category	Theorems
toWeakFEPair 📖	CompOp	14 math math: functional_equation, Λ_eq, hf_zero', hg₀, hf₀, HurwitzZeta.hurwitzOddFEPair_f₀, HurwitzZeta.hurwitzOddFEPair_ε, hasMellin, HurwitzZeta.hurwitzOddFEPair_g₀, HurwitzZeta.hurwitzOddFEPair_f, HurwitzZeta.hurwitzOddFEPair_k, symm_Λ_eq, hf_top', HurwitzZeta.hurwitzOddFEPair_g
Λ 📖	CompOp	5 math math: differentiable_Λ, functional_equation, Λ_eq, hasMellin, symm_Λ_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
differentiable_Λ 📖	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 NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace Λ	—	NoMaxOrder.exists_gt instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial NoMinOrder.exists_lt instNoMinOrderOfNontrivial mellin_differentiableAt_of_isBigO_rpow WeakFEPair.hf_int hf_top' hf_zero'
functional_equation 📖	mathematical	—	Λ Complex Complex.instSub Complex.ofReal WeakFEPair.k toWeakFEPair 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 Complex.instSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Complex.instNormedField WeakFEPair.ε symm	—	Λ_eq symm_Λ_eq mellin_comp_rpow mellin_cpow_smul mellin_const_smul smulCommClass_self Real.rpow_neg_one neg_neg div_one div_neg Complex.ofReal_neg one_smul inv_one abs_one Real.instIsOrderedRing abs_neg zero_sub sub_self sub_right_comm sub_eq_add_neg MeasureTheory.setIntegral_congr_fun measurableSet_Ioi BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid WeakFEPair.h_feq' Complex.cpow_neg Complex.ofReal_cpow le_of_lt LT.lt.le LT.lt.ne' Real.rpow_pos_of_pos Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ one_mul Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero WeakFEPair.hε Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one
hasMellin 📖	mathematical	—	HasMellin WeakFEPair.f toWeakFEPair Λ	—	NoMaxOrder.exists_gt instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial NoMinOrder.exists_lt instNoMinOrderOfNontrivial mellinConvergent_of_isBigO_rpow WeakFEPair.hf_int hf_top' hf_zero'
hf_top' 📖	mathematical	—	Asymptotics.IsBigO Real NormedAddCommGroup.toNorm Real.norm Filter.atTop Real.instPreorder WeakFEPair.f toWeakFEPair Real.instPow	—	hf₀ sub_zero WeakFEPair.hf_top
hf_zero' 📖	mathematical	—	Asymptotics.IsBigO Real NormedAddCommGroup.toNorm Real.norm nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero Set.Ioi Real.instPreorder WeakFEPair.f toWeakFEPair Real.instPow	—	smul_zero sub_zero WeakFEPair.hf_zero hg₀
hf₀ 📖	mathematical	—	WeakFEPair.f₀ toWeakFEPair NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	—
hg₀ 📖	mathematical	—	WeakFEPair.g₀ toWeakFEPair NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	—
symm_Λ_eq 📖	mathematical	—	Λ symm mellin WeakFEPair.g toWeakFEPair	—	—
Λ_eq 📖	mathematical	—	Λ mellin WeakFEPair.f toWeakFEPair	—	—

WeakFEPair

Definitions

Name	Category	Theorems
f 📖	CompOp	14 math math: hf_zero', h_feq, StrongFEPair.Λ_eq, StrongFEPair.hf_zero', h_feq', hf_zero, StrongFEPair.hasMellin, HurwitzZeta.hurwitzOddFEPair_f, hasMellin, hf_int, StrongFEPair.hf_top', f_modif_aux1, f_modif_aux2, hf_top
f_modif 📖	CompOp	4 math math: hf_modif_int, hf_modif_FE, f_modif_aux1, f_modif_aux2
f₀ 📖	CompOp	10 math math: symm_Λ₀_eq, hf_zero', Λ₀_eq, StrongFEPair.hf₀, HurwitzZeta.hurwitzOddFEPair_f₀, hasMellin, f_modif_aux1, f_modif_aux2, Λ_residue_zero, hf_top
g 📖	CompOp	6 math math: h_feq, h_feq', hg_top, hg_int, StrongFEPair.symm_Λ_eq, HurwitzZeta.hurwitzOddFEPair_g
g_modif 📖	CompOp	1 math math: hf_modif_FE
g₀ 📖	CompOp	9 math math: symm_Λ₀_eq, StrongFEPair.hg₀, Λ₀_eq, hg_top, hf_zero, HurwitzZeta.hurwitzOddFEPair_g₀, f_modif_aux1, f_modif_aux2, Λ_residue_k
k 📖	CompOp	14 math math: symm_Λ₀_eq, hf_zero', h_feq, StrongFEPair.functional_equation, hk, Λ₀_eq, h_feq', hf_zero, functional_equation₀, hf_modif_FE, functional_equation, HurwitzZeta.hurwitzOddFEPair_k, f_modif_aux1, Λ_residue_k
toStrongFEPair 📖	CompOp	—
Λ 📖	CompOp	7 math math: differentiableAt_Λ, symm_Λ₀_eq, Λ₀_eq, functional_equation, hasMellin, Λ_residue_zero, Λ_residue_k
Λ₀ 📖	CompOp	4 math math: symm_Λ₀_eq, Λ₀_eq, functional_equation₀, differentiable_Λ₀
ε 📖	CompOp	13 math math: symm_Λ₀_eq, h_feq, StrongFEPair.functional_equation, Λ₀_eq, h_feq', hf_zero, HurwitzZeta.hurwitzOddFEPair_ε, functional_equation₀, hf_modif_FE, functional_equation, f_modif_aux1, f_modif_aux2, Λ_residue_k

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
differentiableAt_Λ 📖	mathematical	f₀ NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup g₀	DifferentiableAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace Λ	—	DifferentiableAt.sub differentiable_Λ₀ one_div DifferentiableAt.smul_const NormedSpace.toIsBoundedSMul IsScalarTower.left differentiableAt_inv smul_zero DifferentiableAt.div differentiableAt_const differentiable_id
differentiable_Λ₀ 📖	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 NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace Λ₀	—	StrongFEPair.differentiable_Λ
f_modif_aux1 📖	mathematical	—	Set.EqOn Real AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup f_modif f f₀ Pi.instAdd Set.indicator NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Set.Ioo Real.instPreorder Real.instZero Real.instOne Complex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Module.toDistribMulAction NormedSpace.toModule Complex.instNormedField Complex.instMul ε Complex.ofReal Real.instPow Real.instNeg k g₀ Set Set.instSingletonSet Set.Ioi	—	lt_trichotomy Set.indicator_of_notMem Set.notMem_Ioi LT.lt.le Set.indicator_of_mem Set.mem_Ioo Iff.not Set.mem_singleton_iff LT.lt.ne Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isInt_neg add_zero Mathlib.Tactic.Abel.zero_termg Mathlib.Tactic.Abel.const_add_termg sub_eq_add_neg add_comm Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Set.mem_Ioi Set.notMem_Ioo_of_ge LT.lt.ne'
f_modif_aux2 📖	mathematical	Real Real.instLT k Complex.re	mellin AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup f_modif f f₀ Complex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Module.toDistribMulAction NormedSpace.toModule Complex.instNormedField DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne ε Complex.instSub Complex.ofReal g₀	—	IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add contravariant_lt_of_covariant_le LT.lt.trans hk MeasureTheory.setIntegral_congr_fun measurableSet_Ioi BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal f_modif_aux1 Set.indicator_singleton smul_add MeasureTheory.setIntegral_congr_ae Filter.eventually_of_mem MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.compl_mem_ae_iff Set.Subsingleton.measure_zero Set.subsingleton_singleton Real.noAtoms_volume Set.indicator_of_notMem add_zero MeasureTheory.setIntegral_indicator measurableSet_Ioo Set.inter_eq_right Set.Ioo_subset_Ioi_self MeasureTheory.integral_Ioc_eq_integral_Ioo measurableSet_Ioc Complex.ofReal_cpow LT.lt.le Complex.ofReal_neg smul_sub SemigroupAction.mul_smul mul_comm mul_assoc Complex.cpow_add Complex.ofReal_ne_zero LT.lt.ne' sub_eq_add_neg sub_right_comm MeasureTheory.integral_sub MeasureTheory.Integrable.smul_const NormedSpace.toIsBoundedSMul MeasureTheory.IntegrableOn.eq_1 intervalIntegrable_iff_integrableOn_Ioc_of_le PseudoEMetricSpace.pseudoMetrizableSpace zero_le_one Real.instZeroLEOneClass intervalIntegral.intervalIntegrable_cpow' MeasureTheory.Integrable.smul MeasureTheory.integral_smul NormedSpace.toNormSMulClass SMulCommClass.complexToReal smulCommClass_self integral_smul_const intervalIntegral.integral_of_le integral_cpow Complex.one_cpow sub_add_cancel Complex.zero_cpow lt_irrefl LE.le.trans_lt Complex.zero_re sub_ne_zero Complex.ofReal_re sub_zero mul_one_div neg_sub
functional_equation 📖	mathematical	—	Λ Complex Complex.instSub Complex.ofReal k 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 Complex.instSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Complex.instNormedField ε symm	—	Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.add_eq_eq functional_equation₀ Λ₀_eq symm_Λ₀_eq mul_inv_cancel₀ hε Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval Mathlib.Tactic.Module.NF.sub_eq_eval Mathlib.Tactic.Module.NF.add_eq_eval Mathlib.Tactic.Module.NF.atom_eq_eval Mathlib.Tactic.Module.NF.smul_eq_eval Mathlib.Tactic.Module.NF.eval_algebraMap AddCommMonoid.nat_isScalarTower Mathlib.Tactic.Module.NF.add_eq_eval₁ zero_add Mathlib.Tactic.Module.NF.add_eq_eval₂ Mathlib.Tactic.Module.NF.add_eq_eval₃ add_zero Mathlib.Tactic.Module.NF.sub_eq_eval₂ Mathlib.Tactic.Module.NF.zero_sub_eq_eval Mathlib.Tactic.Module.NF.zero_eq_eval Mathlib.Tactic.Module.NF.eq_cons_const eq_natCast RingHom.instRingHomClass Nat.cast_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf 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.neg_mul Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.atom_pf'
functional_equation₀ 📖	mathematical	—	Λ₀ Complex Complex.instSub Complex.ofReal k 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 Complex.instSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Complex.instNormedField ε symm	—	StrongFEPair.functional_equation
h_feq 📖	mathematical	Real Set Set.instMembership Set.Ioi Real.instPreorder Real.instZero	f DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne Complex 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 Complex.instSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Complex.instNormedField Complex.instMul ε Complex.ofReal Real.instPow k g	—	—
h_feq' 📖	mathematical	Real Real.instLT Real.instZero	g DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne Complex 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 Complex.instSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Complex.instNormedField Complex.instMul Complex.instInv ε Complex.ofReal Real.instPow k f	—	h_feq one_div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing div_div_cancel₀ one_ne_zero' NeZero.charZero_one RCLike.charZero_rclike SemigroupAction.mul_smul one_div Real.inv_rpow LT.lt.le Complex.ofReal_inv Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ one_mul Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero hε LT.lt.ne' Real.rpow_pos_of_pos Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst div_one Mathlib.Tactic.FieldSimp.NF.one_eq_eval one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one one_smul
hasMellin 📖	mathematical	Real Real.instLT k Complex.re	HasMellin SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup f f₀ Λ	—	NoMaxOrder.exists_gt instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial mellinConvergent_of_isBigO_rpow MeasureTheory.LocallyIntegrableOn.sub hf_int MeasureTheory.locallyIntegrableOn_const Real.locallyFinite_volume hf_top hf_zero' StrongFEPair.hasMellin f_modif_aux2 hasMellin_sub
hf_int 📖	mathematical	—	MeasureTheory.LocallyIntegrableOn Real Real.measurableSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup f Set.Ioi Real.instPreorder Real.instZero MeasureTheory.MeasureSpace.volume Real.measureSpace	—	—
hf_modif_FE 📖	mathematical	Real Real.instLT Real.instZero	f_modif DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne Complex 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 Complex.instSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Complex.instNormedField Complex.instMul ε Complex.ofReal Real.instPow k g_modif	—	lt_trichotomy one_div_lt PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing one_pos Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike div_one f_modif.eq_1 Pi.add_apply Set.indicator_of_notMem Set.notMem_Ioi LT.lt.le zero_add Set.indicator_of_mem Set.mem_Ioo div_pos g_modif.eq_1 Set.mem_Ioi Set.notMem_Ioo_of_ge add_zero h_feq smul_sub Real.rpow_neg one_div_pos one_div Real.inv_rpow inv_inv div_self Real.one_rpow mul_one smul_zero lt_one_div Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval Mathlib.Tactic.Module.NF.add_eq_eval Mathlib.Tactic.Module.NF.sub_eq_eval Mathlib.Tactic.Module.NF.smul_eq_eval Mathlib.Tactic.Module.NF.atom_eq_eval Mathlib.Tactic.Module.NF.eval_algebraMap AddCommMonoid.nat_isScalarTower AddCommGroup.intIsScalarTower Mathlib.Tactic.Module.NF.sub_eq_eval₁ Mathlib.Tactic.Module.NF.zero_sub_eq_eval Mathlib.Tactic.Module.NF.zero_eq_eval Mathlib.Tactic.Module.NF.eq_cons_cons eq_natCast RingHom.instRingHomClass Nat.cast_one eq_intCast Int.cast_one Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_ne_zero LT.lt.ne' Real.rpow_pos_of_pos hε one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Complex.ofReal_inv mul_neg Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero
hf_modif_int 📖	mathematical	—	MeasureTheory.LocallyIntegrableOn Real Real.measurableSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup f_modif Set.Ioi Real.instPreorder Real.instZero MeasureTheory.MeasureSpace.volume Real.measureSpace	—	ContinuousOn.locallyIntegrableOn BorelSpace.opensMeasurable Real.borelSpace Real.locallyFinite_volume secondCountableTopologyEither_of_left instSecondCountableTopologyReal continuousOn_of_forall_continuousAt LT.lt.ne' ContinuousAt.smul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ContinuousAt.fun_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing continuousAt_const ContinuousAt.comp' Continuous.continuousAt Complex.continuous_ofReal Real.continuousAt_rpow_const measurableSet_Ioi instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid MeasureTheory.LocallyIntegrableOn.add IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.LocallyIntegrableOn.sub hf_int MeasureTheory.locallyIntegrableOn_const MeasureTheory.IntegrableOn.eq_1 MeasureTheory.integrable_indicator_iff MeasureTheory.Measure.restrict_restrict MeasureTheory.IntegrableOn.mono_set Set.inter_subset_right measurableSet_Ioo
hf_top 📖	mathematical	—	Asymptotics.IsBigO Real NormedAddCommGroup.toNorm Real.norm Filter.atTop Real.instPreorder SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup f f₀ Real.instPow	—	—
hf_zero 📖	mathematical	—	Asymptotics.IsBigO Real NormedAddCommGroup.toNorm Real.norm nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero Set.Ioi Real.instPreorder SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup f Complex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Complex.instNormedField Complex.instMul ε Complex.ofReal Real.instPow Real.instNeg k g₀	—	Asymptotics.IsBigO.comp_tendsto hg_top tendsto_inv_nhdsGT_zero Real.instIsStrictOrderedRing instOrderTopologyReal Asymptotics.IsBigO_def Asymptotics.IsBigOWith_def Filter.mp_mem Filter.univ_mem' Complex.ofReal_ne_zero LT.lt.ne' Real.rpow_pos_of_pos mul_ne_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass hε Real.rpow_neg LT.lt.le Complex.ofReal_inv mul_inv_rev inv_inv Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial norm_mul Complex.norm_real one_div Real.inv_rpow norm_inv Real.norm_of_nonneg Real.rpow_add Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero ne_of_gt Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul le_div_iff₀' PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono lt_of_le_of_ne norm_nonneg norm_ne_zero_iff norm_smul NormedSpace.toNormSMulClass smul_sub SemigroupAction.mul_smul one_smul mul_inv_cancel₀ h_feq'
hf_zero' 📖	mathematical	—	Asymptotics.IsBigO Real NormedAddCommGroup.toNorm Real.norm nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero Set.Ioi Real.instPreorder SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup f f₀ Real.instPow Real.instNeg k	—	sub_add_sub_cancel Asymptotics.IsBigO.add hf_zero Asymptotics.IsBigO.sub Asymptotics.isBigO_norm_norm SemigroupAction.mul_smul norm_smul NormedSpace.toNormSMulClass mul_comm Complex.norm_real Asymptotics.IsBigO.const_mul_left Asymptotics.isBigO_refl Asymptotics.IsBigO.of_bound eventually_nhdsWithin_iff Filter.mp_mem eventually_le_nhds instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Filter.univ_mem' le_mul_of_one_le_right IsOrderedRing.toPosMulMono Real.instIsOrderedRing norm_nonneg Real.norm_of_nonneg LT.lt.le Real.rpow_pos_of_pos Real.rpow_neg one_le_inv₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.rpow_le_one hk
hg_int 📖	mathematical	—	MeasureTheory.LocallyIntegrableOn Real Real.measurableSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup g Set.Ioi Real.instPreorder Real.instZero MeasureTheory.MeasureSpace.volume Real.measureSpace	—	—
hg_top 📖	mathematical	—	Asymptotics.IsBigO Real NormedAddCommGroup.toNorm Real.norm Filter.atTop Real.instPreorder SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup g g₀ Real.instPow	—	—
hk 📖	mathematical	—	Real Real.instLT Real.instZero k	—	—
hε 📖	—	—	—	—	—
symm_Λ₀_eq 📖	mathematical	—	Λ₀ symm AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Λ Complex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Module.toDistribMulAction NormedSpace.toModule Complex.instNormedField DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne g₀ Complex.instInv ε Complex.instSub Complex.ofReal k f₀	—	Λ₀_eq
Λ_residue_k 📖	mathematical	—	Filter.Tendsto Complex 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 Complex.instSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Complex.instNormedField Complex.instSub Complex.ofReal k Λ nhdsWithin SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Compl.compl Set Set.instCompl Set.instSingletonSet nhds ε g₀	—	smul_sub sub_self neg_smul sub_neg_eq_add zero_add Filter.Tendsto.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup Filter.Tendsto.mono_left zero_smul Continuous.tendsto Continuous.smul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul continuous_sub_right Differentiable.continuous IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalAddGroup.toContinuousAdd differentiable_Λ₀ ContinuousAt.smul Continuous.continuousAt Complex.ofReal_ne_zero LT.lt.ne' hk ContinuousAt.div₀ IsTopologicalDivisionRing.toContinuousInv₀ IsTopologicalSemiring.toContinuousMul continuousAt_const continuousAt_id' nhdsWithin_le_nhds Filter.Tendsto.congr' eventually_nhdsWithin_of_forall Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval Mathlib.Tactic.Module.NF.smul_eq_eval Mathlib.Tactic.Module.NF.atom_eq_eval Mathlib.Tactic.Module.NF.eval_algebraMap AddCommMonoid.nat_isScalarTower Mathlib.Tactic.Module.NF.eq_cons_cons eq_natCast RingHom.instRingHomClass Nat.cast_one Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul neg_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.one_eq_eval mul_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg sub_ne_zero Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul mul_neg Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_gt tendsto_const_nhds
Λ_residue_zero 📖	mathematical	—	Filter.Tendsto Complex 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 Complex.instSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Complex.instNormedField Λ nhdsWithin SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instZero Compl.compl Set Set.instCompl Set.instSingletonSet nhds NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup f₀	—	smul_sub zero_smul zero_sub sub_zero Filter.Tendsto.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup Filter.Tendsto.mono_left Continuous.tendsto Continuous.smul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul continuous_id Differentiable.continuous IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalAddGroup.toContinuousAdd differentiable_Λ₀ nhdsWithin_le_nhds Filter.Tendsto.congr' eventually_nhdsWithin_of_forall Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval Mathlib.Tactic.Module.NF.atom_eq_eval Mathlib.Tactic.Module.NF.smul_eq_eval Mathlib.Tactic.Module.NF.eval_algebraMap AddCommMonoid.nat_isScalarTower Mathlib.Tactic.Module.NF.eq_cons_cons eq_natCast RingHom.instRingHomClass Nat.cast_one Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.one_eq_eval one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst div_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval mul_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat tendsto_const_nhds ContinuousAt.smul continuousAt_id ContinuousAt.div IsTopologicalDivisionRing.toContinuousInv₀ IsTopologicalSemiring.toContinuousMul continuousAt_const Continuous.continuousAt continuous_sub_left LT.lt.ne' hk
Λ₀_eq 📖	mathematical	—	Λ₀ AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Λ Complex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Module.toDistribMulAction NormedSpace.toModule Complex.instNormedField DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne f₀ ε Complex.instSub Complex.ofReal k g₀	—	Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat add_zero Mathlib.Tactic.Abel.zero_termg

(root)

Definitions

Name	Category	Theorems
StrongFEPair 📖	CompData	—
WeakFEPair 📖	CompData	—

---

← Back to Index