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, 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	22
Total	23

Stirling

Definitions

Name	Category	Theorems
stirlingSeq 📖	CompOp	17 math math: log_stirlingSeq_bounded_aux, log_stirlingSeq_sub_log_stirlingSeq_succ, log_stirlingSeq_formula, log_stirlingSeq_diff_hasSum, stirlingSeq_one, stirlingSeq'_antitone, log_stirlingSeq_diff_le, 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.toPow 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.toPow 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 Real.instInv instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat le_imp_le_of_le_of_le log_stirlingSeq_diff_le le_refl Nat.cast_add Nat.cast_one one_div mul_inv_rev Mathlib.Tactic.FieldSimp.le_eq_cancel_le PosMulStrictMono.toPosMulMono IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing PosMulStrictMono.toPosMulReflectLE Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.subst_add 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.one_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg LT.lt.ne' add_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Nat.cast_pos' 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 Real.instIsOrderedRing Real.instNontrivial Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval ne_of_gt Nat.cast_nonneg' Mathlib.Tactic.FieldSimp.NF.cons_pos PosMulReflectLE.toPosMulReflectLT Mathlib.Meta.NormNum.instAtLeastTwo zero_lt_one NeZero.one GroupWithZero.toNontrivial add_sub_cancel_left instReflLe Finset.sum_le_sum zero_add Finset.sum_range_sub' CharP.cast_eq_zero CharP.ofCharZero AddGroup.toOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsStrictOrderedRing.toMulPosStrictMono
log_stirlingSeq_bounded_by_constant 📖	mathematical	—	Real Real.instLE Real.instSub Real.instOne Real.instInv instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat DivInvMonoid.toDiv Real.instDivInvMonoid Real.log stirlingSeq	—	Nat.instAtLeastTwoHAddOfNat log_stirlingSeq_bounded_aux Real.log_sqrt Real.log_exp Real.log_div ne_of_gt Real.exp_pos stirlingSeq_one
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.toPow 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 📖	mathematical	—	Real Real.instLE Real.instSub Real.log stirlingSeq DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instAdd	—	Nat.instAtLeastTwoHAddOfNat Real.log_nonneg one_le_div PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE 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 Real.sqrt_le_left le_of_lt Real.exp_pos le_imp_le_of_le_of_le le_refl pow_le_pow_left₀ IsOrderedRing.toPosMulMono IsOrderedRing.toMulPosMono add_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Nat.cast_one Real.add_one_le_exp Mathlib.Meta.NormNum.isNat_le_true Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 stirlingSeq_zero Real.log_zero zero_add stirlingSeq_one zero_sub CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike MulZeroClass.mul_zero mul_one div_zero lt_imp_lt_of_le_of_le div_pos mul_pos Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add Nat.cast_nonneg' Real.instZeroLEOneClass div_le_div₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono add_le_add_left mul_le_mul_of_nonneg_left Nat.mono_cast Mathlib.Meta.NormNum.isNNRat_lt_true instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.isNNRat_pow Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.one_natPow hasSum_le HasSolidNorm.orderClosedTopology instHasSolidNormReal Nat.cast_add one_div inv_pow Mathlib.Tactic.FieldSimp.le_eq_cancel_le PosMulStrictMono.toPosMulMono Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.subst_add 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.one_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg LT.lt.ne' Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.cons_pos pow_pos IsStrictOrderedRing.toZeroLEOneClass zero_lt_one NeZero.one GroupWithZero.toNontrivial log_stirlingSeq_diff_hasSum SummationFilter.instNeBotUnconditional
log_stirlingSeq_diff_le_geo_sum 📖	mathematical	—	Real Real.instLE Real.instSub Real.log stirlingSeq DivInvMonoid.toDiv Real.instDivInvMonoid Monoid.toPow 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 instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le 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.toPow Real.instMonoid	—	le_imp_le_of_le_of_le Nat.instAtLeastTwoHAddOfNat log_stirlingSeq_diff_le le_refl CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike MulZeroClass.mul_zero zero_add mul_one div_zero zero_pow Nat.instCharZero instReflLe Nat.cast_add Nat.cast_one one_div mul_inv_rev Mathlib.Tactic.FieldSimp.le_eq_cancel_le PosMulStrictMono.toPosMulMono IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing PosMulStrictMono.toPosMulReflectLE Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.subst_add 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.one_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg LT.lt.ne' Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.pow_eq_eval add_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add Nat.cast_nonneg' Real.instZeroLEOneClass Mathlib.Tactic.FieldSimp.NF.cons_pos PosMulReflectLE.toPosMulReflectLT zero_lt_one NeZero.one GroupWithZero.toNontrivial
second_wallis_limit 📖	mathematical	Filter.Tendsto Real stirlingSeq Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	Filter.Tendsto Real Real.Wallis.W Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DivInvMonoid.toDiv Real.instDivInvMonoid Monoid.toPow 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	—	Nat.instAtLeastTwoHAddOfNat 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.toPow 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 instSeparatelyContinuousAddOfContinuousAdd IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal tendsto_const_div_atTop_nhds_zero_nat NNRat.instContinuousSMulOfIsScalarTowerOfRat IsScalarTower.nnrat Rat.instCharZero NNRat.instContinuousSMulRatReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring 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