Asymptotics

We introduce these relations:

• IsBigOWith c l f g : "f is big O of g along l with constant c";
• f =O[l] g : "f is big O of g along l";
• f =Θ[l] g : "f is big O of g along l and vice versa";
• f =o[l] g : "f is little o of g along l";

Here l is any filter on the domain of f and g, which are assumed to be the same. The codomains of f and g do not need to be the same; all that is needed is that there is a norm associated with these types, and it is the norm that is compared asymptotically.

The relation IsBigOWith c is introduced to factor out common algebraic arguments in the proofs of similar properties of IsBigO and IsLittleO. Usually proofs outside of this file should use IsBigO instead.

Often the ranges of f and g will be the real numbers, in which case the norm is the absolute value. In general, we have

f =O[l] g ↔ (fun x ↦ ‖f x‖) =O[l] (fun x ↦ ‖g x‖),

and similarly for IsLittleO. But our setup allows us to use the notions e.g. with functions to the integers, rationals, complex numbers, or any normed vector space without mentioning the norm explicitly.

If f and g are functions to a normed field like the reals or complex numbers and g is always nonzero, we have

f =o[l] g ↔ Tendsto (fun x ↦ f x / (g x)) l (𝓝 0).

In fact, the right-to-left direction holds without the hypothesis on g, and in the other direction it suffices to assume that f is zero wherever g is. (This generalization is useful in defining the Fréchet derivative.)

Sometimes Landau notation may be embedded in more complex expressions, such as $f(n) = n ^ {1 + O(g(n))}$. This can be expressed using the existential pattern, for example:

∃ (e : ℕ → ℝ) (he : e =O[l] g), f =ᶠ[l] fun n ↦ n ^ (1 + e n).

Definitions

@[irreducible]

def Asymptotics.IsBigOWith {α : Type u_5} {E : Type u_6} {F : Type u_7} [Norm E] [Norm F] (c : ℝ) (l : Filter α) (f : α → E) (g : α → F) : Prop

This version of the Landau notation IsBigOWith C l f g where f and g are two functions on a type α and l is a filter on α, means that eventually for l, ‖f‖ is bounded by C * ‖g‖. In other words, ‖f‖ / ‖g‖ is eventually bounded by C, modulo division by zero issues that are avoided by this definition. Probably you want to use IsBigO instead of this relation.

Equations

• Asymptotics.IsBigOWith c l f g = ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

theorem Asymptotics.IsBigOWith_def {α : Type u_5} {E : Type u_6} {F : Type u_7} [Norm E] [Norm F] (c : ℝ) (l : Filter α) (f : α → E) (g : α → F) : IsBigOWith c l f g = ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

theorem Asymptotics.isBigOWith_iff {α : Type u_1} {E : Type u_2} {F : Type u_3} {c : ℝ} {f : α → E} {g : α → F} {l : Filter α} [Norm E] [Norm F] : IsBigOWith c l f g ↔ ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Definition of IsBigOWith. We record it in a lemma as IsBigOWith is irreducible.

theorem Asymptotics.IsBigOWith.of_bound {α : Type u_1} {E : Type u_2} {F : Type u_3} {c : ℝ} {f : α → E} {g : α → F} {l : Filter α} [Norm E] [Norm F] : (∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) → IsBigOWith c l f g

Alias of the reverse direction of Asymptotics.isBigOWith_iff.

---

Definition of IsBigOWith. We record it in a lemma as IsBigOWith is irreducible.

theorem Asymptotics.IsBigOWith.bound {α : Type u_1} {E : Type u_2} {F : Type u_3} {c : ℝ} {f : α → E} {g : α → F} {l : Filter α} [Norm E] [Norm F] : IsBigOWith c l f g → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Alias of the forward direction of Asymptotics.isBigOWith_iff.

---

Definition of IsBigOWith. We record it in a lemma as IsBigOWith is irreducible.

theorem Asymptotics.IsBigO_def {α : Type u_5} {E : Type u_6} {F : Type u_7} [Norm E] [Norm F] (l : Filter α) (f : α → E) (g : α → F) : f =O[l] g = ∃ (c : ℝ), IsBigOWith c l f g

@[irreducible]

def Asymptotics.IsBigO {α : Type u_5} {E : Type u_6} {F : Type u_7} [Norm E] [Norm F] (l : Filter α) (f : α → E) (g : α → F) : Prop

The Landau notation f =O[l] g where f and g are two functions on a type α and l is a filter on α, means that eventually for l, ‖f‖ is bounded by a constant multiple of ‖g‖. In other words, ‖f‖ / ‖g‖ is eventually bounded, modulo division by zero issues that are avoided by this definition.

Equations

• f =O[l] g = ∃ (c : ℝ), Asymptotics.IsBigOWith c l f g

def Asymptotics.«term_=O[_]_» : Lean.TrailingParserDescr

The Landau notation f =O[l] g where f and g are two functions on a type α and l is a filter on α, means that eventually for l, ‖f‖ is bounded by a constant multiple of ‖g‖. In other words, ‖f‖ / ‖g‖ is eventually bounded, modulo division by zero issues that are avoided by this definition.

Equations

• One or more equations did not get rendered due to their size.

theorem Asymptotics.isBigO_iff_isBigOWith {α : Type u_1} {E : Type u_2} {F : Type u_3} {f : α → E} {g : α → F} {l : Filter α} [Norm E] [Norm F] : f =O[l] g ↔ ∃ (c : ℝ), IsBigOWith c l f g

Definition of IsBigO in terms of IsBigOWith. We record it in a lemma as IsBigO is irreducible.

theorem Asymptotics.isBigO_iff {α : Type u_1} {E : Type u_2} {F : Type u_3} {f : α → E} {g : α → F} {l : Filter α} [Norm E] [Norm F] : f =O[l] g ↔ ∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Definition of IsBigO in terms of filters.

theorem Asymptotics.isBigO_iff' {α : Type u_1} {E : Type u_2} {E' : Type u_4} {f : α → E} {l : Filter α} [Norm E] [SeminormedAddGroup E'] {g : α → E'} : f =O[l] g ↔ ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Definition of IsBigO in terms of filters, with a positive constant.

theorem Asymptotics.isBigO_iff'' {α : Type u_1} {E : Type u_2} {E' : Type u_4} {f : α → E} {l : Filter α} [Norm E] [SeminormedAddGroup E'] {g : α → E'} : f =O[l] g ↔ ∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖

Definition of IsBigO in terms of filters, with the constant in the lower bound.

theorem Asymptotics.IsBigO.of_bound {α : Type u_1} {E : Type u_2} {F : Type u_3} {f : α → E} {g : α → F} {l : Filter α} [Norm E] [Norm F] (c : ℝ) (h : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) : f =O[l] g

theorem Asymptotics.IsBigO.of_bound' {α : Type u_1} {E : Type u_2} {F : Type u_3} {f : α → E} {g : α → F} {l : Filter α} [Norm E] [Norm F] (h : ∀ᶠ (x : α) in l, ‖f x‖ ≤ ‖g x‖) : f =O[l] g

theorem Asymptotics.IsBigO.bound {α : Type u_1} {E : Type u_2} {F : Type u_3} {f : α → E} {g : α → F} {l : Filter α} [Norm E] [Norm F] : f =O[l] g → ∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

theorem Asymptotics.IsBigO.of_norm_eventuallyLE {α : Type u_1} {E : Type u_2} {f : α → E} {l : Filter α} [Norm E] {g : α → ℝ} (h : (fun (x : α) => ‖f x‖) ≤ᶠ[l] g) : f =O[l] g

See also Filter.Eventually.isBigO, which is the same lemma stated using Filter.Eventually instead of Filter.EventuallyLE.

theorem Asymptotics.IsBigO.of_norm_le {α : Type u_1} {E : Type u_2} {f : α → E} {l : Filter α} [Norm E] {g : α → ℝ} (h : ∀ (x : α), ‖f x‖ ≤ g x) : f =O[l] g

def Asymptotics.IsTheta {α : Type u_1} {E : Type u_2} {F : Type u_3} [Norm E] [Norm F] (l : Filter α) (f : α → E) (g : α → F) : Prop

We say that f is Θ(g) along a filter l (notation: f =Θ[l] g) if f =O[l] g and g =O[l] f.

Equations

• f =Θ[l] g = (f =O[l] g ∧ g =O[l] f)

def Asymptotics.«term_=Θ[_]_» : Lean.TrailingParserDescr

We say that f is Θ(g) along a filter l (notation: f =Θ[l] g) if f =O[l] g and g =O[l] f.

Equations

• One or more equations did not get rendered due to their size.

theorem Asymptotics.IsBigO.antisymm {α : Type u_1} {E : Type u_2} {F : Type u_3} {f : α → E} {g : α → F} {l : Filter α} [Norm E] [Norm F] (h₁ : f =O[l] g) (h₂ : g =O[l] f) : f =Θ[l] g

theorem Asymptotics.IsTheta.isBigO {α : Type u_1} {E : Type u_2} {F : Type u_3} {f : α → E} {g : α → F} {l : Filter α} [Norm E] [Norm F] (h : f =Θ[l] g) : f =O[l] g

theorem Asymptotics.IsTheta.isBigO_symm {α : Type u_1} {E : Type u_2} {F : Type u_3} {f : α → E} {g : α → F} {l : Filter α} [Norm E] [Norm F] (h : f =Θ[l] g) : g =O[l] f

theorem Asymptotics.IsLittleO_def {α : Type u_5} {E : Type u_6} {F : Type u_7} [Norm E] [Norm F] (l : Filter α) (f : α → E) (g : α → F) : f =o[l] g = ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g

@[irreducible]

def Asymptotics.IsLittleO {α : Type u_5} {E : Type u_6} {F : Type u_7} [Norm E] [Norm F] (l : Filter α) (f : α → E) (g : α → F) : Prop

The Landau notation f =o[l] g where f and g are two functions on a type α and l is a filter on α, means that eventually for l, ‖f‖ is bounded by an arbitrarily small constant multiple of ‖g‖. In other words, ‖f‖ / ‖g‖ tends to 0 along l, modulo division by zero issues that are avoided by this definition.

Equations

• f =o[l] g = ∀ ⦃c : ℝ⦄, 0 < c → Asymptotics.IsBigOWith c l f g

def Asymptotics.«term_=o[_]_» : Lean.TrailingParserDescr

The Landau notation f =o[l] g where f and g are two functions on a type α and l is a filter on α, means that eventually for l, ‖f‖ is bounded by an arbitrarily small constant multiple of ‖g‖. In other words, ‖f‖ / ‖g‖ tends to 0 along l, modulo division by zero issues that are avoided by this definition.

Equations

• One or more equations did not get rendered due to their size.

theorem Asymptotics.isLittleO_iff_forall_isBigOWith {α : Type u_1} {E : Type u_2} {F : Type u_3} {f : α → E} {g : α → F} {l : Filter α} [Norm E] [Norm F] : f =o[l] g ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g

Definition of IsLittleO in terms of IsBigOWith.

theorem Asymptotics.IsLittleO.forall_isBigOWith {α : Type u_1} {E : Type u_2} {F : Type u_3} {f : α → E} {g : α → F} {l : Filter α} [Norm E] [Norm F] : f =o[l] g → ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g

Alias of the forward direction of Asymptotics.isLittleO_iff_forall_isBigOWith.

---

Definition of IsLittleO in terms of IsBigOWith.

theorem Asymptotics.IsLittleO.of_isBigOWith {α : Type u_1} {E : Type u_2} {F : Type u_3} {f : α → E} {g : α → F} {l : Filter α} [Norm E] [Norm F] : (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g) → f =o[l] g

Alias of the reverse direction of Asymptotics.isLittleO_iff_forall_isBigOWith.

---

Definition of IsLittleO in terms of IsBigOWith.

theorem Asymptotics.isLittleO_iff {α : Type u_1} {E : Type u_2} {F : Type u_3} {f : α → E} {g : α → F} {l : Filter α} [Norm E] [Norm F] : f =o[l] g ↔ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Definition of IsLittleO in terms of filters.

theorem Asymptotics.IsLittleO.bound {α : Type u_1} {E : Type u_2} {F : Type u_3} {f : α → E} {g : α → F} {l : Filter α} [Norm E] [Norm F] : f =o[l] g → ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Alias of the forward direction of Asymptotics.isLittleO_iff.

---

Definition of IsLittleO in terms of filters.

theorem Asymptotics.IsLittleO.of_bound {α : Type u_1} {E : Type u_2} {F : Type u_3} {f : α → E} {g : α → F} {l : Filter α} [Norm E] [Norm F] : (∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) → f =o[l] g

Alias of the reverse direction of Asymptotics.isLittleO_iff.

---

Definition of IsLittleO in terms of filters.

theorem Asymptotics.IsLittleO.def {α : Type u_1} {E : Type u_2} {F : Type u_3} {c : ℝ} {f : α → E} {g : α → F} {l : Filter α} [Norm E] [Norm F] (h : f =o[l] g) (hc : 0 < c) : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

theorem Asymptotics.IsLittleO.def' {α : Type u_1} {E : Type u_2} {F : Type u_3} {c : ℝ} {f : α → E} {g : α → F} {l : Filter α} [Norm E] [Norm F] (h : f =o[l] g) (hc : 0 < c) : IsBigOWith c l f g

theorem Asymptotics.IsLittleO.eventuallyLE {α : Type u_1} {E : Type u_2} {F : Type u_3} {f : α → E} {g : α → F} {l : Filter α} [Norm E] [Norm F] (h : f =o[l] g) : ∀ᶠ (x : α) in l, ‖f x‖ ≤ ‖g x‖

theorem Asymptotics.IsLittleO.eventuallyLT_norm_of_eventually_pos {α : Type u_1} {E : Type u_2} {F : Type u_3} {f : α → E} {g : α → F} {l : Filter α} [Norm E] [Norm F] (h : f =o[l] g) (hg : ∀ᶠ (x : α) in l, 0 < ‖g x‖) : ∀ᶠ (x : α) in l, ‖f x‖ < ‖g x‖