ZetaAsymp

📁 Source: Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean

Statistics

Metric	Count
Definitions term, term_sum, term_tsum	3
Theorems continuousOn_term, continuousOn_term_tsum, tendsto_Gamma_term_aux, tendsto_riemannZeta_sub_one_div_Gammaℝ, tendsto_riemannZeta_sub_one_div_nhds_right, term_nonneg, term_of_lt, term_one, term_sum_of_lt, term_sum_one, term_tsum_of_lt, term_tsum_one, term_welldef, zeta_limit_aux1, completedRiemannZeta_one, completedRiemannZeta₀_one, isBigO_riemannZeta_sub_one_div, riemannZeta_one, riemannZeta_one_ne_zero, tendsto_riemannZeta_sub_one_div	20
Total	23

ZetaAsymptotics

Definitions

Name	Category	Theorems
term 📖	CompOp	5 math math: continuousOn_term, term_one, term_tsum_one, term_nonneg, term_of_lt
term_sum 📖	CompOp	2 math math: term_sum_of_lt, term_sum_one
term_tsum 📖	CompOp	3 math math: term_tsum_of_lt, zeta_limit_aux1, continuousOn_term_tsum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousOn_term 📖	mathematical	—	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace term Set.Ici Real.instPreorder Real.instOne	—	intervalIntegral.integral_of_le le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one 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.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_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.Linarith.add_neg Real.instIsStrictOrderedRing neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing MeasureTheory.continuousOn_of_dominated TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace Nat.instAtLeastTwoHAddOfNat term_welldef IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Nat.instNoMaxOrder Nat.instCanonicallyOrderedAdd LT.lt.trans_le zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_restrict_iff' measurableSet_Ioc BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Filter.univ_mem' lt_of_le_of_lt Nat.cast_add IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT Real.norm_of_nonneg div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono sub_nonneg LT.lt.le le_of_lt Real.rpow_pos_of_pos lt_trans Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Nat.cast_add_one div_le_div₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono le_refl Real.rpow_le_rpow_of_exponent_le Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.sub_nonpos_of_le MeasureTheory.IntegrableOn.eq_1 intervalIntegrable_iff_integrableOn_Ioc_of_le Real.rpow_natCast continuousOn_of_forall_continuousAt ContinuousAt.div IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal continuousAt_const ContinuousAt.rpow ContinuousAt.add IsTopologicalSemiring.toContinuousAdd continuousAt_id lt_of_not_ge Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.mul_neg Mathlib.Meta.NormNum.isNat_lt_true LT.lt.ne' LT.lt.trans Nat.cast_pos
continuousOn_term_tsum 📖	mathematical	—	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace term_tsum Set.Ici Real.instPreorder Real.instOne	—	continuousOn_tsum Real.instCompleteSpace continuousOn_term HasSum.summable term_tsum_one term.eq_1 Real.norm_of_nonneg intervalIntegral.integral_of_le le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one 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.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_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.Linarith.add_neg Real.instIsStrictOrderedRing neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing MeasureTheory.setIntegral_nonneg measurableSet_Ioc BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.rpow_nonneg Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Tactic.Linarith.natCast_nonneg MeasureTheory.setIntegral_mono_on IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule instClosedIciTopology term_welldef LT.lt.trans_le zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike le_trans Nat.cast_add covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le LT.lt.le div_le_div₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono sub_nonneg le_refl Real.rpow_pos_of_pos lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Real.rpow_le_rpow_of_exponent_le add_le_add_left
tendsto_Gamma_term_aux 📖	mathematical	—	Filter.Tendsto Complex Complex.instSub DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Complex.Gammaℝ nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Compl.compl Set Set.instCompl Set.instSingletonSet nhds Complex.instNeg Complex.instAdd Complex.ofReal Real.eulerMascheroniConstant Complex.log Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi	—	IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Nat.instAtLeastTwoHAddOfNat Complex.hasDerivAt_Gammaℝ_one Filter.Tendsto.div IsTopologicalDivisionRing.toContinuousInv₀ IsTopologicalSemiring.toContinuousMul Complex.Gammaℝ_one slope_fun_def_field IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul hasDerivAt_iff_tendsto_slope Filter.Tendsto.mono_left ContinuousAt.tendsto HasDerivAt.continuousAt nhdsWithin_le_nhds Eq.trans_ne one_ne_zero NeZero.charZero_one Complex.instCharZero Filter.Tendsto.congr' IsOpen.mem_nhds Continuous.isOpen_preimage Complex.continuous_re isOpen_Ioi instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike Filter.EventuallyEq.eq_1 eventually_nhdsWithin_iff Filter.mp_mem Filter.univ_mem' Pi.div_apply sub_div div_right_comm sub_div' Complex.Gammaℝ_ne_zero_of_re_pos one_mul div_one
tendsto_riemannZeta_sub_one_div_Gammaℝ 📖	mathematical	—	Filter.Tendsto Complex Complex.instSub riemannZeta DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Complex.Gammaℝ nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Compl.compl Set Set.instCompl Set.instSingletonSet nhds Complex.ofReal Real.eulerMascheroniConstant Complex.log Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi	—	Nat.instAtLeastTwoHAddOfNat Filter.Tendsto.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing tendsto_riemannZeta_sub_one_div tendsto_Gamma_term_aux Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.atom_pf' Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one add_zero 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.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.RingNF.nnrat_rawCast Mathlib.Tactic.RingNF.rat_rawCast_neg Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_add Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz sub_add_sub_cancel
tendsto_riemannZeta_sub_one_div_nhds_right 📖	mathematical	—	Filter.Tendsto Real Complex Complex.instSub riemannZeta Complex.ofReal DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instOne Set.Ioi Real.instPreorder nhds SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Real.eulerMascheroniConstant	—	Filter.Tendsto.congr' Filter.mp_mem self_mem_nhdsWithin Filter.univ_mem' zeta_limit_aux1 Filter.Tendsto.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal tendsto_const_nhds one_mul Filter.Tendsto.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Filter.Tendsto.mono_left Filter.tendsto_id nhdsWithin_le_nhds ContinuousOn.continuousWithinAt continuousOn_term_tsum Set.self_mem_Ici nhdsWithin_mono Set.Ioi_subset_Ici_self HasSum.tsum_eq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SummationFilter.instNeBotUnconditional term_tsum_one eq_sub_iff_add_eq' eq_sub_iff_add_eq term_tsum.eq_1 Filter.Tendsto.comp Continuous.tendsto Complex.continuous_ofReal Complex.ofReal_sub Complex.ofReal_tsum Complex.ofReal_div zeta_eq_tsum_one_div_nat_add_one_cpow Complex.ofReal_cpow le_of_lt Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Nat.cast_nonneg' Real.instZeroLEOneClass Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Nat.cast_add Complex.ofReal_add
term_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero term	—	term.eq_1 intervalIntegral.integral_of_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Real.instZeroLEOneClass MeasureTheory.setIntegral_nonneg measurableSet_Ioc BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf 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.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Real.rpow_nonneg Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Tactic.Linarith.natCast_nonneg
term_of_lt 📖	mathematical	Real Real.instLT Real.instOne	term Real.instSub Real.instMul DivInvMonoid.toDiv Real.instDivInvMonoid Real.instPow Real.instNatCast Real.instAdd	—	LT.lt.trans_le Nat.cast_pos Real.instIsOrderedRing Real.instNontrivial Set.uIcc_of_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Real.instZeroLEOneClass intervalIntegral.integral_congr sub_div Real.rpow_add_one LT.lt.ne' mul_comm div_div div_self Real.rpow_neg LT.lt.le one_div div_eq_mul_inv intervalIntegral.integral_sub intervalIntegral.intervalIntegrable_rpow Real.locallyFinite_volume Set.notMem_uIcc_of_lt Nat.cast_zero RCLike.charZero_rclike lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one 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.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Tactic.Linarith.natCast_nonneg IntervalIntegrable.const_mul intervalIntegral.integral_const_mul lt_irrefl integral_rpow Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.sub_neg_of_lt neg_eq_zero sub_eq_zero_of_eq Mathlib.Tactic.Linarith.add_neg div_neg neg_div mul_one_div neg_sub Nat.cast_nonneg le_of_not_gt div_mul_eq_mul_div mul_div_assoc
term_one 📖	mathematical	—	term Real Real.instOne Real.instSub Real.log Real.instAdd Real.instNatCast DivInvMonoid.toDiv Real.instDivInvMonoid	—	LT.lt.trans_le Nat.cast_pos Real.instIsOrderedRing Real.instNontrivial Set.uIcc_of_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Real.instZeroLEOneClass Nat.instAtLeastTwoHAddOfNat one_add_one_eq_two Real.rpow_natCast intervalIntegral.integral_congr Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.atom_eq_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.pow_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' Mathlib.Tactic.FieldSimp.zpow'_ofNat Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf 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.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul 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 RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one mul_one_div intervalIntegral.integral_sub intervalIntegral.intervalIntegrable_one_div Real.locallyFinite_volume LT.lt.ne' continuousOn_id' IntervalIntegrable.const_mul sq_pos_of_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing ContinuousOn.pow IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal intervalIntegral.integral_const_mul integral_one_div_of_pos Nat.cast_pos' NeZero.charZero_one add_pos' Mathlib.Meta.Positivity.pos_of_isNat Nat.cast_one Real.log_div ne_of_gt Real.rpow_neg LT.lt.le one_div Nat.cast_two integral_rpow Set.notMem_uIcc_of_lt sub_div Mathlib.Meta.NormNum.isInt_eq_true Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.instAtLeastTwo div_neg neg_sub_neg Real.rpow_neg_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Mathlib.Tactic.FieldSimp.NF.cons_ne_zero add_sub_cancel_left
term_sum_of_lt 📖	mathematical	Real Real.instLT Real.instOne	term_sum Real.instSub Real.instMul DivInvMonoid.toDiv Real.instDivInvMonoid Real.instPow Real.instAdd Real.instNatCast Finset.sum Real.instAddCommMonoid Finset.range	—	term_of_lt IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Nat.instNoMaxOrder Nat.instCanonicallyOrderedAdd Finset.sum_sub_distrib Finset.sum_congr one_div Nat.cast_add Nat.cast_one CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike zero_add Real.one_rpow div_self NeZero.charZero_one sub_self MulZeroClass.mul_zero Finset.sum_range_succ Nat.cast_add_one Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf 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_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.atom_pf' Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one add_zero Mathlib.Tactic.RingNF.int_rawCast_neg 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 Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.RingNF.mul_neg Mathlib.Tactic.RingNF.add_neg mul_comm div_eq_mul_inv div_one sub_eq_add_neg add_assoc Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.mul_one
term_sum_one 📖	mathematical	—	term_sum Real Real.instOne Real.instAdd Real.instSub Real.log Real.instNatCast Real.instRatCast harmonic	—	Finset.sum_range_zero harmonic_succ Nat.cast_zero zero_add Nat.cast_one inv_one Rat.cast_one Real.log_one sub_add_cancel Finset.sum_range_succ term_one Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid zero_le Nat.instCanonicallyOrderedAdd Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_add Rat.cast_add RCLike.charZero_rclike Rat.cast_inv Rat.cast_natCast Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf' Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one add_zero 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_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg Mathlib.Tactic.RingNF.add_neg Mathlib.Tactic.RingNF.add_assoc_rev Mathlib.Tactic.Ring.inv_congr
term_tsum_of_lt 📖	mathematical	Real Real.instLT Real.instOne	term_tsum Real.instSub DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul tsum Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instPow Real.instAdd Real.instNatCast SummationFilter.unconditional	—	HasSum.tsum_eq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SummationFilter.instNeBotUnconditional hasSum_iff_tendsto_nat_of_nonneg term_nonneg term_sum_of_lt Filter.Tendsto.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal one_div MulZeroClass.mul_zero sub_zero mul_sub mul_one tendsto_const_nhds Filter.Tendsto.const_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Filter.Tendsto.div_atTop Real.instIsStrictOrderedRing instOrderTopologyReal Filter.Tendsto.comp tendsto_rpow_atTop lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.atom_pf 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_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Filter.tendsto_atTop_add_const_right Real.instIsOrderedAddMonoid tendsto_natCast_atTop_atTop Real.instArchimedean HasSum.tendsto_sum_nat Summable.hasSum summable_nat_add_iff Real.summable_one_div_nat_rpow tendsto_of_tendsto_of_tendsto_of_le_of_le Real.zero_rpow Mathlib.Tactic.Linarith.lt_of_lt_of_eq sub_eq_zero_of_eq Filter.Tendsto.rpow_const tendsto_const_div_atTop_nhds_zero_nat RCLike.charZero_rclike NNRat.instContinuousSMulOfIsScalarTowerOfRat IsScalarTower.nnrat Rat.instCharZero NNRat.instContinuousSMulRatReal Filter.tendsto_add_atTop_nat le_of_not_gt Mathlib.Tactic.Linarith.add_neg Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono Real.instZeroLEOneClass Real.rpow_pos_of_pos Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Mathlib.Tactic.Ring.neg_congr neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one le_of_lt le_of_eq Real.rpow_sub_one ne_of_gt div_pos Nat.cast_pos' NeZero.charZero_one Nat.instIsOrderedAddMonoid zero_le Nat.instCanonicallyOrderedAdd IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial div_mul div_one mul_comm Real.inv_rpow div_eq_mul_inv
term_tsum_one 📖	mathematical	—	HasSum Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace term Real.instOne Real.instSub Real.eulerMascheroniConstant SummationFilter.unconditional	—	hasSum_iff_tendsto_nat_of_nonneg term_nonneg term_sum_one sub_eq_neg_add Filter.Tendsto.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Filter.Tendsto.neg IsTopologicalRing.toContinuousNeg Filter.Tendsto.comp Real.tendsto_eulerMascheroniSeq' Filter.tendsto_add_atTop_nat Filter.Tendsto.congr' Filter.Eventually.of_forall Nat.cast_add Nat.cast_one Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat tendsto_const_nhds
term_welldef 📖	mathematical	Real Real.instLT Real.instZero	IntervalIntegrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup Real.normedAddCommGroup DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub Real.instNatCast Real.instPow Real.instAdd Real.instOne MeasureTheory.MeasureSpace.volume Real.measureSpace	—	intervalIntegrable_iff_integrableOn_Icc_of_le PseudoEMetricSpace.pseudoMetrizableSpace Real.noAtoms_volume le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one 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.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_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.Linarith.add_neg Real.instIsStrictOrderedRing neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing enorm_ne_top ContinuousOn.integrableOn_Icc BorelSpace.opensMeasurable Real.borelSpace MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace continuousOn_of_forall_continuousAt ContinuousAt.div IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousAt.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal continuousAt_id' continuousAt_const ContinuousAt.rpow_const continuousAt_id LT.lt.ne' Real.rpow_pos_of_pos LT.lt.trans_le Nat.cast_pos Real.instNontrivial
zeta_limit_aux1 📖	mathematical	Real Real.instLT Real.instOne	Real.instSub tsum Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DivInvMonoid.toDiv Real.instDivInvMonoid Real.instPow Real.instAdd Real.instNatCast SummationFilter.unconditional Real.instMul term_tsum	—	term_tsum_of_lt Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.atom_pf 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_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing sub_eq_zero_of_eq 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.div_eq_eval Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval ne_of_gt lt_trans Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Tactic.FieldSimp.NF.mul_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.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.mul_congr 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_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
completedRiemannZeta_one 📖	mathematical	—	completedRiemannZeta Complex Complex.instOne DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instSub Complex.ofReal Real.eulerMascheroniConstant Complex.log Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi	—	Nat.instAtLeastTwoHAddOfNat riemannZeta_def_of_ne_zero one_ne_zero NeZero.charZero_one Complex.instCharZero Complex.Gammaℝ_one div_one riemannZeta_one
completedRiemannZeta₀_one 📖	mathematical	—	completedRiemannZeta₀ Complex Complex.instOne Complex.instAdd DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instSub Complex.ofReal Real.eulerMascheroniConstant Complex.log Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi	—	completedRiemannZeta_eq Nat.instAtLeastTwoHAddOfNat eq_sub_iff_add_eq sub_zero div_one div_zero sub_self completedRiemannZeta_one
isBigO_riemannZeta_sub_one_div 📖	mathematical	—	Asymptotics.IsBigO Complex Complex.instNorm nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instOne Complex.instSub riemannZeta DivInvMonoid.toDiv Complex.instDivInvMonoid	—	Filter.Tendsto.isBigO_one tendsto_riemannZeta_sub_one_div
riemannZeta_one 📖	mathematical	—	riemannZeta Complex Complex.instOne DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instSub Complex.ofReal Real.eulerMascheroniConstant Complex.log Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi	—	Filter.Tendsto.mono_left HurwitzZeta.tendsto_hurwitzZetaEven_sub_one_div_nhds_one nhdsWithin_le_nhds tendsto_nhds_unique Complex.instT2Space Nat.instAtLeastTwoHAddOfNat PerfectSpace.not_isolated instPerfectSpace div_right_comm ZetaAsymptotics.tendsto_riemannZeta_sub_one_div_Gammaℝ
riemannZeta_one_ne_zero 📖	—	—	—	—	Nat.instAtLeastTwoHAddOfNat div_ne_zero LT.lt.ne sub_lt_zero IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid lt_trans LT.lt.trans Real.eulerMascheroniConstant_lt_two_thirds Mathlib.Meta.NormNum.isNNRat_lt_true Real.instIsStrictOrderedRing instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Nat.cast_one Real.lt_log_iff_exp_lt mul_pos IsStrictOrderedRing.toPosMulStrictMono Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Real.pi_pos LT.lt.trans_le Real.exp_one_lt_d9 Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true Mathlib.Meta.NormNum.isNNRat_ratCast Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_mkRat Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.IsNat.raw_refl Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.trans Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Meta.NormNum.IsNatPowT.bit1 Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.isNat_intCast Mathlib.Meta.NormNum.isNat_intOfNat Rat.instCharZero Mathlib.Meta.NormNum.isNat_mul mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.two_le_pi two_ne_zero CharZero.NeZero.two riemannZeta_one Complex.ofReal_div Complex.ofReal_sub Complex.ofReal_log le_of_lt Complex.ofReal_mul
tendsto_riemannZeta_sub_one_div 📖	mathematical	—	Filter.Tendsto Complex Complex.instSub riemannZeta DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Compl.compl Set Set.instCompl Set.instSingletonSet nhds Complex.ofReal Real.eulerMascheroniConstant	—	AddTorsor.nonempty Complex.tendsto_limUnder_of_differentiable_on_punctured_nhds_of_isLittleO Complex.instCompleteSpace Filter.mp_mem self_mem_nhdsWithin Filter.univ_mem' DifferentiableAt.sub differentiableAt_riemannZeta DifferentiableAt.div differentiableAt_const DifferentiableAt.sub_const differentiableAt_id sub_ne_zero Set.mem_compl_singleton_iff Asymptotics.isLittleO_of_tendsto' sub_eq_zero inv_eq_zero div_eq_mul_inv inv_inv sub_mul Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one 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.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Filter.Tendsto.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup mul_comm mul_sub riemannZeta_residue_one Filter.Tendsto.congr' 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.subst_sub Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.one_div_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 one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Filter.Tendsto.mono_left tendsto_const_nhds nhdsWithin_le_nhds Filter.Tendsto.const_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Filter.tendsto_id Filter.Tendsto.comp tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within Continuous.tendsto Complex.continuous_ofReal Complex.ofReal_one ne_of_gt tendsto_nhds_unique Complex.instT2Space nhdsGT_neBot instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial ZetaAsymptotics.tendsto_riemannZeta_sub_one_div_nhds_right

---

← Back to Index