Stirling

📁 Source: Mathlib/Analysis/SpecialFunctions/Stirling.lean

Statistics

Metric	Count
Definitions `stirlingSeq`	1
Theorems `factorial_isEquivalent_stirling`, `le_factorial_stirling`, `le_log_factorial_stirling`, `log_stirlingSeq'_antitone`, `log_stirlingSeq_bounded_aux`, `log_stirlingSeq_bounded_by_constant`, `log_stirlingSeq_diff_hasSum`, `log_stirlingSeq_diff_le_geo_sum`, `log_stirlingSeq_formula`, `log_stirlingSeq_sub_log_stirlingSeq_succ`, `second_wallis_limit`, `sqrt_pi_le_stirlingSeq`, `stirlingSeq'_antitone`, `stirlingSeq'_bounded_by_pos_constant`, `stirlingSeq'_pos`, `stirlingSeq_has_pos_limit_a`, `stirlingSeq_one`, `stirlingSeq_pow_four_div_stirlingSeq_pow_two_eq`, `stirlingSeq_zero`, `tendsto_self_div_two_mul_self_add_one`, `tendsto_stirlingSeq_sqrt_pi`	21
Total	22

Stirling

Definitions

Name	Category	Theorems
`stirlingSeq` 📖	CompOp	16 math math: `log_stirlingSeq_bounded_aux`, `log_stirlingSeq_sub_log_stirlingSeq_succ`, `log_stirlingSeq_formula`, `log_stirlingSeq_diff_hasSum`, `stirlingSeq_one`, `stirlingSeq'_antitone`, `sqrt_pi_le_stirlingSeq`, `stirlingSeq'_bounded_by_pos_constant`, `log_stirlingSeq_bounded_by_constant`, `log_stirlingSeq'_antitone`, `stirlingSeq'_pos`, `stirlingSeq_zero`, `log_stirlingSeq_diff_le_geo_sum`, `stirlingSeq_pow_four_div_stirlingSeq_pow_two_eq`, `tendsto_stirlingSeq_sqrt_pi`, `stirlingSeq_has_pos_limit_a`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`factorial_isEquivalent_stirling` 📖	mathematical	—	`Asymptotics.IsEquivalent` `Real` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Filter.atTop` `Nat.instPreorder` `Real.instNatCast` `Nat.factorial` `Real.instMul` `Real.sqrt` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `Monoid.toNatPow` `Real.instMonoid` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.exp` `Real.instOne`	—	`Asymptotics.isEquivalent_of_tendsto_one` `Nat.instAtLeastTwoHAddOfNat` `ne_of_gt` `Real.sqrt_pos_of_pos` `Real.pi_pos` `div_self` `mul_right_comm` `Real.sqrt_mul'` `Real.instIsOrderedRing` `Real.sqrt_mul` `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.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_subst` `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.cons_ne_zero` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Real.instNontrivial` `RCLike.charZero_rclike` `Mathlib.Meta.Positivity.pos_of_isNat` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `Nat.factorial_pos` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `one_div` `Filter.Tendsto.div` `IsTopologicalDivisionRing.toContinuousInv₀` `instIsTopologicalDivisionRingReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `tendsto_stirlingSeq_sqrt_pi` `tendsto_const_nhds`
`le_factorial_stirling` 📖	mathematical	—	`Real` `Real.instLE` `Real.instMul` `Real.sqrt` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `Monoid.toNatPow` `Real.instMonoid` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.exp` `Real.instOne` `Nat.factorial`	—	`Nat.instAtLeastTwoHAddOfNat` `eq_or_ne` `CharP.cast_eq_zero` `CharP.ofCharZero` `RCLike.charZero_rclike` `MulZeroClass.mul_zero` `Real.sqrt_zero` `zero_div` `pow_zero` `mul_one` `Nat.cast_one` `Real.instZeroLEOneClass` `Real.sqrt_mul'` `Real.instIsOrderedRing` `Real.sqrt_mul` `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` `Mathlib.Tactic.Ring.pow_congr` `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` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `le_div_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.sqrt_pos_of_pos` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `NeZero.charZero_one` `lt_of_le_of_ne'` `zero_le` `Nat.instCanonicallyOrderedAdd` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `Real.exp_pos` `sqrt_pi_le_stirlingSeq`
`le_log_factorial_stirling` 📖	mathematical	—	`Real` `Real.instLE` `Real.instAdd` `Real.instSub` `Real.instMul` `Real.instNatCast` `Real.log` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `Nat.factorial`	—	`Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `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` `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_gt` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Nat.cast_one` `Real.log_mul` `ne_of_gt` `Real.sqrt_pos_of_pos` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Real.pi_pos` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `lt_of_le_of_ne'` `zero_le` `Nat.instCanonicallyOrderedAdd` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `Real.exp_pos` `Real.log_sqrt` `le_of_lt` `Real.log_pow` `Real.log_div` `Real.log_exp` `Real.log_le_log` `le_factorial_stirling`
`log_stirlingSeq'_antitone` 📖	mathematical	—	`Antitone` `Real` `Nat.instPreorder` `Real.instPreorder` `Real.log` `stirlingSeq`	—	`antitone_nat_of_succ_le` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `HasSum.nonneg` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Nat.instAtLeastTwoHAddOfNat` `SummationFilter.instNeBotUnconditional` `le_of_lt` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `add_pos'` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_pos'` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Right.add_pos_of_nonneg_of_pos` `Nat.instIsOrderedAddMonoid` `zero_le` `Nat.instCanonicallyOrderedAdd` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instNontrivial` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `log_stirlingSeq_diff_hasSum`
`log_stirlingSeq_bounded_aux` 📖	mathematical	—	`Real` `Real.instLE` `Real.instSub` `Real.log` `stirlingSeq`	—	`Nat.instAtLeastTwoHAddOfNat` `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.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.pow_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `div_one` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `ne_of_gt` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Right.add_pos_of_nonneg_of_pos` `covariant_swap_add_of_covariant_add` `Nat.instIsOrderedAddMonoid` `zero_le` `Nat.instCanonicallyOrderedAdd` `Mathlib.Meta.Positivity.pos_of_isNat` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.isNat_eq_false` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.cast_pos` `Nat.cast_one` `log_stirlingSeq_sub_log_stirlingSeq_succ` `summable_nat_add_iff` `instIsTopologicalAddGroupReal` `Real.summable_one_div_nat_pow` `one_lt_two` `Nat.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Summable.sum_le_tsum` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `SummationFilter.instNeBotUnconditional` `SummationFilter.instLeAtTopUnconditional` `le_of_lt` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.instIsOrderedRing` `Real.instNontrivial` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `Finset.sum_range_sub'` `Finset.sum_le_sum` `Finset.mul_sum` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono`
`log_stirlingSeq_bounded_by_constant` 📖	mathematical	—	`Real` `Real.instLE` `Real.log` `stirlingSeq`	—	`log_stirlingSeq_bounded_aux` `sub_le_comm` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`
`log_stirlingSeq_diff_hasSum` 📖	mathematical	—	`HasSum` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instMul` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `Real.instAdd` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Monoid.toNatPow` `Real.instMonoid` `Real.instSub` `Real.log` `stirlingSeq` `SummationFilter.unconditional`	—	`Nat.instAtLeastTwoHAddOfNat` `hasSum_nat_add_iff` `instIsTopologicalAddGroupReal` `pow_mul` `pow_add` `Nat.cast_add` `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.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `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_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `Mathlib.Meta.NormNum.isNat_eq_false` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_zero` `Mathlib.Tactic.FieldSimp.NF.pow_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` `ne_of_gt` `add_pos'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Right.add_pos_of_nonneg_of_pos` `covariant_swap_add_of_covariant_add` `Nat.cast_nonneg'` `Real.instZeroLEOneClass` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `mul_nonneg` `IsOrderedRing.toPosMulMono` `le_of_lt` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `log_stirlingSeq_formula` `Nat.cast_mul` `Nat.cast_succ` `Real.log_mul` `Nat.cast_pos'` `NeZero.charZero_one` `Nat.factorial_pos` `Real.log_div` `Real.exp_pos` `Real.log_exp` `Finset.sum_singleton` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsRat.to_raw_eq` `Mathlib.Meta.NormNum.isRat_mul` `Mathlib.Meta.NormNum.IsInt.to_isRat` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz` `Mathlib.Tactic.Ring.neg_zero` `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` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsRat.to_isInt` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf'` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Meta.NormNum.isNNRat_add` `HasSum.mul_left` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Real.hasSum_log_one_add_inv` `Nat.cast_add_one_pos`
`log_stirlingSeq_diff_le_geo_sum` 📖	mathematical	—	`Real` `Real.instLE` `Real.instSub` `Real.log` `stirlingSeq` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Monoid.toNatPow` `Real.instMonoid` `Real.instOne` `Real.instAdd` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `sq_nonneg` `AddGroup.existsAddOfLE` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `HasSum.mul_left` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `hasSum_geometric_of_lt_one` `one_div` `inv_pow` `inv_lt_one_of_one_lt₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.instZeroLEOneClass` `one_lt_pow₀` `lt_add_of_pos_left` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `mul_pos` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_pos'` `NeZero.charZero_one` `RCLike.charZero_rclike` `Right.add_pos_of_nonneg_of_pos` `Nat.instIsOrderedAddMonoid` `zero_le` `Nat.instCanonicallyOrderedAdd` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instNontrivial` `two_ne_zero` `mul_le_of_le_one_left` `IsOrderedRing.toMulPosMono` `pow_nonneg` `inv_le_one_of_one_le₀` `le_add_of_nonneg_left` `le_of_lt` `hasSum_le` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `log_stirlingSeq_diff_hasSum` `SummationFilter.instNeBotUnconditional`
`log_stirlingSeq_formula` 📖	mathematical	—	`Real.log` `stirlingSeq` `Real` `Real.instSub` `Real.instNatCast` `Nat.factorial` `Real.instMul` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat` `Real.exp`	—	`Nat.instAtLeastTwoHAddOfNat` `stirlingSeq_zero` `Real.log_zero` `Nat.cast_one` `Real.log_one` `one_div` `CharP.cast_eq_zero` `CharP.ofCharZero` `RCLike.charZero_rclike` `MulZeroClass.mul_zero` `sub_self` `zero_div` `stirlingSeq.eq_1` `Real.log_div` `ne_of_gt` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `Nat.factorial_pos` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.sqrt_pos_of_pos` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Right.add_pos_of_nonneg_of_pos` `covariant_swap_add_of_covariant_add` `Nat.instIsOrderedAddMonoid` `zero_le` `Nat.instCanonicallyOrderedAdd` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instNontrivial` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `Real.exp_pos` `Real.log_mul` `Real.sqrt_eq_rpow` `Real.log_rpow` `Real.log_pow` `tsub_tsub` `AddGroup.toOrderedSub`
`log_stirlingSeq_sub_log_stirlingSeq_succ` 📖	mathematical	—	`Real` `Real.instLE` `Real.instSub` `Real.log` `stirlingSeq` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Monoid.toNatPow` `Real.instMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `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` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.pow_nat` `Mathlib.Tactic.Ring.coeff_one` `Mathlib.Tactic.Ring.pow_one_cast` `Mathlib.Tactic.Ring.pow_bit0` `Mathlib.Tactic.Ring.pow_one` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Tactic.Ring.pow_zero` `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.Tactic.Ring.neg_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `add_zero` `Mathlib.Tactic.RingNF.add_assoc_rev` `add_pos_of_pos_of_nonneg` `mul_nonneg` `IsOrderedRing.toPosMulMono` `le_of_lt` `Even.pow_nonneg` `IsStrictOrderedRing.toIsOrderedRing` `AddGroup.existsAddOfLE` `even_two_mul` `LE.le.trans` `log_stirlingSeq_diff_le_geo_sum` `Nat.cast_add` `Mathlib.Tactic.FieldSimp.le_eq_cancel_le` `PosMulStrictMono.toPosMulMono` `PosMulStrictMono.toPosMulReflectLE` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.pow_eq_eval` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `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.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `ne_of_gt` `add_pos'` `Mathlib.Tactic.FieldSimp.zpow'_ofNat` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂` `LT.lt.ne'` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.cons_pos` `PosMulReflectLE.toPosMulReflectLT` `zero_lt_one` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.one_mul` `RCLike.charZero_rclike`
`second_wallis_limit` 📖	mathematical	`Filter.Tendsto` `Real` `stirlingSeq` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`Real.Wallis.W` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Monoid.toNatPow` `Real.instMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Filter.Tendsto.congr'` `Nat.instAtLeastTwoHAddOfNat` `Filter.eventually_atTop` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `stirlingSeq_pow_four_div_stirlingSeq_pow_two_eq` `mul_one_div` `one_div` `pow_sub_of_lt` `Filter.Tendsto.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Filter.Tendsto.div` `IsTopologicalDivisionRing.toContinuousInv₀` `instIsTopologicalDivisionRingReal` `Filter.Tendsto.pow` `Filter.Tendsto.comp` `Filter.Tendsto.const_mul_atTop'` `two_pos` `Nat.instZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Filter.tendsto_id` `pow_ne_zero` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `tendsto_self_div_two_mul_self_add_one`
`sqrt_pi_le_stirlingSeq` 📖	mathematical	—	`Real` `Real.instLE` `Real.sqrt` `Real.pi` `stirlingSeq`	—	`Antitone.le_of_tendsto` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `stirlingSeq'_antitone` `Filter.Tendsto.comp` `tendsto_stirlingSeq_sqrt_pi` `Filter.tendsto_add_atTop_nat`
`stirlingSeq'_antitone` 📖	mathematical	—	`Antitone` `Real` `Nat.instPreorder` `Real.instPreorder` `stirlingSeq`	—	`Real.log_le_log_iff` `stirlingSeq'_pos` `log_stirlingSeq'_antitone`
`stirlingSeq'_bounded_by_pos_constant` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `Real.instLE` `stirlingSeq`	—	`log_stirlingSeq_bounded_by_constant` `Real.exp_pos` `Real.le_log_iff_exp_le` `stirlingSeq'_pos`
`stirlingSeq'_pos` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `stirlingSeq`	—	`div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Nat.factorial_pos` `mul_pos` `Real.sqrt_pos_of_pos` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Right.add_pos_of_nonneg_of_pos` `covariant_swap_add_of_covariant_add` `Nat.instIsOrderedAddMonoid` `zero_le` `Nat.instCanonicallyOrderedAdd` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instNontrivial` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `Real.exp_pos`
`stirlingSeq_has_pos_limit_a` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `Filter.Tendsto` `stirlingSeq` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	—	`stirlingSeq'_bounded_by_pos_constant` `lt_of_lt_of_le` `le_csInf` `Set.range_nonempty` `Filter.tendsto_add_atTop_iff_nat` `tendsto_atTop_ciInf` `LinearOrder.infConvergenceClass` `instOrderTopologyReal` `stirlingSeq'_antitone`
`stirlingSeq_one` 📖	mathematical	—	`stirlingSeq` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.exp` `Real.instOne` `Real.sqrt` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `stirlingSeq.eq_1` `pow_one` `Nat.factorial_one` `Nat.cast_one` `mul_one` `mul_one_div` `one_div_div`
`stirlingSeq_pow_four_div_stirlingSeq_pow_two_eq` 📖	mathematical	—	`Real` `Real.instMul` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Monoid.toNatPow` `Real.instMonoid` `stirlingSeq` `Real.instNatCast` `Real.instAdd` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat` `Real.instOne` `Real.Wallis.W`	—	`Nat.instAtLeastTwoHAddOfNat` `stirlingSeq.eq_1` `pow_mul` `Real.Wallis.W_eq_factorial_ratio` `div_pow` `mul_pow` `Real.sq_sqrt` `le_of_lt` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `lt_of_le_of_ne'` `zero_le` `Nat.instCanonicallyOrderedAdd` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instNontrivial` `nsmul_eq_mul` `mul_one` `Nat.cast_mul` `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.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.pow_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `div_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `one_mul` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `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` `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.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `Mathlib.Meta.NormNum.isNat_eq_false` `Nat.cast_zero` `ne_of_gt` `Mathlib.Tactic.FieldSimp.zpow'_ofNat` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `Real.exp_pos` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `add_pos'` `Nat.cast_one` `Nat.factorial_pos` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf'` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.atom_pf` `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.pow_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.pow_prod_atom` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.RingNF.mul_assoc_rev`
`stirlingSeq_zero` 📖	mathematical	—	`stirlingSeq` `Real` `Real.instZero`	—	`stirlingSeq.eq_1` `Nat.cast_zero` `MulZeroClass.mul_zero` `Real.sqrt_zero` `MulZeroClass.zero_mul` `div_zero`
`tendsto_self_div_two_mul_self_add_one` 📖	mathematical	—	`Filter.Tendsto` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNatCast` `Real.instAdd` `Real.instMul` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat` `Real.instOne` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	—	`Nat.instAtLeastTwoHAddOfNat` `one_div` `add_zero` `Filter.Tendsto.congr'` `Filter.eventually_atTop` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `add_div'` `Nat.cast_ne_zero` `RCLike.charZero_rclike` `inv_div` `Filter.Tendsto.inv₀` `IsTopologicalDivisionRing.toContinuousInv₀` `instIsTopologicalDivisionRingReal` `Filter.Tendsto.const_add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `tendsto_const_div_atTop_nhds_zero_nat` `NNRat.instContinuousSMulOfIsScalarTowerOfRat` `IsScalarTower.nnrat` `Rat.instCharZero` `NNRat.instContinuousSMulRatReal` `IsTopologicalSemiring.toContinuousMul` `two_ne_zero` `CharZero.NeZero.two`
`tendsto_stirlingSeq_sqrt_pi` 📖	mathematical	—	`Filter.Tendsto` `Real` `stirlingSeq` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.sqrt` `Real.pi`	—	`stirlingSeq_has_pos_limit_a` `Nat.instAtLeastTwoHAddOfNat` `tendsto_nhds_unique` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Real.Wallis.tendsto_W_nhds_pi_div_two` `second_wallis_limit` `LT.lt.ne'` `div_left_inj'` `two_ne_zero'` `CharZero.NeZero.two` `RCLike.charZero_rclike` `Real.sqrt_sq` `LT.lt.le`

---

← Back to Index