Exponential growth

This file defines the exponential growth of a sequence u : ℕ → ℝ≥0∞. This notion comes in two versions, using a liminf and a limsup respectively.

Main definitions

• expGrowthInf, expGrowthSup: respectively, liminf and limsup of log (u n) / n.
• expGrowthInfTopHom, expGrowthSupBotHom: the functions expGrowthInf, expGrowthSup as homomorphisms preserving finitary Inf/Sup respectively.

Tags

asymptotics, exponential

Definition

noncomputable def ExpGrowth.expGrowthInf (u : ℕ → ENNReal) : EReal

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

Equations

• ExpGrowth.expGrowthInf u = Filter.liminf (fun (n : ℕ) => (u n).log / ↑n) Filter.atTop

noncomputable def ExpGrowth.expGrowthSup (u : ℕ → ENNReal) : EReal

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

Equations

• ExpGrowth.expGrowthSup u = Filter.limsup (fun (n : ℕ) => (u n).log / ↑n) Filter.atTop

Basic properties

theorem ExpGrowth.expGrowthInf_congr {u v : ℕ → ENNReal} (h : u =ᶠ[Filter.atTop] v) : expGrowthInf u = expGrowthInf v

theorem ExpGrowth.expGrowthSup_congr {u v : ℕ → ENNReal} (h : u =ᶠ[Filter.atTop] v) : expGrowthSup u = expGrowthSup v

theorem ExpGrowth.expGrowthInf_eventually_monotone {u v : ℕ → ENNReal} (h : u ≤ᶠ[Filter.atTop] v) : expGrowthInf u ≤ expGrowthInf v

theorem ExpGrowth.expGrowthInf_monotone : Monotone expGrowthInf

theorem ExpGrowth.expGrowthSup_eventually_monotone {u v : ℕ → ENNReal} (h : u ≤ᶠ[Filter.atTop] v) : expGrowthSup u ≤ expGrowthSup v

theorem ExpGrowth.expGrowthSup_monotone : Monotone expGrowthSup

theorem ExpGrowth.expGrowthInf_le_expGrowthSup {u : ℕ → ENNReal} : expGrowthInf u ≤ expGrowthSup u

theorem ExpGrowth.expGrowthInf_le_expGrowthSup_of_frequently_le {u v : ℕ → ENNReal} (h : ∃ᶠ (n : ℕ) in Filter.atTop, u n ≤ v n) : expGrowthInf u ≤ expGrowthSup v

theorem ExpGrowth.expGrowthInf_le_iff {u : ℕ → ENNReal} {a : EReal} : expGrowthInf u ≤ a ↔ ∀ b > a, ∃ᶠ (n : ℕ) in Filter.atTop, u n ≤ (b * ↑n).exp

theorem ExpGrowth.le_expGrowthInf_iff {u : ℕ → ENNReal} {a : EReal} : a ≤ expGrowthInf u ↔ ∀ b < a, ∀ᶠ (n : ℕ) in Filter.atTop, (b * ↑n).exp ≤ u n

theorem ExpGrowth.expGrowthSup_le_iff {u : ℕ → ENNReal} {a : EReal} : expGrowthSup u ≤ a ↔ ∀ b > a, ∀ᶠ (n : ℕ) in Filter.atTop, u n ≤ (b * ↑n).exp

theorem ExpGrowth.le_expGrowthSup_iff {u : ℕ → ENNReal} {a : EReal} : a ≤ expGrowthSup u ↔ ∀ b < a, ∃ᶠ (n : ℕ) in Filter.atTop, (b * ↑n).exp ≤ u n

theorem ExpGrowth.frequently_le_exp {u : ℕ → ENNReal} {a : EReal} (h : expGrowthInf u < a) : ∃ᶠ (n : ℕ) in Filter.atTop, u n ≤ (a * ↑n).exp

theorem ExpGrowth.eventually_exp_le {u : ℕ → ENNReal} {a : EReal} (h : a < expGrowthInf u) : ∀ᶠ (n : ℕ) in Filter.atTop, (a * ↑n).exp ≤ u n

theorem ExpGrowth.eventually_le_exp {u : ℕ → ENNReal} {a : EReal} (h : expGrowthSup u < a) : ∀ᶠ (n : ℕ) in Filter.atTop, u n ≤ (a * ↑n).exp

theorem ExpGrowth.frequently_exp_le {u : ℕ → ENNReal} {a : EReal} (h : a < expGrowthSup u) : ∃ᶠ (n : ℕ) in Filter.atTop, (a * ↑n).exp ≤ u n

theorem Frequently.expGrowthInf_le {u : ℕ → ENNReal} {a : EReal} (h : ∃ᶠ (n : ℕ) in Filter.atTop, u n ≤ (a * ↑n).exp) : ExpGrowth.expGrowthInf u ≤ a

theorem Eventually.le_expGrowthInf {u : ℕ → ENNReal} {a : EReal} (h : ∀ᶠ (n : ℕ) in Filter.atTop, (a * ↑n).exp ≤ u n) : a ≤ ExpGrowth.expGrowthInf u

theorem Eventually.expGrowthSup_le {u : ℕ → ENNReal} {a : EReal} (h : ∀ᶠ (n : ℕ) in Filter.atTop, u n ≤ (a * ↑n).exp) : ExpGrowth.expGrowthSup u ≤ a

theorem Frequently.le_expGrowthSup {u : ℕ → ENNReal} {a : EReal} (h : ∃ᶠ (n : ℕ) in Filter.atTop, (a * ↑n).exp ≤ u n) : a ≤ ExpGrowth.expGrowthSup u

Special cases

theorem ExpGrowth.expGrowthSup_zero : expGrowthSup 0 = ⊥

theorem ExpGrowth.expGrowthInf_zero : expGrowthInf 0 = ⊥

theorem ExpGrowth.expGrowthInf_top : expGrowthInf ⊤ = ⊤

theorem ExpGrowth.expGrowthSup_top : expGrowthSup ⊤ = ⊤

theorem ExpGrowth.expGrowthInf_const {b : ENNReal} (h : b ≠ 0) (h' : b ≠ ⊤) : (expGrowthInf fun (x : ℕ) => b) = 0

theorem ExpGrowth.expGrowthSup_const {b : ENNReal} (h : b ≠ 0) (h' : b ≠ ⊤) : (expGrowthSup fun (x : ℕ) => b) = 0

theorem ExpGrowth.expGrowthInf_pow {b : ENNReal} : (expGrowthInf fun (n : ℕ) => b ^ n) = b.log

theorem ExpGrowth.expGrowthSup_pow {b : ENNReal} : (expGrowthSup fun (n : ℕ) => b ^ n) = b.log

theorem ExpGrowth.expGrowthInf_exp {a : EReal} : (expGrowthInf fun (n : ℕ) => (a * ↑n).exp) = a

theorem ExpGrowth.expGrowthSup_exp {a : EReal} : (expGrowthSup fun (n : ℕ) => (a * ↑n).exp) = a

Multiplication and inversion

theorem ExpGrowth.le_expGrowthInf_mul {u v : ℕ → ENNReal} : expGrowthInf u + expGrowthInf v ≤ expGrowthInf (u * v)

theorem ExpGrowth.expGrowthInf_mul_le {u v : ℕ → ENNReal} (h : expGrowthSup u ≠ ⊥ ∨ expGrowthInf v ≠ ⊤) (h' : expGrowthSup u ≠ ⊤ ∨ expGrowthInf v ≠ ⊥) : expGrowthInf (u * v) ≤ expGrowthSup u + expGrowthInf v

See expGrowthInf_mul_le' for a version with swapped argument u and v.

theorem ExpGrowth.expGrowthInf_mul_le' {u v : ℕ → ENNReal} (h : expGrowthInf u ≠ ⊥ ∨ expGrowthSup v ≠ ⊤) (h' : expGrowthInf u ≠ ⊤ ∨ expGrowthSup v ≠ ⊥) : expGrowthInf (u * v) ≤ expGrowthInf u + expGrowthSup v

See expGrowthInf_mul_le for a version with swapped argument u and v.

theorem ExpGrowth.le_expGrowthSup_mul {u v : ℕ → ENNReal} : expGrowthSup u + expGrowthInf v ≤ expGrowthSup (u * v)

See le_expGrowthSup_mul' for a version with swapped argument u and v.

theorem ExpGrowth.le_expGrowthSup_mul' {u v : ℕ → ENNReal} : expGrowthInf u + expGrowthSup v ≤ expGrowthSup (u * v)

See le_expGrowthSup_mul for a version with swapped argument u and v.

theorem ExpGrowth.expGrowthSup_mul_le {u v : ℕ → ENNReal} (h : expGrowthSup u ≠ ⊥ ∨ expGrowthSup v ≠ ⊤) (h' : expGrowthSup u ≠ ⊤ ∨ expGrowthSup v ≠ ⊥) : expGrowthSup (u * v) ≤ expGrowthSup u + expGrowthSup v

theorem ExpGrowth.expGrowthInf_inv {u : ℕ → ENNReal} : expGrowthInf u⁻¹ = -expGrowthSup u

theorem ExpGrowth.expGrowthSup_inv {u : ℕ → ENNReal} : expGrowthSup u⁻¹ = -expGrowthInf u

Comparison

theorem ExpGrowth.expGrowthInf_le_of_eventually_le {u v : ℕ → ENNReal} {b : ENNReal} (hb : b ≠ ⊤) (h : ∀ᶠ (n : ℕ) in Filter.atTop, u n ≤ b * v n) : expGrowthInf u ≤ expGrowthInf v

theorem ExpGrowth.expGrowthSup_le_of_eventually_le {u v : ℕ → ENNReal} {b : ENNReal} (hb : b ≠ ⊤) (h : ∀ᶠ (n : ℕ) in Filter.atTop, u n ≤ b * v n) : expGrowthSup u ≤ expGrowthSup v

theorem ExpGrowth.expGrowthInf_of_eventually_ge {u v : ℕ → ENNReal} {b : ENNReal} (hb : b ≠ 0) (h : ∀ᶠ (n : ℕ) in Filter.atTop, b * u n ≤ v n) : expGrowthInf u ≤ expGrowthInf v

theorem ExpGrowth.expGrowthSup_of_eventually_ge {u v : ℕ → ENNReal} {b : ENNReal} (hb : b ≠ 0) (h : ∀ᶠ (n : ℕ) in Filter.atTop, b * u n ≤ v n) : expGrowthSup u ≤ expGrowthSup v

Infimum and supremum

theorem ExpGrowth.expGrowthInf_inf {u v : ℕ → ENNReal} : expGrowthInf (u ⊓ v) = expGrowthInf u ⊓ expGrowthInf v

noncomputable def ExpGrowth.expGrowthInfTopHom : InfTopHom (ℕ → ENNReal) EReal

Lower exponential growth as an InfTopHom.

Equations

• ExpGrowth.expGrowthInfTopHom = { toFun := ExpGrowth.expGrowthInf, map_inf' := ⋯, map_top' := ExpGrowth.expGrowthInf_top }

theorem ExpGrowth.expGrowthInf_biInf {α : Type u_1} (u : α → ℕ → ENNReal) {s : Set α} (hs : s.Finite) : expGrowthInf (⨅ x ∈ s, u x) = ⨅ x ∈ s, expGrowthInf (u x)

theorem ExpGrowth.expGrowthInf_iInf {ι : Type u_1} [Finite ι] (u : ι → ℕ → ENNReal) : expGrowthInf (⨅ (i : ι), u i) = ⨅ (i : ι), expGrowthInf (u i)

theorem ExpGrowth.expGrowthSup_sup {u v : ℕ → ENNReal} : expGrowthSup (u ⊔ v) = expGrowthSup u ⊔ expGrowthSup v

noncomputable def ExpGrowth.expGrowthSupBotHom : SupBotHom (ℕ → ENNReal) EReal

Upper exponential growth as a SupBotHom.

Equations

• ExpGrowth.expGrowthSupBotHom = { toFun := ExpGrowth.expGrowthSup, map_sup' := ⋯, map_bot' := ExpGrowth.expGrowthSup_zero }

theorem ExpGrowth.expGrowthSup_biSup {α : Type u_1} (u : α → ℕ → ENNReal) {s : Set α} (hs : s.Finite) : expGrowthSup (⨆ x ∈ s, u x) = ⨆ x ∈ s, expGrowthSup (u x)

theorem ExpGrowth.expGrowthSup_iSup {ι : Type u_1} [Finite ι] (u : ι → ℕ → ENNReal) : expGrowthSup (⨆ (i : ι), u i) = ⨆ (i : ι), expGrowthSup (u i)

Addition

theorem ExpGrowth.le_expGrowthInf_add {u v : ℕ → ENNReal} : expGrowthInf u ⊔ expGrowthInf v ≤ expGrowthInf (u + v)

theorem ExpGrowth.expGrowthSup_add {u v : ℕ → ENNReal} : expGrowthSup (u + v) = expGrowthSup u ⊔ expGrowthSup v

theorem ExpGrowth.expGrowthSup_sum {α : Type u_1} (u : α → ℕ → ENNReal) (s : Finset α) : expGrowthSup (∑ x ∈ s, u x) = ⨆ x ∈ s, expGrowthSup (u x)

Composition

theorem ExpGrowth.Real.eventually_atTop_exists_int_between {a b : ℝ} (h : a < b) : ∀ᶠ (x : ℝ) in Filter.atTop, ∃ (n : ℤ), a * x ≤ ↑n ∧ ↑n ≤ b * x

theorem ExpGrowth.Real.eventually_atTop_exists_nat_between {a b : ℝ} (h : a < b) (hb : 0 ≤ b) : ∀ᶠ (x : ℝ) in Filter.atTop, ∃ (n : ℕ), a * x ≤ ↑n ∧ ↑n ≤ b * x

theorem ExpGrowth.EReal.eventually_atTop_exists_nat_between {a b : EReal} (h : a < b) (hb : 0 ≤ b) : ∀ᶠ (n : ℕ) in Filter.atTop, ∃ (m : ℕ), a * ↑n ≤ ↑m ∧ ↑m ≤ b * ↑n

theorem ExpGrowth.linGrowthInf_nonneg (v : ℕ → ℕ) : 0 ≤ Filter.liminf (fun (n : ℕ) => ↑(v n) / ↑n) Filter.atTop

theorem ExpGrowth.tendsto_atTop_of_linGrowthInf_pos {v : ℕ → ℕ} (h : Filter.liminf (fun (n : ℕ) => ↑(v n) / ↑n) Filter.atTop ≠ 0) : Filter.Tendsto v Filter.atTop Filter.atTop

theorem ExpGrowth.le_expGrowthInf_comp {u : ℕ → ENNReal} {v : ℕ → ℕ} (hu : 1 ≤ᶠ[Filter.atTop] u) (hv : Filter.Tendsto v Filter.atTop Filter.atTop) : Filter.liminf (fun (n : ℕ) => ↑(v n) / ↑n) Filter.atTop * expGrowthInf u ≤ expGrowthInf (u ∘ v)

theorem ExpGrowth.expGrowthSup_comp_le {u : ℕ → ENNReal} {v : ℕ → ℕ} (hu : ∃ᶠ (n : ℕ) in Filter.atTop, 1 ≤ u n) (hv₀ : Filter.limsup (fun (n : ℕ) => ↑(v n) / ↑n) Filter.atTop ≠ 0) (hv₁ : Filter.limsup (fun (n : ℕ) => ↑(v n) / ↑n) Filter.atTop ≠ ⊤) (hv₂ : Filter.Tendsto v Filter.atTop Filter.atTop) : expGrowthSup (u ∘ v) ≤ Filter.limsup (fun (n : ℕ) => ↑(v n) / ↑n) Filter.atTop * expGrowthSup u

Monotone sequences

theorem Monotone.expGrowthInf_nonneg {u : ℕ → ENNReal} (h : Monotone u) (h' : u ≠ 0) : 0 ≤ ExpGrowth.expGrowthInf u

theorem Monotone.expGrowthSup_nonneg {u : ℕ → ENNReal} (h : Monotone u) (h' : u ≠ 0) : 0 ≤ ExpGrowth.expGrowthSup u

theorem ExpGrowth.expGrowthInf_comp_nonneg {u : ℕ → ENNReal} {v : ℕ → ℕ} (h : Monotone u) (h' : u ≠ 0) (hv : Filter.Tendsto v Filter.atTop Filter.atTop) : 0 ≤ expGrowthInf (u ∘ v)

theorem ExpGrowth.expGrowthSup_comp_nonneg {u : ℕ → ENNReal} {v : ℕ → ℕ} (h : Monotone u) (h' : u ≠ 0) (hv : Filter.Tendsto v Filter.atTop Filter.atTop) : 0 ≤ expGrowthSup (u ∘ v)

theorem Monotone.expGrowthInf_comp_le {u : ℕ → ENNReal} {v : ℕ → ℕ} (h : Monotone u) (hv₀ : Filter.limsup (fun (n : ℕ) => ↑(v n) / ↑n) Filter.atTop ≠ 0) (hv₁ : Filter.limsup (fun (n : ℕ) => ↑(v n) / ↑n) Filter.atTop ≠ ⊤) : ExpGrowth.expGrowthInf (u ∘ v) ≤ Filter.limsup (fun (n : ℕ) => ↑(v n) / ↑n) Filter.atTop * ExpGrowth.expGrowthInf u

theorem Monotone.le_expGrowthSup_comp {u : ℕ → ENNReal} {v : ℕ → ℕ} (h : Monotone u) (hv : Filter.liminf (fun (n : ℕ) => ↑(v n) / ↑n) Filter.atTop ≠ 0) : Filter.liminf (fun (n : ℕ) => ↑(v n) / ↑n) Filter.atTop * ExpGrowth.expGrowthSup u ≤ ExpGrowth.expGrowthSup (u ∘ v)

theorem Monotone.expGrowthInf_comp {u : ℕ → ENNReal} {v : ℕ → ℕ} {a : EReal} (h : Monotone u) (hv : Filter.Tendsto (fun (n : ℕ) => ↑(v n) / ↑n) Filter.atTop (nhds a)) (ha : a ≠ 0) (ha' : a ≠ ⊤) : ExpGrowth.expGrowthInf (u ∘ v) = a * ExpGrowth.expGrowthInf u

theorem Monotone.expGrowthSup_comp {u : ℕ → ENNReal} {v : ℕ → ℕ} {a : EReal} (hu : Monotone u) (hv : Filter.Tendsto (fun (n : ℕ) => ↑(v n) / ↑n) Filter.atTop (nhds a)) (ha : a ≠ 0) (ha' : a ≠ ⊤) : ExpGrowth.expGrowthSup (u ∘ v) = a * ExpGrowth.expGrowthSup u

theorem Monotone.expGrowthInf_comp_mul {u : ℕ → ENNReal} {m : ℕ} (hu : Monotone u) (hm : m ≠ 0) : (ExpGrowth.expGrowthInf fun (n : ℕ) => u (m * n)) = ↑m * ExpGrowth.expGrowthInf u

theorem Monotone.expGrowthSup_comp_mul {u : ℕ → ENNReal} {m : ℕ} (hu : Monotone u) (hm : m ≠ 0) : (ExpGrowth.expGrowthSup fun (n : ℕ) => u (m * n)) = ↑m * ExpGrowth.expGrowthSup u