Documentation

Mathlib.Analysis.Asymptotics.ExpGrowth

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) :

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

Equations

Instances For

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

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

Equations

Instances For

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.

Equations

Instances For

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.

Equations

Instances For

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