ExpGrowth

📁 Source: Mathlib/Analysis/Asymptotics/ExpGrowth.lean

Statistics

Metric	Count
Definitions expGrowthInf, expGrowthInfTopHom, expGrowthSup, expGrowthSupBotHom	4
Theorems expGrowthSup_le, le_expGrowthInf, eventually_exp_le, eventually_le_exp, expGrowthInf_biInf, expGrowthInf_comp_nonneg, expGrowthInf_congr, expGrowthInf_const, expGrowthInf_def, expGrowthInf_eventually_monotone, expGrowthInf_exp, expGrowthInf_iInf, expGrowthInf_inf, expGrowthInf_inv, expGrowthInf_le_expGrowthSup, expGrowthInf_le_expGrowthSup_of_frequently_le, expGrowthInf_le_iff, expGrowthInf_le_of_eventually_le, expGrowthInf_monotone, expGrowthInf_mul_le, expGrowthInf_mul_le', expGrowthInf_of_eventually_ge, expGrowthInf_pow, expGrowthInf_top, expGrowthInf_zero, expGrowthSup_add, expGrowthSup_biSup, expGrowthSup_comp_le, expGrowthSup_comp_nonneg, expGrowthSup_congr, expGrowthSup_const, expGrowthSup_def, expGrowthSup_eventually_monotone, expGrowthSup_exp, expGrowthSup_iSup, expGrowthSup_inv, expGrowthSup_le_iff, expGrowthSup_le_of_eventually_le, expGrowthSup_monotone, expGrowthSup_mul_le, expGrowthSup_of_eventually_ge, expGrowthSup_pow, expGrowthSup_sum, expGrowthSup_sup, expGrowthSup_top, expGrowthSup_zero, frequently_exp_le, frequently_le_exp, le_expGrowthInf_add, le_expGrowthInf_comp, le_expGrowthInf_iff, le_expGrowthInf_mul, le_expGrowthSup_iff, le_expGrowthSup_mul, le_expGrowthSup_mul', expGrowthInf_le, le_expGrowthSup, expGrowthInf_comp, expGrowthInf_comp_le, expGrowthInf_comp_mul, expGrowthInf_nonneg, expGrowthSup_comp, expGrowthSup_comp_mul, expGrowthSup_nonneg, le_expGrowthSup_comp	65
Total	69

Eventually

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
expGrowthSup_le 📖	mathematical	Filter.Eventually ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EReal.exp EReal EReal.instMul AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneEReal Filter.atTop Nat.instPreorder	instPartialOrderEReal ExpGrowth.expGrowthSup	—	ExpGrowth.expGrowthSup_le_iff Filter.Eventually.mono LE.le.trans EReal.exp_monotone mul_le_mul_of_nonneg_right EReal.instMulPosMono le_of_lt Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoidEReal instZeroLEOneClassEReal
le_expGrowthInf 📖	mathematical	Filter.Eventually ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EReal.exp EReal EReal.instMul AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneEReal Filter.atTop Nat.instPreorder	instPartialOrderEReal ExpGrowth.expGrowthInf	—	ExpGrowth.le_expGrowthInf_iff Filter.Eventually.mono LE.le.trans' EReal.exp_monotone mul_le_mul_of_nonneg_right EReal.instMulPosMono le_of_lt Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoidEReal instZeroLEOneClassEReal

ExpGrowth

Definitions

Name	Category	Theorems
expGrowthInf 📖	CompOp	34 math math: expGrowthInf_of_eventually_ge, expGrowthInf_exp, Monotone.expGrowthInf_comp_mul, expGrowthInf_le_iff, expGrowthInf_eventually_monotone, expGrowthInf_mul_le, Monotone.expGrowthInf_comp, expGrowthInf_comp_nonneg, expGrowthInf_inv, expGrowthSup_inv, expGrowthInf_le_expGrowthSup_of_frequently_le, expGrowthInf_monotone, le_expGrowthInf_comp, expGrowthInf_le_of_eventually_le, Frequently.expGrowthInf_le, expGrowthInf_inf, le_expGrowthInf_add, le_expGrowthInf_iff, expGrowthInf_iInf, Monotone.expGrowthInf_comp_le, expGrowthInf_congr, Monotone.expGrowthInf_nonneg, expGrowthInf_biInf, Eventually.le_expGrowthInf, le_expGrowthSup_mul', expGrowthInf_def, expGrowthInf_mul_le', expGrowthInf_const, expGrowthInf_pow, expGrowthInf_top, expGrowthInf_zero, le_expGrowthSup_mul, le_expGrowthInf_mul, expGrowthInf_le_expGrowthSup
expGrowthInfTopHom 📖	CompOp	—
expGrowthSup 📖	CompOp	35 math math: Monotone.expGrowthSup_nonneg, expGrowthSup_add, expGrowthSup_sum, expGrowthSup_def, expGrowthSup_biSup, expGrowthInf_mul_le, expGrowthInf_inv, expGrowthSup_inv, expGrowthInf_le_expGrowthSup_of_frequently_le, expGrowthSup_const, expGrowthSup_zero, expGrowthSup_exp, expGrowthSup_of_eventually_ge, expGrowthSup_mul_le, expGrowthSup_congr, expGrowthSup_pow, expGrowthSup_comp_le, Frequently.le_expGrowthSup, expGrowthSup_comp_nonneg, expGrowthSup_eventually_monotone, le_expGrowthSup_mul', expGrowthInf_mul_le', expGrowthSup_top, expGrowthSup_le_iff, expGrowthSup_sup, Eventually.expGrowthSup_le, expGrowthSup_le_of_eventually_le, Monotone.expGrowthSup_comp, Monotone.expGrowthSup_comp_mul, le_expGrowthSup_mul, expGrowthSup_iSup, le_expGrowthSup_iff, expGrowthInf_le_expGrowthSup, expGrowthSup_monotone, Monotone.le_expGrowthSup_comp
expGrowthSupBotHom 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eventually_exp_le 📖	mathematical	EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal expGrowthInf	Filter.Eventually ENNReal Preorder.toLE ENNReal.instPartialOrder EReal.exp EReal.instMul AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneEReal Filter.atTop Nat.instPreorder	—	le_expGrowthInf_iff le_refl
eventually_le_exp 📖	mathematical	EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal expGrowthSup	Filter.Eventually ENNReal Preorder.toLE ENNReal.instPartialOrder EReal.exp EReal.instMul AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneEReal Filter.atTop Nat.instPreorder	—	expGrowthSup_le_iff le_refl
expGrowthInf_biInf 📖	mathematical	—	expGrowthInf iInf Pi.infSet ENNReal ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder Set Set.instMembership EReal instInfSetEReal	—	map_finset_inf InfTopHom.instInfTopHomClass expGrowthInf_inf expGrowthInf_top Finset.inf_eq_iInf iInf_congr_Prop Set.Finite.mem_toFinset
expGrowthInf_comp_nonneg 📖	mathematical	Monotone ENNReal Nat.instPreorder PartialOrder.toPreorder ENNReal.instPartialOrder Filter.Tendsto Filter.atTop	EReal Preorder.toLE instPartialOrderEReal instZeroEReal expGrowthInf	—	LinearGrowth.linearGrowthInf_comp_nonneg Monotone.comp ENNReal.log_monotone
expGrowthInf_congr 📖	mathematical	Filter.EventuallyEq ENNReal Filter.atTop Nat.instPreorder	expGrowthInf	—	Filter.liminf_congr Filter.Eventually.mono
expGrowthInf_const 📖	mathematical	—	expGrowthInf EReal instZeroEReal	—	Filter.Tendsto.liminf_eq EReal.instOrderTopology Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat EReal.tendsto_const_div_atTop_nhds_zero_nat ENNReal.log_eq_bot_iff ENNReal.log_eq_top_iff
expGrowthInf_def 📖	mathematical	—	expGrowthInf LinearGrowth.linearGrowthInf EReal ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderEReal DivInvMonoid.toDiv EReal.instDivInvMonoid AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneEReal ENNReal ENNReal.log	—	—
expGrowthInf_eventually_monotone 📖	mathematical	Filter.EventuallyLE ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Filter.atTop Nat.instPreorder	EReal instPartialOrderEReal expGrowthInf	—	Filter.liminf_le_liminf Filter.Eventually.mono EReal.monotone_div_right_of_nonneg Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoidEReal instZeroLEOneClassEReal ENNReal.log_monotone Filter.isBounded_ge_of_bot Filter.isCobounded_ge_of_top
expGrowthInf_exp 📖	mathematical	—	expGrowthInf EReal.exp EReal EReal.instMul AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneEReal	—	le_antisymm Frequently.expGrowthInf_le Filter.Frequently.of_forall Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat le_refl Eventually.le_expGrowthInf Filter.Eventually.of_forall
expGrowthInf_iInf 📖	mathematical	—	expGrowthInf iInf Pi.infSet ENNReal ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder EReal instInfSetEReal	—	iInf_univ expGrowthInf_biInf Set.finite_univ
expGrowthInf_inf 📖	mathematical	—	expGrowthInf Pi.instMinForall_mathlib ENNReal ENNReal.instMin EReal SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderEReal	—	expGrowthInf.eq_1 liminf_min Filter.isCobounded_ge_of_top Filter.isBounded_ge_of_bot Filter.liminf_congr Filter.Eventually.of_forall Pi.inf_apply Monotone.map_min ENNReal.log_monotone EReal.monotone_div_right_of_nonneg Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoidEReal instZeroLEOneClassEReal
expGrowthInf_inv 📖	mathematical	—	expGrowthInf Pi.instInv ENNReal ENNReal.instInv EReal EReal.instNeg expGrowthSup	—	expGrowthSup.eq_1 EReal.liminf_neg Filter.liminf_congr Filter.Eventually.of_forall Pi.neg_apply Pi.inv_apply div_eq_mul_inv EReal.neg_mul ENNReal.log_inv
expGrowthInf_le_expGrowthSup 📖	mathematical	—	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal expGrowthInf expGrowthSup	—	Filter.liminf_le_limsup Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.isBounded_le_of_top Filter.isBounded_ge_of_bot
expGrowthInf_le_expGrowthSup_of_frequently_le 📖	mathematical	Filter.Frequently ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Filter.atTop Nat.instPreorder	EReal instPartialOrderEReal expGrowthInf expGrowthSup	—	Filter.liminf_le_limsup_of_frequently_le Filter.Frequently.mono EReal.div_le_div_right_of_nonneg Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoidEReal instZeroLEOneClassEReal ENNReal.log_le_log Filter.isBounded_ge_of_bot Filter.isBounded_le_of_top
expGrowthInf_le_iff 📖	mathematical	—	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal expGrowthInf Filter.Frequently ENNReal ENNReal.instPartialOrder EReal.exp EReal.instMul AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneEReal Filter.atTop Nat.instPreorder	—	expGrowthInf.eq_1 Filter.liminf_le_iff' instDenselyOrderedEReal Filter.isCobounded_ge_of_top Filter.isBounded_ge_of_bot Filter.frequently_congr Filter.eventually_atTop instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat EReal.div_le_iff_le_mul Nat.cast_zero IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoidEReal instZeroLEOneClassEReal instCharZeroEReal EReal.natCast_ne_top EReal.log_exp mul_comm OrderIso.le_iff_le
expGrowthInf_le_of_eventually_le 📖	mathematical	Filter.Eventually ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Filter.atTop Nat.instPreorder	EReal instPartialOrderEReal expGrowthInf	—	LE.le.trans expGrowthInf_eventually_monotone eq_zero_or_pos ENNReal.instCanonicallyOrderedAdd MulZeroClass.zero_mul expGrowthInf_zero LE.le.trans_eq expGrowthInf_mul_le expGrowthSup_const LT.lt.ne' EReal.zero_ne_bot EReal.zero_ne_top zero_add
expGrowthInf_monotone 📖	mathematical	—	Monotone EReal Pi.preorder ENNReal PartialOrder.toPreorder ENNReal.instPartialOrder instPartialOrderEReal expGrowthInf	—	expGrowthInf_eventually_monotone Filter.Eventually.of_forall
expGrowthInf_mul_le 📖	mathematical	—	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal expGrowthInf Pi.instMul ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instAddCommMonoidEReal expGrowthSup	—	LE.le.trans_eq' EReal.liminf_add_le Filter.liminf_congr Filter.Eventually.of_forall Pi.add_apply Pi.mul_apply EReal.add_div_of_nonneg_right Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoidEReal instZeroLEOneClassEReal ENNReal.log_mul_add
expGrowthInf_mul_le' 📖	mathematical	—	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal expGrowthInf Pi.instMul ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instAddCommMonoidEReal expGrowthSup	—	mul_comm add_comm expGrowthInf_mul_le
expGrowthInf_of_eventually_ge 📖	mathematical	Filter.Eventually ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Filter.atTop Nat.instPreorder	EReal instPartialOrderEReal expGrowthInf	—	LE.le.trans' expGrowthInf_eventually_monotone le_expGrowthInf_mul eq_top_or_lt_top Pi.top_def expGrowthInf_top le_add_of_nonneg_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoidEReal le_top expGrowthInf_const LT.lt.ne zero_add le_refl
expGrowthInf_pow 📖	mathematical	—	expGrowthInf ENNReal Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.log	—	expGrowthInf.eq_1 Filter.liminf_const Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.liminf_congr Filter.eventually_atTop EReal.div_eq_iff EReal.natCast_ne_bot EReal.natCast_ne_top LT.lt.ne LT.lt.trans_le zero_lt_one instZeroLEOneClassEReal NeZero.charZero_one instCharZeroEReal Nat.one_le_cast IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoidEReal ENNReal.log_pow mul_comm
expGrowthInf_top 📖	mathematical	—	expGrowthInf Top.top Pi.instTopForall ENNReal instTopENNReal EReal EReal.instTop	—	LinearGrowth.linearGrowthInf_top expGrowthInf_def
expGrowthInf_zero 📖	mathematical	—	expGrowthInf Pi.instZero ENNReal instZeroENNReal Bot.bot EReal instBotEReal	—	le_bot_iff expGrowthSup_zero expGrowthInf_le_expGrowthSup
expGrowthSup_add 📖	mathematical	—	expGrowthSup Pi.instAdd ENNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring EReal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderEReal	—	expGrowthSup_sup le_antisymm expGrowthSup_le_of_eventually_le Nat.instAtLeastTwoHAddOfNat ENNReal.ofNat_ne_top Filter.Eventually.of_forall Pi.sup_apply Pi.add_apply two_mul add_le_add IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add le_max_left le_max_right expGrowthSup_monotone sup_le self_le_add_right ENNReal.instCanonicallyOrderedAdd self_le_add_left
expGrowthSup_biSup 📖	mathematical	—	expGrowthSup iSup Pi.supSet ENNReal ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder Set Set.instMembership EReal instSupSetEReal	—	map_finset_sup SupBotHom.instSupBotHomClass expGrowthSup_sup expGrowthSup_zero Finset.sup_eq_iSup iSup_congr_Prop Set.Finite.mem_toFinset
expGrowthSup_comp_le 📖	mathematical	Filter.Frequently ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Filter.atTop Nat.instPreorder Filter.Tendsto	EReal instPartialOrderEReal expGrowthSup EReal.instMul LinearGrowth.linearGrowthSup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderEReal DivInvMonoid.toDiv EReal.instDivInvMonoid AddMonoidWithOne.toNatCast instAddCommMonoidWithOneEReal	—	LinearGrowth.linearGrowthSup_comp_le Filter.Frequently.mono ENNReal.zero_le_log_iff
expGrowthSup_comp_nonneg 📖	mathematical	Monotone ENNReal Nat.instPreorder PartialOrder.toPreorder ENNReal.instPartialOrder Filter.Tendsto Filter.atTop	EReal Preorder.toLE instPartialOrderEReal instZeroEReal expGrowthSup	—	LE.le.trans expGrowthInf_comp_nonneg expGrowthInf_le_expGrowthSup
expGrowthSup_congr 📖	mathematical	Filter.EventuallyEq ENNReal Filter.atTop Nat.instPreorder	expGrowthSup	—	Filter.limsup_congr Filter.Eventually.mono
expGrowthSup_const 📖	mathematical	—	expGrowthSup EReal instZeroEReal	—	Filter.Tendsto.limsup_eq EReal.instOrderTopology Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat EReal.tendsto_const_div_atTop_nhds_zero_nat ENNReal.log_eq_bot_iff ENNReal.log_eq_top_iff
expGrowthSup_def 📖	mathematical	—	expGrowthSup LinearGrowth.linearGrowthSup EReal ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderEReal DivInvMonoid.toDiv EReal.instDivInvMonoid AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneEReal ENNReal ENNReal.log	—	—
expGrowthSup_eventually_monotone 📖	mathematical	Filter.EventuallyLE ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Filter.atTop Nat.instPreorder	EReal instPartialOrderEReal expGrowthSup	—	Filter.limsup_le_limsup Filter.Eventually.mono EReal.monotone_div_right_of_nonneg Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoidEReal instZeroLEOneClassEReal ENNReal.log_monotone Filter.isCobounded_le_of_bot Filter.isBounded_le_of_top
expGrowthSup_exp 📖	mathematical	—	expGrowthSup EReal.exp EReal EReal.instMul AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneEReal	—	le_antisymm Eventually.expGrowthSup_le Filter.Eventually.of_forall le_refl Frequently.le_expGrowthSup Filter.Frequently.of_forall Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat
expGrowthSup_iSup 📖	mathematical	—	expGrowthSup iSup Pi.supSet ENNReal ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder EReal instSupSetEReal	—	iSup_univ expGrowthSup_biSup Set.finite_univ
expGrowthSup_inv 📖	mathematical	—	expGrowthSup Pi.instInv ENNReal ENNReal.instInv EReal EReal.instNeg expGrowthInf	—	expGrowthInf.eq_1 EReal.limsup_neg Filter.limsup_congr Filter.Eventually.of_forall Pi.neg_apply Pi.inv_apply div_eq_mul_inv EReal.neg_mul ENNReal.log_inv
expGrowthSup_le_iff 📖	mathematical	—	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal expGrowthSup Filter.Eventually ENNReal ENNReal.instPartialOrder EReal.exp EReal.instMul AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneEReal Filter.atTop Nat.instPreorder	—	expGrowthSup.eq_1 Filter.limsup_le_iff' instDenselyOrderedEReal Filter.isCobounded_le_of_bot Filter.isBounded_le_of_top Filter.eventually_congr Filter.eventually_atTop instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat EReal.div_le_iff_le_mul Nat.cast_zero IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoidEReal instZeroLEOneClassEReal instCharZeroEReal EReal.natCast_ne_top EReal.log_exp mul_comm OrderIso.le_iff_le
expGrowthSup_le_of_eventually_le 📖	mathematical	Filter.Eventually ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Filter.atTop Nat.instPreorder	EReal instPartialOrderEReal expGrowthSup	—	LE.le.trans expGrowthSup_eventually_monotone eq_zero_or_pos ENNReal.instCanonicallyOrderedAdd MulZeroClass.zero_mul expGrowthSup_zero LE.le.trans_eq expGrowthSup_mul_le expGrowthSup_const LT.lt.ne' EReal.zero_ne_bot EReal.zero_ne_top zero_add
expGrowthSup_monotone 📖	mathematical	—	Monotone EReal Pi.preorder ENNReal PartialOrder.toPreorder ENNReal.instPartialOrder instPartialOrderEReal expGrowthSup	—	expGrowthSup_eventually_monotone Filter.Eventually.of_forall
expGrowthSup_mul_le 📖	mathematical	—	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal expGrowthSup Pi.instMul ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instAddCommMonoidEReal	—	LE.le.trans_eq' EReal.limsup_add_le Filter.limsup_congr Filter.Eventually.of_forall Pi.add_apply Pi.mul_apply ENNReal.log_mul_add EReal.add_div_of_nonneg_right Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoidEReal instZeroLEOneClassEReal
expGrowthSup_of_eventually_ge 📖	mathematical	Filter.Eventually ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Filter.atTop Nat.instPreorder	EReal instPartialOrderEReal expGrowthSup	—	LE.le.trans' expGrowthSup_eventually_monotone le_expGrowthSup_mul' eq_top_or_lt_top le_add_of_nonneg_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoidEReal le_top expGrowthInf_top expGrowthInf_const LT.lt.ne zero_add le_refl
expGrowthSup_pow 📖	mathematical	—	expGrowthSup ENNReal Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.log	—	expGrowthSup.eq_1 Filter.limsup_const Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.limsup_congr Filter.eventually_atTop EReal.div_eq_iff EReal.natCast_ne_bot EReal.natCast_ne_top LT.lt.ne LT.lt.trans_le zero_lt_one instZeroLEOneClassEReal NeZero.charZero_one instCharZeroEReal Nat.one_le_cast IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoidEReal ENNReal.log_pow mul_comm
expGrowthSup_sum 📖	mathematical	—	expGrowthSup Finset.sum Pi.addCommMonoid ENNReal ENNReal.instAddCommMonoid iSup EReal instSupSetEReal Finset Finset.instMembership	—	Finset.induction_on Finset.sum_empty Finset.iSup_coe Finset.coe_empty iSup_emptyset expGrowthSup_zero Finset.sum_insert expGrowthSup_add Finset.coe_insert iSup_insert
expGrowthSup_sup 📖	mathematical	—	expGrowthSup Pi.instMaxForall_mathlib ENNReal ENNReal.instMax EReal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderEReal	—	expGrowthSup.eq_1 limsup_max Filter.isCobounded_le_of_bot Filter.isBounded_le_of_top Filter.limsup_congr Filter.Eventually.of_forall Pi.sup_apply Monotone.map_max ENNReal.log_monotone EReal.monotone_div_right_of_nonneg Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoidEReal instZeroLEOneClassEReal
expGrowthSup_top 📖	mathematical	—	expGrowthSup Top.top Pi.instTopForall ENNReal instTopENNReal EReal EReal.instTop	—	top_le_iff expGrowthInf_top expGrowthInf_le_expGrowthSup
expGrowthSup_zero 📖	mathematical	—	expGrowthSup Pi.instZero ENNReal instZeroENNReal Bot.bot EReal instBotEReal	—	LinearGrowth.linearGrowthSup_bot expGrowthSup_def Pi.zero_apply Pi.bot_apply ENNReal.log_zero
frequently_exp_le 📖	mathematical	EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal expGrowthSup	Filter.Frequently ENNReal Preorder.toLE ENNReal.instPartialOrder EReal.exp EReal.instMul AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneEReal Filter.atTop Nat.instPreorder	—	le_expGrowthSup_iff le_refl
frequently_le_exp 📖	mathematical	EReal Preorder.toLT PartialOrder.toPreorder instPartialOrderEReal expGrowthInf	Filter.Frequently ENNReal Preorder.toLE ENNReal.instPartialOrder EReal.exp EReal.instMul AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneEReal Filter.atTop Nat.instPreorder	—	expGrowthInf_le_iff le_refl
le_expGrowthInf_add 📖	mathematical	—	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderEReal expGrowthInf Pi.instAdd ENNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	sup_le expGrowthInf_monotone le_self_add Pi.instCanonicallyOrderedAddForall ENNReal.instCanonicallyOrderedAdd le_add_self
le_expGrowthInf_comp 📖	mathematical	Filter.EventuallyLE ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Filter.atTop Nat.instPreorder Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Filter.Tendsto	EReal instPartialOrderEReal EReal.instMul LinearGrowth.linearGrowthInf ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderEReal DivInvMonoid.toDiv EReal.instDivInvMonoid AddMonoidWithOne.toNatCast instAddCommMonoidWithOneEReal expGrowthInf	—	LinearGrowth.le_linearGrowthInf_comp Filter.Eventually.mono Pi.zero_apply ENNReal.zero_le_log_iff Pi.one_apply
le_expGrowthInf_iff 📖	mathematical	—	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal expGrowthInf Filter.Eventually ENNReal ENNReal.instPartialOrder EReal.exp EReal.instMul AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneEReal Filter.atTop Nat.instPreorder	—	expGrowthInf.eq_1 Filter.le_liminf_iff' instDenselyOrderedEReal Filter.isCobounded_ge_of_top Filter.isBounded_ge_of_bot Filter.eventually_congr Filter.eventually_atTop instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat EReal.le_div_iff_mul_le Nat.cast_zero IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoidEReal instZeroLEOneClassEReal instCharZeroEReal EReal.natCast_ne_top EReal.log_exp OrderIso.le_iff_le
le_expGrowthInf_mul 📖	mathematical	—	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instAddCommMonoidEReal expGrowthInf Pi.instMul ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	LE.le.trans_eq EReal.le_liminf_add Filter.liminf_congr Filter.Eventually.of_forall Pi.add_apply Pi.mul_apply EReal.add_div_of_nonneg_right Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoidEReal instZeroLEOneClassEReal ENNReal.log_mul_add
le_expGrowthSup_iff 📖	mathematical	—	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal expGrowthSup Filter.Frequently ENNReal ENNReal.instPartialOrder EReal.exp EReal.instMul AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneEReal Filter.atTop Nat.instPreorder	—	expGrowthSup.eq_1 Filter.le_limsup_iff' instDenselyOrderedEReal Filter.isCobounded_le_of_bot Filter.isBounded_le_of_top Filter.frequently_congr Filter.eventually_atTop instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat EReal.le_div_iff_mul_le Nat.cast_zero IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoidEReal instZeroLEOneClassEReal instCharZeroEReal EReal.natCast_ne_top EReal.log_exp OrderIso.le_iff_le
le_expGrowthSup_mul 📖	mathematical	—	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instAddCommMonoidEReal expGrowthSup expGrowthInf Pi.instMul ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	LE.le.trans_eq EReal.le_limsup_add Filter.limsup_congr Filter.Eventually.of_forall Pi.add_apply Pi.mul_apply ENNReal.log_mul_add EReal.add_div_of_nonneg_right Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoidEReal instZeroLEOneClassEReal
le_expGrowthSup_mul' 📖	mathematical	—	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instAddCommMonoidEReal expGrowthInf expGrowthSup Pi.instMul ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	mul_comm add_comm le_expGrowthSup_mul

Frequently

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
expGrowthInf_le 📖	mathematical	Filter.Frequently ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EReal.exp EReal EReal.instMul AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneEReal Filter.atTop Nat.instPreorder	instPartialOrderEReal ExpGrowth.expGrowthInf	—	ExpGrowth.expGrowthInf_le_iff Filter.Frequently.mono LE.le.trans EReal.exp_monotone mul_le_mul_of_nonneg_right EReal.instMulPosMono le_of_lt Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoidEReal instZeroLEOneClassEReal
le_expGrowthSup 📖	mathematical	Filter.Frequently ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EReal.exp EReal EReal.instMul AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneEReal Filter.atTop Nat.instPreorder	instPartialOrderEReal ExpGrowth.expGrowthSup	—	ExpGrowth.le_expGrowthSup_iff Filter.Frequently.mono LE.le.trans' EReal.exp_monotone mul_le_mul_of_nonneg_right EReal.instMulPosMono le_of_lt Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoidEReal instZeroLEOneClassEReal

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
expGrowthInf_comp 📖	mathematical	Monotone ENNReal Nat.instPreorder PartialOrder.toPreorder ENNReal.instPartialOrder Filter.Tendsto EReal DivInvMonoid.toDiv EReal.instDivInvMonoid AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneEReal Filter.atTop nhds EReal.instTopologicalSpace	ExpGrowth.expGrowthInf EReal.instMul	—	linearGrowthInf_comp comp ENNReal.log_monotone
expGrowthInf_comp_le 📖	mathematical	Monotone ENNReal Nat.instPreorder PartialOrder.toPreorder ENNReal.instPartialOrder	EReal Preorder.toLE instPartialOrderEReal ExpGrowth.expGrowthInf EReal.instMul LinearGrowth.linearGrowthSup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderEReal DivInvMonoid.toDiv EReal.instDivInvMonoid AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneEReal	—	linearGrowthInf_comp_le comp ENNReal.log_monotone
expGrowthInf_comp_mul 📖	mathematical	Monotone ENNReal Nat.instPreorder PartialOrder.toPreorder ENNReal.instPartialOrder	ExpGrowth.expGrowthInf EReal EReal.instMul AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneEReal	—	linearGrowthInf_comp_mul comp ENNReal.log_monotone
expGrowthInf_nonneg 📖	mathematical	Monotone ENNReal Nat.instPreorder PartialOrder.toPreorder ENNReal.instPartialOrder	EReal Preorder.toLE instPartialOrderEReal instZeroEReal ExpGrowth.expGrowthInf	—	linearGrowthInf_nonneg comp ENNReal.log_monotone
expGrowthSup_comp 📖	mathematical	Monotone ENNReal Nat.instPreorder PartialOrder.toPreorder ENNReal.instPartialOrder Filter.Tendsto EReal DivInvMonoid.toDiv EReal.instDivInvMonoid AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneEReal Filter.atTop nhds EReal.instTopologicalSpace	ExpGrowth.expGrowthSup EReal.instMul	—	linearGrowthSup_comp comp ENNReal.log_monotone
expGrowthSup_comp_mul 📖	mathematical	Monotone ENNReal Nat.instPreorder PartialOrder.toPreorder ENNReal.instPartialOrder	ExpGrowth.expGrowthSup EReal EReal.instMul AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneEReal	—	linearGrowthSup_comp_mul comp ENNReal.log_monotone
expGrowthSup_nonneg 📖	mathematical	Monotone ENNReal Nat.instPreorder PartialOrder.toPreorder ENNReal.instPartialOrder	EReal Preorder.toLE instPartialOrderEReal instZeroEReal ExpGrowth.expGrowthSup	—	LE.le.trans expGrowthInf_nonneg ExpGrowth.expGrowthInf_le_expGrowthSup
le_expGrowthSup_comp 📖	mathematical	Monotone ENNReal Nat.instPreorder PartialOrder.toPreorder ENNReal.instPartialOrder	EReal Preorder.toLE instPartialOrderEReal EReal.instMul LinearGrowth.linearGrowthInf ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderEReal DivInvMonoid.toDiv EReal.instDivInvMonoid AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneEReal ExpGrowth.expGrowthSup	—	le_linearGrowthSup_comp comp ENNReal.log_monotone

---

← Back to Index