BohrMollerup

📁 Source: Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean

Statistics

Metric	Count
Definitions logGammaSeq, doublingGamma	2
Theorems f_add_nat_eq, f_add_nat_ge, f_add_nat_le, f_nat_eq, ge_logGammaSeq, le_logGammaSeq, logGammaSeq_add_one, tendsto_logGammaSeq, tendsto_logGammaSeq_of_le_one, tendsto_log_gamma, Gamma_mul_Gamma_add_half_of_pos, Gamma_mul_add_mul_le_rpow_Gamma_mul_rpow_Gamma, Gamma_strictAntiOn_Ioc, Gamma_strictMonoOn_Ici, Gamma_three_div_two_lt_one, Gamma_two, convexOn_Gamma, convexOn_log_Gamma, doublingGamma_add_one, doublingGamma_eq_Gamma, doublingGamma_log_convex_Ioi, doublingGamma_one, eq_Gamma_of_log_convex, exists_isMinOn_Gamma_Ioi, log_doublingGamma_eq	25
Total	27

Real

Definitions

Name	Category	Theorems
doublingGamma 📖	CompOp	5 math math: doublingGamma_eq_Gamma, doublingGamma_log_convex_Ioi, doublingGamma_add_one, doublingGamma_one, log_doublingGamma_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Gamma_mul_Gamma_add_half_of_pos 📖	mathematical	Real instLT instZero	instMul Gamma instAdd DivInvMonoid.toDiv instDivInvMonoid instOne instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instPow instSub sqrt pi	—	Nat.instAtLeastTwoHAddOfNat doublingGamma_eq_Gamma mul_pos IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing two_pos instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid doublingGamma.eq_1 mul_div_cancel_left₀ EuclideanDomain.toMulDivCancelClass two_ne_zero' CharZero.NeZero.two Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.const_add_termg add_zero 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 rpow_neg zero_le_two Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ 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.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.inv_eq_eval 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 ne_of_gt rpow_pos_of_pos Mathlib.Meta.Positivity.pos_of_isNat instIsOrderedRing instNontrivial Mathlib.Meta.NormNum.instAtLeastTwo sqrt_pos_of_pos pi_pos Mathlib.Tactic.FieldSimp.NF.cons_ne_zero Gamma_pos_of_pos add_pos' div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Nat.cast_one one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.cast_pos
Gamma_mul_add_mul_le_rpow_Gamma_mul_rpow_Gamma 📖	mathematical	Real instLT instZero instAdd instOne	instLE Gamma instMul instPow	—	holderConjugate_one_div Mathlib.Tactic.Linarith.eq_of_not_lt_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.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add 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_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.lt_of_eq_of_lt neg_eq_zero sub_eq_zero_of_eq Mathlib.Tactic.Linarith.sub_neg_of_lt instIsOrderedRing add_pos' IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid mul_pos IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing mul_nonneg IsOrderedRing.toPosMulMono LT.lt.le exp_pos rpow_pos_of_pos MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_restrict_iff' measurableSet_Ioi BorelSpace.opensMeasurable borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal MeasureTheory.ae_of_all mul_rpow rpow_nonneg exp_mul rpow_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.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval one_mul mul_neg Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst div_one neg_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval 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.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ mul_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero ne_of_gt Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.FieldSimp.subst_sub 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 ENNReal.ofReal_eq_zero not_le one_div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE ENNReal.ofReal_ne_top MeasureTheory.memLp_norm_rpow_iff ContinuousOn.aestronglyMeasurable secondCountableTopologyEither_of_right instSecondCountableTopologyReal PseudoEMetricSpace.pseudoMetrizableSpace ContinuousOn.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousOn.rexp ContinuousOn.fun_mul continuousOn_const continuousOn_id' continuousOn_of_forall_continuousAt continuousAt_rpow_const LT.lt.ne' Set.mem_Ioi ENNReal.toReal_ofReal one_div_nonneg ENNReal.div_self MeasureTheory.memLp_one_iff_integrable MeasureTheory.Integrable.congr GammaIntegral_convergent Filter.eventuallyEq_of_mem MeasureTheory.self_mem_ae_restrict norm_of_nonneg Gamma_eq_integral MeasureTheory.setIntegral_congr_fun exp_add add_mul Distrib.rightDistribClass neg_add neg_one_mul rpow_add Mathlib.Tactic.Ring.mul_congr 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.zero_mul Mathlib.Tactic.Ring.mul_one one_div_one_div MeasureTheory.integral_mul_le_Lp_mul_Lq_of_nonneg
Gamma_strictAntiOn_Ioc 📖	mathematical	—	StrictAntiOn Real instPreorder Gamma Set.Ioc instZero instOne	—	ConvexOn.strictAntiOn instIsStrictOrderedRing convexOn_Gamma Nat.instAtLeastTwoHAddOfNat PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsOrderedRing instNontrivial Mathlib.Meta.NormNum.isNNRat_lt_true instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Gamma_three_div_two_lt_one Gamma_one
Gamma_strictMonoOn_Ici 📖	mathematical	—	StrictMonoOn Real instPreorder Gamma Set.Ici instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Set.inter_eq_right LT.lt.trans_le two_pos instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid Set.mem_Ici ConvexOn.strictMonoOn instIsStrictOrderedRing convexOn_Gamma PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsOrderedRing instNontrivial Mathlib.Meta.NormNum.isNNRat_lt_true 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 Gamma_three_div_two_lt_one Gamma_two
Gamma_three_div_two_lt_one 📖	mathematical	—	Real instLT Gamma DivInvMonoid.toDiv instDivInvMonoid instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instOne	—	Nat.instAtLeastTwoHAddOfNat PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing instIsOrderedRing instNontrivial BohrMollerup.f_add_nat_le convexOn_log_Gamma Gamma_add_one LT.lt.ne' log_mul Gamma_pos_of_pos add_comm two_ne_zero one_half_pos Mathlib.Meta.NormNum.isRat_le_true Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.instAtLeastTwo LE.le.trans_lt log_le_iff_le_exp le_sub_iff_add_le' IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid Mathlib.Meta.NormNum.isNNRat_eq_true Mathlib.Meta.NormNum.isNNRat_add zero_add log_one Gamma_two Nat.cast_two exp_lt_one_iff mul_comm mul_div_assoc div_sub' CharZero.NeZero.two div_neg_of_neg_of_pos sub_neg IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add mul_one log_pow exp_lt_exp exp_log two_pos instZeroLEOneClass NeZero.charZero_one Mathlib.Meta.NormNum.isNNRat_lt_true instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Nat.cast_zero Mathlib.Meta.NormNum.isNNRat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0
Gamma_two 📖	mathematical	—	Gamma Real instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instOne	—	Nat.instAtLeastTwoHAddOfNat Gamma_ofNat_eq_factorial Nat.cast_one
convexOn_Gamma 📖	mathematical	—	ConvexOn Real semiring partialOrder instAddCommMonoid Algebra.toSMul instCommSemiring CommSemiring.toSemiring Algebra.id Set.Ioi instPreorder instZero Gamma	—	ConvexOn.congr ConvexOn.comp ConvexOn.subset convexOn_exp Set.subset_univ convex_iff_isPreconnected IsPreconnected.image isPreconnected_Ioi instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing ContinuousAt.continuousWithinAt ContinuousAt.log DifferentiableAt.continuousAt IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology differentiableAt_Gamma LT.lt.ne' neg_lt_iff_pos_add IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid add_pos_of_pos_of_nonneg Set.mem_Ioi Nat.cast_nonneg instIsOrderedRing Gamma_pos_of_pos convexOn_log_Gamma Monotone.monotoneOn exp_monotone exp_log
convexOn_log_Gamma 📖	mathematical	—	ConvexOn Real semiring partialOrder instAddCommMonoid Algebra.toSMul instCommSemiring CommSemiring.toSemiring Algebra.id Set.Ioi instPreorder instZero log Gamma	—	convexOn_iff_forall_pos convex_Ioi instIsOrderedCancelAddMonoid IsStrictOrderedModule.toPosSMulStrictMono IsStrictOrderedRing.toIsStrictOrderedModule instIsStrictOrderedRing Mathlib.Tactic.Linarith.eq_of_not_lt_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.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add 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_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.lt_of_eq_of_lt neg_eq_zero sub_eq_zero_of_eq Mathlib.Tactic.Linarith.sub_neg_of_lt instIsOrderedRing log_rpow Gamma_pos_of_pos log_mul ne_of_gt rpow_pos_of_pos log_le_log add_pos' IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid mul_pos IsStrictOrderedRing.toPosMulStrictMono Gamma_mul_add_mul_le_rpow_Gamma_mul_rpow_Gamma
doublingGamma_add_one 📖	mathematical	—	doublingGamma Real instAdd instOne instMul	—	doublingGamma.eq_1 Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Tactic.Abel.zero_termg add_div add_assoc Nat.instAtLeastTwoHAddOfNat add_halves CharZero.NeZero.two RCLike.charZero_rclike Gamma_add_one div_ne_zero two_ne_zero rpow_add two_pos instZeroLEOneClass NeZero.charZero_one IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid rpow_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos 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 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.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.inv_mul
doublingGamma_eq_Gamma 📖	mathematical	Real instLT instZero	doublingGamma Gamma	—	eq_Gamma_of_log_convex doublingGamma_log_convex_Ioi doublingGamma_add_one LT.lt.ne' mul_pos IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing Gamma_pos_of_pos inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE two_pos instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid add_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd one_pos rpow_pos_of_pos sqrt_pos_of_pos pi_pos doublingGamma_one
doublingGamma_log_convex_Ioi 📖	mathematical	—	ConvexOn Real semiring partialOrder instAddCommMonoid Algebra.toSMul instCommSemiring CommSemiring.toSemiring Algebra.id Set.Ioi instPreorder instZero log doublingGamma	—	ConvexOn.congr Nat.instAtLeastTwoHAddOfNat ConvexOn.add_const instIsOrderedAddMonoid ConvexOn.add Algebra.to_smulCommClass zero_div Set.preimage_const_mul_Ioi₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing one_half_pos smul_eq_mul mul_comm mul_one_div ConvexOn.comp_affineMap convexOn_log_Gamma ConvexOn.subset Set.preimage_comp Set.preimage_add_const_Ioi zero_sub neg_div div_self LT.lt.ne' Set.Ioi_subset_Ioi LT.lt.le neg_one_lt_zero instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono convex_Ioi instIsOrderedCancelAddMonoid IsStrictOrderedModule.toPosSMulStrictMono IsStrictOrderedRing.toIsStrictOrderedModule ConvexOn.smul IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule log_pos one_lt_two convexOn_id Set.EqOn.symm log_doublingGamma_eq
doublingGamma_one 📖	mathematical	—	doublingGamma Real instOne	—	Gamma_one_half_eq add_halves CharZero.NeZero.two RCLike.charZero_rclike sub_self Gamma_one mul_one rpow_zero div_self sqrt_ne_zero' pi_pos
eq_Gamma_of_log_convex 📖	mathematical	ConvexOn Real semiring partialOrder instAddCommMonoid Algebra.toSMul instCommSemiring CommSemiring.toSemiring Algebra.id Set.Ioi instPreorder instZero log instAdd instOne instMul instLT	Set.EqOn Gamma	—	BohrMollerup.tendsto_logGammaSeq log_mul LT.lt.ne' Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf 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 tendsto_nhds_unique TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat sub_zero log_one BohrMollerup.tendsto_log_gamma log_injOn_pos Gamma_pos_of_pos
exists_isMinOn_Gamma_Ioi 📖	mathematical	—	Real Set Set.instMembership Set.Ioo instPreorder instOne instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat IsMinOn Gamma Set.Ioi instZero	—	Nat.instAtLeastTwoHAddOfNat IsCompact.exists_isMinOn instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal instIsOrderedAddMonoid CompactIccSpace.isCompact_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal Set.nonempty_Icc one_le_two instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono ContinuousOn.mono DifferentiableOn.continuousOn IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology differentiableOn_Gamma_Ioi Gamma_one Gamma_ofNat_eq_factorial Nat.cast_one Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.isRat_le_true instIsStrictOrderedRing Mathlib.Meta.NormNum.IsNNRat.to_isRat LE.le.trans LT.lt.le StrictAntiOn.antitoneOn Gamma_strictAntiOn_Ioc NeZero.charZero_one StrictMonoOn.monotoneOn Gamma_strictMonoOn_Ici
log_doublingGamma_eq 📖	mathematical	—	Set.EqOn Real log doublingGamma instSub instAdd Gamma DivInvMonoid.toDiv instDivInvMonoid instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instOne instMul sqrt pi Set.Ioi instPreorder instZero	—	sqrt_ne_zero' pi_pos Nat.instAtLeastTwoHAddOfNat LT.lt.ne' Gamma_pos_of_pos div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing two_pos instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid add_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd one_half_pos rpow_pos_of_pos doublingGamma.eq_1 log_div mul_ne_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass log_mul log_rpow two_ne_zero CharZero.NeZero.two Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf' Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.atom_pf 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 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.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.nnrat_rawCast add_zero Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_congr 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.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.neg_mul mul_one Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg Mathlib.Tactic.RingNF.add_neg Mathlib.Tactic.RingNF.add_assoc_rev

Real.BohrMollerup

Definitions

Name	Category	Theorems
logGammaSeq 📖	CompOp	6 math math: le_logGammaSeq, tendsto_logGammaSeq, logGammaSeq_add_one, tendsto_logGammaSeq_of_le_one, ge_logGammaSeq, tendsto_log_gamma

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
f_add_nat_eq 📖	mathematical	Real Real.instAdd Real.instOne Real.log Real.instLT Real.instZero	Real.instNatCast Finset.sum Real.instAddCommMonoid Finset.range	—	CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike add_zero Nat.cast_succ Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Nat.cast_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_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.instIsOrderedRing Mathlib.Tactic.Linarith.natCast_nonneg Mathlib.Tactic.Linarith.sub_neg_of_lt Finset.range_add_one Finset.sum_insert Finset.notMem_range_self Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.const_add_termg
f_add_nat_ge 📖	mathematical	ConvexOn Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set.Ioi Real.instPreorder Real.instZero Real.instAdd Real.instOne Real.log Real.instLT	Real.instLE Real.instNatCast Real.instMul Real.instSub	—	Nat.cast_one sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Nat.cast_lt Real.instZeroLEOneClass RCLike.charZero_rclike convexOn_iff_slope_mono_adjacent Real.instIsStrictOrderedRing 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 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 Nat.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.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.add_neg neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le eq_sub_iff_add_eq sub_add_cancel add_comm mul_comm le_sub_iff_add_le sub_sub_cancel le_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono div_one add_sub_cancel_left
f_add_nat_le 📖	mathematical	ConvexOn Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set.Ioi Real.instPreorder Real.instZero Real.instAdd Real.instOne Real.log Real.instLT Real.instLE	Real.instNatCast Real.instMul	—	Nat.cast_pos Real.instIsOrderedRing Real.instNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_congr 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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add 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_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.mul_one 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_add_gt lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.add_neg neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Tactic.Linarith.sub_nonpos_of_le le_of_not_gt Mathlib.Tactic.Linarith.add_lt_of_le_of_neg LT.lt.le Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt
f_nat_eq 📖	mathematical	Real Real.instAdd Real.instOne Real.log	Real.instNatCast Nat.factorial	—	Nat.le_induction Nat.cast_one tsub_self Nat.instCanonicallyOrderedAdd Nat.instOrderedSub Real.log_one add_zero Nat.cast_pos Real.instIsOrderedRing Real.instNontrivial Nat.cast_add add_assoc Real.log_mul Nat.cast_ne_zero RCLike.charZero_rclike Nat.factorial_ne_zero LT.lt.ne' Nat.cast_mul Nat.factorial_succ mul_comm
ge_logGammaSeq 📖	mathematical	ConvexOn Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set.Ioi Real.instPreorder Real.instZero Real.instAdd Real.instOne Real.log Real.instLT	Real.instLE logGammaSeq	—	add_sub_assoc sub_le_iff_le_add covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid f_add_nat_eq add_comm le_trans le_of_eq f_nat_eq Nat.cast_add_one add_sub_cancel_right Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_congr 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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt f_add_nat_ge
le_logGammaSeq 📖	mathematical	ConvexOn Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set.Ioi Real.instPreorder Real.instZero Real.instAdd Real.instOne Real.log Real.instLT Real.instLE	Real.instSub Real.instMul Real.instNatCast logGammaSeq	—	logGammaSeq.eq_1 add_sub_assoc le_sub_iff_add_le covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid f_add_nat_eq add_comm LE.le.trans f_add_nat_le le_of_eq f_nat_eq Nat.cast_add_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_congr 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_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_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
logGammaSeq_add_one 📖	mathematical	—	logGammaSeq Real Real.instAdd Real.instOne Real.instSub Real.log Real.instMul Real.instNatCast	—	Finset.sum_range_succ' Nat.cast_zero add_zero Nat.cast_mul Real.log_mul Nat.cast_ne_zero RCLike.charZero_rclike Nat.factorial_ne_zero Finset.sum_congr Nat.cast_add Nat.cast_one Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.const_add_termg Nat.cast_add_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat 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_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add 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_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsNat.to_raw_eq
tendsto_logGammaSeq 📖	mathematical	ConvexOn Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set.Ioi Real.instPreorder Real.instZero Real.instAdd Real.instOne Real.log Real.instLT	Filter.Tendsto logGammaSeq Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instSub	—	Nat.cast_zero zero_add tendsto_logGammaSeq_of_le_one Filter.Eventually.mp Filter.eventually_ge_atTop Filter.Eventually.of_forall logGammaSeq_add_one sub_add_cancel Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Filter.Tendsto.comp Filter.Tendsto.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Filter.Tendsto.congr' LE.le.trans_lt Nat.cast_nonneg Real.instIsOrderedRing lt_sub_iff_add_lt IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Nat.cast_succ sub_le_iff_le_add tendsto_const_nhds Filter.tendsto_add_atTop_nat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Filter.Tendsto.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal Filter.Tendsto.const_mul IsTopologicalSemiring.toContinuousMul Real.tendsto_log_nat_add_one_sub_log Real.instIsStrictOrderedRing lt_or_ge Nat.ceil_eq_zero le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.cast_pos Nat.cast_one Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isInt_neg Mathlib.Tactic.Abel.zero_termg Nat.ceil_lt_add_one Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.sub_nonpos_of_le Nat.le_ceil
tendsto_logGammaSeq_of_le_one 📖	mathematical	ConvexOn Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set.Ioi Real.instPreorder Real.instZero Real.instAdd Real.instOne Real.log Real.instLT Real.instLE	Filter.Tendsto logGammaSeq Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instSub	—	tendsto_of_tendsto_of_tendsto_of_le_of_le' instOrderTopologyReal Mathlib.Tactic.Ring.of_eq 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.mul_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_zero Filter.Tendsto.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal tendsto_const_nhds Filter.Tendsto.const_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Real.tendsto_log_nat_add_one_sub_log Filter.univ_mem' sub_le_iff_le_add' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul le_logGammaSeq Filter.mp_mem Filter.eventually_ne_atTop instNoTopOrderOfNoMaxOrder Nat.instNoMaxOrder le_sub_iff_add_le' ge_logGammaSeq
tendsto_log_gamma 📖	mathematical	Real Real.instLT Real.instZero	Filter.Tendsto logGammaSeq Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.log Real.Gamma	—	Real.Gamma_one Real.log_one sub_zero tendsto_logGammaSeq Real.convexOn_log_Gamma Real.Gamma_add_one LT.lt.ne' Real.log_mul Real.Gamma_pos_of_pos add_comm

---

← Back to Index