Basic

📁 Source: Mathlib/Analysis/SpecialFunctions/Log/Basic.lean

Statistics

Metric	Count
Definitions evalLogIntCast, evalLogNatCast, evalLogNatLit, expPartialHomeomorph	4
Theorems log_prod, log_nonneg_of_isNat, log_nonneg_of_isNegNat, log_nz_of_isNNRat, log_nz_of_isRat_neg, log_pos_of_isNNRat, log_pos_of_isNat, log_pos_of_isNegNat, log_pos_of_isRat_neg, abs_log_mul_self_lt, continuousAt_log, continuousAt_log_iff, continuousOn_log, continuous_log, continuous_log', cosh_log, eq_one_of_pos_of_log_eq_zero, expPartialHomeomorph_apply, expPartialHomeomorph_source, expPartialHomeomorph_symm_apply, expPartialHomeomorph_target, exp_log, exp_log_eq_abs, exp_log_of_neg, exp_one_mul_le_exp, isLittleO_const_log_atTop, isLittleO_log_id_atTop, isLittleO_pow_log_id_atTop, le_exp_log, le_log_iff_exp_le, log_abs, log_comp_exp, log_div, log_div_self, log_eq_zero, log_exp, log_injOn_pos, log_intCast_nonneg, log_inv, log_le_iff_le_exp, log_le_log, log_le_log_iff, log_le_self, log_le_sub_one_of_pos, log_list_prod, log_lt_iff_lt_exp, log_lt_log, log_lt_log_iff, log_lt_sub_one_of_pos, log_mul, log_multiset_prod, log_natCast_nonneg, log_nat_eq_sum_factorization, log_ne_zero, log_ne_zero_of_pos_of_ne_one, log_neg, log_neg_eq_log, log_neg_iff, log_neg_natCast_nonneg, log_neg_of_lt_zero, log_nonneg, log_nonneg_iff, log_nonpos, log_nonpos_iff, log_of_ne_zero, log_of_pos, log_one, log_pos, log_pos_iff, log_pos_of_lt_neg_one, log_pow, log_prod, log_sqrt, log_surjective, log_zero, log_zpow, lt_log_iff_exp_lt, neg_inv_le_log, one_sub_inv_le_log_of_pos, range_log, sinh_log, strictAntiOn_log, strictMonoOn_log, surjOn_log, surjOn_log', tendsto_log_atTop, tendsto_log_comp_add_sub_log, tendsto_log_nat_add_one_sub_log, tendsto_log_nhdsGT_zero, tendsto_log_nhdsLT_zero, tendsto_log_nhdsNE_zero, tendsto_pow_log_div_mul_add_atTop, two_mul_le_exp	93
Total	97

Finsupp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
log_prod 📖	mathematical	DFunLike.coe Finsupp instFunLike	Real.log prod Real Real.instCommMonoid sum Real.instAddCommMonoid	—	Real.log_prod mem_support_iff

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
evalLogIntCast 📖	CompOp	—
evalLogNatCast 📖	CompOp	—
evalLogNatLit 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
log_nonneg_of_isNat 📖	mathematical	Mathlib.Meta.NormNum.IsNat Real AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instRing	Real.instLE Real.instZero Real.log	—	Mathlib.Meta.NormNum.IsNat.to_eq Real.log_natCast_nonneg
log_nonneg_of_isNegNat 📖	mathematical	Mathlib.Meta.NormNum.IsInt Real Real.instRing	Real.instLE Real.instZero Real.log	—	Mathlib.Meta.NormNum.IsInt.neg_to_eq Real.log_neg_natCast_nonneg
log_nz_of_isNNRat 📖	—	Mathlib.Meta.NormNum.IsNNRat Real Real.semiring	—	—	invOf_eq_inv div_eq_mul_inv Rat.cast_div RCLike.charZero_rclike Rat.cast_natCast Rat.cast_pos Real.instIsStrictOrderedRing Rat.cast_one Rat.cast_lt ne_of_lt Real.log_neg
log_nz_of_isRat_neg 📖	—	Mathlib.Meta.NormNum.IsRat Real Real.instRing	—	—	invOf_eq_inv div_eq_mul_inv Nat.cast_zero Int.cast_natCast Rat.instCharZero Rat.instIsStrictOrderedRing RCLike.charZero_rclike Real.instIsStrictOrderedRing Nat.cast_one ne_of_lt Real.log_neg_of_lt_zero
log_pos_of_isNNRat 📖	mathematical	Mathlib.Meta.NormNum.IsNNRat Real Real.semiring	Real.instLT Real.instZero Real.log	—	invOf_eq_inv div_eq_mul_inv Rat.cast_one Rat.cast_div RCLike.charZero_rclike Rat.cast_natCast Rat.cast_lt Real.instIsStrictOrderedRing Real.log_pos
log_pos_of_isNat 📖	mathematical	Mathlib.Meta.NormNum.IsNat Real AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instRing	Real.instLT Real.instZero Real.log	—	Mathlib.Meta.NormNum.IsNat.to_eq Real.log_pos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike
log_pos_of_isNegNat 📖	mathematical	Mathlib.Meta.NormNum.IsInt Real Real.instRing	Real.instLT Real.instZero Real.log	—	Mathlib.Meta.NormNum.IsInt.neg_to_eq Real.log_neg_eq_log Real.log_pos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike
log_pos_of_isRat_neg 📖	mathematical	Mathlib.Meta.NormNum.IsRat Real Real.instRing	Real.instLT Real.instZero Real.log	—	invOf_eq_inv div_eq_mul_inv Nat.cast_one Int.cast_natCast Rat.instCharZero Rat.instIsStrictOrderedRing RCLike.charZero_rclike Real.instIsStrictOrderedRing Real.log_pos_of_lt_neg_one

Real

Definitions

Name	Category	Theorems
expPartialHomeomorph 📖	CompOp	4 math math: expPartialHomeomorph_apply, expPartialHomeomorph_symm_apply, expPartialHomeomorph_source, expPartialHomeomorph_target

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_log_mul_self_lt 📖	mathematical	Real instLT instZero instLE instOne	abs lattice instAddGroup instMul log	—	one_div PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing log_le_sub_one_of_pos lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul 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 RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add 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.add_lt_of_neg_of_le neg_neg_of_pos instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.without_one_mul CancelDenoms.sub_subst Mathlib.Tactic.Linarith.sub_nonpos_of_le instIsOrderedRing mul_nonneg IsOrderedRing.toPosMulMono log_inv log_nonneg le_inv_comm₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono zero_lt_one instZeroLEOneClass NeZero.charZero_one inv_one LT.lt.le abs_neg neg_mul abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono lt_div_iff₀ zero_sub log_one log_div one_ne_zero LT.lt.ne'
continuousAt_log 📖	mathematical	—	ContinuousAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace log	—	ContinuousWithinAt.continuousAt continuousOn_log IsOpen.mem_nhds isOpen_compl_singleton T5Space.toT1Space OrderTopology.t5Space instOrderTopologyReal
continuousAt_log_iff 📖	mathematical	—	ContinuousAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace log	—	not_tendsto_nhds_of_tendsto_atBot instNoBotOrderOfNoMinOrder instNoMinOrderOfNontrivial instIsOrderedRing instNontrivial instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal instIsOrderedAddMonoid punctured_nhds_module_neBot IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul tendsto_log_nhdsNE_zero Filter.Tendsto.mono_left ContinuousAt.tendsto nhdsWithin_le_nhds continuousAt_log
continuousOn_log 📖	mathematical	—	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace log Compl.compl Set Set.instCompl Set.instSingletonSet instZero	—	abs_pos IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid log_of_ne_zero Continuous.comp OrderIso.continuous orderTopology_of_ordConnected instOrderTopologyReal Set.ordConnected_Ioi Continuous.norm continuous_subtype_val
continuous_log 📖	mathematical	—	Continuous Real instZero instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace log	—	continuousOn_iff_continuous_restrict ContinuousOn.mono continuousOn_log
continuous_log' 📖	mathematical	—	Continuous Real instLT instZero instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace log	—	continuousOn_iff_continuous_restrict ContinuousOn.mono continuousOn_log ne_of_gt
cosh_log 📖	mathematical	Real instLT instZero	cosh log DivInvMonoid.toDiv instDivInvMonoid instAdd instInv instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat cosh_eq exp_neg exp_log
eq_one_of_pos_of_log_eq_zero 📖	mathematical	Real instLT instZero log	instOne	—	log_injOn_pos Set.mem_Ioi zero_lt_one instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike log_one
expPartialHomeomorph_apply 📖	mathematical	—	OpenPartialHomeomorph.toFun' Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace expPartialHomeomorph exp	—	—
expPartialHomeomorph_source 📖	mathematical	—	PartialEquiv.source Real OpenPartialHomeomorph.toPartialEquiv UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace expPartialHomeomorph Set.univ	—	—
expPartialHomeomorph_symm_apply 📖	mathematical	—	OpenPartialHomeomorph.toFun' Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace OpenPartialHomeomorph.symm expPartialHomeomorph log	—	—
expPartialHomeomorph_target 📖	mathematical	—	PartialEquiv.target Real OpenPartialHomeomorph.toPartialEquiv UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace expPartialHomeomorph Set.Ioi instPreorder instZero	—	—
exp_log 📖	mathematical	Real instLT instZero	exp log	—	exp_log_eq_abs LT.lt.ne' abs_of_pos IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid
exp_log_eq_abs 📖	mathematical	—	exp log abs Real lattice instAddGroup	—	abs_pos IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid log_of_ne_zero coe_expOrderIso_apply OrderIso.apply_symm_apply
exp_log_of_neg 📖	mathematical	Real instLT instZero	exp log instNeg	—	exp_log_eq_abs ne_of_lt abs_of_neg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid
exp_one_mul_le_exp 📖	mathematical	—	Real instLE instMul exp instOne	—	le_trans mul_nonpos_of_nonneg_of_nonpos IsOrderedRing.toPosMulMono instIsOrderedRing LT.lt.le exp_pos exp_nonneg add_one_le_exp mul_comm exp_log lt_of_not_ge exp_add exp_le_exp
isLittleO_const_log_atTop 📖	mathematical	—	Asymptotics.IsLittleO Real norm Filter.atTop instPreorder log	—	Asymptotics.isLittleO_of_tendsto' Filter.mp_mem Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial instIsOrderedRing instNontrivial Filter.univ_mem' log_zero log_pos log_neg_eq_log log_one Filter.Tendsto.div_atTop instIsStrictOrderedRing instOrderTopologyReal T5Space.toT1Space OrderTopology.t5Space Filter.atTop_neBot instIsDirectedOrder instArchimedean tendsto_log_atTop
isLittleO_log_id_atTop 📖	mathematical	—	Asymptotics.IsLittleO Real norm Filter.atTop instPreorder log	—	Asymptotics.IsLittleO.congr_left isLittleO_pow_log_id_atTop pow_one
isLittleO_pow_log_id_atTop 📖	mathematical	—	Asymptotics.IsLittleO Real norm Filter.atTop instPreorder Monoid.toNatPow instMonoid log	—	Asymptotics.isLittleO_iff_tendsto' Filter.mp_mem Filter.eventually_ne_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial instIsOrderedRing instNontrivial Filter.univ_mem' one_mul add_zero tendsto_pow_log_div_mul_add_atTop one_ne_zero NeZero.charZero_one RCLike.charZero_rclike
le_exp_log 📖	mathematical	—	Real instLE exp log	—	log.eq_1 exp_zero zero_le_one instZeroLEOneClass exp_log_eq_abs le_abs_self
le_log_iff_exp_le 📖	mathematical	Real instLT instZero	instLE log exp	—	exp_le_exp exp_log
log_abs 📖	mathematical	—	log abs Real lattice instAddGroup	—	abs_zero IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid log_zero exp_eq_exp exp_log_eq_abs LT.lt.ne' abs_pos abs_abs covariant_swap_add_of_covariant_add
log_comp_exp 📖	mathematical	—	Real log exp	—	log_exp
log_div 📖	mathematical	—	log Real DivInvMonoid.toDiv instDivInvMonoid instSub	—	exp_injective exp_log_eq_abs div_ne_zero exp_sub abs_div instIsStrictOrderedRing
log_div_self 📖	mathematical	—	log Real DivInvMonoid.toDiv instDivInvMonoid instZero	—	eq_or_ne div_zero log_zero div_self log_one
log_eq_zero 📖	mathematical	—	log Real instZero instOne instNeg	—	lt_trichotomy neg_eq_iff_eq_neg eq_one_of_pos_of_log_eq_zero neg_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid log_neg_eq_log log_zero log_one
log_exp 📖	mathematical	—	log exp	—	exp_injective exp_log exp_pos
log_injOn_pos 📖	mathematical	—	Set.InjOn Real log Set.Ioi instPreorder instZero	—	StrictMonoOn.injOn strictMonoOn_log
log_intCast_nonneg 📖	mathematical	—	Real instLE instZero log instIntCast	—	lt_trichotomy Nat.cast_zero Nat.cast_one Int.cast_one IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike log_nonneg Int.cast_zero log_zero lt_neg IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Int.instAddLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add neg_zero log_neg_eq_log
log_inv 📖	mathematical	—	log Real instInv instNeg	—	inv_zero log_zero neg_zero exp_eq_exp exp_log_eq_abs inv_ne_zero exp_neg abs_inv instIsStrictOrderedRing
log_le_iff_le_exp 📖	mathematical	Real instLT instZero	instLE log exp	—	exp_le_exp exp_log
log_le_log 📖	mathematical	Real instLT instZero instLE	log	—	log_le_log_iff LT.lt.trans_le
log_le_log_iff 📖	mathematical	Real instLT instZero	instLE log	—	exp_le_exp exp_log
log_le_self 📖	mathematical	Real instLE instZero	log	—	LE.le.eq_or_lt log_zero LE.le.trans log_le_sub_one_of_pos le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf 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.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_neg instIsStrictOrderedRing neg_neg_of_pos instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_neg_of_lt instIsOrderedRing
log_le_sub_one_of_pos 📖	mathematical	Real instLT instZero	instLE log instSub instOne	—	le_sub_iff_add_le covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid exp_log add_one_le_exp
log_list_prod 📖	mathematical	—	log Real instMul instOne instAdd instZero	—	log_one log_mul AddLeftCancelSemigroup.toIsLeftCancelAdd
log_lt_iff_lt_exp 📖	mathematical	Real instLT instZero	log exp	—	exp_lt_exp exp_log
log_lt_log 📖	mathematical	Real instLT instZero	log	—	exp_lt_exp exp_log lt_trans
log_lt_log_iff 📖	mathematical	Real instLT instZero	log	—	exp_lt_exp exp_log
log_lt_sub_one_of_pos 📖	mathematical	Real instLT instZero	log instSub instOne	—	log_one Set.InjOn.ne_iff log_injOn_pos Set.mem_Ioi zero_lt_one instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf 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.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.add_lt_of_le_of_neg instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le instIsOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt add_one_lt_exp sub_eq_zero_of_eq exp_log
log_mul 📖	mathematical	—	log Real instMul instAdd	—	exp_injective exp_log_eq_abs mul_ne_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass exp_add abs_mul instIsOrderedRing
log_multiset_prod 📖	mathematical	—	log Multiset.prod Real instCommMonoid Multiset.sum instAddCommMonoid Multiset.map	—	Multiset.prod_toList log_list_prod Multiset.sum_map_toList
log_natCast_nonneg 📖	mathematical	—	Real instLE instZero log instNatCast	—	CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike log_zero Nat.cast_one IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid instZeroLEOneClass log_nonneg
log_nat_eq_sum_factorization 📖	mathematical	—	log Real instNatCast Finsupp.sum MulZeroClass.toZero Nat.instMulZeroClass instAddCommMonoid Nat.factorization instMul	—	eq_or_ne CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike log_zero Nat.factorization_zero Finsupp.log_prod eq_zero_of_pow_eq_zero isReduced_of_noZeroDivisors IsStrictOrderedRing.noZeroDivisors Nat.instIsStrictOrderedRing StarOrderedRing.toExistsAddOfLE Nat.instStarOrderedRing Nat.cast_eq_zero Nat.factorization_zero_right Nat.cast_finsuppProd Nat.factorization_prod_pow_eq_self
log_ne_zero 📖	—	—	—	—	Iff.not log_eq_zero
log_ne_zero_of_pos_of_ne_one 📖	—	Real instLT instZero	—	—	eq_one_of_pos_of_log_eq_zero
log_neg 📖	mathematical	Real instLT instZero instOne	log	—	log_neg_iff
log_neg_eq_log 📖	mathematical	—	log Real instNeg	—	log_abs abs_neg
log_neg_iff 📖	mathematical	Real instLT instZero	log instOne	—	log_one log_lt_log_iff zero_lt_one instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike
log_neg_natCast_nonneg 📖	mathematical	—	Real instLE instZero log instNeg instNatCast	—	log_neg_eq_log neg_neg log_natCast_nonneg
log_neg_of_lt_zero 📖	mathematical	Real instLT instZero instNeg instOne	log	—	neg_neg log_neg_eq_log lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.neg_congr 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.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Linarith.add_lt_of_neg_of_le instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Tactic.Ring.cast_pos Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Meta.NormNum.IsNat.to_raw_eq log_neg
log_nonneg 📖	mathematical	Real instLE instOne	instZero log	—	log_nonneg_iff LT.lt.trans_le zero_lt_one instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike
log_nonneg_iff 📖	mathematical	Real instLT instZero	instLE log instOne	—	not_lt log_neg_iff
log_nonpos 📖	mathematical	Real instLE instZero instOne	log	—	log_nonpos_iff
log_nonpos_iff 📖	mathematical	Real instLE instZero	log instOne	—	LE.le.eq_or_lt log_zero instZeroLEOneClass not_lt log_pos_iff LT.lt.le
log_of_ne_zero 📖	mathematical	—	log DFunLike.coe OrderIso Set.Elem Real Set.Ioi instPreorder instZero instLE Set Set.instMembership instFunLikeOrderIso OrderIso.symm expOrderIso abs lattice instAddGroup Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid abs_pos IsOrderedAddMonoid.toAddLeftMono instAddCommMonoid partialOrder instIsOrderedAddMonoid	—	—
log_of_pos 📖	mathematical	Real instLT instZero	log DFunLike.coe OrderIso Set.Elem Set.Ioi instPreorder instLE Set Set.instMembership instFunLikeOrderIso OrderIso.symm expOrderIso	—	abs_pos IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid LT.lt.ne' log_of_ne_zero abs_of_pos
log_one 📖	mathematical	—	log Real instOne instZero	—	exp_injective exp_log zero_lt_one instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike exp_zero
log_pos 📖	mathematical	Real instLT instOne	instZero log	—	log_pos_iff LT.lt.le lt_trans zero_lt_one instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike
log_pos_iff 📖	mathematical	Real instLE instZero	instLT log instOne	—	LE.le.eq_or_lt log_zero instZeroLEOneClass log_one log_lt_log_iff zero_lt_one NeZero.charZero_one RCLike.charZero_rclike
log_pos_of_lt_neg_one 📖	mathematical	Real instLT instNeg instOne	instZero log	—	neg_neg log_neg_eq_log lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero 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.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le log_pos
log_pow 📖	mathematical	—	log Real Monoid.toNatPow instMonoid instMul instNatCast	—	pow_zero log_one CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike MulZeroClass.zero_mul eq_or_ne zero_pow log_zero Nat.cast_add Nat.cast_one MulZeroClass.mul_zero pow_succ log_mul pow_ne_zero isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Nat.cast_succ add_mul Distrib.rightDistribClass one_mul
log_prod 📖	mathematical	—	log Finset.prod Real instCommMonoid Finset.sum instAddCommMonoid	—	Finset.prod_map_toList log_list_prod Finset.sum_map_toList Finset.sum_congr
log_sqrt 📖	mathematical	Real instLE instZero	log sqrt DivInvMonoid.toDiv instDivInvMonoid instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat eq_div_iff two_ne_zero CharZero.NeZero.two RCLike.charZero_rclike mul_comm Nat.cast_two log_pow sq_sqrt
log_surjective 📖	mathematical	—	Real log	—	log_exp
log_zero 📖	mathematical	—	log Real instZero	—	—
log_zpow 📖	mathematical	—	log Real DivInvMonoid.toZPow instDivInvMonoid instMul instIntCast	—	zpow_natCast log_pow Int.cast_natCast zpow_negSucc log_inv Int.cast_negSucc Nat.cast_add_one neg_mul_eq_neg_mul
lt_log_iff_exp_lt 📖	mathematical	Real instLT instZero	log exp	—	exp_lt_exp exp_log
neg_inv_le_log 📖	mathematical	Real instLE instZero	instNeg instInv log	—	neg_le IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid covariant_swap_add_of_covariant_add log_inv log_le_self inv_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing
one_sub_inv_le_log_of_pos 📖	mathematical	Real instLT instZero	instLE instSub instOne instInv log	—	AddGroup.toOrderedSub covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid add_comm log_inv log_le_sub_one_of_pos inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing
range_log 📖	mathematical	—	Set.range Real log Set.univ	—	Function.Surjective.range_eq log_surjective
sinh_log 📖	mathematical	Real instLT instZero	sinh log DivInvMonoid.toDiv instDivInvMonoid instSub instInv instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat sinh_eq exp_neg exp_log
strictAntiOn_log 📖	mathematical	—	StrictAntiOn Real instPreorder log Set.Iio instZero	—	log_abs log_lt_log abs_pos IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid LT.lt.ne abs_of_neg neg_lt_neg_iff IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add
strictMonoOn_log 📖	mathematical	—	StrictMonoOn Real instPreorder log Set.Ioi instZero	—	log_lt_log
surjOn_log 📖	mathematical	—	Set.SurjOn Real log Set.Ioi instPreorder instZero Set.univ	—	exp_pos log_exp
surjOn_log' 📖	mathematical	—	Set.SurjOn Real log Set.Iio instPreorder instZero Set.univ	—	neg_lt_zero IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid exp_pos log_neg_eq_log log_exp
tendsto_log_atTop 📖	mathematical	—	Filter.Tendsto Real log Filter.atTop instPreorder	—	tendsto_comp_exp_atTop log_exp Filter.tendsto_id
tendsto_log_comp_add_sub_log 📖	mathematical	—	Filter.Tendsto Real instSub log instAdd Filter.atTop instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instZero	—	Filter.Tendsto.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal tendsto_const_nhds Filter.Tendsto.div_atTop instIsStrictOrderedRing instOrderTopologyReal Filter.tendsto_id comap_exp_nhds_exp exp_zero Filter.tendsto_comap_iff add_zero Filter.Tendsto.congr' Filter.mp_mem Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial instIsOrderedRing instNontrivial Filter.univ_mem' exp_sub exp_log lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.atom_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.sub_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 Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_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 Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Tactic.Linarith.sub_nonpos_of_le one_add_div Mathlib.Tactic.Linarith.lt_of_lt_of_eq sub_eq_zero_of_eq
tendsto_log_nat_add_one_sub_log 📖	mathematical	—	Filter.Tendsto Real instSub log instAdd instNatCast instOne Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instZero	—	Filter.Tendsto.comp tendsto_log_comp_add_sub_log tendsto_natCast_atTop_atTop instIsOrderedRing instArchimedean
tendsto_log_nhdsGT_zero 📖	mathematical	—	Filter.Tendsto Real log nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instZero Set.Ioi instPreorder Filter.atBot	—	log_exp Filter.tendsto_id
tendsto_log_nhdsLT_zero 📖	mathematical	—	Filter.Tendsto Real log nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instZero Set.Iio instPreorder Filter.atBot	—	Filter.Tendsto.mono_left tendsto_log_nhdsNE_zero nhdsWithin_mono ne_of_lt
tendsto_log_nhdsNE_zero 📖	mathematical	—	Filter.Tendsto Real log nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instZero Compl.compl Set Set.instCompl Set.instSingletonSet Filter.atBot instPreorder	—	log_abs Filter.Tendsto.comp tendsto_log_nhdsGT_zero tendsto_abs_nhdsNE_zero instIsOrderedAddMonoid instOrderTopologyReal
tendsto_pow_log_div_mul_add_atTop 📖	mathematical	—	Filter.Tendsto Real DivInvMonoid.toDiv instDivInvMonoid Monoid.toNatPow instMonoid log instAdd instMul Filter.atTop instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instZero	—	Filter.Tendsto.congr' Filter.mp_mem Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial instIsOrderedRing instNontrivial Filter.univ_mem' exp_log Filter.Tendsto.comp tendsto_div_pow_mul_exp_add_atTop tendsto_log_atTop
two_mul_le_exp 📖	mathematical	—	Real instLE instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat exp	—	Nat.instAtLeastTwoHAddOfNat le_trans mul_nonpos_of_nonneg_of_nonpos IsOrderedRing.toPosMulMono instIsOrderedRing LT.lt.le exp_nonneg mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono add_one_le_exp one_add_one_eq_two le_of_not_gt exp_one_mul_le_exp

---

← Back to Index