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.

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

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

theorem ExpGrowth.expGrowthInf_def {u : ℕ → ENNReal} : expGrowthInf u = LinearGrowth.linearGrowthInf (ENNReal.log ∘ u)

theorem ExpGrowth.expGrowthSup_def {u : ℕ → ENNReal} : expGrowthSup u = LinearGrowth.linearGrowthSup (ENNReal.log ∘ u)

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) = min (expGrowthInf u) (expGrowthInf v)

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

Lower exponential growth as an InfTopHom.

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) = max (expGrowthSup u) (expGrowthSup v)

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

Upper exponential growth as a SupBotHom.

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} : max (expGrowthInf u) (expGrowthInf v) ≤ expGrowthInf (u + v)

theorem ExpGrowth.expGrowthSup_add {u v : ℕ → ENNReal} : expGrowthSup (u + v) = max (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.le_expGrowthInf_comp {u : ℕ → ENNReal} {v : ℕ → ℕ} (hu : 1 ≤ᶠ[Filter.atTop] u) (hv : Filter.Tendsto v Filter.atTop Filter.atTop) : (LinearGrowth.linearGrowthInf fun (n : ℕ) => ↑(v n)) * expGrowthInf u ≤ expGrowthInf (u ∘ v)

theorem ExpGrowth.expGrowthSup_comp_le {u : ℕ → ENNReal} {v : ℕ → ℕ} (hu : ∃ᶠ (n : ℕ) in Filter.atTop, 1 ≤ u n) (hv₀ : (LinearGrowth.linearGrowthSup fun (n : ℕ) => ↑(v n)) ≠ 0) (hv₁ : (LinearGrowth.linearGrowthSup fun (n : ℕ) => ↑(v n)) ≠ ⊤) (hv₂ : Filter.Tendsto v Filter.atTop Filter.atTop) : expGrowthSup (u ∘ v) ≤ (LinearGrowth.linearGrowthSup fun (n : ℕ) => ↑(v n)) * 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₀ : (LinearGrowth.linearGrowthSup fun (n : ℕ) => ↑(v n)) ≠ 0) (hv₁ : (LinearGrowth.linearGrowthSup fun (n : ℕ) => ↑(v n)) ≠ ⊤) : ExpGrowth.expGrowthInf (u ∘ v) ≤ (LinearGrowth.linearGrowthSup fun (n : ℕ) => ↑(v n)) * ExpGrowth.expGrowthInf u

theorem Monotone.le_expGrowthSup_comp {u : ℕ → ENNReal} {v : ℕ → ℕ} (h : Monotone u) (hv : (LinearGrowth.linearGrowthInf fun (n : ℕ) => ↑(v n)) ≠ 0) : (LinearGrowth.linearGrowthInf fun (n : ℕ) => ↑(v n)) * 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} (h : 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 : ℕ} (h : Monotone u) (hm : m ≠ 0) : (ExpGrowth.expGrowthInf fun (n : ℕ) => u (m * n)) = ↑m * ExpGrowth.expGrowthInf u

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