Mathlib Map

Theorems · Definition · approximation theory

ExpGrowth.expGrowthSup

(ℕ → ENNReal) → EReal

Upper exponential growth of a sequence of extended nonnegative real numbers.

Defined in
Mathlib.Analysis.Asymptotics.ExpGrowth
Cited by
42 results in Mathlib
Foundations
Depth 170 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Dynamics.coverEntropyEntourage · cited by 20Dynamics.coverEntropyEnto…ExpGrowth.expGrowthSup_monotone · cited by 12ExpGrowth.expGrowthSup_mo…Dynamics.netEntropyEntourage · cited by 11Dynamics.netEntropyEntour…ExpGrowth.expGrowthSup_zero · cited by 6ExpGrowth.expGrowthSup_ze…ExpGrowth.expGrowthInf_le_expGrowthSup · cited by 6ExpGrowth.expGrowthInf_le…ExpGrowth.expGrowthSup_const · cited by 4ExpGrowth.expGrowthSup_co…ExpGrowth.expGrowthSup_eventually_monotone · cited by 3ExpGrowth.expGrowthSup_ev…ExpGrowth.expGrowthInf_mul_le · cited by 2ExpGrowth.expGrowthInf_mu…ExpGrowth.expGrowthSup_add · cited by 2ExpGrowth.expGrowthSup_addExpGrowth.expGrowthSup_le_iff · cited by 2ExpGrowth.expGrowthSup_le…ExpGrowth.expGrowthSup_sup · cited by 2ExpGrowth.expGrowthSup_supDynamics.coverEntropyEntourage_empty · cited by 2Dynamics.coverEntropyEnto…Dynamics.coverEntropyEntourage_le_log_coverMincard_div · cited by 2Dynamics.coverEntropyEnto…ExpGrowth.le_expGrowthSup_iff · cited by 2ExpGrowth.le_expGrowthSup…ExpGrowth.le_expGrowthSup_mul' · cited by 1ExpGrowth.le_expGrowthSup…ENNReal · cited by 9879ENNRealFilter.atTop · cited by 2405Filter.atTopEReal · cited by 793ERealFilter.limsup · cited by 226Filter.limsupENNReal.log · cited by 72ENNReal.logExpGrowth.expGrowthSupCITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by45

Results whose statement or proof uses this declaration.