Asymptotics

📁 Source: Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean

Statistics

Metric	Count
Definitions	0
Theorems id_rpow_of_le_one, mul_atTop_rpow_natCast_of_isBigO_rpow, mul_atTop_rpow_of_isBigO_rpow, rpow, rpow_rpow_nhdsGE_zero_of_le, rpow_rpow_nhdsGE_zero_of_le_of_imp, rpow, rpow, rpow, isBigO_atTop_natCast_rpow_of_tendsto_div_rpow, isBigO_cpow_rpow, isTheta_cpow_const_rpow, isTheta_cpow_rpow, isTheta_exp_arg_mul_im, tendsto_rpow_at_top, tendsto_rpow_atTop, isLittleO_abs_log_rpow_rpow_nhdsGT_zero, isLittleO_exp_mul_rpow_of_lt, isLittleO_exp_neg_mul_rpow_atTop, isLittleO_log_rpow_atTop, isLittleO_log_rpow_nhdsGT_zero, isLittleO_log_rpow_rpow_atTop, isLittleO_pow_exp_pos_mul_atTop, isLittleO_rpow_exp_atTop, isLittleO_rpow_exp_pos_mul_atTop, isLittleO_zpow_exp_pos_mul_atTop, tendsto_exp_div_rpow_atTop, tendsto_exp_mul_div_rpow_atTop, tendsto_log_div_rpow_nhdsGT_zero, tendsto_log_mul_rpow_nhdsGT_zero, tendsto_log_mul_self_nhdsLT_zero, tendsto_rpow_atBot_of_base_gt_one, tendsto_rpow_atBot_of_base_lt_one, tendsto_rpow_atTop, tendsto_rpow_atTop_of_base_gt_one, tendsto_rpow_atTop_of_base_lt_one, tendsto_rpow_div, tendsto_rpow_div_mul_add, tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero, tendsto_rpow_neg_atTop, tendsto_rpow_neg_div, tendsto_rpow_neg_nhdsGT_zero	42
Total	42

Asymptotics

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isBigO_atTop_natCast_rpow_of_tendsto_div_rpow 📖	mathematical	Filter.Tendsto DivInvMonoid.toDiv DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField RCLike.ofReal Real Real.instPow Real.instNatCast Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing	IsBigO NormedField.toNorm Real.norm	—	IsBigO.of_norm_left isBigO_of_div_tendsto_nhds Filter.mp_mem Filter.eventually_ne_atTop instNoTopOrderOfNoMaxOrder Nat.instNoMaxOrder Filter.univ_mem' Real.instIsOrderedRing RCLike.charZero_rclike instIsEmptyFalse Filter.Tendsto.congr norm_div norm_algebraMap' NormedDivisionRing.to_normOneClass abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.rpow_nonneg Nat.cast_nonneg' Real.instZeroLEOneClass Filter.Tendsto.norm

Asymptotics.IsBigO

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
id_rpow_of_le_one 📖	mathematical	Real Real.instLE Real.instOne	Asymptotics.IsBigO Real.norm nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero Set.Ici Real.instPreorder Real.instPow	—	Real.rpow_one rpow_rpow_nhdsGE_zero_of_le NeZero.charZero_one RCLike.charZero_rclike
mul_atTop_rpow_natCast_of_isBigO_rpow 📖	mathematical	Asymptotics.IsBigO Real SeminormedRing.toNorm Real.norm Filter.atTop Nat.instPreorder Real.instPow Real.instNatCast Real.instLE Real.instAdd	Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SeminormedRing.toRing	—	trans mul NormedDivisionRing.toNormMulClass Filter.Eventually.isBigO Filter.mp_mem Filter.eventually_ge_atTop Filter.univ_mem' Nat.one_le_cast IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike Real.rpow_add LT.lt.trans_le zero_lt_one NeZero.charZero_one Real.norm_of_nonneg Real.rpow_nonneg LE.le.trans zero_le_one Real.rpow_le_rpow_of_exponent_le
mul_atTop_rpow_of_isBigO_rpow 📖	mathematical	Asymptotics.IsBigO Real SeminormedRing.toNorm Real.norm Filter.atTop Real.instPreorder Real.instPow Real.instLE Real.instAdd	Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SeminormedRing.toRing	—	trans mul NormedDivisionRing.toNormMulClass Filter.Eventually.isBigO Filter.mp_mem Filter.eventually_ge_atTop Filter.univ_mem' Real.rpow_add LT.lt.trans_le zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Real.norm_of_nonneg Real.rpow_nonneg LE.le.trans zero_le_one Real.rpow_le_rpow_of_exponent_le
rpow 📖	mathematical	Real Real.instLE Real.instZero Filter.EventuallyLE Pi.instZero Asymptotics.IsBigO Real.norm	Real.instPow	—	exists_nonneg Asymptotics.IsBigOWith.isBigO Asymptotics.IsBigOWith.rpow
rpow_rpow_nhdsGE_zero_of_le 📖	mathematical	Real Real.instLE	Asymptotics.IsBigO Real.norm nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero Set.Ici Real.instPreorder Real.instPow	—	rpow_rpow_nhdsGE_zero_of_le_of_imp
rpow_rpow_nhdsGE_zero_of_le_of_imp 📖	mathematical	Real Real.instLE Real.instZero	Asymptotics.IsBigO Real.norm nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Ici Real.instPreorder Real.instPow	—	of_bound' Filter.mem_of_superset Icc_mem_nhdsGE instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid one_pos Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Real.abs_rpow_of_nonneg abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.rpow_le_rpow_of_exponent_ge_of_imp

Asymptotics.IsBigOWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rpow 📖	mathematical	Asymptotics.IsBigOWith Real Real.norm Real.instLE Real.instZero Filter.EventuallyLE Pi.instZero	Real.instPow	—	of_bound Filter.mp_mem bound Filter.univ_mem' Real.abs_rpow_le_abs_rpow Real.rpow_le_rpow abs_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Real.mul_rpow Real.abs_rpow_of_nonneg

Asymptotics.IsLittleO

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rpow 📖	mathematical	Real Real.instLT Real.instZero Filter.EventuallyLE Real.instLE Pi.instZero Asymptotics.IsLittleO Real.norm	Real.instPow	—	of_isBigOWith Real.rpow_inv_rpow LT.lt.le LT.lt.ne' Asymptotics.IsBigOWith.rpow forall_isBigOWith Real.rpow_pos_of_pos le_of_lt

Asymptotics.IsTheta

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rpow 📖	mathematical	Real Real.instLE Real.instZero Filter.EventuallyLE Pi.instZero Asymptotics.IsTheta Real.norm	Real.instPow	—	Asymptotics.IsBigO.rpow

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isBigO_cpow_rpow 📖	mathematical	Filter.IsBoundedUnder Real Real.instLE abs Real.lattice Real.instAddGroup im	Asymptotics.IsBigO Complex instNorm Real.norm instPow Real.instPow Norm.norm re	—	Asymptotics.isBigO_of_le LE.le.trans norm_cpow_le le_abs_self Asymptotics.IsTheta.div Asymptotics.isTheta_refl isTheta_exp_arg_mul_im div_one
isTheta_cpow_const_rpow 📖	mathematical	Filter.Eventually Complex instZero	Asymptotics.IsTheta Real instNorm Real.norm instPow Real.instPow Norm.norm re	—	isTheta_cpow_rpow Filter.isBoundedUnder_const instReflLe Imp.swap
isTheta_cpow_rpow 📖	mathematical	Filter.IsBoundedUnder Real Real.instLE abs Real.lattice Real.instAddGroup im Filter.Eventually	Asymptotics.IsTheta Complex instNorm Real.norm instPow Real.instPow Norm.norm re	—	Asymptotics.IsTheta.of_norm_eventuallyEq Filter.Eventually.mono norm_cpow_of_imp Asymptotics.IsTheta.div Asymptotics.isTheta_refl isTheta_exp_arg_mul_im div_one
isTheta_exp_arg_mul_im 📖	mathematical	Filter.IsBoundedUnder Real Real.instLE abs Real.lattice Real.instAddGroup im	Asymptotics.IsTheta Real.norm Real.exp Real.instMul arg Real.instOne	—	Real.isTheta_exp_comp_one Filter.eventually_map Filter.Eventually.mono abs_mul Real.instIsOrderedRing mul_le_mul IsOrderedRing.toPosMulMono IsOrderedRing.toMulPosMono abs_arg_le_pi abs_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add LT.lt.le Real.pi_pos

ENNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tendsto_rpow_at_top 📖	mathematical	Real Real.instLT Real.instZero	Filter.Tendsto ENNReal instPowReal nhds instTopologicalSpace Top.top instTopENNReal	—	tendsto_nhds_top_iff_nnreal Filter.HasBasis.tendsto_iff Filter.atTop_basis_Ioi instIsDirectedOrder NNReal.instIsOrderedRing NNReal.instArchimedean IsStrictOrderedRing.toNoMaxOrder NNReal.instIsStrictOrderedRing NNReal.tendsto_rpow_atTop Ioi_mem_nhds instClosedIicTopology OrderTopology.to_orderClosedTopology instOrderTopology coe_lt_top Filter.mp_mem Filter.univ_mem' top_rpow_of_pos CanLift.prf canLift coe_rpow_of_nonneg LT.lt.le

NNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tendsto_rpow_atTop 📖	mathematical	Real Real.instLT Real.instZero	Filter.Tendsto NNReal instPowReal Filter.atTop PartialOrder.toPreorder instPartialOrderNNReal	—	Filter.tendsto_atTop_atTop instIsDirectedOrder instIsOrderedRing instArchimedean Real.instIsOrderedRing Real.instArchimedean tendsto_rpow_atTop Real.toNNReal_le_iff_le_coe

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLittleO_abs_log_rpow_rpow_nhdsGT_zero 📖	mathematical	Real Real.instLT Real.instZero	Asymptotics.IsLittleO Real.norm nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Ioi Real.instPreorder Real.instPow abs Real.lattice Real.instAddGroup Real.log	—	Asymptotics.IsLittleO.congr' Asymptotics.IsLittleO.comp_tendsto isLittleO_log_rpow_rpow_atTop neg_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid tendsto_inv_nhdsGT_zero Real.instIsStrictOrderedRing instOrderTopologyReal Filter.mem_of_superset Icc_mem_nhdsGT instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal one_pos Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Real.log_inv abs_of_nonpos Real.log_nonpos Filter.Eventually.mono eventually_mem_nhdsWithin Real.inv_rpow LT.lt.le Membership.mem.out Real.rpow_neg inv_inv
isLittleO_exp_mul_rpow_of_lt 📖	mathematical	Real Real.instLT	Asymptotics.IsLittleO Real.norm Filter.atTop Real.instPreorder Real.instMul Real.exp Real.instPow	—	Asymptotics.isLittleO_of_tendsto Real.exp_ne_zero neg_sub mul_comm tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
isLittleO_exp_neg_mul_rpow_atTop 📖	mathematical	Real Real.instLT Real.instZero	Asymptotics.IsLittleO Real.norm Filter.atTop Real.instPreorder Real.exp Real.instMul Real.instNeg Real.instPow	—	Asymptotics.isLittleO_of_tendsto' Filter.Eventually.mono Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial LT.lt.ne' Real.rpow_eq_zero_iff_of_nonneg LT.lt.le Filter.Tendsto.congr' Filter.eventually_ge_atTop Real.rpow_neg div_inv_eq_mul mul_inv_rev neg_mul Real.exp_neg 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.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_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.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.cons_ne_zero ne_of_gt Real.exp_pos one_ne_zero NeZero.one GroupWithZero.toNontrivial one_div Filter.Tendsto.inv_tendsto_atTop Real.instIsStrictOrderedRing instOrderTopologyReal tendsto_exp_mul_div_rpow_atTop
isLittleO_log_rpow_atTop 📖	mathematical	Real Real.instLT Real.instZero	Asymptotics.IsLittleO Real.norm Filter.atTop Real.instPreorder Real.log Real.instPow	—	Asymptotics.isBigO_self_const_mul NormedDivisionRing.toNormMulClass LT.lt.ne' Filter.Eventually.mono Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Real.log_rpow Asymptotics.IsLittleO.comp_tendsto Real.isLittleO_log_id_atTop tendsto_rpow_atTop
isLittleO_log_rpow_nhdsGT_zero 📖	mathematical	Real Real.instLT Real.instZero	Asymptotics.IsLittleO Real.norm nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Ioi Real.instPreorder Real.log Real.instPow	—	Asymptotics.IsLittleO.congr' Asymptotics.IsLittleO.neg_left isLittleO_abs_log_rpow_rpow_nhdsGT_zero Filter.mem_of_superset Icc_mem_nhdsGT instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid one_pos Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Real.rpow_one abs_of_nonpos IsOrderedAddMonoid.toAddLeftMono Real.log_nonpos neg_neg Filter.EventuallyEq.rfl
isLittleO_log_rpow_rpow_atTop 📖	mathematical	Real Real.instLT Real.instZero	Asymptotics.IsLittleO Real.norm Filter.atTop Real.instPreorder Real.instPow Real.log	—	lt_max_iff one_pos Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Asymptotics.IsBigO.of_norm_eventuallyLE Filter.mp_mem Filter.Tendsto.eventually_ge_atTop Real.tendsto_log_atTop Filter.univ_mem' Real.norm_of_nonneg le_of_lt Real.rpow_pos_of_pos lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Real.rpow_le_rpow_of_exponent_le le_max_left Asymptotics.IsLittleO.rpow Filter.Tendsto.eventually tendsto_rpow_atTop Filter.eventually_ge_atTop isLittleO_log_rpow_atTop Filter.Eventually.mono Real.rpow_mul div_mul_cancel₀ LT.lt.ne'
isLittleO_pow_exp_pos_mul_atTop 📖	mathematical	Real Real.instLT Real.instZero	Asymptotics.IsLittleO Real.norm Filter.atTop Real.instPreorder Monoid.toNatPow Real.instMonoid Real.exp Real.instMul	—	zpow_natCast isLittleO_zpow_exp_pos_mul_atTop
isLittleO_rpow_exp_atTop 📖	mathematical	—	Asymptotics.IsLittleO Real Real.norm Filter.atTop Real.instPreorder Real.instPow Real.exp	—	one_mul isLittleO_rpow_exp_pos_mul_atTop one_pos Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike
isLittleO_rpow_exp_pos_mul_atTop 📖	mathematical	Real Real.instLT Real.instZero	Asymptotics.IsLittleO Real.norm Filter.atTop Real.instPreorder Real.instPow Real.exp Real.instMul	—	Asymptotics.isLittleO_of_tendsto LT.lt.ne' Real.exp_pos div_eq_mul_inv neg_mul Real.exp_neg tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero
isLittleO_zpow_exp_pos_mul_atTop 📖	mathematical	Real Real.instLT Real.instZero	Asymptotics.IsLittleO Real.norm Filter.atTop Real.instPreorder DivInvMonoid.toZPow Real.instDivInvMonoid Real.exp Real.instMul	—	Real.rpow_intCast isLittleO_rpow_exp_pos_mul_atTop
tendsto_exp_div_rpow_atTop 📖	mathematical	—	Filter.Tendsto Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.exp Real.instPow Filter.atTop Real.instPreorder	—	archimedean_iff_nat_lt Real.instIsStrictOrderedRing Real.instArchimedean Filter.tendsto_atTop_mono' Filter.mp_mem Filter.eventually_ge_atTop Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Filter.univ_mem' div_le_div₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono le_of_lt Real.exp_pos le_refl Real.rpow_pos_of_pos Real.rpow_natCast Real.rpow_le_rpow_of_exponent_le LT.lt.le Real.tendsto_exp_div_pow_atTop
tendsto_exp_mul_div_rpow_atTop 📖	mathematical	Real Real.instLT Real.instZero	Filter.Tendsto DivInvMonoid.toDiv Real.instDivInvMonoid Real.exp Real.instMul Real.instPow Filter.atTop Real.instPreorder	—	Filter.Tendsto.congr' Filter.mp_mem Filter.eventually_ge_atTop Filter.univ_mem' Real.div_rpow LT.lt.le Real.exp_pos mul_comm IsUnit.div_mul_cancel LT.lt.ne' Filter.Tendsto.comp tendsto_rpow_atTop tendsto_exp_div_rpow_atTop
tendsto_log_div_rpow_nhdsGT_zero 📖	mathematical	Real Real.instLT Real.instZero	Filter.Tendsto DivInvMonoid.toDiv Real.instDivInvMonoid Real.log Real.instPow nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Ioi Real.instPreorder nhds	—	Asymptotics.IsLittleO.tendsto_div_nhds_zero isLittleO_log_rpow_nhdsGT_zero
tendsto_log_mul_rpow_nhdsGT_zero 📖	mathematical	Real Real.instLT Real.instZero	Filter.Tendsto Real.instMul Real.log Real.instPow nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Ioi Real.instPreorder nhds	—	Filter.Tendsto.congr' Filter.Eventually.mono eventually_mem_nhdsWithin Real.rpow_neg LT.lt.le Membership.mem.out div_inv_eq_mul tendsto_log_div_rpow_nhdsGT_zero neg_lt_zero IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
tendsto_log_mul_self_nhdsLT_zero 📖	mathematical	—	Filter.Tendsto Real Real.instMul Real.log nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero Set.Iio Real.instPreorder nhds	—	tendsto_log_mul_rpow_nhdsGT_zero zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Real.log_abs abs_of_nonpos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid LT.lt.le mul_neg neg_neg tendsto_nhdsWithin_congr neg_zero Filter.Tendsto.neg IsTopologicalRing.toContinuousNeg instIsTopologicalRingReal Filter.Tendsto.comp Real.rpow_one Filter.Tendsto.mono_left tendsto_abs_nhdsNE_zero instOrderTopologyReal nhdsWithin_mono LT.lt.ne
tendsto_rpow_atBot_of_base_gt_one 📖	mathematical	Real Real.instLT Real.instOne	Filter.Tendsto Real.instPow Filter.atBot Real.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	—	Real.rpow_def_of_pos lt_trans Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Filter.Tendsto.comp Real.tendsto_exp_atBot Filter.tendsto_const_mul_atBot_of_pos Real.instIsStrictOrderedRing Real.log_pos_iff le_of_lt Filter.tendsto_id
tendsto_rpow_atBot_of_base_lt_one 📖	mathematical	Real Real.instLT Real.instZero Real.instOne	Filter.Tendsto Real.instPow Filter.atBot Real.instPreorder Filter.atTop	—	Real.rpow_def_of_pos Filter.Tendsto.comp Real.tendsto_exp_atTop Filter.tendsto_const_mul_atTop_iff_neg Real.instIsStrictOrderedRing Filter.atBot_neBot instIsCodirectedOrder Real.instIsOrderedRing Real.instArchimedean Filter.tendsto_id Real.log_neg_iff
tendsto_rpow_atTop 📖	mathematical	Real Real.instLT Real.instZero	Filter.Tendsto Real.instPow Filter.atTop Real.instPreorder	—	Filter.HasBasis.tendsto_right_iff Filter.atTop_basis' instIsDirectedOrder Real.instIsOrderedRing Real.instArchimedean Filter.mp_mem Filter.eventually_ge_atTop Filter.univ_mem' one_div
tendsto_rpow_atTop_of_base_gt_one 📖	mathematical	Real Real.instLT Real.instOne	Filter.Tendsto Real.instPow Filter.atBot Real.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	—	tendsto_rpow_atBot_of_base_gt_one
tendsto_rpow_atTop_of_base_lt_one 📖	mathematical	Real Real.instLT Real.instNeg Real.instOne	Filter.Tendsto Real.instPow Filter.atTop Real.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	—	lt_trichotomy Real.rpow_def_of_nonpos LT.lt.le LT.lt.ne Asymptotics.isLittleO_const_iff one_ne_zero NeZero.charZero_one RCLike.charZero_rclike one_mul Asymptotics.IsLittleO.mul_isBigO NormedDivisionRing.toNormMulClass Filter.Tendsto.comp Real.tendsto_exp_atBot Filter.tendsto_const_mul_atBot_of_neg Real.instIsStrictOrderedRing Real.log_neg_eq_log Real.log_neg_iff 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 Mathlib.Tactic.Linarith.sub_neg_of_lt Real.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 Filter.tendsto_id Asymptotics.isBigO_iff Filter.Eventually.of_forall CStarRing.norm_of_mem_unitary instCStarRingReal Real.instNontrivial SubmonoidClass.toOneMemClass Submonoid.instSubmonoidClass mul_one Filter.Tendsto.mono_right Filter.tendsto_pure Filter.mp_mem Filter.eventually_ne_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Filter.univ_mem' Real.zero_rpow pure_le_nhds_iff T5Space.toT1Space OrderTopology.t5Space instOrderTopologyReal Real.rpow_def_of_pos
tendsto_rpow_div 📖	mathematical	—	Filter.Tendsto Real Real.instPow DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne Filter.atTop Real.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one 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.cast_zero Nat.cast_zero tendsto_rpow_div_mul_add zero_ne_one NeZero.charZero_one RCLike.charZero_rclike
tendsto_rpow_div_mul_add 📖	mathematical	—	Filter.Tendsto Real Real.instPow DivInvMonoid.toDiv Real.instDivInvMonoid Real.instAdd Real.instMul Filter.atTop Real.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instOne	—	Filter.Tendsto.congr' Filter.eventuallyEq_of_mem Filter.Ioi_mem_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Real.exp_log Real.rpow_pos_of_pos Real.log_rpow 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.div_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq 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.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.cons_ne_zero ne_of_gt Real.exp_pos one_ne_zero NeZero.one GroupWithZero.toNontrivial Filter.Tendsto.comp Real.tendsto_exp_nhds_zero_nhds_one pow_one MulZeroClass.mul_zero Filter.Tendsto.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal tendsto_const_nhds Real.tendsto_div_pow_mul_exp_add_atTop Real.tendsto_log_atTop
tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero 📖	mathematical	Real Real.instLT Real.instZero	Filter.Tendsto Real.instMul Real.instPow Real.exp Real.instNeg Filter.atTop Real.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	Filter.Tendsto.congr' Filter.univ_mem' inv_div div_eq_mul_inv neg_mul Real.exp_neg Filter.Tendsto.inv_tendsto_atTop Real.instIsStrictOrderedRing instOrderTopologyReal tendsto_exp_mul_div_rpow_atTop
tendsto_rpow_neg_atTop 📖	mathematical	Real Real.instLT Real.instZero	Filter.Tendsto Real.instPow Real.instNeg Filter.atTop Real.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	Filter.Tendsto.congr' Filter.eventuallyEq_of_mem Filter.Ioi_mem_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Real.rpow_neg le_of_lt Filter.Tendsto.inv_tendsto_atTop Real.instIsStrictOrderedRing instOrderTopologyReal tendsto_rpow_atTop
tendsto_rpow_neg_div 📖	mathematical	—	Filter.Tendsto Real Real.instPow DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNeg Real.instOne Filter.atTop Real.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one 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.cast_zero Nat.cast_zero tendsto_rpow_div_mul_add zero_ne_one NeZero.charZero_one RCLike.charZero_rclike
tendsto_rpow_neg_nhdsGT_zero 📖	mathematical	Real Real.instLT Real.instZero	Filter.Tendsto Real.instPow nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Ioi Real.instPreorder Filter.atTop	—	neg_neg Real.rpow_neg_eq_inv_rpow Filter.Tendsto.comp tendsto_rpow_atTop neg_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid tendsto_inv_nhdsGT_zero Real.instIsStrictOrderedRing instOrderTopologyReal

---

← Back to Index