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_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	41
Total	41

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 Real NormedField.toNorm DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.norm Filter.atTop Nat.instPreorder Real.instPow Real.instNatCast	—	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 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	Asymptotics.IsBigO Real SeminormedRing.toNorm Real.norm Filter.atTop Nat.instPreorder Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SeminormedRing.toRing Real.instPow Real.instNatCast	—	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	Asymptotics.IsBigO Real SeminormedRing.toNorm Real.norm Filter.atTop Real.instPreorder Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SeminormedRing.toRing Real.instPow	—	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	Asymptotics.IsBigO Real 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 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 Real.norm nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero 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	Asymptotics.IsBigOWith Real Real.norm 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	Asymptotics.IsLittleO Real 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	Filter.EventuallyLE Real Real.instLE Pi.instZero Real.instZero Asymptotics.IsTheta Real.norm	Asymptotics.IsTheta Real Real.norm Real.instPow	—	Asymptotics.IsBigO.rpow Asymptotics.isTheta_inv Mathlib.Tactic.GCongr.rel_imp_rel instIsTransOfTrans symm Filter.EventuallyEq.isTheta Filter.Eventually.mono Real.rpow_neg Asymptotics.isTheta_refl 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.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_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing lt_of_not_ge

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 Real 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 Complex 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 Real 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 Real.norm Real.exp Real.instMul arg im 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 Real instPowReal nhds instTopologicalSpace Top.top instTopENNReal	—	tendsto_nhds_top_iff_nnreal Filter.HasBasis.tendsto_iff Filter.atTop_basis_Ioi instIsDirectedOrder IsStrictOrderedRing.toNoMaxOrder 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 Real instPowReal Filter.atTop PartialOrder.toPreorder instPartialOrder	—	Filter.tendsto_atTop_atTop instIsDirectedOrder 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 Real.norm nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero 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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid 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 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 instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add
isLittleO_exp_neg_mul_rpow_atTop 📖	mathematical	Real Real.instLT Real.instZero	Asymptotics.IsLittleO Real 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 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 Real.norm nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero 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 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 Real.norm Filter.atTop Real.instPreorder Monoid.toPow 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 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 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 Real 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 Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.log Real.instPow nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero 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 Real.instMul Real.log Real.instPow nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero 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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid 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 IsSemitopologicalRing.toContinuousNeg IsTopologicalRing.toIsSemitopologicalRing 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 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 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 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_lt_one 📖	mathematical	Real Real.instLT Real.instNeg Real.instOne	Filter.Tendsto Real 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 Real.instMul Real.instPow Real.exp Real.instNeg Filter.atTop Real.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	—	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 Real.instPow Real.instNeg Filter.atTop Real.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	—	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 Real.instPow nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero 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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid tendsto_inv_nhdsGT_zero Real.instIsStrictOrderedRing instOrderTopologyReal

---

← Back to Index