LogBounds

📁 Source: Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean

Statistics

Metric	Count
Definitions logTaylor	1
Theorems continuousOn_one_add_mul_inv, hasDerivAt_logTaylor, hasDerivAt_log_sub_logTaylor, hasSum_taylorSeries_log, hasSum_taylorSeries_neg_log, integrable_pow_mul_norm_one_add_mul_inv, logTaylor_at_zero, logTaylor_succ, logTaylor_zero, log_eq_integral, log_inv_eq_integral, log_sub_logTaylor_isBigO, log_sub_self_isBigO, norm_log_one_add_half_le_self, norm_log_one_add_le, norm_log_one_add_sub_self_le, norm_log_one_sub_inv_add_logTaylor_neg_le, norm_log_one_sub_inv_sub_self_le, norm_log_sub_logTaylor_le, norm_one_add_mul_inv_le, tendsto_mul_log_one_add_of_tendsto, tendsto_nat_mul_log_one_add_of_tendsto, tendsto_one_add_cpow_exp_of_tendsto, tendsto_one_add_div_cpow_exp, tendsto_one_add_div_pow_exp, tendsto_one_add_pow_exp_of_tendsto, tendsto_mul_log_one_add_div_atTop, tendsto_mul_log_one_add_of_tendsto, tendsto_nat_mul_log_one_add_of_tendsto, tendsto_one_add_div_pow_exp, tendsto_one_add_div_rpow_exp, tendsto_one_add_pow_exp_of_tendsto, tendsto_one_add_rpow_exp_of_tendsto	33
Total	34

Complex

Definitions

Name	Category	Theorems
logTaylor 📖	CompOp	8 math math: norm_log_one_sub_inv_add_logTaylor_neg_le, norm_log_sub_logTaylor_le, hasDerivAt_logTaylor, logTaylor_zero, log_sub_logTaylor_isBigO, logTaylor_at_zero, hasDerivAt_log_sub_logTaylor, logTaylor_succ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousOn_one_add_mul_inv 📖	mathematical	Complex Set Set.instMembership slitPlane instAdd instOne	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField instInv Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra RCLike.toNormedAlgebra instRCLike Set.Icc Real.instPreorder Real.instZero Real.instOne	—	ContinuousOn.inv₀ IsTopologicalDivisionRing.toContinuousInv₀ NormedDivisionRing.to_isTopologicalDivisionRing ContinuousOn.fun_add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing continuousOn_const ContinuousOn.smul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul continuousOn_id' slitPlane_ne_zero StarConvex.add_smul_mem covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid starConvex_one_slitPlane
hasDerivAt_logTaylor 📖	mathematical	—	HasDerivAt Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField IsModuleTopology.toContinuousSMul NontriviallyNormedField.toNormedField instAdd SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid IsTopologicalSemiring.toIsModuleTopology instSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing logTaylor Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup Finset.range instMul Monoid.toNatPow instNeg instOne	—	IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing HasDerivAt.congr_simp zero_add logTaylor_succ logTaylor_zero pow_one pow_zero mul_one CharP.cast_eq_zero CharP.ofCharZero instCharZero div_zero add_zero Nat.cast_add Nat.cast_one Finset.sum_range_succ HasDerivAt.add IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul mul_div_assoc div_eq_mul_inv add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid 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_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.inv_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 one_ne_zero NeZero.one GroupWithZero.toNontrivial HasDerivAt.mul_const hasDerivAt_pow Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.pow_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.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_zero 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.add_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_pow Mathlib.Meta.NormNum.intPow_negOfNat_bit0 Mathlib.Meta.NormNum.one_natPow Mathlib.Tactic.Ring.mul_pf_right HasDerivAt.const_mul
hasDerivAt_log_sub_logTaylor 📖	mathematical	Complex Set Set.instMembership slitPlane instAdd instOne	HasDerivAt DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField IsModuleTopology.toContinuousSMul NontriviallyNormedField.toNormedField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid IsTopologicalSemiring.toIsModuleTopology instSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing instSub log logTaylor instMul Monoid.toNatPow instNeg instInv	—	IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul slitPlane_ne_zero neg_eq_iff_eq_neg add_neg_cancel Finset.sum_congr neg_one_mul geom_sum_eq div_neg add_comm sub_neg_eq_add 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.inv_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.one_eq_eval one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst div_one 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 Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval one_ne_zero NeZero.one GroupWithZero.toNontrivial add_sub_cancel HasDerivAt.sub HasDerivAt.comp_const_add hasDerivAt_log hasDerivAt_logTaylor
hasSum_taylorSeries_log 📖	mathematical	Real Real.instLT Norm.norm Complex instNorm Real.instOne	HasSum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup DivInvMonoid.toDiv instDivInvMonoid instMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring instNeg instOne instNatCast log instAdd SummationFilter.unconditional	—	hasSum_iff_tendsto_nat_of_summable_norm Summable.of_nonneg_of_le norm_nonneg norm_div norm_mul NormedDivisionRing.toNormMulClass norm_pow NormedDivisionRing.to_normOneClass norm_neg NormOneClass.norm_one one_pow one_mul norm_natCast pow_zero CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike div_zero Real.instZeroLEOneClass div_one div_le_div₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono pow_nonneg IsOrderedRing.toZeroLEOneClass Real.instIsOrderedRing IsOrderedRing.toPosMulMono le_refl Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Summable.norm FiniteDimensional.rclike_to_real summable_geometric_of_norm_lt_one instHasSummableGeomSeries tendsto_sub_nhds_zero_iff SeminormedAddCommGroup.toIsTopologicalAddGroup logTaylor.eq_1 Asymptotics.isLittleO_iff_tendsto one_ne_zero NeZero.charZero_one instCharZero Asymptotics.IsLittleO.trans_isBigO norm_sub_rev norm_norm logTaylor_zero sub_zero mul_one LE.le.trans norm_log_sub_logTaylor_le mul_comm mul_nonneg le_max_of_le_left mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono le_max_right le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr 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_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_zero_add Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero 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.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Tactic.Linarith.natCast_nonneg Mathlib.Tactic.Linarith.sub_neg_of_lt Asymptotics.IsBigOWith.isBigO Asymptotics.isBigOWith_of_le' Asymptotics.IsBigO.trans_isLittleO isLittleO_pow_pow_of_lt_left Asymptotics.isBigO_const_one
hasSum_taylorSeries_neg_log 📖	mathematical	Real Real.instLT Norm.norm Complex instNorm Real.instOne	HasSum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instNormedAddCommGroup DivInvMonoid.toDiv instDivInvMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring instNatCast instNeg log instSub instOne SummationFilter.unconditional	—	neg_neg HasSum.neg SeminormedAddCommGroup.toIsTopologicalAddGroup pow_zero CharP.cast_eq_zero CharP.ofCharZero instCharZero div_zero neg_zero zero_add pow_one mul_one pow_add mul_neg neg_mul one_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.div_eq_eval₃ div_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one neg_div one_ne_zero NeZero.one GroupWithZero.toNontrivial hasSum_taylorSeries_log norm_neg
integrable_pow_mul_norm_one_add_mul_inv 📖	mathematical	Real Real.instLT Norm.norm Complex instNorm Real.instOne	IntervalIntegrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup Real.normedAddCommGroup Real.instMul Monoid.toNatPow Real.instMonoid instInv instAdd instOne instMul ofReal MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instZero	—	continuousOn_one_add_mul_inv mem_slitPlane_of_norm_lt_one ContinuousOn.intervalIntegrable Real.locallyFinite_volume ContinuousOn.fun_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousOn.pow continuousOn_id' ContinuousOn.norm Set.uIcc_of_le zero_le_one Real.instZeroLEOneClass
logTaylor_at_zero 📖	mathematical	—	logTaylor Complex instZero	—	logTaylor_zero logTaylor_succ zero_add NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass isReduced_of_noZeroDivisors NeZero.charZero_one instCharZero instNontrivial ne_or_eq
logTaylor_succ 📖	mathematical	—	logTaylor Pi.instAdd Complex instAdd DivInvMonoid.toDiv instDivInvMonoid instMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring instNeg instOne instNatCast	—	Finset.sum_range_succ
logTaylor_zero 📖	mathematical	—	logTaylor Complex instZero	—	—
log_eq_integral 📖	mathematical	Complex Set Set.instMembership slitPlane instAdd instOne	log instMul intervalIntegral instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex instInv Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField NormedAlgebra.toAlgebra RCLike.toNormedAlgebra instRCLike Real.instZero Real.instOne MeasureTheory.MeasureSpace.volume Real.measureSpace	—	log_one sub_zero intervalIntegral.integral_unitInterval_deriv_eq_sub instCompleteSpace IsScalarTower.right continuousOn_one_add_mul_inv hasDerivAt_log StarConvex.add_smul_mem covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid starConvex_one_slitPlane
log_inv_eq_integral 📖	mathematical	Complex Set Set.instMembership slitPlane instSub instOne	log instInv instMul intervalIntegral instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField NormedAlgebra.toAlgebra RCLike.toNormedAlgebra instRCLike Real.instZero Real.instOne MeasureTheory.MeasureSpace.volume Real.measureSpace	—	sub_eq_add_neg log_inv slitPlane_arg_ne_pi neg_eq_iff_eq_neg neg_mul smul_neg log_eq_integral
log_sub_logTaylor_isBigO 📖	mathematical	—	Asymptotics.IsBigO Complex instNorm nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField instZero instSub log instAdd instOne logTaylor Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring	—	Asymptotics.isBigO_iff Nat.instAtLeastTwoHAddOfNat Filter.mp_mem eventually_norm_sub_lt one_div PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instIsOrderedRing Real.instNontrivial one_pos Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Filter.univ_mem' inv_le_comm₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono sub_pos_of_lt IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid sub_zero two_pos le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat 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 Nat.cast_one Mathlib.Tactic.Ring.one_mul 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.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_neg CancelDenoms.derive_trans 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.isNNRat_inv_pos CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Meta.NormNum.isNat_lt_true LE.le.trans norm_log_sub_logTaylor_le mul_div_assoc mul_comm norm_pow NormedDivisionRing.to_normOneClass NormedDivisionRing.toNormMulClass mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono div_le_div_of_nonneg_right le_of_lt Right.add_pos_of_nonneg_of_pos Nat.cast_nonneg' Mathlib.Meta.Positivity.pos_of_isNat pow_nonneg IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono norm_nonneg
log_sub_self_isBigO 📖	mathematical	—	Asymptotics.IsBigO Complex instNorm nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField instZero instSub log instAdd instOne Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring	—	logTaylor_succ logTaylor_zero zero_add pow_one pow_zero mul_one CharP.cast_eq_zero CharP.ofCharZero instCharZero div_zero Even.neg_pow Nat.instAtLeastTwoHAddOfNat one_pow one_mul Nat.cast_one div_one add_zero log_sub_logTaylor_isBigO
norm_log_one_add_half_le_self 📖	mathematical	Real Real.instLE Norm.norm Complex instNorm DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	log instAdd instOne Real.instMul	—	Nat.instAtLeastTwoHAddOfNat le_trans norm_log_one_add_le lt_of_le_of_lt one_half_lt_one PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing inv_eq_one_div div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo 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.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one CancelDenoms.derive_trans 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.isNNRat_inv_pos RCLike.charZero_rclike CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_nonpos Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Meta.NormNum.isNat_lt_true le_of_not_gt Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.sub_neg_of_lt div_le_div_of_nonneg_right mul_le_mul IsOrderedRing.toPosMulMono IsOrderedRing.toMulPosMono sq div_eq_mul_one_div mul_le_mul_of_nonneg_left norm_nonneg inv_nonneg Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.mul_neg Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial le_of_lt Mathlib.Tactic.Ring.pow_congr 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.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.atom_pf' Mathlib.Tactic.Ring.add_overlap_pf CancelDenoms.mul_subst CancelDenoms.pow_subst Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.one_natPow IsUnit.div_mul_cancel CancelDenoms.add_subst
norm_log_one_add_le 📖	mathematical	Real Real.instLT Norm.norm Complex instNorm Real.instOne	Real.instLE log instAdd instOne Real.instAdd DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul Monoid.toNatPow Real.instMonoid Real.instInv Real.instSub instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat sub_add_cancel norm_add_le_of_le norm_log_one_add_sub_self_le le_rfl
norm_log_one_add_sub_self_le 📖	mathematical	Real Real.instLT Norm.norm Complex instNorm Real.instOne	Real.instLE instSub log instAdd instOne DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul Monoid.toNatPow Real.instMonoid Real.instInv Real.instSub instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat sub_eq_add_neg logTaylor_succ logTaylor_zero zero_add pow_one pow_zero mul_one CharP.cast_eq_zero CharP.ofCharZero instCharZero div_zero Even.neg_pow one_pow one_mul Nat.cast_one div_one add_zero Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_natCast norm_log_sub_logTaylor_le
norm_log_one_sub_inv_add_logTaylor_neg_le 📖	mathematical	Real Real.instLT Norm.norm Complex instNorm Real.instOne	Real.instLE instAdd log instInv instSub instOne logTaylor instNeg DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul Monoid.toNatPow Real.instMonoid Real.instInv Real.instSub Real.instAdd Real.instNatCast	—	sub_eq_add_neg log_inv slitPlane_arg_ne_pi mem_slitPlane_of_norm_lt_one norm_neg sub_neg_eq_add neg_sub' norm_log_sub_logTaylor_le
norm_log_one_sub_inv_sub_self_le 📖	mathematical	Real Real.instLT Norm.norm Complex instNorm Real.instOne	Real.instLE instSub log instInv instOne DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul Monoid.toNatPow Real.instMonoid Real.instInv Real.instSub instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat sub_eq_add_neg logTaylor_succ logTaylor_zero zero_add pow_one pow_zero mul_one CharP.cast_eq_zero CharP.ofCharZero instCharZero div_zero Even.neg_pow one_pow one_mul Nat.cast_one div_one add_zero Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_natCast norm_log_one_sub_inv_add_logTaylor_neg_le
norm_log_sub_logTaylor_le 📖	mathematical	Real Real.instLT Norm.norm Complex instNorm Real.instOne	Real.instLE instSub log instAdd instOne logTaylor DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul Monoid.toNatPow Real.instMonoid Real.instInv Real.instSub Real.instAdd Real.instNatCast	—	IntervalIntegrable.mul_const Continuous.intervalIntegrable Real.locallyFinite_volume Continuous.pow IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal continuous_id' IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing zero_add hasDerivAt_log_sub_logTaylor StarConvex.add_smul_mem covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid starConvex_one_slitPlane mem_slitPlane_of_norm_lt_one ContinuousOn.mul Continuous.continuousOn Continuous.comp' Continuous.neg IsTopologicalRing.toContinuousNeg Continuous.fun_mul continuous_const continuous_ofReal continuousOn_one_add_mul_inv add_zero log_one logTaylor_at_zero sub_self sub_zero intervalIntegral.integral_unitInterval_deriv_eq_sub instCompleteSpace IsScalarTower.right norm_mul NormedDivisionRing.toNormMulClass neg_pow mul_assoc intervalIntegral.integral_const_mul mul_pow mul_comm norm_pow NormedDivisionRing.to_normOneClass norm_neg NormOneClass.norm_one one_pow one_mul mul_div_assoc mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing intervalIntegral.norm_integral_le_of_norm_le zero_le_one Real.instZeroLEOneClass Filter.univ_mem' MeasureTheory.Measure.instOuterMeasureClass norm_of_nonneg LT.lt.le norm_one_add_mul_inv_le le_of_lt pow_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsStrictOrderedRing.toZeroLEOneClass intervalIntegral.integral_mul_const integral_pow zero_pow one_div Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst div_one Mathlib.Tactic.FieldSimp.NF.atom_eq_eval 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 Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.cons_ne_zero ne_of_gt Right.add_pos_of_nonneg_of_pos Nat.cast_nonneg' Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one one_ne_zero NeZero.one GroupWithZero.toNontrivial pow_nonneg IsOrderedRing.toZeroLEOneClass norm_nonneg
norm_one_add_mul_inv_le 📖	mathematical	Real Set Set.instMembership Set.Icc Real.instPreorder Real.instZero Real.instOne Real.instLT Norm.norm Complex instNorm	Real.instLE instInv instAdd instOne instMul ofReal Real.instInv Real.instSub	—	norm_inv inv_anti₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono 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.cast_zero Nat.cast_zero 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.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le le_of_not_gt 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.Meta.NormNum.IsNat.to_raw_eq mul_nonneg_of_nonpos_of_nonpos AddGroup.existsAddOfLE IsOrderedRing.toMulPosMono covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Set.mem_Icc norm_nonneg norm_mul NormedDivisionRing.toNormMulClass norm_of_nonneg norm_neg sub_neg_eq_add NormOneClass.norm_one NormedDivisionRing.to_normOneClass norm_sub_norm_le
tendsto_mul_log_one_add_of_tendsto 📖	mathematical	Filter.Tendsto Real Complex instMul ofReal Filter.atTop Real.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField	log instAdd instOne	—	Filter.Tendsto.congr_dist Asymptotics.IsBigO.trans_tendsto dist_comm tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors NormedSpace.toNormSMulClass Filter.Tendsto.isBoundedUnder_le BoundedLENhdsClass.of_closedIciTopology instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Filter.Tendsto.norm RCLike.tendsto_ofReal_atTop_cobounded Asymptotics.IsBigO.mul NormedDivisionRing.toNormMulClass Asymptotics.isBigO_refl Asymptotics.IsBigO.comp_tendsto log_sub_self_isBigO Filter.mp_mem Filter.eventually_ne_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Filter.univ_mem' ofReal_inv eq_mul_inv_iff_mul_eq₀ Nat.cast_zero Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left 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_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw one_pow one_mul Asymptotics.IsBigO.pow NormedDivisionRing.to_normOneClass Asymptotics.isBigO_const_of_tendsto one_ne_zero NeZero.charZero_one instCharZero Filter.Tendsto.ofReal tendsto_inv_atTop_zero Real.instIsStrictOrderedRing instOrderTopologyReal
tendsto_nat_mul_log_one_add_of_tendsto 📖	mathematical	Filter.Tendsto Complex instMul instNatCast Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField	log instAdd instOne	—	Filter.Tendsto.congr Real.instIsStrictOrderedRing Nat.floor_natCast Filter.Tendsto.comp tendsto_mul_log_one_add_of_tendsto tendsto_smul_comp_nat_floor_of_tendsto_mul instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors Real.instIsDomain GroupWithZero.toNoZeroSMulDivisors NormedSpace.toNormSMulClass RCLike.instNormSMulClassInt instHasSolidNormReal tendsto_natCast_atTop_atTop Real.instIsOrderedRing Real.instArchimedean
tendsto_one_add_cpow_exp_of_tendsto 📖	mathematical	Filter.Tendsto Real Complex instMul ofReal Filter.atTop Real.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField	instPow instAdd instOne exp	—	Filter.Tendsto.congr' Filter.Tendsto.comp Continuous.tendsto continuous_exp tendsto_mul_log_one_add_of_tendsto tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors NormedSpace.toNormSMulClass Filter.Tendsto.isBoundedUnder_le BoundedLENhdsClass.of_closedIciTopology instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Filter.Tendsto.norm RCLike.tendsto_ofReal_atTop_cobounded Filter.mp_mem Filter.Tendsto.eventually_ne T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace NeZero.charZero_one instCharZero Filter.univ_mem' cpow_def_of_ne_zero Mathlib.Meta.NormNum.isInt_eq_true Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one add_eq_zero_iff_neg_eq mul_comm
tendsto_one_add_div_cpow_exp 📖	mathematical	—	Filter.Tendsto Real Complex instPow instAdd instOne DivInvMonoid.toDiv instDivInvMonoid ofReal Filter.atTop Real.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField exp	—	tendsto_one_add_cpow_exp_of_tendsto tendsto_nhds_of_eventually_eq Filter.mp_mem Filter.eventually_ne_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Filter.univ_mem' mul_div_cancel₀ Nat.cast_zero
tendsto_one_add_div_pow_exp 📖	mathematical	—	Filter.Tendsto Complex Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring instAdd instOne DivInvMonoid.toDiv instDivInvMonoid instNatCast Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField exp	—	Filter.Tendsto.congr cpow_natCast Filter.Tendsto.comp tendsto_one_add_div_cpow_exp tendsto_natCast_atTop_atTop Real.instIsOrderedRing Real.instArchimedean
tendsto_one_add_pow_exp_of_tendsto 📖	mathematical	Filter.Tendsto Complex instMul instNatCast Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring instAdd instOne exp	—	Filter.Tendsto.congr Real.instIsStrictOrderedRing Nat.floor_natCast cpow_natCast Filter.Tendsto.comp tendsto_one_add_cpow_exp_of_tendsto tendsto_smul_comp_nat_floor_of_tendsto_mul instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors Real.instIsDomain GroupWithZero.toNoZeroSMulDivisors NormedSpace.toNormSMulClass RCLike.instNormSMulClassInt instHasSolidNormReal tendsto_natCast_atTop_atTop Real.instIsOrderedRing Real.instArchimedean

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tendsto_mul_log_one_add_div_atTop 📖	mathematical	—	Filter.Tendsto Real instMul log instAdd instOne DivInvMonoid.toDiv instDivInvMonoid Filter.atTop instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace	—	tendsto_mul_log_one_add_of_tendsto Filter.Tendsto.congr' Filter.EventuallyEq.trans Filter.EventuallyEq.symm Filter.EventuallyEq.div_mul_cancel_atTop instIsStrictOrderedRing Filter.tendsto_id Filter.EventuallyEq.of_eq mul_comm tendsto_const_nhds
tendsto_mul_log_one_add_of_tendsto 📖	mathematical	Filter.Tendsto Real instMul Filter.atTop instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace	log instAdd instOne	—	tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors NormedSpace.toNormSMulClass Filter.Tendsto.isBoundedUnder_le BoundedLENhdsClass.of_closedIciTopology instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal instIsOrderedAddMonoid Filter.Tendsto.norm Filter.tendsto_id' cobounded_eq Filter.tendsto_ofReal_iff Complex.ofReal_mul Filter.Tendsto.congr' Complex.tendsto_mul_log_one_add_of_tendsto Filter.mp_mem Filter.Tendsto.eventually_const_le instClosedIicTopology IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Filter.univ_mem' Complex.ofReal_log le_of_not_gt 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.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.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_zero 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.Linarith.add_lt_of_le_of_neg instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le instIsOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Complex.ofReal_add Complex.ofReal_one
tendsto_nat_mul_log_one_add_of_tendsto 📖	mathematical	Filter.Tendsto Real instMul instNatCast Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace	log instAdd instOne	—	Filter.Tendsto.congr instIsStrictOrderedRing Nat.floor_natCast Filter.Tendsto.comp tendsto_mul_log_one_add_of_tendsto tendsto_smul_comp_nat_floor_of_tendsto_mul instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors instIsDomain GroupWithZero.toNoZeroSMulDivisors NormedSpace.toNormSMulClass RCLike.instNormSMulClassInt instHasSolidNormReal tendsto_natCast_atTop_atTop instIsOrderedRing instArchimedean
tendsto_one_add_div_pow_exp 📖	mathematical	—	Filter.Tendsto Real Monoid.toNatPow instMonoid instAdd instOne DivInvMonoid.toDiv instDivInvMonoid instNatCast Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace exp	—	Filter.Tendsto.congr rpow_natCast Filter.Tendsto.comp tendsto_one_add_div_rpow_exp tendsto_natCast_atTop_atTop instIsOrderedRing instArchimedean
tendsto_one_add_div_rpow_exp 📖	mathematical	—	Filter.Tendsto Real instPow instAdd instOne DivInvMonoid.toDiv instDivInvMonoid Filter.atTop instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace exp	—	tendsto_one_add_rpow_exp_of_tendsto tendsto_nhds_of_eventually_eq Filter.mp_mem Filter.eventually_ne_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial instIsOrderedRing instNontrivial Filter.univ_mem' mul_div_cancel₀ Nat.cast_zero
tendsto_one_add_pow_exp_of_tendsto 📖	mathematical	Filter.Tendsto Real instMul instNatCast Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace	Monoid.toNatPow instMonoid instAdd instOne exp	—	Filter.Tendsto.congr instIsStrictOrderedRing Nat.floor_natCast rpow_natCast Filter.Tendsto.comp tendsto_one_add_rpow_exp_of_tendsto tendsto_smul_comp_nat_floor_of_tendsto_mul instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors instIsDomain GroupWithZero.toNoZeroSMulDivisors NormedSpace.toNormSMulClass RCLike.instNormSMulClassInt instHasSolidNormReal tendsto_natCast_atTop_atTop instIsOrderedRing instArchimedean
tendsto_one_add_rpow_exp_of_tendsto 📖	mathematical	Filter.Tendsto Real instMul Filter.atTop instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace	instPow instAdd instOne exp	—	tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors NormedSpace.toNormSMulClass Filter.Tendsto.isBoundedUnder_le BoundedLENhdsClass.of_closedIciTopology instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal instIsOrderedAddMonoid Filter.Tendsto.norm Filter.tendsto_id' cobounded_eq Filter.tendsto_ofReal_iff Complex.ofReal_exp Filter.Tendsto.congr' Complex.tendsto_one_add_cpow_exp_of_tendsto Complex.ofReal_mul Filter.mp_mem Filter.Tendsto.eventually_const_le instClosedIicTopology IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Filter.univ_mem' Complex.ofReal_cpow le_of_not_gt 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.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.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_zero 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.Linarith.add_lt_of_le_of_neg instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le instIsOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Complex.ofReal_add Complex.ofReal_one

---

← Back to Index