Linear growth

This file defines the linear growth of a sequence u : ℕ → R. This notion comes in two versions, using a liminf and a limsup respectively. Most properties are developed for R = EReal.

Main definitions

• linearGrowthInf, linearGrowthSup: respectively, liminf and limsup of (u n) / n.
• linearGrowthInfTopHom, linearGrowthSupBotHom: the functions linearGrowthInf, linearGrowthSup as homomorphisms preserving finitary Inf/Sup respectively.

TODO

Generalize statements from EReal to ENNReal (or others). This may need additional typeclasses.

Lemma about coercion from ENNReal to EReal. This needs additional lemmas about ENNReal.toEReal.

Definition

noncomputable def LinearGrowth.linearGrowthInf {R : Type u_1} [ConditionallyCompleteLattice R] [Div R] [NatCast R] (u : ℕ → R) : R

Lower linear growth of a sequence.

noncomputable def LinearGrowth.linearGrowthSup {R : Type u_1} [ConditionallyCompleteLattice R] [Div R] [NatCast R] (u : ℕ → R) : R

Upper linear growth of a sequence.

Basic properties

theorem LinearGrowth.linearGrowthInf_congr {R : Type u_1} [ConditionallyCompleteLattice R] [Div R] [NatCast R] {u v : ℕ → R} (h : u =ᶠ[Filter.atTop] v) : linearGrowthInf u = linearGrowthInf v

theorem LinearGrowth.linearGrowthSup_congr {R : Type u_1} [ConditionallyCompleteLattice R] [Div R] [NatCast R] {u v : ℕ → R} (h : u =ᶠ[Filter.atTop] v) : linearGrowthSup u = linearGrowthSup v

theorem LinearGrowth.linearGrowthInf_le_linearGrowthSup {R : Type u_1} [ConditionallyCompleteLattice R] [Div R] [NatCast R] {u : ℕ → R} (h : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≤ x2) Filter.atTop fun (n : ℕ) => u n / ↑n := by isBoundedDefault) (h' : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≥ x2) Filter.atTop fun (n : ℕ) => u n / ↑n := by isBoundedDefault) : linearGrowthInf u ≤ linearGrowthSup u

theorem LinearGrowth.linearGrowthInf_eventually_monotone {u v : ℕ → EReal} (h : u ≤ᶠ[Filter.atTop] v) : linearGrowthInf u ≤ linearGrowthInf v

theorem LinearGrowth.linearGrowthInf_monotone {u v : ℕ → EReal} (h : u ≤ v) : linearGrowthInf u ≤ linearGrowthInf v

theorem LinearGrowth.linearGrowthSup_eventually_monotone {u v : ℕ → EReal} (h : u ≤ᶠ[Filter.atTop] v) : linearGrowthSup u ≤ linearGrowthSup v

theorem LinearGrowth.linearGrowthSup_monotone {u v : ℕ → EReal} (h : u ≤ v) : linearGrowthSup u ≤ linearGrowthSup v

theorem LinearGrowth.linearGrowthInf_le_linearGrowthSup_of_frequently_le {u v : ℕ → EReal} (h : ∃ᶠ (n : ℕ) in Filter.atTop, u n ≤ v n) : linearGrowthInf u ≤ linearGrowthSup v

theorem LinearGrowth.linearGrowthInf_le_iff {u : ℕ → EReal} {a : EReal} : linearGrowthInf u ≤ a ↔ ∀ b > a, ∃ᶠ (n : ℕ) in Filter.atTop, u n ≤ b * ↑n

theorem LinearGrowth.le_linearGrowthInf_iff {u : ℕ → EReal} {a : EReal} : a ≤ linearGrowthInf u ↔ ∀ b < a, ∀ᶠ (n : ℕ) in Filter.atTop, b * ↑n ≤ u n

theorem LinearGrowth.linearGrowthSup_le_iff {u : ℕ → EReal} {a : EReal} : linearGrowthSup u ≤ a ↔ ∀ b > a, ∀ᶠ (n : ℕ) in Filter.atTop, u n ≤ b * ↑n

theorem LinearGrowth.le_linearGrowthSup_iff {u : ℕ → EReal} {a : EReal} : a ≤ linearGrowthSup u ↔ ∀ b < a, ∃ᶠ (n : ℕ) in Filter.atTop, b * ↑n ≤ u n

theorem LinearGrowth.frequently_le_mul {u : ℕ → EReal} {a : EReal} (h : linearGrowthInf u < a) : ∃ᶠ (n : ℕ) in Filter.atTop, u n ≤ a * ↑n

theorem LinearGrowth.eventually_mul_le {u : ℕ → EReal} {a : EReal} (h : a < linearGrowthInf u) : ∀ᶠ (n : ℕ) in Filter.atTop, a * ↑n ≤ u n

theorem LinearGrowth.eventually_le_mul {u : ℕ → EReal} {a : EReal} (h : linearGrowthSup u < a) : ∀ᶠ (n : ℕ) in Filter.atTop, u n ≤ a * ↑n

theorem LinearGrowth.frequently_mul_le {u : ℕ → EReal} {a : EReal} (h : a < linearGrowthSup u) : ∃ᶠ (n : ℕ) in Filter.atTop, a * ↑n ≤ u n

theorem Frequently.linearGrowthInf_le {u : ℕ → EReal} {a : EReal} (h : ∃ᶠ (n : ℕ) in Filter.atTop, u n ≤ a * ↑n) : LinearGrowth.linearGrowthInf u ≤ a

theorem Eventually.le_linearGrowthInf {u : ℕ → EReal} {a : EReal} (h : ∀ᶠ (n : ℕ) in Filter.atTop, a * ↑n ≤ u n) : a ≤ LinearGrowth.linearGrowthInf u

theorem Eventually.linearGrowthSup_le {u : ℕ → EReal} {a : EReal} (h : ∀ᶠ (n : ℕ) in Filter.atTop, u n ≤ a * ↑n) : LinearGrowth.linearGrowthSup u ≤ a

theorem Frequently.le_linearGrowthSup {u : ℕ → EReal} {a : EReal} (h : ∃ᶠ (n : ℕ) in Filter.atTop, a * ↑n ≤ u n) : a ≤ LinearGrowth.linearGrowthSup u

Special cases

theorem LinearGrowth.linearGrowthSup_bot : linearGrowthSup ⊥ = ⊥

theorem LinearGrowth.linearGrowthInf_bot : linearGrowthInf ⊥ = ⊥

theorem LinearGrowth.linearGrowthInf_top : linearGrowthInf ⊤ = ⊤

theorem LinearGrowth.linearGrowthSup_top : linearGrowthSup ⊤ = ⊤

theorem LinearGrowth.linearGrowthInf_const {b : EReal} (h : b ≠ ⊥) (h' : b ≠ ⊤) : (linearGrowthInf fun (x : ℕ) => b) = 0

theorem LinearGrowth.linearGrowthSup_const {b : EReal} (h : b ≠ ⊥) (h' : b ≠ ⊤) : (linearGrowthSup fun (x : ℕ) => b) = 0

theorem LinearGrowth.linearGrowthInf_zero : linearGrowthInf 0 = 0

theorem LinearGrowth.linearGrowthSup_zero : linearGrowthSup 0 = 0

theorem LinearGrowth.linearGrowthInf_const_mul_self {a : EReal} : (linearGrowthInf fun (n : ℕ) => a * ↑n) = a

theorem LinearGrowth.linearGrowthSup_const_mul_self {a : EReal} : (linearGrowthSup fun (n : ℕ) => a * ↑n) = a

theorem LinearGrowth.linearGrowthInf_natCast_nonneg (v : ℕ → ℕ) : 0 ≤ linearGrowthInf fun (n : ℕ) => ↑(v n)

theorem LinearGrowth.tendsto_atTop_of_linearGrowthInf_pos {u : ℕ → EReal} (h : 0 < linearGrowthInf u) : Filter.Tendsto u Filter.atTop (nhds ⊤)

Addition and negation

theorem LinearGrowth.le_linearGrowthInf_add {u v : ℕ → EReal} : linearGrowthInf u + linearGrowthInf v ≤ linearGrowthInf (u + v)

theorem LinearGrowth.linearGrowthInf_add_le {u v : ℕ → EReal} (h : linearGrowthSup u ≠ ⊥ ∨ linearGrowthInf v ≠ ⊤) (h' : linearGrowthSup u ≠ ⊤ ∨ linearGrowthInf v ≠ ⊥) : linearGrowthInf (u + v) ≤ linearGrowthSup u + linearGrowthInf v

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

theorem LinearGrowth.linearGrowthInf_add_le' {u v : ℕ → EReal} (h : linearGrowthInf u ≠ ⊥ ∨ linearGrowthSup v ≠ ⊤) (h' : linearGrowthInf u ≠ ⊤ ∨ linearGrowthSup v ≠ ⊥) : linearGrowthInf (u + v) ≤ linearGrowthInf u + linearGrowthSup v

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

theorem LinearGrowth.le_linearGrowthSup_add {u v : ℕ → EReal} : linearGrowthSup u + linearGrowthInf v ≤ linearGrowthSup (u + v)

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

theorem LinearGrowth.le_linearGrowthSup_add' {u v : ℕ → EReal} : linearGrowthInf u + linearGrowthSup v ≤ linearGrowthSup (u + v)

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

theorem LinearGrowth.linearGrowthSup_add_le {u v : ℕ → EReal} (h : linearGrowthSup u ≠ ⊥ ∨ linearGrowthSup v ≠ ⊤) (h' : linearGrowthSup u ≠ ⊤ ∨ linearGrowthSup v ≠ ⊥) : linearGrowthSup (u + v) ≤ linearGrowthSup u + linearGrowthSup v

theorem LinearGrowth.linearGrowthInf_neg {u : ℕ → EReal} : linearGrowthInf (-u) = -linearGrowthSup u

theorem LinearGrowth.linearGrowthSup_inv {u : ℕ → EReal} : linearGrowthSup (-u) = -linearGrowthInf u

Affine bounds

theorem LinearGrowth.linearGrowthInf_le_of_eventually_le {u v : ℕ → EReal} {b : EReal} (hb : b ≠ ⊤) (h : ∀ᶠ (n : ℕ) in Filter.atTop, u n ≤ v n + b) : linearGrowthInf u ≤ linearGrowthInf v

theorem LinearGrowth.linearGrowthSup_le_of_eventually_le {u v : ℕ → EReal} {b : EReal} (hb : b ≠ ⊤) (h : ∀ᶠ (n : ℕ) in Filter.atTop, u n ≤ v n + b) : linearGrowthSup u ≤ linearGrowthSup v

Infimum and supremum

theorem LinearGrowth.linearGrowthInf_inf {u v : ℕ → EReal} : linearGrowthInf (u ⊓ v) = min (linearGrowthInf u) (linearGrowthInf v)

noncomputable def LinearGrowth.linearGrowthInfTopHom : InfTopHom (ℕ → EReal) EReal

Lower linear growth as an InfTopHom.

theorem LinearGrowth.linearGrowthInf_biInf {α : Type u_1} (u : α → ℕ → EReal) {s : Set α} (hs : s.Finite) : linearGrowthInf (⨅ x ∈ s, u x) = ⨅ x ∈ s, linearGrowthInf (u x)

theorem LinearGrowth.linearGrowthInf_iInf {ι : Type u_1} [Finite ι] (u : ι → ℕ → EReal) : linearGrowthInf (⨅ (i : ι), u i) = ⨅ (i : ι), linearGrowthInf (u i)

theorem LinearGrowth.linearGrowthSup_sup {u v : ℕ → EReal} : linearGrowthSup (u ⊔ v) = max (linearGrowthSup u) (linearGrowthSup v)

noncomputable def LinearGrowth.linearGrowthSupBotHom : SupBotHom (ℕ → EReal) EReal

Upper linear growth as a SupBotHom.

theorem LinearGrowth.linearGrowthSup_biSup {α : Type u_1} (u : α → ℕ → EReal) {s : Set α} (hs : s.Finite) : linearGrowthSup (⨆ x ∈ s, u x) = ⨆ x ∈ s, linearGrowthSup (u x)

theorem LinearGrowth.linearGrowthSup_iSup {ι : Type u_1} [Finite ι] (u : ι → ℕ → EReal) : linearGrowthSup (⨆ (i : ι), u i) = ⨆ (i : ι), linearGrowthSup (u i)

Composition

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

theorem LinearGrowth.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 LinearGrowth.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 LinearGrowth.tendsto_atTop_of_linearGrowthInf_natCast_pos {v : ℕ → ℕ} (h : (linearGrowthInf fun (n : ℕ) => ↑(v n)) ≠ 0) : Filter.Tendsto v Filter.atTop Filter.atTop

theorem LinearGrowth.le_linearGrowthInf_comp {u : ℕ → EReal} {v : ℕ → ℕ} (hu : 0 ≤ᶠ[Filter.atTop] u) (hv : Filter.Tendsto v Filter.atTop Filter.atTop) : (linearGrowthInf fun (n : ℕ) => ↑(v n)) * linearGrowthInf u ≤ linearGrowthInf (u ∘ v)

theorem LinearGrowth.linearGrowthSup_comp_le {u : ℕ → EReal} {v : ℕ → ℕ} (hu : ∃ᶠ (n : ℕ) in Filter.atTop, 0 ≤ u n) (hv₀ : (linearGrowthSup fun (n : ℕ) => ↑(v n)) ≠ 0) (hv₁ : (linearGrowthSup fun (n : ℕ) => ↑(v n)) ≠ ⊤) (hv₂ : Filter.Tendsto v Filter.atTop Filter.atTop) : linearGrowthSup (u ∘ v) ≤ (linearGrowthSup fun (n : ℕ) => ↑(v n)) * linearGrowthSup u

Monotone sequences

theorem Monotone.linearGrowthInf_nonneg {u : ℕ → EReal} (h : Monotone u) (h' : u ≠ ⊥) : 0 ≤ LinearGrowth.linearGrowthInf u

theorem Monotone.linearGrowthSup_nonneg {u : ℕ → EReal} (h : Monotone u) (h' : u ≠ ⊥) : 0 ≤ LinearGrowth.linearGrowthSup u

theorem LinearGrowth.linearGrowthInf_comp_nonneg {u : ℕ → EReal} {v : ℕ → ℕ} (h : Monotone u) (h' : u ≠ ⊥) (hv : Filter.Tendsto v Filter.atTop Filter.atTop) : 0 ≤ linearGrowthInf (u ∘ v)

theorem LinearGrowth.linearGrowthSup_comp_nonneg {u : ℕ → EReal} {v : ℕ → ℕ} (h : Monotone u) (h' : u ≠ ⊥) (hv : Filter.Tendsto v Filter.atTop Filter.atTop) : 0 ≤ linearGrowthSup (u ∘ v)

theorem Monotone.linearGrowthInf_comp_le {u : ℕ → EReal} {v : ℕ → ℕ} (h : Monotone u) (hv₀ : (LinearGrowth.linearGrowthSup fun (n : ℕ) => ↑(v n)) ≠ 0) (hv₁ : (LinearGrowth.linearGrowthSup fun (n : ℕ) => ↑(v n)) ≠ ⊤) : LinearGrowth.linearGrowthInf (u ∘ v) ≤ (LinearGrowth.linearGrowthSup fun (n : ℕ) => ↑(v n)) * LinearGrowth.linearGrowthInf u

theorem Monotone.le_linearGrowthSup_comp {u : ℕ → EReal} {v : ℕ → ℕ} (h : Monotone u) (hv : (LinearGrowth.linearGrowthInf fun (n : ℕ) => ↑(v n)) ≠ 0) : (LinearGrowth.linearGrowthInf fun (n : ℕ) => ↑(v n)) * LinearGrowth.linearGrowthSup u ≤ LinearGrowth.linearGrowthSup (u ∘ v)

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

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

theorem Monotone.linearGrowthInf_comp_mul {u : ℕ → EReal} {m : ℕ} (h : Monotone u) (hm : m ≠ 0) : (LinearGrowth.linearGrowthInf fun (n : ℕ) => u (m * n)) = ↑m * LinearGrowth.linearGrowthInf u

theorem Monotone.linearGrowthSup_comp_mul {u : ℕ → EReal} {m : ℕ} (h : Monotone u) (hm : m ≠ 0) : (LinearGrowth.linearGrowthSup fun (n : ℕ) => u (m * n)) = ↑m * LinearGrowth.linearGrowthSup u