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

TODO

Get bounds on expGrowthSup (u ∘ v) with suitable hypotheses on v : ℕ → ℕ : linear growth of v, monotonicity.

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

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 {a : ENNReal} (h : a ≠ 0) (h' : a ≠ ⊤) : (expGrowthInf fun (x : ℕ) => a) = 0

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

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

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

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} {C : ENNReal} (hC : C ≠ ⊤) (h : ∀ᶠ (n : ℕ) in Filter.atTop, u n ≤ C * v n) : expGrowthInf u ≤ expGrowthInf v

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

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

theorem ExpGrowth.expGrowthSup_of_eventually_ge {u v : ℕ → ENNReal} {c : ENNReal} (hc : c ≠ 0) (h : ∀ᶠ (n : ℕ) in Filter.atTop, c * 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)