Documentation Verification Report

EulerMascheroni

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

Statistics

Metric	Count
Definitions `eulerMascheroniConstant`, `eulerMascheroniSeq`, `eulerMascheroniSeq'`	3
Theorems `eulerMascheroniConstant_lt_eulerMascheroniSeq'`, `eulerMascheroniConstant_lt_two_thirds`, `eulerMascheroniSeq'_one`, `eulerMascheroniSeq'_six_lt_two_thirds`, `eulerMascheroniSeq_lt_eulerMascheroniConstant`, `eulerMascheroniSeq_lt_eulerMascheroniSeq'`, `eulerMascheroniSeq_zero`, `one_half_lt_eulerMascheroniConstant`, `one_half_lt_eulerMascheroniSeq_six`, `strictAnti_eulerMascheroniSeq'`, `strictMono_eulerMascheroniSeq`, `tendsto_eulerMascheroniSeq`, `tendsto_eulerMascheroniSeq'`, `tendsto_harmonic_sub_log`, `tendsto_harmonic_sub_log_add_one`	15
Total	18

Real

Definitions

Name	Category	Theorems
`eulerMascheroniConstant` 📖	CompOp	29 math math: `eulerMascheroniConstant_lt_two_thirds`, `Complex.digamma_one_half`, `tendsto_eulerMascheroniSeq'`, `Complex.hasDerivAt_Gammaℝ_one`, `deriv_Gamma_nat`, `tendsto_riemannZeta_sub_one_div`, `ZetaAsymptotics.tendsto_Gamma_term_aux`, `tendsto_harmonic_sub_log`, `Complex.deriv_Gamma_nat`, `ZetaAsymptotics.tendsto_riemannZeta_sub_one_div_Gammaℝ`, `Complex.hasDerivAt_Gammaℂ_one`, `ZetaAsymptotics.term_tsum_one`, `eulerMascheroniConstant_eq_neg_deriv`, `riemannZeta_one`, `one_half_lt_eulerMascheroniConstant`, `hasDerivAt_Gamma_one_half`, `eulerMascheroniConstant_lt_eulerMascheroniSeq'`, `completedRiemannZeta₀_one`, `hasDerivAt_Gamma_one`, `Complex.digamma_one`, `tendsto_eulerMascheroniSeq`, `Complex.hasDerivAt_Gamma_one`, `Complex.hasDerivAt_Gamma_one_half`, `eulerMascheroniSeq_lt_eulerMascheroniConstant`, `completedRiemannZeta_one`, `hasDerivAt_Gamma_nat`, `tendsto_harmonic_sub_log_add_one`, `ZetaAsymptotics.tendsto_riemannZeta_sub_one_div_nhds_right`, `Complex.hasDerivAt_Gamma_nat`
`eulerMascheroniSeq` 📖	CompOp	6 math math: `strictMono_eulerMascheroniSeq`, `eulerMascheroniSeq_zero`, `one_half_lt_eulerMascheroniSeq_six`, `eulerMascheroniSeq_lt_eulerMascheroniSeq'`, `tendsto_eulerMascheroniSeq`, `eulerMascheroniSeq_lt_eulerMascheroniConstant`
`eulerMascheroniSeq'` 📖	CompOp	6 math math: `tendsto_eulerMascheroniSeq'`, `strictAnti_eulerMascheroniSeq'`, `eulerMascheroniSeq_lt_eulerMascheroniSeq'`, `eulerMascheroniConstant_lt_eulerMascheroniSeq'`, `eulerMascheroniSeq'_six_lt_two_thirds`, `eulerMascheroniSeq'_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eulerMascheroniConstant_lt_eulerMascheroniSeq'` 📖	mathematical	—	`Real` `instLT` `eulerMascheroniConstant` `eulerMascheroniSeq'`	—	`lt_of_le_of_lt` `Antitone.le_of_tendsto` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `instIsOrderedAddMonoid` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `StrictAnti.antitone` `strictAnti_eulerMascheroniSeq'` `tendsto_eulerMascheroniSeq'`
`eulerMascheroniConstant_lt_two_thirds` 📖	mathematical	—	`Real` `instLT` `eulerMascheroniConstant` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`LT.lt.trans` `Nat.instAtLeastTwoHAddOfNat` `eulerMascheroniConstant_lt_eulerMascheroniSeq'` `eulerMascheroniSeq'_six_lt_two_thirds`
`eulerMascheroniSeq'_one` 📖	mathematical	—	`eulerMascheroniSeq'` `Real` `instOne`	—	`harmonic_succ` `zero_add` `Nat.cast_one` `inv_one` `Rat.cast_one` `log_one` `sub_zero`
`eulerMascheroniSeq'_six_lt_two_thirds` 📖	mathematical	—	`Real` `instLT` `eulerMascheroniSeq'` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `eulerMascheroniSeq'.eq_1` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.isNat_eq_false` `Nat.instCharZero` `Mathlib.Meta.NormNum.isNat_ofNat` `harmonic_succ` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Rat.instCharZero` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Meta.NormNum.isNat_add` `zero_add` `Mathlib.Meta.NormNum.IsNNRat.to_eq` `Mathlib.Meta.NormNum.isNNRat_add` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Rat.cast_div` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.isNat_ratCast` `sub_lt_iff_lt_add` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `sub_lt_iff_lt_add'` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `lt_log_iff_exp_lt` `Mathlib.Meta.Positivity.pos_of_isNat` `instIsOrderedRing` `instNontrivial` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_sub` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `rpow_lt_rpow` `LT.lt.le` `exp_pos` `exp_one_lt_d9` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `lt_trans` `exp_one_rpow` `rpow_lt_rpow_iff` `le_of_lt` `rpow_pos_of_pos` `Mathlib.Meta.Positivity.pos_of_isNNRat` `Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true` `Mathlib.Meta.NormNum.isNNRat_ratCast` `Mathlib.Meta.NormNum.isRat_mkRat` `Mathlib.Meta.NormNum.IsNat.to_isInt` `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.isNat_intCast` `Mathlib.Meta.NormNum.isNat_intOfNat` `rpow_mul` `div_mul_cancel₀` `ne_of_gt` `Nat.cast_ofNat` `rpow_natCast` `Mathlib.Meta.NormNum.isNNRat_lt_true` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.isNNRat_pow`
`eulerMascheroniSeq_lt_eulerMascheroniConstant` 📖	mathematical	—	`Real` `instLT` `eulerMascheroniSeq` `eulerMascheroniConstant`	—	`LT.lt.trans_le` `strictMono_eulerMascheroniSeq` `Monotone.ge_of_tendsto` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `instIsOrderedAddMonoid` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `StrictMono.monotone` `tendsto_eulerMascheroniSeq`
`eulerMascheroniSeq_lt_eulerMascheroniSeq'` 📖	mathematical	—	`Real` `instLT` `eulerMascheroniSeq` `eulerMascheroniSeq'`	—	`eq_zero_or_pos` `Nat.instCanonicallyOrderedAdd` `Rat.cast_zero` `CharP.cast_eq_zero` `CharP.ofCharZero` `RCLike.charZero_rclike` `zero_add` `log_one` `sub_self` `instIsOrderedRing` `instNontrivial` `LT.lt.ne'` `sub_lt_sub_left` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `log_lt_log` `Nat.cast_pos'` `instZeroLEOneClass` `NeZero.charZero_one` `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.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_lt_of_neg_of_le` `instIsStrictOrderedRing` `neg_neg_of_pos` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `LE.le.trans_lt` `StrictMono.monotone` `strictMono_eulerMascheroniSeq` `le_max_left` `LT.lt.trans_le` `StrictAnti.antitone` `strictAnti_eulerMascheroniSeq'` `le_max_right`
`eulerMascheroniSeq_zero` 📖	mathematical	—	`eulerMascheroniSeq` `Real` `instZero`	—	`Rat.cast_zero` `CharP.cast_eq_zero` `CharP.ofCharZero` `RCLike.charZero_rclike` `zero_add` `log_one` `sub_self`
`one_half_lt_eulerMascheroniConstant` 📖	mathematical	—	`Real` `instLT` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOne` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `eulerMascheroniConstant`	—	`LT.lt.trans` `Nat.instAtLeastTwoHAddOfNat` `one_half_lt_eulerMascheroniSeq_six` `eulerMascheroniSeq_lt_eulerMascheroniConstant`
`one_half_lt_eulerMascheroniSeq_six` 📖	mathematical	—	`Real` `instLT` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOne` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `eulerMascheroniSeq`	—	`Nat.instAtLeastTwoHAddOfNat` `eulerMascheroniSeq.eq_1` `Mathlib.Meta.NormNum.instAtLeastTwo` `harmonic_succ` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Rat.instCharZero` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.isNat_ofNat` `zero_add` `Mathlib.Meta.NormNum.IsNNRat.to_eq` `Mathlib.Meta.NormNum.isNNRat_add` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Rat.cast_div` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.isNat_ratCast` `Nat.cast_one` `lt_sub_iff_add_lt` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `lt_sub_iff_add_lt'` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `log_lt_iff_lt_exp` `Mathlib.Meta.Positivity.pos_of_isNat` `instIsOrderedRing` `instNontrivial` `lt_of_lt_of_le` `Finset.sum_range_succ` `Finset.sum_congr` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_sub` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.isNNRat_pow` `Mathlib.Meta.NormNum.natPow_zero` `div_one` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Meta.NormNum.natPow_one` `mul_one` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Mathlib.Meta.NormNum.IsNatPowT.bit1` `Mathlib.Meta.NormNum.IsNatPowT.trans` `Mathlib.Meta.NormNum.isNNRat_lt_true` `instIsStrictOrderedRing` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `sum_le_exp_of_nonneg` `Mathlib.Meta.NormNum.isRat_le_true` `Nat.cast_zero`
`strictAnti_eulerMascheroniSeq'` 📖	mathematical	—	`StrictAnti` `Real` `Nat.instPreorder` `instPreorder` `eulerMascheroniSeq'`	—	`strictAnti_nat_of_succ_lt` `zero_add` `harmonic_succ` `Nat.cast_one` `inv_one` `Rat.cast_one` `log_one` `sub_zero` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `instZeroLEOneClass` `RCLike.charZero_rclike` `eq_false_intro` `LT.lt.ne'` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `sub_sub_sub_comm` `Rat.cast_add` `sub_sub` `sub_self` `zero_sub` `sub_eq_add_neg` `neg_sub` `sub_eq_neg_add` `log_div` `ne_of_gt` `Nat.cast_pos'` `NeZero.charZero_one` `add_pos'` `Nat.instIsOrderedAddMonoid` `Mathlib.Meta.Positivity.pos_of_isNat` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `neg_lt_neg_iff` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `log_inv` `LT.lt.trans_le` `log_lt_sub_one_of_pos` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `div_pos` `Nat.cast_add` `inv_div` `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.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.subst_add` `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.one_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `instIsOrderedRing` `instNontrivial` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `le_of_eq` `Rat.cast_inv` `Rat.cast_natCast` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `mul_neg` `sub_add_cancel_left`
`strictMono_eulerMascheroniSeq` 📖	mathematical	—	`StrictMono` `Real` `Nat.instPreorder` `instPreorder` `eulerMascheroniSeq`	—	`strictMono_nat_of_lt_succ` `eulerMascheroniSeq.eq_1` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `sub_sub_sub_comm` `harmonic_succ` `add_comm` `Rat.cast_add` `RCLike.charZero_rclike` `add_sub_cancel_right` `log_div` `ne_of_gt` `add_pos'` `Nat.cast_pos'` `instZeroLEOneClass` `NeZero.charZero_one` `Right.add_pos_of_nonneg_of_pos` `Nat.instIsOrderedAddMonoid` `zero_le` `Nat.instCanonicallyOrderedAdd` `Mathlib.Meta.Positivity.pos_of_isNat` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `instIsOrderedRing` `instNontrivial` `Nat.cast_one` `Nat.cast_nonneg'` `add_div` `Nat.cast_add_one` `div_self` `one_div` `Rat.cast_inv` `Rat.cast_one` `Rat.cast_natCast` `LT.lt.trans_le` `log_lt_sub_one_of_pos` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `lt_add_of_pos_right` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `le_of_eq` `add_sub_cancel_left`
`tendsto_eulerMascheroniSeq` 📖	mathematical	—	`Filter.Tendsto` `Real` `eulerMascheroniSeq` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `eulerMascheroniConstant`	—	`tendsto_atTop_ciSup` `LinearOrder.supConvergenceClass` `instOrderTopologyReal` `StrictMono.monotone` `strictMono_eulerMascheroniSeq` `LT.lt.le` `eulerMascheroniSeq_lt_eulerMascheroniSeq'` `eulerMascheroniConstant.eq_1` `Filter.Tendsto.limUnder_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat`
`tendsto_eulerMascheroniSeq'` 📖	mathematical	—	`Filter.Tendsto` `Real` `eulerMascheroniSeq'` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `eulerMascheroniConstant`	—	`tendsto_log_comp_add_sub_log` `Filter.Tendsto.congr'` `Filter.Tendsto.comp` `tendsto_natCast_atTop_atTop` `instIsOrderedRing` `instArchimedean` `Filter.mp_mem` `Filter.eventually_ne_atTop` `instNoTopOrderOfNoMaxOrder` `Nat.instNoMaxOrder` `Filter.univ_mem'` `eq_false_intro` `sub_sub_sub_cancel_left` `sub_add_cancel` `zero_add` `Filter.Tendsto.add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `tendsto_eulerMascheroniSeq`
`tendsto_harmonic_sub_log` 📖	mathematical	—	`Filter.Tendsto` `Real` `instSub` `instRatCast` `harmonic` `log` `instNatCast` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `eulerMascheroniConstant`	—	`Filter.Tendsto.congr'` `tendsto_eulerMascheroniSeq'` `Filter.mp_mem` `Filter.eventually_ne_atTop` `instNoTopOrderOfNoMaxOrder` `Nat.instNoMaxOrder` `Filter.univ_mem'`
`tendsto_harmonic_sub_log_add_one` 📖	mathematical	—	`Filter.Tendsto` `Real` `instSub` `instRatCast` `harmonic` `log` `instAdd` `instNatCast` `instOne` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `eulerMascheroniConstant`	—	`tendsto_eulerMascheroniSeq`

---

← Back to Index