# 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 =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 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.)

### Definitions #

theorem Asymptotics.IsBigOWith_def {α : Type u_17} {E : Type u_18} {F : Type u_19} [Norm E] [Norm F] (c : ) (l : ) (f : αE) (g : αF) :
= ∀ᶠ (x : α) in l, f x c * g x
@[irreducible]
def Asymptotics.IsBigOWith {α : Type u_17} {E : Type u_18} {F : Type u_19} [Norm E] [Norm F] (c : ) (l : ) (f : αE) (g : αF) :

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
Instances For
theorem Asymptotics.isBigOWith_iff {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : } {f : αE} {g : αF} {l : } :
∀ᶠ (x : α) in l, f x c * g x

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

theorem Asymptotics.IsBigOWith.bound {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : } {f : αE} {g : αF} {l : } :
∀ᶠ (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.IsBigOWith.of_bound {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : } {f : αE} {g : αF} {l : } :
(∀ᶠ (x : α) in l, f x c * g x)

Alias of the reverse direction of Asymptotics.isBigOWith_iff.

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

theorem Asymptotics.IsBigO_def {α : Type u_17} {E : Type u_18} {F : Type u_19} [Norm E] [Norm F] (l : ) (f : αE) (g : αF) :
f =O[l] g = ∃ (c : ),
@[irreducible]
def Asymptotics.IsBigO {α : Type u_17} {E : Type u_18} {F : Type u_19} [Norm E] [Norm F] (l : ) (f : αE) (g : αF) :

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
Instances For

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.
Instances For
theorem Asymptotics.isBigO_iff_isBigOWith {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : } :
f =O[l] g ∃ (c : ),

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_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : } :
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_3} {E''' : Type u_12} [Norm E] [] {f : αE} {l : } {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_3} {E''' : Type u_12} [Norm E] [] {f : αE} {l : } {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_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : } (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_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : } (h : ∀ᶠ (x : α) in l, f x g x) :
f =O[l] g
theorem Asymptotics.IsBigO.bound {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : } :
f =O[l] g∃ (c : ), ∀ᶠ (x : α) in l, f x c * g x
theorem Asymptotics.IsLittleO_def {α : Type u_17} {E : Type u_18} {F : Type u_19} [Norm E] [Norm F] (l : ) (f : αE) (g : αF) :
f =o[l] g = ∀ ⦃c : ⦄, 0 < c
@[irreducible]
def Asymptotics.IsLittleO {α : Type u_17} {E : Type u_18} {F : Type u_19} [Norm E] [Norm F] (l : ) (f : αE) (g : αF) :

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
Instances For

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.
Instances For
theorem Asymptotics.isLittleO_iff_forall_isBigOWith {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : } :
f =o[l] g ∀ ⦃c : ⦄, 0 < c

Definition of IsLittleO in terms of IsBigOWith.

theorem Asymptotics.IsLittleO.of_isBigOWith {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : } :
(∀ ⦃c : ⦄, 0 < c)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.forall_isBigOWith {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : } :
f =o[l] g∀ ⦃c : ⦄, 0 < c

Alias of the forward direction of Asymptotics.isLittleO_iff_forall_isBigOWith.

Definition of IsLittleO in terms of IsBigOWith.

theorem Asymptotics.isLittleO_iff {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : } :
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.of_bound {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : } :
(∀ ⦃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.bound {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : } :
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.def {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : } {f : αE} {g : αF} {l : } (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_3} {F : Type u_4} [Norm E] [Norm F] {c : } {f : αE} {g : αF} {l : } (h : f =o[l] g) (hc : 0 < c) :
theorem Asymptotics.IsLittleO.eventuallyLE {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : } (h : f =o[l] g) :
∀ᶠ (x : α) in l, f x g x

### Conversions #

theorem Asymptotics.IsBigOWith.isBigO {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : } {f : αE} {g : αF} {l : } (h : ) :
f =O[l] g
theorem Asymptotics.IsLittleO.isBigOWith {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : } (hgf : f =o[l] g) :
theorem Asymptotics.IsLittleO.isBigO {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : } (hgf : f =o[l] g) :
f =O[l] g
theorem Asymptotics.IsBigO.isBigOWith {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : } :
f =O[l] g∃ (c : ),
theorem Asymptotics.IsBigOWith.weaken {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] {c : } {c' : } {f : αE} {g' : αF'} {l : } (h : ) (hc : c c') :
theorem Asymptotics.IsBigOWith.exists_pos {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] {c : } {f : αE} {g' : αF'} {l : } (h : ) :
c' > 0, Asymptotics.IsBigOWith c' l f g'
theorem Asymptotics.IsBigO.exists_pos {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] {f : αE} {g' : αF'} {l : } (h : f =O[l] g') :
c > 0,
theorem Asymptotics.IsBigOWith.exists_nonneg {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] {c : } {f : αE} {g' : αF'} {l : } (h : ) :
c'0, Asymptotics.IsBigOWith c' l f g'
theorem Asymptotics.IsBigO.exists_nonneg {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] {f : αE} {g' : αF'} {l : } (h : f =O[l] g') :
c0,
theorem Asymptotics.isBigO_iff_eventually_isBigOWith {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] {f : αE} {g' : αF'} {l : } :
f =O[l] g' ∀ᶠ (c : ) in Filter.atTop,

f = O(g) if and only if IsBigOWith c f g for all sufficiently large c.

theorem Asymptotics.isBigO_iff_eventually {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] {f : αE} {g' : αF'} {l : } :
f =O[l] g' ∀ᶠ (c : ) in Filter.atTop, ∀ᶠ (x : α) in l, f x c * g' x

f = O(g) if and only if ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖ for all sufficiently large c.

theorem Asymptotics.IsBigO.exists_mem_basis {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] {f : αE} {g' : αF'} {l : } {ι : Sort u_17} {p : ιProp} {s : ιSet α} (h : f =O[l] g') (hb : l.HasBasis p s) :
c > 0, ∃ (i : ι), p i xs i, f x c * g' x
theorem Asymptotics.isBigOWith_inv {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : } {f : αE} {g : αF} {l : } (hc : 0 < c) :
∀ᶠ (x : α) in l, c * f x g x
theorem Asymptotics.isLittleO_iff_nat_mul_le_aux {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : } (h₀ : (∀ (x : α), 0 f x) ∀ (x : α), 0 g x) :
f =o[l] g ∀ (n : ), ∀ᶠ (x : α) in l, n * f x g x
theorem Asymptotics.isLittleO_iff_nat_mul_le {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] {f : αE} {g' : αF'} {l : } :
f =o[l] g' ∀ (n : ), ∀ᶠ (x : α) in l, n * f x g' x
theorem Asymptotics.isLittleO_iff_nat_mul_le' {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {g : αF} {f' : αE'} {l : } :
f' =o[l] g ∀ (n : ), ∀ᶠ (x : α) in l, n * f' x g x

### Subsingleton #

theorem Asymptotics.isLittleO_of_subsingleton {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {f' : αE'} {g' : αF'} {l : } [] :
f' =o[l] g'
theorem Asymptotics.isBigO_of_subsingleton {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {f' : αE'} {g' : αF'} {l : } [] :
f' =O[l] g'

### Congruence #

theorem Asymptotics.isBigOWith_congr {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c₁ : } {c₂ : } {l : } {f₁ : αE} {f₂ : αE} {g₁ : αF} {g₂ : αF} (hc : c₁ = c₂) (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) :
Asymptotics.IsBigOWith c₁ l f₁ g₁ Asymptotics.IsBigOWith c₂ l f₂ g₂
theorem Asymptotics.IsBigOWith.congr' {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c₁ : } {c₂ : } {l : } {f₁ : αE} {f₂ : αE} {g₁ : αF} {g₂ : αF} (h : Asymptotics.IsBigOWith c₁ l f₁ g₁) (hc : c₁ = c₂) (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) :
Asymptotics.IsBigOWith c₂ l f₂ g₂
theorem Asymptotics.IsBigOWith.congr {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c₁ : } {c₂ : } {l : } {f₁ : αE} {f₂ : αE} {g₁ : αF} {g₂ : αF} (h : Asymptotics.IsBigOWith c₁ l f₁ g₁) (hc : c₁ = c₂) (hf : ∀ (x : α), f₁ x = f₂ x) (hg : ∀ (x : α), g₁ x = g₂ x) :
Asymptotics.IsBigOWith c₂ l f₂ g₂
theorem Asymptotics.IsBigOWith.congr_left {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : } {g : αF} {l : } {f₁ : αE} {f₂ : αE} (h : ) (hf : ∀ (x : α), f₁ x = f₂ x) :
theorem Asymptotics.IsBigOWith.congr_right {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : } {f : αE} {l : } {g₁ : αF} {g₂ : αF} (h : ) (hg : ∀ (x : α), g₁ x = g₂ x) :
theorem Asymptotics.IsBigOWith.congr_const {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c₁ : } {c₂ : } {f : αE} {g : αF} {l : } (h : ) (hc : c₁ = c₂) :
theorem Asymptotics.isBigO_congr {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : } {f₁ : αE} {f₂ : αE} {g₁ : αF} {g₂ : αF} (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) :
f₁ =O[l] g₁ f₂ =O[l] g₂
theorem Asymptotics.IsBigO.congr' {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : } {f₁ : αE} {f₂ : αE} {g₁ : αF} {g₂ : αF} (h : f₁ =O[l] g₁) (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) :
f₂ =O[l] g₂
theorem Asymptotics.IsBigO.congr {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : } {f₁ : αE} {f₂ : αE} {g₁ : αF} {g₂ : αF} (h : f₁ =O[l] g₁) (hf : ∀ (x : α), f₁ x = f₂ x) (hg : ∀ (x : α), g₁ x = g₂ x) :
f₂ =O[l] g₂
theorem Asymptotics.IsBigO.congr_left {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {g : αF} {l : } {f₁ : αE} {f₂ : αE} (h : f₁ =O[l] g) (hf : ∀ (x : α), f₁ x = f₂ x) :
f₂ =O[l] g
theorem Asymptotics.IsBigO.congr_right {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {l : } {g₁ : αF} {g₂ : αF} (h : f =O[l] g₁) (hg : ∀ (x : α), g₁ x = g₂ x) :
f =O[l] g₂
theorem Asymptotics.isLittleO_congr {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : } {f₁ : αE} {f₂ : αE} {g₁ : αF} {g₂ : αF} (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) :
f₁ =o[l] g₁ f₂ =o[l] g₂
theorem Asymptotics.IsLittleO.congr' {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : } {f₁ : αE} {f₂ : αE} {g₁ : αF} {g₂ : αF} (h : f₁ =o[l] g₁) (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) :
f₂ =o[l] g₂
theorem Asymptotics.IsLittleO.congr {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : } {f₁ : αE} {f₂ : αE} {g₁ : αF} {g₂ : αF} (h : f₁ =o[l] g₁) (hf : ∀ (x : α), f₁ x = f₂ x) (hg : ∀ (x : α), g₁ x = g₂ x) :
f₂ =o[l] g₂
theorem Asymptotics.IsLittleO.congr_left {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {g : αF} {l : } {f₁ : αE} {f₂ : αE} (h : f₁ =o[l] g) (hf : ∀ (x : α), f₁ x = f₂ x) :
f₂ =o[l] g
theorem Asymptotics.IsLittleO.congr_right {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {l : } {g₁ : αF} {g₂ : αF} (h : f =o[l] g₁) (hg : ∀ (x : α), g₁ x = g₂ x) :
f =o[l] g₂
theorem Filter.EventuallyEq.trans_isBigO {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : } {f₁ : αE} {f₂ : αE} {g : αF} (hf : f₁ =ᶠ[l] f₂) (h : f₂ =O[l] g) :
f₁ =O[l] g
instance Asymptotics.transEventuallyEqIsBigO {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : } :
Trans (fun (x x_1 : αE) => x =ᶠ[l] x_1) (fun (x : αE) (x_1 : αF) => x =O[l] x_1) fun (x : αE) (x_1 : αF) => x =O[l] x_1
Equations
• Asymptotics.transEventuallyEqIsBigO = { trans := }
theorem Filter.EventuallyEq.trans_isLittleO {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : } {f₁ : αE} {f₂ : αE} {g : αF} (hf : f₁ =ᶠ[l] f₂) (h : f₂ =o[l] g) :
f₁ =o[l] g
instance Asymptotics.transEventuallyEqIsLittleO {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : } :
Trans (fun (x x_1 : αE) => x =ᶠ[l] x_1) (fun (x : αE) (x_1 : αF) => x =o[l] x_1) fun (x : αE) (x_1 : αF) => x =o[l] x_1
Equations
• Asymptotics.transEventuallyEqIsLittleO = { trans := }
theorem Asymptotics.IsBigO.trans_eventuallyEq {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : } {f : αE} {g₁ : αF} {g₂ : αF} (h : f =O[l] g₁) (hg : g₁ =ᶠ[l] g₂) :
f =O[l] g₂
instance Asymptotics.transIsBigOEventuallyEq {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : } :
Trans (fun (x : αE) (x_1 : αF) => x =O[l] x_1) (fun (x x_1 : αF) => x =ᶠ[l] x_1) fun (x : αE) (x_1 : αF) => x =O[l] x_1
Equations
• Asymptotics.transIsBigOEventuallyEq = { trans := }
theorem Asymptotics.IsLittleO.trans_eventuallyEq {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : } {f : αE} {g₁ : αF} {g₂ : αF} (h : f =o[l] g₁) (hg : g₁ =ᶠ[l] g₂) :
f =o[l] g₂
instance Asymptotics.transIsLittleOEventuallyEq {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : } :
Trans (fun (x : αE) (x_1 : αF) => x =o[l] x_1) (fun (x x_1 : αF) => x =ᶠ[l] x_1) fun (x : αE) (x_1 : αF) => x =o[l] x_1
Equations
• Asymptotics.transIsLittleOEventuallyEq = { trans := }

### Filter operations and transitivity #

theorem Asymptotics.IsBigOWith.comp_tendsto {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : } {f : αE} {g : αF} {l : } (hcfg : ) {k : βα} {l' : } (hk : Filter.Tendsto k l' l) :
Asymptotics.IsBigOWith c l' (f k) (g k)
theorem Asymptotics.IsBigO.comp_tendsto {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : } (hfg : f =O[l] g) {k : βα} {l' : } (hk : Filter.Tendsto k l' l) :
(f k) =O[l'] (g k)
theorem Asymptotics.IsLittleO.comp_tendsto {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : } (hfg : f =o[l] g) {k : βα} {l' : } (hk : Filter.Tendsto k l' l) :
(f k) =o[l'] (g k)
@[simp]
theorem Asymptotics.isBigOWith_map {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : } {f : αE} {g : αF} {k : βα} {l : } :
@[simp]
theorem Asymptotics.isBigO_map {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {k : βα} {l : } :
f =O[] g (f k) =O[l] (g k)
@[simp]
theorem Asymptotics.isLittleO_map {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {k : βα} {l : } :
f =o[] g (f k) =o[l] (g k)
theorem Asymptotics.IsBigOWith.mono {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : } {f : αE} {g : αF} {l : } {l' : } (h : ) (hl : l l') :
theorem Asymptotics.IsBigO.mono {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : } {l' : } (h : f =O[l'] g) (hl : l l') :
f =O[l] g
theorem Asymptotics.IsLittleO.mono {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : } {l' : } (h : f =o[l'] g) (hl : l l') :
f =o[l] g
theorem Asymptotics.IsBigOWith.trans {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [Norm E] [Norm F] [Norm G] {c : } {c' : } {f : αE} {g : αF} {k : αG} {l : } (hfg : ) (hgk : ) (hc : 0 c) :
theorem Asymptotics.IsBigO.trans {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [Norm E] [Norm G] {l : } {f : αE} {g : αF'} {k : αG} (hfg : f =O[l] g) (hgk : g =O[l] k) :
f =O[l] k
instance Asymptotics.transIsBigOIsBigO {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [Norm E] [Norm G] {l : } :
Trans (fun (x : αE) (x_1 : αF') => x =O[l] x_1) (fun (x : αF') (x_1 : αG) => x =O[l] x_1) fun (x : αE) (x_1 : αG) => x =O[l] x_1
Equations
• Asymptotics.transIsBigOIsBigO = { trans := }
theorem Asymptotics.IsLittleO.trans_isBigOWith {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [Norm E] [Norm F] [Norm G] {c : } {f : αE} {g : αF} {k : αG} {l : } (hfg : f =o[l] g) (hgk : ) (hc : 0 < c) :
f =o[l] k
theorem Asymptotics.IsLittleO.trans_isBigO {α : Type u_1} {E : Type u_3} {F : Type u_4} {G' : Type u_8} [Norm E] [Norm F] {l : } {f : αE} {g : αF} {k : αG'} (hfg : f =o[l] g) (hgk : g =O[l] k) :
f =o[l] k
instance Asymptotics.transIsLittleOIsBigO {α : Type u_1} {E : Type u_3} {F : Type u_4} {G' : Type u_8} [Norm E] [Norm F] {l : } :
Trans (fun (x : αE) (x_1 : αF) => x =o[l] x_1) (fun (x : αF) (x_1 : αG') => x =O[l] x_1) fun (x : αE) (x_1 : αG') => x =o[l] x_1
Equations
• Asymptotics.transIsLittleOIsBigO = { trans := }
theorem Asymptotics.IsBigOWith.trans_isLittleO {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [Norm E] [Norm F] [Norm G] {c : } {f : αE} {g : αF} {k : αG} {l : } (hfg : ) (hgk : g =o[l] k) (hc : 0 < c) :
f =o[l] k
theorem Asymptotics.IsBigO.trans_isLittleO {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [Norm E] [Norm G] {l : } {f : αE} {g : αF'} {k : αG} (hfg : f =O[l] g) (hgk : g =o[l] k) :
f =o[l] k
instance Asymptotics.transIsBigOIsLittleO {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [Norm E] [Norm G] {l : } :
Trans (fun (x : αE) (x_1 : αF') => x =O[l] x_1) (fun (x : αF') (x_1 : αG) => x =o[l] x_1) fun (x : αE) (x_1 : αG) => x =o[l] x_1
Equations
• Asymptotics.transIsBigOIsLittleO = { trans := }
theorem Asymptotics.IsLittleO.trans {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [Norm E] [Norm F] [Norm G] {l : } {f : αE} {g : αF} {k : αG} (hfg : f =o[l] g) (hgk : g =o[l] k) :
f =o[l] k
instance Asymptotics.transIsLittleOIsLittleO {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [Norm E] [Norm F] [Norm G] {l : } :
Trans (fun (x : αE) (x_1 : αF) => x =o[l] x_1) (fun (x : αF) (x_1 : αG) => x =o[l] x_1) fun (x : αE) (x_1 : αG) => x =o[l] x_1
Equations
• Asymptotics.transIsLittleOIsLittleO = { trans := }
theorem Filter.Eventually.trans_isBigO {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [Norm E] [Norm G] {l : } {f : αE} {g : αF'} {k : αG} (hfg : ∀ᶠ (x : α) in l, f x g x) (hgk : g =O[l] k) :
f =O[l] k
theorem Filter.Eventually.isBigO {α : Type u_1} {E : Type u_3} [Norm E] {f : αE} {g : α} {l : } (hfg : ∀ᶠ (x : α) in l, f x g x) :
f =O[l] g
theorem Asymptotics.isBigOWith_of_le' {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : } {f : αE} {g : αF} (l : ) (hfg : ∀ (x : α), f x c * g x) :
theorem Asymptotics.isBigOWith_of_le {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} (l : ) (hfg : ∀ (x : α), f x g x) :
theorem Asymptotics.isBigO_of_le' {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : } {f : αE} {g : αF} (l : ) (hfg : ∀ (x : α), f x c * g x) :
f =O[l] g
theorem Asymptotics.isBigO_of_le {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} (l : ) (hfg : ∀ (x : α), f x g x) :
f =O[l] g
theorem Asymptotics.isBigOWith_refl {α : Type u_1} {E : Type u_3} [Norm E] (f : αE) (l : ) :
theorem Asymptotics.isBigO_refl {α : Type u_1} {E : Type u_3} [Norm E] (f : αE) (l : ) :
f =O[l] f
theorem Filter.EventuallyEq.isBigO {α : Type u_1} {E : Type u_3} [Norm E] {l : } {f₁ : αE} {f₂ : αE} (hf : f₁ =ᶠ[l] f₂) :
f₁ =O[l] f₂
theorem Asymptotics.IsBigOWith.trans_le {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [Norm E] [Norm F] [Norm G] {c : } {f : αE} {g : αF} {k : αG} {l : } (hfg : ) (hgk : ∀ (x : α), g x k x) (hc : 0 c) :
theorem Asymptotics.IsBigO.trans_le {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [Norm E] [Norm G] {f : αE} {k : αG} {g' : αF'} {l : } (hfg : f =O[l] g') (hgk : ∀ (x : α), g' x k x) :
f =O[l] k
theorem Asymptotics.IsLittleO.trans_le {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [Norm E] [Norm F] [Norm G] {f : αE} {g : αF} {k : αG} {l : } (hfg : f =o[l] g) (hgk : ∀ (x : α), g x k x) :
f =o[l] k
theorem Asymptotics.isLittleO_irrefl' {α : Type u_1} {E' : Type u_6} {f' : αE'} {l : } (h : ∃ᶠ (x : α) in l, f' x 0) :
¬f' =o[l] f'
theorem Asymptotics.isLittleO_irrefl {α : Type u_1} {E'' : Type u_9} [] {f'' : αE''} {l : } (h : ∃ᶠ (x : α) in l, f'' x 0) :
¬f'' =o[l] f''
theorem Asymptotics.IsBigO.not_isLittleO {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} [] {g' : αF'} {f'' : αE''} {l : } (h : f'' =O[l] g') (hf : ∃ᶠ (x : α) in l, f'' x 0) :
¬g' =o[l] f''
theorem Asymptotics.IsLittleO.not_isBigO {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} [] {g' : αF'} {f'' : αE''} {l : } (h : f'' =o[l] g') (hf : ∃ᶠ (x : α) in l, f'' x 0) :
¬g' =O[l] f''
@[simp]
theorem Asymptotics.isBigOWith_bot {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] (c : ) (f : αE) (g : αF) :
@[simp]
theorem Asymptotics.isBigO_bot {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] (f : αE) (g : αF) :
@[simp]
theorem Asymptotics.isLittleO_bot {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] (f : αE) (g : αF) :
@[simp]
theorem Asymptotics.isBigOWith_pure {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : } {f : αE} {g : αF} {x : α} :
theorem Asymptotics.IsBigOWith.sup {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : } {f : αE} {g : αF} {l : } {l' : } (h : ) (h' : ) :
theorem Asymptotics.IsBigOWith.sup' {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] {c : } {c' : } {f : αE} {g' : αF'} {l : } {l' : } (h : ) (h' : Asymptotics.IsBigOWith c' l' f g') :
Asymptotics.IsBigOWith (max c c') (l l') f g'
theorem Asymptotics.IsBigO.sup {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] {f : αE} {g' : αF'} {l : } {l' : } (h : f =O[l] g') (h' : f =O[l'] g') :
f =O[l l'] g'
theorem Asymptotics.IsLittleO.sup {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : } {l' : } (h : f =o[l] g) (h' : f =o[l'] g) :
f =o[l l'] g
@[simp]
theorem Asymptotics.isBigO_sup {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] {f : αE} {g' : αF'} {l : } {l' : } :
f =O[l l'] g' f =O[l] g' f =O[l'] g'
@[simp]
theorem Asymptotics.isLittleO_sup {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {l : } {l' : } :
f =o[l l'] g f =o[l] g f =o[l'] g
theorem Asymptotics.isBigOWith_insert {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] [] {x : α} {s : Set α} {C : } {g : αE} {g' : αF} (h : g x C * g' x) :
theorem Asymptotics.IsBigOWith.insert {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] [] {x : α} {s : Set α} {C : } {g : αE} {g' : αF} (h1 : Asymptotics.IsBigOWith C () g g') (h2 : g x C * g' x) :
theorem Asymptotics.isLittleO_insert {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [] {x : α} {s : Set α} {g : αE'} {g' : αF'} (h : g x = 0) :
g =o[nhdsWithin x (insert x s)] g' g =o[] g'
theorem Asymptotics.IsLittleO.insert {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [] {x : α} {s : Set α} {g : αE'} {g' : αF'} (h1 : g =o[] g') (h2 : g x = 0) :
g =o[nhdsWithin x (insert x s)] g'

### Simplification : norm, abs #

@[simp]
theorem Asymptotics.isBigOWith_norm_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] {c : } {f : αE} {g' : αF'} {l : } :
(Asymptotics.IsBigOWith c l f fun (x : α) => g' x)
@[simp]
theorem Asymptotics.isBigOWith_abs_right {α : Type u_1} {E : Type u_3} [Norm E] {c : } {f : αE} {l : } {u : α} :
(Asymptotics.IsBigOWith c l f fun (x : α) => |u x|)
theorem Asymptotics.IsBigOWith.of_norm_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] {c : } {f : αE} {g' : αF'} {l : } :
(Asymptotics.IsBigOWith c l f fun (x : α) => g' x)

Alias of the forward direction of Asymptotics.isBigOWith_norm_right.

theorem Asymptotics.IsBigOWith.norm_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] {c : } {f : αE} {g' : αF'} {l : } :
Asymptotics.IsBigOWith c l f fun (x : α) => g' x

Alias of the reverse direction of Asymptotics.isBigOWith_norm_right.

theorem Asymptotics.IsBigOWith.of_abs_right {α : Type u_1} {E : Type u_3} [Norm E] {c : } {f : αE} {l : } {u : α} :
(Asymptotics.IsBigOWith c l f fun (x : α) => |u x|)

Alias of the forward direction of Asymptotics.isBigOWith_abs_right.

theorem Asymptotics.IsBigOWith.abs_right {α : Type u_1} {E : Type u_3} [Norm E] {c : } {f : αE} {l : } {u : α} :
Asymptotics.IsBigOWith c l f fun (x : α) => |u x|

Alias of the reverse direction of Asymptotics.isBigOWith_abs_right.

@[simp]
theorem Asymptotics.isBigO_norm_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] {f : αE} {g' : αF'} {l : } :
(f =O[l] fun (x : α) => g' x) f =O[l] g'
@[simp]
theorem Asymptotics.isBigO_abs_right {α : Type u_1} {E : Type u_3} [Norm E] {f : αE} {l : } {u : α} :
(f =O[l] fun (x : α) => |u x|) f =O[l] u
theorem Asymptotics.IsBigO.of_norm_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] {f : αE} {g' : αF'} {l : } :
(f =O[l] fun (x : α) => g' x)f =O[l] g'

Alias of the forward direction of Asymptotics.isBigO_norm_right.

theorem Asymptotics.IsBigO.norm_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] {f : αE} {g' : αF'} {l : } :
f =O[l] g'f =O[l] fun (x : α) => g' x

Alias of the reverse direction of Asymptotics.isBigO_norm_right.

theorem Asymptotics.IsBigO.abs_right {α : Type u_1} {E : Type u_3} [Norm E] {f : αE} {l : } {u : α} :
f =O[l] uf =O[l] fun (x : α) => |u x|

Alias of the reverse direction of Asymptotics.isBigO_abs_right.

theorem Asymptotics.IsBigO.of_abs_right {α : Type u_1} {E : Type u_3} [Norm E] {f : αE} {l : } {u : α} :
(f =O[l] fun (x : α) => |u x|)f =O[l] u

Alias of the forward direction of Asymptotics.isBigO_abs_right.

@[simp]
theorem Asymptotics.isLittleO_norm_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] {f : αE} {g' : αF'} {l : } :
(f =o[l] fun (x : α) => g' x) f =o[l] g'
@[simp]
theorem Asymptotics.isLittleO_abs_right {α : Type u_1} {E : Type u_3} [Norm E] {f : αE} {l : } {u : α} :
(f =o[l] fun (x : α) => |u x|) f =o[l] u
theorem Asymptotics.IsLittleO.norm_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] {f : αE} {g' : αF'} {l : } :
f =o[l] g'f =o[l] fun (x : α) => g' x

Alias of the reverse direction of Asymptotics.isLittleO_norm_right.

theorem Asymptotics.IsLittleO.of_norm_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] {f : αE} {g' : αF'} {l : } :
(f =o[l] fun (x : α) => g' x)f =o[l] g'

Alias of the forward direction of Asymptotics.isLittleO_norm_right.

theorem Asymptotics.IsLittleO.of_abs_right {α : Type u_1} {E : Type u_3} [Norm E] {f : αE} {l : } {u : α} :
(f =o[l] fun (x : α) => |u x|)f =o[l] u

Alias of the forward direction of Asymptotics.isLittleO_abs_right.

theorem Asymptotics.IsLittleO.abs_right {α : Type u_1} {E : Type u_3} [Norm E] {f : αE} {l : } {u : α} :
f =o[l] uf =o[l] fun (x : α) => |u x|

Alias of the reverse direction of Asymptotics.isLittleO_abs_right.

@[simp]
theorem Asymptotics.isBigOWith_norm_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {c : } {g : αF} {f' : αE'} {l : } :
Asymptotics.IsBigOWith c l (fun (x : α) => f' x) g
@[simp]
theorem Asymptotics.isBigOWith_abs_left {α : Type u_1} {F : Type u_4} [Norm F] {c : } {g : αF} {l : } {u : α} :
Asymptotics.IsBigOWith c l (fun (x : α) => |u x|) g
theorem Asymptotics.IsBigOWith.norm_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {c : } {g : αF} {f' : αE'} {l : } :
Asymptotics.IsBigOWith c l (fun (x : α) => f' x) g

Alias of the reverse direction of Asymptotics.isBigOWith_norm_left.

theorem Asymptotics.IsBigOWith.of_norm_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {c : } {g : αF} {f' : αE'} {l : } :
Asymptotics.IsBigOWith c l (fun (x : α) => f' x) g

Alias of the forward direction of Asymptotics.isBigOWith_norm_left.

theorem Asymptotics.IsBigOWith.of_abs_left {α : Type u_1} {F : Type u_4} [Norm F] {c : } {g : αF} {l : } {u : α} :
Asymptotics.IsBigOWith c l (fun (x : α) => |u x|) g

Alias of the forward direction of Asymptotics.isBigOWith_abs_left.

theorem Asymptotics.IsBigOWith.abs_left {α : Type u_1} {F : Type u_4} [Norm F] {c : } {g : αF} {l : } {u : α} :
Asymptotics.IsBigOWith c l (fun (x : α) => |u x|) g

Alias of the reverse direction of Asymptotics.isBigOWith_abs_left.

@[simp]
theorem Asymptotics.isBigO_norm_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {g : αF} {f' : αE'} {l : } :
(fun (x : α) => f' x) =O[l] g f' =O[l] g
@[simp]
theorem Asymptotics.isBigO_abs_left {α : Type u_1} {F : Type u_4} [Norm F] {g : αF} {l : } {u : α} :
(fun (x : α) => |u x|) =O[l] g u =O[l] g
theorem Asymptotics.IsBigO.of_norm_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {g : αF} {f' : αE'} {l : } :
(fun (x : α) => f' x) =O[l] gf' =O[l] g

Alias of the forward direction of Asymptotics.isBigO_norm_left.

theorem Asymptotics.IsBigO.norm_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {g : αF} {f' : αE'} {l : } :
f' =O[l] g(fun (x : α) => f' x) =O[l] g

Alias of the reverse direction of Asymptotics.isBigO_norm_left.

theorem Asymptotics.IsBigO.abs_left {α : Type u_1} {F : Type u_4} [Norm F] {g : αF} {l : } {u : α} :
u =O[l] g(fun (x : α) => |u x|) =O[l] g

Alias of the reverse direction of Asymptotics.isBigO_abs_left.

theorem Asymptotics.IsBigO.of_abs_left {α : Type u_1} {F : Type u_4} [Norm F] {g : αF} {l : } {u : α} :
(fun (x : α) => |u x|) =O[l] gu =O[l] g

Alias of the forward direction of Asymptotics.isBigO_abs_left.

@[simp]
theorem Asymptotics.isLittleO_norm_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {g : αF} {f' : αE'} {l : } :
(fun (x : α) => f' x) =o[l] g f' =o[l] g
@[simp]
theorem Asymptotics.isLittleO_abs_left {α : Type u_1} {F : Type u_4} [Norm F] {g : αF} {l : } {u : α} :
(fun (x : α) => |u x|) =o[l] g u =o[l] g
theorem Asymptotics.IsLittleO.of_norm_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {g : αF} {f' : αE'} {l : } :
(fun (x : α) => f' x) =o[l] gf' =o[l] g

Alias of the forward direction of Asymptotics.isLittleO_norm_left.

theorem Asymptotics.IsLittleO.norm_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {g : αF} {f' : αE'} {l : } :
f' =o[l] g(fun (x : α) => f' x) =o[l] g

Alias of the reverse direction of Asymptotics.isLittleO_norm_left.

theorem Asymptotics.IsLittleO.of_abs_left {α : Type u_1} {F : Type u_4} [Norm F] {g : αF} {l : } {u : α} :
(fun (x : α) => |u x|) =o[l] gu =o[l] g

Alias of the forward direction of Asymptotics.isLittleO_abs_left.

theorem Asymptotics.IsLittleO.abs_left {α : Type u_1} {F : Type u_4} [Norm F] {g : αF} {l : } {u : α} :
u =o[l] g(fun (x : α) => |u x|) =o[l] g

Alias of the reverse direction of Asymptotics.isLittleO_abs_left.

theorem Asymptotics.isBigOWith_norm_norm {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {c : } {f' : αE'} {g' : αF'} {l : } :
(Asymptotics.IsBigOWith c l (fun (x : α) => f' x) fun (x : α) => g' x) Asymptotics.IsBigOWith c l f' g'
theorem Asymptotics.isBigOWith_abs_abs {α : Type u_1} {c : } {l : } {u : α} {v : α} :
(Asymptotics.IsBigOWith c l (fun (x : α) => |u x|) fun (x : α) => |v x|)
theorem Asymptotics.IsBigOWith.of_norm_norm {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {c : } {f' : αE'} {g' : αF'} {l : } :
(Asymptotics.IsBigOWith c l (fun (x : α) => f' x) fun (x : α) => g' x)Asymptotics.IsBigOWith c l f' g'

Alias of the forward direction of Asymptotics.isBigOWith_norm_norm.

theorem Asymptotics.IsBigOWith.norm_norm {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {c : } {f' : αE'} {g' : αF'} {l : } :
Asymptotics.IsBigOWith c l f' g'Asymptotics.IsBigOWith c l (fun (x : α) => f' x) fun (x : α) => g' x

Alias of the reverse direction of Asymptotics.isBigOWith_norm_norm.

theorem Asymptotics.IsBigOWith.of_abs_abs {α : Type u_1} {c : } {l : } {u : α} {v : α} :
(Asymptotics.IsBigOWith c l (fun (x : α) => |u x|) fun (x : α) => |v x|)

Alias of the forward direction of Asymptotics.isBigOWith_abs_abs.

theorem Asymptotics.IsBigOWith.abs_abs {α : Type u_1} {c : } {l : } {u : α} {v : α} :
Asymptotics.IsBigOWith c l (fun (x : α) => |u x|) fun (x : α) => |v x|

Alias of the reverse direction of Asymptotics.isBigOWith_abs_abs.

theorem Asymptotics.isBigO_norm_norm {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {f' : αE'} {g' : αF'} {l : } :
((fun (x : α) => f' x) =O[l] fun (x : α) => g' x) f' =O[l] g'
theorem Asymptotics.isBigO_abs_abs {α : Type u_1} {l : } {u : α} {v : α} :
((fun (x : α) => |u x|) =O[l] fun (x : α) => |v x|) u =O[l] v
theorem Asymptotics.IsBigO.norm_norm {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {f' : αE'} {g' : αF'} {l : } :
f' =O[l] g'(fun (x : α) => f' x) =O[l] fun (x : α) => g' x

Alias of the reverse direction of Asymptotics.isBigO_norm_norm.

theorem Asymptotics.IsBigO.of_norm_norm {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {f' : αE'} {g' : αF'} {l : } :
((fun (x : α) => f' x) =O[l] fun (x : α) => g' x)f' =O[l] g'

Alias of the forward direction of Asymptotics.isBigO_norm_norm.

theorem Asymptotics.IsBigO.abs_abs {α : Type u_1} {l : } {u : α} {v : α} :
u =O[l] v(fun (x : α) => |u x|) =O[l] fun (x : α) => |v x|

Alias of the reverse direction of Asymptotics.isBigO_abs_abs.

theorem Asymptotics.IsBigO.of_abs_abs {α : Type u_1} {l : } {u : α} {v : α} :
((fun (x : α) => |u x|) =O[l] fun (x : α) => |v x|)u =O[l] v

Alias of the forward direction of Asymptotics.isBigO_abs_abs.

theorem Asymptotics.isLittleO_norm_norm {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {f' : αE'} {g' : αF'} {l : } :
((fun (x : α) => f' x) =o[l] fun (x : α) => g' x) f' =o[l] g'
theorem Asymptotics.isLittleO_abs_abs {α : Type u_1} {l : } {u : α} {v : α} :
((fun (x : α) => |u x|) =o[l] fun (x : α) => |v x|) u =o[l] v
theorem Asymptotics.IsLittleO.norm_norm {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {f' : αE'} {g' : αF'} {l : } :
f' =o[l] g'(fun (x : α) => f' x) =o[l] fun (x : α) => g' x

Alias of the reverse direction of Asymptotics.isLittleO_norm_norm.

theorem Asymptotics.IsLittleO.of_norm_norm {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {f' : αE'} {g' : αF'} {l : } :
((fun (x : α) => f' x) =o[l] fun (x : α) => g' x)f' =o[l] g'

Alias of the forward direction of Asymptotics.isLittleO_norm_norm.

theorem Asymptotics.IsLittleO.abs_abs {α : Type u_1} {l : } {u : α} {v : α} :
u =o[l] v(fun (x : α) => |u x|) =o[l] fun (x : α) => |v x|

Alias of the reverse direction of Asymptotics.isLittleO_abs_abs.

theorem Asymptotics.IsLittleO.of_abs_abs {α : Type u_1} {l : } {u : α} {v : α} :
((fun (x : α) => |u x|) =o[l] fun (x : α) => |v x|)u =o[l] v

Alias of the forward direction of Asymptotics.isLittleO_abs_abs.

### Simplification: negate #

@[simp]
theorem Asymptotics.isBigOWith_neg_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] {c : } {f : αE} {g' : αF'} {l : } :
(Asymptotics.IsBigOWith c l f fun (x : α) => -g' x)
theorem Asymptotics.IsBigOWith.neg_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] {c : } {f : αE} {g' : αF'} {l : } :
Asymptotics.IsBigOWith c l f fun (x : α) => -g' x

Alias of the reverse direction of Asymptotics.isBigOWith_neg_right.

theorem Asymptotics.IsBigOWith.of_neg_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] {c : } {f : αE} {g' : αF'} {l : } :
(Asymptotics.IsBigOWith c l f fun (x : α) => -g' x)

Alias of the forward direction of Asymptotics.isBigOWith_neg_right.

@[simp]
theorem Asymptotics.isBigO_neg_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] {f : αE} {g' : αF'} {l : } :
(f =O[l] fun (x : α) => -g' x) f =O[l] g'
theorem Asymptotics.IsBigO.of_neg_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] {f : αE} {g' : αF'} {l : } :
(f =O[l] fun (x : α) => -g' x)f =O[l] g'

Alias of the forward direction of Asymptotics.isBigO_neg_right.

theorem Asymptotics.IsBigO.neg_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] {f : αE} {g' : αF'} {l : } :
f =O[l] g'f =O[l] fun (x : α) => -g' x

Alias of the reverse direction of Asymptotics.isBigO_neg_right.

@[simp]
theorem Asymptotics.isLittleO_neg_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] {f : αE} {g' : αF'} {l : } :
(f =o[l] fun (x : α) => -g' x) f =o[l] g'
theorem Asymptotics.IsLittleO.of_neg_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] {f : αE} {g' : αF'} {l : } :
(f =o[l] fun (x : α) => -g' x)f =o[l] g'

Alias of the forward direction of Asymptotics.isLittleO_neg_right.

theorem Asymptotics.IsLittleO.neg_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] {f : αE} {g' : αF'} {l : } :
f =o[l] g'f =o[l] fun (x : α) => -g' x

Alias of the reverse direction of Asymptotics.isLittleO_neg_right.

@[simp]
theorem Asymptotics.isBigOWith_neg_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {c : } {g : αF} {f' : αE'} {l : } :
Asymptotics.IsBigOWith c l (fun (x : α) => -f' x) g
theorem Asymptotics.IsBigOWith.of_neg_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {c : } {g : αF} {f' : αE'} {l : } :
Asymptotics.IsBigOWith c l (fun (x : α) => -f' x) g

Alias of the forward direction of Asymptotics.isBigOWith_neg_left.

theorem Asymptotics.IsBigOWith.neg_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {c : } {g : αF} {f' : αE'} {l : } :
Asymptotics.IsBigOWith c l (fun (x : α) => -f' x) g

Alias of the reverse direction of Asymptotics.isBigOWith_neg_left.

@[simp]
theorem Asymptotics.isBigO_neg_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {g : αF} {f' : αE'} {l : } :
(fun (x : α) => -f' x) =O[l] g f' =O[l] g
theorem Asymptotics.IsBigO.of_neg_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {g : αF} {f' : αE'} {l : } :
(fun (x : α) => -f' x) =O[l] gf' =O[l] g

Alias of the forward direction of Asymptotics.isBigO_neg_left.

theorem Asymptotics.IsBigO.neg_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {g : αF} {f' : αE'} {l : } :
f' =O[l] g(fun (x : α) => -f' x) =O[l] g

Alias of the reverse direction of Asymptotics.isBigO_neg_left.

@[simp]
theorem Asymptotics.isLittleO_neg_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {g : αF} {f' : αE'} {l : } :
(fun (x : α) => -f' x) =o[l] g f' =o[l] g
theorem Asymptotics.IsLittleO.neg_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {g : αF} {f' : αE'} {l : } :
f' =o[l] g(fun (x : α) => -f' x) =o[l] g

Alias of the reverse direction of Asymptotics.isLittleO_neg_left.

theorem Asymptotics.IsLittleO.of_neg_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {g : αF} {f' : αE'} {l : } :
(fun (x : α) => -f' x) =o[l] gf' =o[l] g

Alias of the forward direction of Asymptotics.isLittleO_neg_left.

### Product of functions (right) #

theorem Asymptotics.isBigOWith_fst_prod {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {f' : αE'} {g' : αF'} {l : } :
Asymptotics.IsBigOWith 1 l f' fun (x : α) => (f' x, g' x)
theorem Asymptotics.isBigOWith_snd_prod {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {f' : αE'} {g' : αF'} {l : } :
Asymptotics.IsBigOWith 1 l g' fun (x : α) => (f' x, g' x)
theorem Asymptotics.isBigO_fst_prod {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {f' : αE'} {g' : αF'} {l : } :
f' =O[l] fun (x : α) => (f' x, g' x)
theorem Asymptotics.isBigO_snd_prod {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {f' : αE'} {g' : αF'} {l : } :
g' =O[l] fun (x : α) => (f' x, g' x)
theorem Asymptotics.isBigO_fst_prod' {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {l : } {f' : αE' × F'} :
(fun (x : α) => (f' x).1) =O[l] f'
theorem Asymptotics.isBigO_snd_prod' {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {l : } {f' : αE' × F'} :
(fun (x : α) => (f' x).2) =O[l] f'
theorem Asymptotics.IsBigOWith.prod_rightl {α : Type u_1} {E : Type u_3} {F' : Type u_7} {G' : Type u_8} [Norm E] {c : } {f : αE} {g' : αF'} (k' : αG') {l : } (h : ) (hc : 0 c) :
Asymptotics.IsBigOWith c l f fun (x : α) => (g' x, k' x)
theorem Asymptotics.IsBigO.prod_rightl {α : Type u_1} {E : Type u_3} {F' : Type u_7} {G' : Type u_8} [Norm E] {f : αE} {g' : αF'} (k' : αG') {l : } (h : f =O[l] g') :
f =O[l] fun (x : α) => (g' x, k' x)
theorem Asymptotics.IsLittleO.prod_rightl {α : Type u_1} {E : Type u_3} {F' : Type u_7} {G' : Type u_8} [Norm E] {f : αE} {g' : αF'} (k' : αG') {l : } (h : f =o[l] g') :
f =o[l] fun (x : α) => (g' x, k' x)
theorem Asymptotics.IsBigOWith.prod_rightr {α : Type u_1} {E : Type u_3} {E' : Type u_6} {F' : Type u_7} [Norm E] {c : } {f : αE} (f' : αE') {g' : αF'} {l : } (h : ) (hc : 0 c) :
Asymptotics.IsBigOWith c l f fun (x : α) => (f' x, g' x)
theorem Asymptotics.IsBigO.prod_rightr {α : Type u_1} {E : Type u_3} {E' : Type u_6} {F' : Type u_7} [Norm E] {f : αE} (f' : αE') {g' : αF'} {l : } (h : f =O[l] g') :
f =O[l] fun (x : α) => (f' x, g' x)
theorem Asymptotics.IsLittleO.prod_rightr {α : Type u_1} {E : Type u_3} {E' : Type u_6} {F' : Type u_7} [Norm E] {f : αE} (f' : αE') {g' : αF'} {l : } (h : f =o[l] g') :
f =o[l] fun (x : α) => (f' x, g' x)
theorem Asymptotics.IsBigOWith.prod_left_same {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} {c : } {f' : αE'} {g' : αF'} {k' : αG'} {l : } (hf : Asymptotics.IsBigOWith c l f' k') (hg : Asymptotics.IsBigOWith c l g' k') :
Asymptotics.IsBigOWith c l (fun (x : α) => (f' x, g' x)) k'
theorem Asymptotics.IsBigOWith.prod_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} {c : } {c' : } {f' : αE'} {g' : αF'} {k' : αG'} {l : } (hf : Asymptotics.IsBigOWith c l f' k') (hg : Asymptotics.IsBigOWith c' l g' k') :
Asymptotics.IsBigOWith (max c c') l (fun (x : α) => (f' x, g' x)) k'
theorem Asymptotics.IsBigOWith.prod_left_fst {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} {c : } {f' : αE'} {g' : αF'} {k' : αG'} {l : } (h : Asymptotics.IsBigOWith c l (fun (x : α) => (f' x, g' x)) k') :
theorem Asymptotics.IsBigOWith.prod_left_snd {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} {c : } {f' : αE'} {g' : αF'} {k' : αG'} {l : } (h : Asymptotics.IsBigOWith c l (fun (x : α) => (f' x, g' x)) k') :
theorem Asymptotics.isBigOWith_prod_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} {c : } {f' : αE'} {g' : αF'} {k' : αG'} {l : } :
Asymptotics.IsBigOWith c l (fun (x : α) => (f' x, g' x)) k' Asymptotics.IsBigOWith c l f' k' Asymptotics.IsBigOWith c l g' k'
theorem Asymptotics.IsBigO.prod_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} {f' : αE'} {g' : αF'} {k' : αG'} {l : } (hf : f' =O[l] k') (hg : g' =O[l] k') :
(fun (x : α) => (f' x, g' x)) =O[l] k'
theorem Asymptotics.IsBigO.prod_left_fst {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} {f' : αE'} {g' : αF'} {k' : αG'} {l : } :
(fun (x : α) => (f' x, g' x)) =O[l] k'f' =O[l] k'
theorem Asymptotics.IsBigO.prod_left_snd {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} {f' : αE'} {g' : αF'} {k' : αG'} {l : } :
(fun (x : α) => (f' x, g' x)) =O[l] k'g' =O[l] k'
@[simp]
theorem Asymptotics.isBigO_prod_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} {f' : αE'} {g' : αF'} {k' : αG'} {l : } :
(fun (x : α) => (f' x, g' x)) =O[l] k' f' =O[l] k' g' =O[l] k'
theorem Asymptotics.IsLittleO.prod_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} {f' : αE'} {g' : αF'} {k' : αG'} {l : } (hf : f' =o[l] k') (hg : g' =o[l] k') :
(fun (x : α) => (f' x, g' x)) =o[l] k'
theorem Asymptotics.IsLittleO.prod_left_fst {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} {f' : αE'} {g' : αF'} {k' : αG'} {l : } :
(fun (x : α) => (f' x, g' x)) =o[l] k'f' =o[l] k'
theorem Asymptotics.IsLittleO.prod_left_snd {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} {f' : αE'} {g' : αF'} {k' : αG'} {l : } :
(fun (x : α) => (f' x, g' x)) =o[l] k'g' =o[l] k'
@[simp]
theorem Asymptotics.isLittleO_prod_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} {f' : αE'} {g' : αF'} {k' : αG'} {l : } :
(fun (x : α) => (f' x, g' x)) =o[l] k' f' =o[l] k' g' =o[l] k'
theorem Asymptotics.IsBigOWith.eq_zero_imp {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [] [] {c : } {f'' : αE''} {g'' : αF''} {l : } (h : Asymptotics.IsBigOWith c l f'' g'') :
∀ᶠ (x : α) in l, g'' x = 0f'' x = 0
theorem Asymptotics.IsBigO.eq_zero_imp {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [] [] {f'' : αE''} {g'' : αF''} {l : } (h : f'' =O[l] g'') :
∀ᶠ (x : α) in l, g'' x = 0f'' x = 0

theorem Asymptotics.IsBigOWith.add {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {c₁ : } {c₂ : } {g : αF} {l : } {f₁ : αE'} {f₂ : αE'} (h₁ : Asymptotics.IsBigOWith c₁ l f₁ g) (h₂ : Asymptotics.IsBigOWith c₂ l f₂ g) :
Asymptotics.IsBigOWith (c₁ + c₂) l (fun (x : α) => f₁ x + f₂ x) g
theorem Asymptotics.IsBigO.add {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {g : αF} {l : } {f₁ : αE'} {f₂ : αE'} (h₁ : f₁ =O[l] g) (h₂ : f₂ =O[l] g) :
(fun (x : α) => f₁ x + f₂ x) =O[l] g
theorem Asymptotics.IsLittleO.add {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {g : αF} {l : } {f₁ : αE'} {f₂ : αE'} (h₁ : f₁ =o[l] g) (h₂ : f₂ =o[l] g) :
(fun (x : α) => f₁ x + f₂ x) =o[l] g
theorem Asymptotics.IsLittleO.add_add {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {l : } {f₁ : αE'} {f₂ : αE'} {g₁ : αF'} {g₂ : αF'} (h₁ : f₁ =o[l] g₁) (h₂ : f₂ =o[l] g₂) :
(fun (x : α) => f₁ x + f₂ x) =o[l] fun (x : α) => g₁ x + g₂ x
theorem Asymptotics.IsBigO.add_isLittleO {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {g : αF} {l : } {f₁ : αE'} {f₂ : αE'} (h₁ : f₁ =O[l] g) (h₂ : f₂ =o[l] g) :
(fun (x : α) => f₁ x + f₂ x) =O[l] g
theorem Asymptotics.IsLittleO.add_isBigO {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {g : αF} {l : } {f₁ : αE'} {f₂ : αE'} (h₁ : f₁ =o[l] g) (h₂ : f₂ =O[l] g) :
(fun (x : α) => f₁ x + f₂ x) =O[l] g
theorem Asymptotics.IsBigOWith.add_isLittleO {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {c₁ : } {c₂ : } {g : αF} {l : } {f₁ : αE'} {f₂ : αE'} (h₁ : Asymptotics.IsBigOWith c₁ l f₁ g) (h₂ : f₂ =o[l] g) (hc : c₁ < c₂) :
Asymptotics.IsBigOWith c₂ l (fun (x : α) => f₁ x + f₂ x) g
theorem Asymptotics.IsLittleO.add_isBigOWith {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {c₁ : } {c₂ : } {g : αF} {l : } {f₁ : αE'} {f₂ : αE'} (h₁ : f₁ =o[l] g) (h₂ : Asymptotics.IsBigOWith c₁ l f₂ g) (hc : c₁ < c₂) :
Asymptotics.IsBigOWith c₂ l (fun (x : α) => f₁ x + f₂ x) g
theorem Asymptotics.IsBigOWith.sub {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {c₁ : } {c₂ : } {g : αF} {l : } {f₁ : αE'} {f₂ : αE'} (h₁ : Asymptotics.IsBigOWith c₁ l f₁ g) (h₂ : Asymptotics.IsBigOWith c₂ l f₂ g) :
Asymptotics.IsBigOWith (c₁ + c₂) l (fun (x : α) => f₁ x - f₂ x) g
theorem Asymptotics.IsBigOWith.sub_isLittleO {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {c₁ : } {c₂ : } {g : αF} {l : } {f₁ : αE'} {f₂ : αE'} (h₁ : Asymptotics.IsBigOWith c₁ l f₁ g) (h₂ : f₂ =o[l] g) (hc : c₁ < c₂) :
Asymptotics.IsBigOWith c₂ l (fun (x : α) => f₁ x - f₂ x) g
theorem Asymptotics.IsBigO.sub {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {g : αF} {l : } {f₁ : αE'} {f₂ : αE'} (h₁ : f₁ =O[l] g) (h₂ : f₂ =O[l] g) :
(fun (x : α) => f₁ x - f₂ x) =O[l] g
theorem Asymptotics.IsLittleO.sub {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {g : αF} {l : } {f₁ : αE'} {f₂ : αE'} (h₁ : f₁ =o[l] g) (h₂ : f₂ =o[l] g) :
(fun (x : α) => f₁ x - f₂ x) =o[l] g

### Lemmas about IsBigO (f₁ - f₂) g l / IsLittleO (f₁ - f₂) g l treated as a binary relation #

theorem Asymptotics.IsBigOWith.symm {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {c : } {g : αF} {l : } {f₁ : αE'} {f₂ : αE'} (h : Asymptotics.IsBigOWith c l (fun (x : α) => f₁ x - f₂ x) g) :
Asymptotics.IsBigOWith c l (fun (x : α) => f₂ x - f₁ x) g
theorem Asymptotics.isBigOWith_comm {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {c : } {g : αF} {l : } {f₁ : αE'} {f₂ : αE'} :
Asymptotics.IsBigOWith c l (fun (x : α) => f₁ x - f₂ x) g Asymptotics.IsBigOWith c l (fun (x : α) => f₂ x - f₁ x) g
theorem Asymptotics.IsBigO.symm {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {g : αF} {l : } {f₁ : αE'} {f₂ : αE'} (h : (fun (x : α) => f₁ x - f₂ x) =O[l] g) :
(fun (x : α) => f₂ x - f₁ x) =O[l] g
theorem Asymptotics.isBigO_comm {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {g : αF} {l : } {f₁ : αE'} {f₂ : αE'} :
(fun (x : α) => f₁ x - f₂ x) =O[l] g (fun (x : α) => f₂ x - f₁ x) =O[l] g
theorem Asymptotics.IsLittleO.symm {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {g : αF} {l : } {f₁ : αE'} {f₂ : αE'} (h : (fun (x : α) => f₁ x - f₂ x) =o[l] g) :
(fun (x : α) => f₂ x - f₁ x) =o[l] g
theorem Asymptotics.isLittleO_comm {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {g : αF} {l : } {f₁ : αE'} {f₂ : αE'} :
(fun (x : α) => f₁ x - f₂ x) =o[l] g (fun (x : α) => f₂ x - f₁ x) =o[l] g
theorem Asymptotics.IsBigOWith.triangle {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {c : } {c' : } {g : αF} {l : } {f₁ : αE'} {f₂ : αE'} {f₃ : αE'} (h₁ : Asymptotics.IsBigOWith c l (fun (x : α) => f₁ x - f₂ x) g) (h₂ : Asymptotics.IsBigOWith c' l (fun (x : α) => f₂ x - f₃ x) g) :
Asymptotics.IsBigOWith (c + c') l (fun (x : α) => f₁ x - f₃ x) g
theorem Asymptotics.IsBigO.triangle {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {g : αF} {l : } {f₁ : αE'} {f₂ : αE'} {f₃ : αE'} (h₁ : (fun (x : α) => f₁ x - f₂ x) =O[l] g) (h₂ : (fun (x : α) => f₂ x - f₃ x) =O[l] g) :
(fun (x : α) => f₁ x - f₃ x) =O[l] g
theorem Asymptotics.IsLittleO.triangle {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {g : αF} {l : } {f₁ : αE'} {f₂ : αE'} {f₃ : αE'} (h₁ : (fun (x : α) => f₁ x - f₂ x) =o[l] g) (h₂ : (fun (x : α) => f₂ x - f₃ x) =o[l] g) :
(fun (x : α) => f₁ x - f₃ x) =o[l] g
theorem Asymptotics.IsBigO.congr_of_sub {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {g : αF} {l : } {f₁ : αE'} {f₂ : αE'} (h : (fun (x : α) => f₁ x - f₂ x) =O[l] g) :
f₁ =O[l] g f₂ =O[l] g
theorem Asymptotics.IsLittleO.congr_of_sub {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] {g : αF} {l : } {f₁ : αE'} {f₂ : αE'} (h : (fun (x : α) => f₁ x - f₂ x) =o[l] g) :
f₁ =o[l] g f₂ =o[l] g

### Zero, one, and other constants #

theorem Asymptotics.isLittleO_zero {α : Type u_1} {E' : Type u_6} {F' : Type u_7} (g' : αF') (l : ) :
(fun (_x : α) => 0) =o[l] g'
theorem Asymptotics.isBigOWith_zero {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {c : } (g' : αF') (l : ) (hc : 0 c) :
Asymptotics.IsBigOWith c l (fun (_x : α) => 0) g'
theorem Asymptotics.isBigOWith_zero' {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] (g : αF) (l : ) :
Asymptotics.IsBigOWith 0 l (fun (_x : α) => 0) g
theorem Asymptotics.isBigO_zero {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] (g : αF) (l : ) :
(fun (_x : α) => 0) =O[l] g
theorem Asymptotics.isBigO_refl_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {f' : αE'} (g' : αF') (l : ) :
(fun (x : α) => f' x - f' x) =O[l] g'
theorem Asymptotics.isLittleO_refl_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {f' : αE'} (g' : αF') (l : ) :
(fun (x : α) => f' x - f' x) =o[l] g'
@[simp]
theorem Asymptotics.isBigOWith_zero_right_iff {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} [] {c : } {f'' : αE''} {l : } :
(Asymptotics.IsBigOWith c l f'' fun (_x : α) => 0) f'' =ᶠ[l] 0
@[simp]
theorem Asymptotics.isBigO_zero_right_iff {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} [] {f'' : αE''} {l : } :
(f'' =O[l] fun (_x : α) => 0) f'' =ᶠ[l] 0
@[simp]
theorem Asymptotics.isLittleO_zero_right_iff {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} [] {f'' : αE''} {l : } :
(f'' =o[l] fun (_x : α) => 0) f'' =ᶠ[l] 0
theorem Asymptotics.isBigOWith_const_const {α : Type u_1} {E : Type u_3} {F'' : Type u_10} [Norm E] [] (c : E) {c' : F''} (hc' : c' 0) (l : ) :
Asymptotics.IsBigOWith (c / c') l (fun (_x : α) => c) fun (_x : α) => c'
theorem Asymptotics.isBigO_const_const {α : Type u_1} {E : Type u_3} {F'' : Type u_10} [Norm E] [] (c : E) {c' : F''} (hc' : c' 0) (l : ) :
(fun (_x : α) => c) =O[l] fun (_x : α) => c'
@[simp]
theorem Asymptotics.isBigO_const_const_iff {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [] [] {c : E''} {c' : F''} (l : ) [l.NeBot] :
((fun (_x : α) => c) =O[l] fun (_x : α) => c') c' = 0c = 0
@[simp]
theorem Asymptotics.isBigO_pure {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [] [] {f'' : αE''} {g'' : αF''} {x : α} :
f'' =O[pure x] g'' g'' x = 0f'' x = 0
@[simp]
theorem Asymptotics.isBigOWith_principal {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : } {f : αE} {g : αF} {s : Set α} :
xs, f x c * g x
theorem Asymptotics.isBigO_principal {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} {s : Set α} :
∃ (c : ), xs, f x c * g x
@[simp]
theorem Asymptotics.isLittleO_principal {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} [] {g' : αF'} {f'' : αE''} {s : Set α} :
f'' =o[] g' xs, f'' x = 0
@[simp]
theorem Asymptotics.isBigOWith_top {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : } {f : αE} {g : αF} :
∀ (x : α), f x c * g x
@[simp]
theorem Asymptotics.isBigO_top {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {g : αF} :
f =O[] g ∃ (C : ), ∀ (x : α), f x C * g x
@[simp]
theorem Asymptotics.isLittleO_top {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} [] {g' : αF'} {f'' : αE''} :
f'' =o[] g' ∀ (x : α), f'' x = 0
theorem Asymptotics.isBigOWith_const_one {α : Type u_1} {E : Type u_3} (F : Type u_4) [Norm E] [Norm F] [One F] [] (c : E) (l : ) :
Asymptotics.IsBigOWith c l (fun (_x : α) => c) fun (_x : α) => 1
theorem Asymptotics.isBigO_const_one {α : Type u_1} {E : Type u_3} (F : Type u_4) [Norm E] [Norm F] [One F] [] (c : E) (l : ) :
(fun (_x : α) => c) =O[l] fun (_x : α) => 1
theorem Asymptotics.isLittleO_const_iff_isLittleO_one {α : Type u_1} {E : Type u_3} (F : Type u_4) {F'' : Type u_10} [Norm E] [Norm F] [] {f : αE} {l : } [One F] [] {c : F''} (hc : c 0) :
(f =o[l] fun (_x : α) => c) f =o[l] fun (_x : α) => 1
@[simp]
theorem Asymptotics.isLittleO_one_iff {α : Type u_1} (F : Type u_4) {E' : Type u_6} [Norm F] {f' : αE'} {l : } [One F] [] :
(f' =o[l] fun (_x : α) => 1) Filter.Tendsto f' l (nhds 0)
@[simp]
theorem Asymptotics.isBigO_one_iff {α : Type u_1} {E : Type u_3} (F : Type u_4) [Norm E] [Norm F] {f : αE} {l : } [One F] [] :
(f =O[l] fun (_x : α) => 1) Filter.IsBoundedUnder (fun (x x_1 : ) => x x_1) l fun (x : α) => f x
theorem Filter.IsBoundedUnder.isBigO_one {α : Type u_1} {E : Type u_3} (F : Type u_4) [Norm E] [Norm F] {f : αE} {l : } [One F] [] :
(Filter.IsBoundedUnder (fun (x x_1 : ) => x x_1) l fun (x : α) => f x)f =O[l] fun (_x : α) => 1

Alias of the reverse direction of Asymptotics.isBigO_one_iff.

@[simp]
theorem Asymptotics.isLittleO_one_left_iff {α : Type u_1} {E : Type u_3} (F : Type u_4) [Norm E] [Norm F] {f : αE} {l : } [One F] [] :
(fun (_x : α) => 1) =o[l] f Filter.Tendsto (fun (x : α) => f x) l Filter.atTop
theorem Filter.Tendsto.isBigO_one {α : Type u_1} (F : Type u_4) {E' : Type u_6} [Norm F] {f' : αE'} {l : } [One F] [] {c : E'} (h : Filter.Tendsto f' l (nhds c)) :
f' =O[l] fun (_x : α) => 1
theorem Asymptotics.IsBigO.trans_tendsto_nhds {α : Type u_1} {E : Type u_3} (F : Type u_4) {F' : Type u_7} [Norm E] [Norm F] {f : αE} {g' : αF'} {l : } [One F] [] (hfg : f =O[l] g') {y : F'} (hg : Filter.Tendsto g' l (nhds y)) :
f =O[l] fun (_x : α) => 1
theorem Asymptotics.isBigO_one_nhds_ne_iff {α : Type u_1} {E : Type u_3} (F : Type u_4) [Norm E] [Norm F] {f : αE} [One F] [] [] {a : α} :
(f =O[nhdsWithin a {a}] fun (x : α) => 1) f =O[nhds a] fun (x : α) => 1

The condition f = O[𝓝[≠] a] 1 is equivalent to f = O[𝓝 a] 1.

theorem Asymptotics.isLittleO_const_iff {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [] [] {f'' : αE''} {l : } {c : F''} (hc : c 0) :
(f'' =o[l] fun (_x : α) => c) Filter.Tendsto f'' l (nhds 0)
theorem Asymptotics.isLittleO_id_const {E'' : Type u_9} {F'' : Type u_10} [] [] {c : F''} (hc : c 0) :
(fun (x : E'') => x) =o[nhds 0] fun (_x : E'') => c
theorem Filter.IsBoundedUnder.isBigO_const {α : Type u_1} {E : Type u_3} {F'' : Type u_10} [Norm E] [] {f : αE} {l : } (h : Filter.IsBoundedUnder (fun (x x_1 : ) => x x_1) l (norm f)) {c : F''} (hc : c 0) :
f =O[l] fun (_x : α) => c
theorem Asymptotics.isBigO_const_of_tendsto {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [] [] {f'' : αE''} {l : } {y : E''} (h : Filter.Tendsto f'' l (nhds y)) {c : F''} (hc : c 0) :
f'' =O[l] fun (_x : α) => c
theorem Asymptotics.IsBigO.isBoundedUnder_le {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : αE} {l : } {c : F} (h : f =O[l] fun (_x : α) => c) :
Filter.IsBoundedUnder (fun (x x_1 : ) => x x_1) l (norm f)
theorem Asymptotics.isBigO_const_of_ne {α : Type u_1} {E : Type u_3} {F'' : Type u_10} [Norm E] [] {f : αE} {l : } {c : F''} (hc : c 0) :
(f =O[l] fun (_x : α) => c) Filter.IsBoundedUnder (fun (x x_1 : ) => x x_1) l (norm f)
theorem Asymptotics.isBigO_const_iff {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [] [] {f'' : αE''} {l : } {c : F''} :
(f'' =O[l] fun (_x : α) => c) (c = 0f'' =ᶠ[l] 0) Filter.IsBoundedUnder (fun (x x_1 : ) => x x_1) l fun (x : α) => f'' x
theorem Asymptotics.isBigO_iff_isBoundedUnder_le_div {α : Type u_1} {E : Type u_3} {F'' : Type u_10} [Norm E] [] {f : αE} {g'' : αF''} {l : } (h : ∀ᶠ (x : α) in l, g'' x 0) :
f =O[l] g'' Filter.IsBoundedUnder (fun (x x_1 : ) => x x_1) l fun (x : α) => f x / g'' x
theorem Asymptotics.isBigO_const_left_iff_pos_le_norm {α : Type u_1} {E' : Type u_6} {E'' : Type u_9} [] {f' : αE'} {l : } {c : E''} (hc : c 0) :
(fun (_x : α) => c) =O[l] f' ∃ (b : ), 0 < b ∀ᶠ (x : α) in l, b f' x

(fun x ↦ c) =O[l] f if and only if f is bounded away from zero.

theorem Asymptotics.IsBigO.trans_tendsto {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [] [] {f'' : αE''} {g'' : αF''} {l : } (hfg : f'' =O[l] g'') (hg : Filter.Tendsto g'' l (nhds 0)) :
theorem Asymptotics.IsLittleO.trans_tendsto {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [] [] {f'' : αE''} {g'' : αF''} {l : } (hfg : f'' =o[l] g'') (hg : Filter.Tendsto g'' l (nhds 0)) :

### Multiplication by a constant #

theorem Asymptotics.isBigOWith_const_mul_self {α : Type u_1} {R : Type u_13} [] (c : R) (f : αR) (l : ) :
Asymptotics.IsBigOWith c l (fun (x : α) => c * f x) f
theorem Asymptotics.isBigO_const_mul_self {α : Type u_1} {R : Type u_13} [] (c : R) (f : αR) (l : ) :
(fun (x : α) => c * f x) =O[l] f
theorem Asymptotics.IsBigOWith.const_mul_left {α : Type u_1} {F : Type u_4} {R : Type u_13} [Norm F] [] {c : } {g : αF} {l : } {f : αR} (h : ) (c' : R) :
Asymptotics.IsBigOWith (c' * c) l (fun (x : α) => c' * f x) g
theorem Asymptotics.IsBigO.const_mul_left {α : Type u_1} {F : Type u_4} {R : Type u_13} [Norm F] [] {g : αF} {l : } {f : αR} (h : f =O[l] g) (c' : R) :
(fun (x : α) => c' * f x) =O[l] g
theorem Asymptotics.isBigOWith_self_const_mul' {α : Type u_1} {R : Type u_13} [] (u : Rˣ) (f : αR) (l : ) :
Asymptotics.IsBigOWith u⁻¹ l f fun (x : α) => u * f x
theorem Asymptotics.isBigOWith_self_const_mul {α : Type u_1} {𝕜 : Type u_15} (c : 𝕜) (hc : c 0) (f : α𝕜) (l : ) :
Asymptotics.IsBigOWith c⁻¹ l f fun (x : α) => c * f x
theorem Asymptotics.isBigO_self_const_mul' {α : Type u_1} {R : Type u_13} [] {c : R} (hc : ) (f : αR) (l : ) :
f =O[l] fun (x : α) => c * f x
theorem Asymptotics.isBigO_self_const_mul {α : Type u_1} {𝕜 : Type u_15} (c : 𝕜) (hc : c 0) (f : α𝕜) (l : ) :
f =O[l] fun (x : α) => c * f x
theorem Asymptotics.isBigO_const_mul_left_iff' {α : Type u_1} {F : Type u_4} {R : Type u_13} [Norm F] [] {g : αF} {l : } {f : αR} {c : R} (hc : )