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 : Filter α) (f : α → E) (g : α → F) : Asymptotics.IsBigOWith c l f g = ∀ᶠ (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 : 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 = Asymptotics.wrapped✝.1

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

@[irreducible]

def Asymptotics.IsBigO {α : Type u_17} {E : Type u_18} {F : Type u_19} [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

• @Asymptotics.IsBigO = Asymptotics.wrapped✝.1

theorem Asymptotics.IsBigO_def {α : Type u_17} {E : Type u_18} {F : Type u_19} [Norm E] [Norm F] (l : Filter α) (f : α → E) (g : α → F) : 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_3} {F : Type u_4} [Norm E] [Norm F] {f : α → E} {g : α → F} {l : Filter α} : f =O[l] g ↔ ∃ (c : ℝ), Asymptotics.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_3} {F : Type u_4} [Norm E] [Norm F] {f : α → E} {g : α → F} {l : Filter α} : 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] [SeminormedAddGroup E'''] {f : α → E} {l : Filter α} {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] [SeminormedAddGroup E'''] {f : α → E} {l : Filter α} {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 : Filter α} (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 : Filter α} (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 : Filter α} : 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 : Filter α) (f : α → E) (g : α → F) : f =o[l] g = ∀ ⦃c : ℝ⦄, 0 < c → Asymptotics.IsBigOWith c l f g

@[irreducible]

def Asymptotics.IsLittleO {α : Type u_17} {E : Type u_18} {F : Type u_19} [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

• @Asymptotics.IsLittleO = Asymptotics.wrapped✝.1

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_3} {F : Type u_4} [Norm E] [Norm F] {f : α → E} {g : α → F} {l : Filter α} : f =o[l] g ↔ ∀ ⦃c : ℝ⦄, 0 < c → Asymptotics.IsBigOWith c l f g

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 : Filter α} : f =o[l] g → ∀ ⦃c : ℝ⦄, 0 < c → Asymptotics.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_3} {F : Type u_4} [Norm E] [Norm F] {f : α → E} {g : α → F} {l : Filter α} : (∀ ⦃c : ℝ⦄, 0 < c → Asymptotics.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_3} {F : Type u_4} [Norm E] [Norm F] {f : α → E} {g : α → F} {l : Filter α} : 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_3} {F : Type u_4} [Norm E] [Norm F] {f : α → E} {g : α → F} {l : Filter α} : 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_3} {F : Type u_4} [Norm E] [Norm F] {f : α → E} {g : α → F} {l : Filter α} : (∀ ⦃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_3} {F : Type u_4} [Norm E] [Norm F] {c : ℝ} {f : α → E} {g : α → F} {l : Filter α} (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 : Filter α} (h : f =o[l] g) (hc : 0 < c) : Asymptotics.IsBigOWith c l f g

theorem Asymptotics.IsLittleO.eventuallyLE {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : α → E} {g : α → F} {l : Filter α} (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 : Filter α} (h : Asymptotics.IsBigOWith c l f g) : 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 : Filter α} (hgf : f =o[l] g) : Asymptotics.IsBigOWith 1 l f 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 : Filter α} (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 : Filter α} : f =O[l] g → ∃ (c : ℝ), Asymptotics.IsBigOWith c l f g

theorem Asymptotics.IsBigOWith.weaken {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] [SeminormedAddCommGroup F'] {c : ℝ} {c' : ℝ} {f : α → E} {g' : α → F'} {l : Filter α} (h : Asymptotics.IsBigOWith c l f g') (hc : c ≤ c') : Asymptotics.IsBigOWith c' l f g'

theorem Asymptotics.IsBigOWith.exists_pos {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] [SeminormedAddCommGroup F'] {c : ℝ} {f : α → E} {g' : α → F'} {l : Filter α} (h : Asymptotics.IsBigOWith c l f g') : ∃ 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] [SeminormedAddCommGroup F'] {f : α → E} {g' : α → F'} {l : Filter α} (h : f =O[l] g') : ∃ c > 0, Asymptotics.IsBigOWith c l f g'

theorem Asymptotics.IsBigOWith.exists_nonneg {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] [SeminormedAddCommGroup F'] {c : ℝ} {f : α → E} {g' : α → F'} {l : Filter α} (h : Asymptotics.IsBigOWith c l f g') : ∃ 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] [SeminormedAddCommGroup F'] {f : α → E} {g' : α → F'} {l : Filter α} (h : f =O[l] g') : ∃ c ≥ 0, Asymptotics.IsBigOWith c l f g'

theorem Asymptotics.isBigO_iff_eventually_isBigOWith {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] [SeminormedAddCommGroup F'] {f : α → E} {g' : α → F'} {l : Filter α} : f =O[l] g' ↔ ∀ᶠ (c : ℝ) in Filter.atTop, Asymptotics.IsBigOWith c l f g'

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] [SeminormedAddCommGroup F'] {f : α → E} {g' : α → F'} {l : Filter α} : 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] [SeminormedAddCommGroup F'] {f : α → E} {g' : α → F'} {l : Filter α} {ι : Sort u_17} {p : ι → Prop} {s : ι → Set α} (h : f =O[l] g') (hb : l.HasBasis p s) : ∃ c > 0, ∃ (i : ι), p i ∧ ∀ x ∈ s 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 : Filter α} (hc : 0 < c) : Asymptotics.IsBigOWith c⁻¹ l f g ↔ ∀ᶠ (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 : Filter α} (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] [SeminormedAddCommGroup F'] {f : α → E} {g' : α → F'} {l : Filter α} : 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] [SeminormedAddCommGroup E'] {g : α → F} {f' : α → E'} {l : Filter α} : 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} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f' : α → E'} {g' : α → F'} {l : Filter α} [Subsingleton E'] : f' =o[l] g'

theorem Asymptotics.isBigO_of_subsingleton {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f' : α → E'} {g' : α → F'} {l : Filter α} [Subsingleton E'] : 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 : Filter α} {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 : Filter α} {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 : Filter α} {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 : Filter α} {f₁ : α → E} {f₂ : α → E} (h : Asymptotics.IsBigOWith c l f₁ g) (hf : ∀ (x : α), f₁ x = f₂ x) : Asymptotics.IsBigOWith c l f₂ g

theorem Asymptotics.IsBigOWith.congr_right {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : ℝ} {f : α → E} {l : Filter α} {g₁ : α → F} {g₂ : α → F} (h : Asymptotics.IsBigOWith c l f g₁) (hg : ∀ (x : α), g₁ x = g₂ x) : Asymptotics.IsBigOWith c l f g₂

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 : Filter α} (h : Asymptotics.IsBigOWith c₁ l f g) (hc : c₁ = c₂) : Asymptotics.IsBigOWith c₂ l f g

theorem Asymptotics.isBigO_congr {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : Filter α} {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 : Filter α} {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 : Filter α} {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 : Filter α} {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 : Filter α} {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 : Filter α} {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 : Filter α} {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 : Filter α} {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 : Filter α} {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 : Filter α} {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 : Filter α} {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 : Filter α} : Trans (fun (x1 x2 : α → E) => x1 =ᶠ[l] x2) (fun (x1 : α → E) (x2 : α → F) => x1 =O[l] x2) fun (x1 : α → E) (x2 : α → F) => x1 =O[l] x2

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 : Filter α} {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 : Filter α} : Trans (fun (x1 x2 : α → E) => x1 =ᶠ[l] x2) (fun (x1 : α → E) (x2 : α → F) => x1 =o[l] x2) fun (x1 : α → E) (x2 : α → F) => x1 =o[l] x2

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 : Filter α} {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 : Filter α} : Trans (fun (x1 : α → E) (x2 : α → F) => x1 =O[l] x2) (fun (x1 x2 : α → F) => x1 =ᶠ[l] x2) fun (x1 : α → E) (x2 : α → F) => x1 =O[l] x2

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 : Filter α} {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 : Filter α} : Trans (fun (x1 : α → E) (x2 : α → F) => x1 =o[l] x2) (fun (x1 x2 : α → F) => x1 =ᶠ[l] x2) fun (x1 : α → E) (x2 : α → F) => x1 =o[l] x2

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 : Filter α} (hcfg : Asymptotics.IsBigOWith c l f g) {k : β → α} {l' : Filter β} (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 : Filter α} (hfg : f =O[l] g) {k : β → α} {l' : Filter β} (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 : Filter α} (hfg : f =o[l] g) {k : β → α} {l' : Filter β} (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 : Filter β} : Asymptotics.IsBigOWith c (Filter.map k l) f g ↔ Asymptotics.IsBigOWith c l (f ∘ k) (g ∘ k)

@[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 : Filter β} : f =O[Filter.map k l] 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 : Filter β} : f =o[Filter.map k l] 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 : Filter α} {l' : Filter α} (h : Asymptotics.IsBigOWith c l' f g) (hl : l ≤ l') : Asymptotics.IsBigOWith c l f g

theorem Asymptotics.IsBigO.mono {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : α → E} {g : α → F} {l : Filter α} {l' : Filter α} (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 : Filter α} {l' : Filter α} (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 : Filter α} (hfg : Asymptotics.IsBigOWith c l f g) (hgk : Asymptotics.IsBigOWith c' l g k) (hc : 0 ≤ c) : Asymptotics.IsBigOWith (c * c') l f k

theorem Asymptotics.IsBigO.trans {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [Norm E] [Norm G] [SeminormedAddCommGroup F'] {l : Filter α} {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] [SeminormedAddCommGroup F'] {l : Filter α} : Trans (fun (x1 : α → E) (x2 : α → F') => x1 =O[l] x2) (fun (x1 : α → F') (x2 : α → G) => x1 =O[l] x2) fun (x1 : α → E) (x2 : α → G) => x1 =O[l] x2

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 : Filter α} (hfg : f =o[l] g) (hgk : Asymptotics.IsBigOWith c l g k) (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] [SeminormedAddCommGroup G'] {l : Filter α} {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] [SeminormedAddCommGroup G'] {l : Filter α} : Trans (fun (x1 : α → E) (x2 : α → F) => x1 =o[l] x2) (fun (x1 : α → F) (x2 : α → G') => x1 =O[l] x2) fun (x1 : α → E) (x2 : α → G') => x1 =o[l] x2

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 : Filter α} (hfg : Asymptotics.IsBigOWith c l f g) (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] [SeminormedAddCommGroup F'] {l : Filter α} {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] [SeminormedAddCommGroup F'] {l : Filter α} : Trans (fun (x1 : α → E) (x2 : α → F') => x1 =O[l] x2) (fun (x1 : α → F') (x2 : α → G) => x1 =o[l] x2) fun (x1 : α → E) (x2 : α → G) => x1 =o[l] x2

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 : Filter α} {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 : Filter α} : Trans (fun (x1 : α → E) (x2 : α → F) => x1 =o[l] x2) (fun (x1 : α → F) (x2 : α → G) => x1 =o[l] x2) fun (x1 : α → E) (x2 : α → G) => x1 =o[l] x2

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] [SeminormedAddCommGroup F'] {l : Filter α} {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 : Filter α} (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 : Filter α) (hfg : ∀ (x : α), ‖f x‖ ≤ c * ‖g x‖) : Asymptotics.IsBigOWith c l f g

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 : Filter α) (hfg : ∀ (x : α), ‖f x‖ ≤ ‖g x‖) : Asymptotics.IsBigOWith 1 l f g

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 : Filter α) (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 : Filter α) (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 : Filter α) : Asymptotics.IsBigOWith 1 l f f

theorem Asymptotics.isBigO_refl {α : Type u_1} {E : Type u_3} [Norm E] (f : α → E) (l : Filter α) : f =O[l] f

theorem Filter.EventuallyEq.isBigO {α : Type u_1} {E : Type u_3} [Norm E] {l : Filter α} {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 : Filter α} (hfg : Asymptotics.IsBigOWith c l f g) (hgk : ∀ (x : α), ‖g x‖ ≤ ‖k x‖) (hc : 0 ≤ c) : Asymptotics.IsBigOWith c l f k

theorem Asymptotics.IsBigO.trans_le {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [Norm E] [Norm G] [SeminormedAddCommGroup F'] {f : α → E} {k : α → G} {g' : α → F'} {l : Filter α} (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 : Filter α} (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} [SeminormedAddCommGroup E'] {f' : α → E'} {l : Filter α} (h : ∃ᶠ (x : α) in l, ‖f' x‖ ≠ 0) : ¬f' =o[l] f'

theorem Asymptotics.isLittleO_irrefl {α : Type u_1} {E'' : Type u_9} [NormedAddCommGroup E''] {f'' : α → E''} {l : Filter α} (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} [SeminormedAddCommGroup F'] [NormedAddCommGroup E''] {g' : α → F'} {f'' : α → E''} {l : Filter α} (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} [SeminormedAddCommGroup F'] [NormedAddCommGroup E''] {g' : α → F'} {f'' : α → E''} {l : Filter α} (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) : Asymptotics.IsBigOWith c ⊥ f g

@[simp]

theorem Asymptotics.isBigO_bot {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] (f : α → E) (g : α → F) : f =O[⊥] g

@[simp]

theorem Asymptotics.isLittleO_bot {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] (f : α → E) (g : α → F) : f =o[⊥] g

@[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 : α} : Asymptotics.IsBigOWith c (pure x) f g ↔ ‖f x‖ ≤ c * ‖g 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 : Filter α} {l' : Filter α} (h : Asymptotics.IsBigOWith c l f g) (h' : Asymptotics.IsBigOWith c l' f g) : Asymptotics.IsBigOWith c (l ⊔ l') f g

theorem Asymptotics.IsBigOWith.sup' {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] [SeminormedAddCommGroup F'] {c : ℝ} {c' : ℝ} {f : α → E} {g' : α → F'} {l : Filter α} {l' : Filter α} (h : Asymptotics.IsBigOWith c l f g') (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] [SeminormedAddCommGroup F'] {f : α → E} {g' : α → F'} {l : Filter α} {l' : Filter α} (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 : Filter α} {l' : Filter α} (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] [SeminormedAddCommGroup F'] {f : α → E} {g' : α → F'} {l : Filter α} {l' : Filter α} : 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 : Filter α} {l' : Filter α} : 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] [TopologicalSpace α] {x : α} {s : Set α} {C : ℝ} {g : α → E} {g' : α → F} (h : ‖g x‖ ≤ C * ‖g' x‖) : Asymptotics.IsBigOWith C (nhdsWithin x (insert x s)) g g' ↔ Asymptotics.IsBigOWith C (nhdsWithin x s) g g'

theorem Asymptotics.IsBigOWith.insert {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] [TopologicalSpace α] {x : α} {s : Set α} {C : ℝ} {g : α → E} {g' : α → F} (h1 : Asymptotics.IsBigOWith C (nhdsWithin x s) g g') (h2 : ‖g x‖ ≤ C * ‖g' x‖) : Asymptotics.IsBigOWith C (nhdsWithin x (insert x s)) g g'

theorem Asymptotics.isLittleO_insert {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [TopologicalSpace α] {x : α} {s : Set α} {g : α → E'} {g' : α → F'} (h : g x = 0) : g =o[nhdsWithin x (insert x s)] g' ↔ g =o[nhdsWithin x s] g'

theorem Asymptotics.IsLittleO.insert {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [TopologicalSpace α] {x : α} {s : Set α} {g : α → E'} {g' : α → F'} (h1 : g =o[nhdsWithin x s] 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] [SeminormedAddCommGroup F'] {c : ℝ} {f : α → E} {g' : α → F'} {l : Filter α} : (Asymptotics.IsBigOWith c l f fun (x : α) => ‖g' x‖) ↔ Asymptotics.IsBigOWith c l f g'

@[simp]

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

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

Alias of the reverse direction of Asymptotics.isBigOWith_norm_right.

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

Alias of the forward direction of Asymptotics.isBigOWith_norm_right.

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

Alias of the reverse direction of Asymptotics.isBigOWith_abs_right.

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

Alias of the forward 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] [SeminormedAddCommGroup F'] {f : α → E} {g' : α → F'} {l : Filter α} : (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 : Filter α} {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] [SeminormedAddCommGroup F'] {f : α → E} {g' : α → F'} {l : Filter α} : (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] [SeminormedAddCommGroup F'] {f : α → E} {g' : α → F'} {l : Filter α} : f =O[l] g' → f =O[l] fun (x : α) => ‖g' x‖

Alias of the reverse direction of Asymptotics.isBigO_norm_right.

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

Alias of the forward direction of Asymptotics.isBigO_abs_right.

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

Alias of the reverse 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] [SeminormedAddCommGroup F'] {f : α → E} {g' : α → F'} {l : Filter α} : (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 : Filter α} {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] [SeminormedAddCommGroup F'] {f : α → E} {g' : α → F'} {l : Filter α} : 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] [SeminormedAddCommGroup F'] {f : α → E} {g' : α → F'} {l : Filter α} : (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 : Filter α} {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 : Filter α} {u : α → ℝ} : f =o[l] u → f =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] [SeminormedAddCommGroup E'] {c : ℝ} {g : α → F} {f' : α → E'} {l : Filter α} : Asymptotics.IsBigOWith c l (fun (x : α) => ‖f' x‖) g ↔ Asymptotics.IsBigOWith c l f' g

@[simp]

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

theorem Asymptotics.IsBigOWith.norm_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {c : ℝ} {g : α → F} {f' : α → E'} {l : Filter α} : Asymptotics.IsBigOWith c l f' g → 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] [SeminormedAddCommGroup E'] {c : ℝ} {g : α → F} {f' : α → E'} {l : Filter α} : Asymptotics.IsBigOWith c l (fun (x : α) => ‖f' x‖) g → Asymptotics.IsBigOWith c l f' 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 : Filter α} {u : α → ℝ} : Asymptotics.IsBigOWith c l (fun (x : α) => |u x|) g → Asymptotics.IsBigOWith c l u 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 : Filter α} {u : α → ℝ} : Asymptotics.IsBigOWith c l u g → 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] [SeminormedAddCommGroup E'] {g : α → F} {f' : α → E'} {l : Filter α} : (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 : Filter α} {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] [SeminormedAddCommGroup E'] {g : α → F} {f' : α → E'} {l : Filter α} : (fun (x : α) => ‖f' x‖) =O[l] g → f' =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] [SeminormedAddCommGroup E'] {g : α → F} {f' : α → E'} {l : Filter α} : 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 : Filter α} {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 : Filter α} {u : α → ℝ} : (fun (x : α) => |u x|) =O[l] g → u =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] [SeminormedAddCommGroup E'] {g : α → F} {f' : α → E'} {l : Filter α} : (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 : Filter α} {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] [SeminormedAddCommGroup E'] {g : α → F} {f' : α → E'} {l : Filter α} : (fun (x : α) => ‖f' x‖) =o[l] g → f' =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] [SeminormedAddCommGroup E'] {g : α → F} {f' : α → E'} {l : Filter α} : 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 : Filter α} {u : α → ℝ} : (fun (x : α) => |u x|) =o[l] g → u =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 : Filter α} {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} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {c : ℝ} {f' : α → E'} {g' : α → F'} {l : Filter α} : (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 : Filter α} {u : α → ℝ} {v : α → ℝ} : (Asymptotics.IsBigOWith c l (fun (x : α) => |u x|) fun (x : α) => |v x|) ↔ Asymptotics.IsBigOWith c l u v

theorem Asymptotics.IsBigOWith.of_norm_norm {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {c : ℝ} {f' : α → E'} {g' : α → F'} {l : Filter α} : (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} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {c : ℝ} {f' : α → E'} {g' : α → F'} {l : Filter α} : 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 : Filter α} {u : α → ℝ} {v : α → ℝ} : (Asymptotics.IsBigOWith c l (fun (x : α) => |u x|) fun (x : α) => |v x|) → Asymptotics.IsBigOWith c l u v

Alias of the forward direction of Asymptotics.isBigOWith_abs_abs.

theorem Asymptotics.IsBigOWith.abs_abs {α : Type u_1} {c : ℝ} {l : Filter α} {u : α → ℝ} {v : α → ℝ} : Asymptotics.IsBigOWith 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} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f' : α → E'} {g' : α → F'} {l : Filter α} : ((fun (x : α) => ‖f' x‖) =O[l] fun (x : α) => ‖g' x‖) ↔ f' =O[l] g'

theorem Asymptotics.isBigO_abs_abs {α : Type u_1} {l : Filter α} {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} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f' : α → E'} {g' : α → F'} {l : Filter α} : 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} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f' : α → E'} {g' : α → F'} {l : Filter α} : ((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 : Filter α} {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 : Filter α} {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} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f' : α → E'} {g' : α → F'} {l : Filter α} : ((fun (x : α) => ‖f' x‖) =o[l] fun (x : α) => ‖g' x‖) ↔ f' =o[l] g'

theorem Asymptotics.isLittleO_abs_abs {α : Type u_1} {l : Filter α} {u : α → ℝ} {v : α → ℝ} : ((fun (x : α) => |u x|) =o[l] fun (x : α) => |v x|) ↔ u =o[l] v

theorem Asymptotics.IsLittleO.of_norm_norm {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f' : α → E'} {g' : α → F'} {l : Filter α} : ((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.norm_norm {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f' : α → E'} {g' : α → F'} {l : Filter α} : 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.abs_abs {α : Type u_1} {l : Filter α} {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 : Filter α} {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] [SeminormedAddCommGroup F'] {c : ℝ} {f : α → E} {g' : α → F'} {l : Filter α} : (Asymptotics.IsBigOWith c l f fun (x : α) => -g' x) ↔ Asymptotics.IsBigOWith c l f g'

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

Alias of the forward direction of Asymptotics.isBigOWith_neg_right.

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

Alias of the reverse 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] [SeminormedAddCommGroup F'] {f : α → E} {g' : α → F'} {l : Filter α} : (f =O[l] fun (x : α) => -g' x) ↔ f =O[l] g'

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

Alias of the reverse direction of Asymptotics.isBigO_neg_right.

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

Alias of the forward 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] [SeminormedAddCommGroup F'] {f : α → E} {g' : α → F'} {l : Filter α} : (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] [SeminormedAddCommGroup F'] {f : α → E} {g' : α → F'} {l : Filter α} : (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] [SeminormedAddCommGroup F'] {f : α → E} {g' : α → F'} {l : Filter α} : 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] [SeminormedAddCommGroup E'] {c : ℝ} {g : α → F} {f' : α → E'} {l : Filter α} : Asymptotics.IsBigOWith c l (fun (x : α) => -f' x) g ↔ Asymptotics.IsBigOWith c l f' g

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

Alias of the reverse direction of Asymptotics.isBigOWith_neg_left.

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

Alias of the forward 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] [SeminormedAddCommGroup E'] {g : α → F} {f' : α → E'} {l : Filter α} : (fun (x : α) => -f' x) =O[l] g ↔ f' =O[l] g

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

Alias of the reverse direction of Asymptotics.isBigO_neg_left.

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

Alias of the forward 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] [SeminormedAddCommGroup E'] {g : α → F} {f' : α → E'} {l : Filter α} : (fun (x : α) => -f' x) =o[l] g ↔ f' =o[l] g

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

Alias of the forward direction of Asymptotics.isLittleO_neg_left.

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

Alias of the reverse 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} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f' : α → E'} {g' : α → F'} {l : Filter α} : 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} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f' : α → E'} {g' : α → F'} {l : Filter α} : 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} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f' : α → E'} {g' : α → F'} {l : Filter α} : 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} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f' : α → E'} {g' : α → F'} {l : Filter α} : 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} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {l : Filter α} {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} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {l : Filter α} {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] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {c : ℝ} {f : α → E} {g' : α → F'} (k' : α → G') {l : Filter α} (h : Asymptotics.IsBigOWith c l f g') (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] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {f : α → E} {g' : α → F'} (k' : α → G') {l : Filter α} (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] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {f : α → E} {g' : α → F'} (k' : α → G') {l : Filter α} (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] [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {c : ℝ} {f : α → E} (f' : α → E') {g' : α → F'} {l : Filter α} (h : Asymptotics.IsBigOWith c l f g') (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] [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f : α → E} (f' : α → E') {g' : α → F'} {l : Filter α} (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] [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f : α → E} (f' : α → E') {g' : α → F'} {l : Filter α} (h : f =o[l] g') : f =o[l] fun (x : α) => (f' x, g' x)

theorem Asymptotics.IsBigO.fiberwise_right {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : Filter α} {f : α × β → E} {g : α × β → F} {l' : Filter β} : f =O[l ×ˢ l'] g → ∀ᶠ (a : α) in l, (fun (x : β) => f (a, x)) =O[l'] fun (x : β) => g (a, x)

theorem Asymptotics.IsBigO.fiberwise_left {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {l : Filter α} {f : α × β → E} {g : α × β → F} {l' : Filter β} : f =O[l ×ˢ l'] g → ∀ᶠ (b : β) in l', (fun (x : α) => f (x, b)) =O[l] fun (x : α) => g (x, b)

theorem Asymptotics.IsBigO.comp_fst {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : α → E} {g : α → F} {l : Filter α} (l' : Filter β) : f =O[l] g → (f ∘ Prod.fst) =O[l ×ˢ l'] (g ∘ Prod.fst)

theorem Asymptotics.IsBigO.comp_snd {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : α → E} {g : α → F} {l : Filter α} (l' : Filter β) : f =O[l] g → (f ∘ Prod.snd) =O[l' ×ˢ l] (g ∘ Prod.snd)

theorem Asymptotics.IsLittleO.comp_fst {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : α → E} {g : α → F} {l : Filter α} (l' : Filter β) : f =o[l] g → (f ∘ Prod.fst) =o[l ×ˢ l'] (g ∘ Prod.fst)

theorem Asymptotics.IsLittleO.comp_snd {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : α → E} {g : α → F} {l : Filter α} (l' : Filter β) : f =o[l] g → (f ∘ Prod.snd) =o[l' ×ˢ l] (g ∘ Prod.snd)

theorem Asymptotics.IsBigOWith.prod_left_same {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {c : ℝ} {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : Filter α} (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} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {c : ℝ} {c' : ℝ} {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : Filter α} (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} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {c : ℝ} {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : Filter α} (h : Asymptotics.IsBigOWith c l (fun (x : α) => (f' x, g' x)) k') : Asymptotics.IsBigOWith c l f' k'

theorem Asymptotics.IsBigOWith.prod_left_snd {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {c : ℝ} {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : Filter α} (h : Asymptotics.IsBigOWith c l (fun (x : α) => (f' x, g' x)) k') : Asymptotics.IsBigOWith c l g' k'

theorem Asymptotics.isBigOWith_prod_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {c : ℝ} {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : Filter α} : 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} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : Filter α} (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} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : Filter α} : (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} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : Filter α} : (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} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : Filter α} : (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} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : Filter α} (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} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : Filter α} : (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} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : Filter α} : (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} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedAddCommGroup G'] {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : Filter α} : (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} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {c : ℝ} {f'' : α → E''} {g'' : α → F''} {l : Filter α} (h : Asymptotics.IsBigOWith c l f'' g'') : ∀ᶠ (x : α) in l, g'' x = 0 → f'' x = 0

theorem Asymptotics.IsBigO.eq_zero_imp {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {f'' : α → E''} {g'' : α → F''} {l : Filter α} (h : f'' =O[l] g'') : ∀ᶠ (x : α) in l, g'' x = 0 → f'' x = 0

Addition and subtraction

theorem Asymptotics.IsBigOWith.add {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {c₁ : ℝ} {c₂ : ℝ} {g : α → F} {l : Filter α} {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] [SeminormedAddCommGroup E'] {g : α → F} {l : Filter α} {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] [SeminormedAddCommGroup E'] {g : α → F} {l : Filter α} {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} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {l : Filter α} {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] [SeminormedAddCommGroup E'] {g : α → F} {l : Filter α} {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] [SeminormedAddCommGroup E'] {g : α → F} {l : Filter α} {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] [SeminormedAddCommGroup E'] {c₁ : ℝ} {c₂ : ℝ} {g : α → F} {l : Filter α} {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] [SeminormedAddCommGroup E'] {c₁ : ℝ} {c₂ : ℝ} {g : α → F} {l : Filter α} {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] [SeminormedAddCommGroup E'] {c₁ : ℝ} {c₂ : ℝ} {g : α → F} {l : Filter α} {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] [SeminormedAddCommGroup E'] {c₁ : ℝ} {c₂ : ℝ} {g : α → F} {l : Filter α} {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] [SeminormedAddCommGroup E'] {g : α → F} {l : Filter α} {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] [SeminormedAddCommGroup E'] {g : α → F} {l : Filter α} {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] [SeminormedAddCommGroup E'] {c : ℝ} {g : α → F} {l : Filter α} {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] [SeminormedAddCommGroup E'] {c : ℝ} {g : α → F} {l : Filter α} {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] [SeminormedAddCommGroup E'] {g : α → F} {l : Filter α} {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] [SeminormedAddCommGroup E'] {g : α → F} {l : Filter α} {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] [SeminormedAddCommGroup E'] {g : α → F} {l : Filter α} {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] [SeminormedAddCommGroup E'] {g : α → F} {l : Filter α} {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] [SeminormedAddCommGroup E'] {c : ℝ} {c' : ℝ} {g : α → F} {l : Filter α} {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] [SeminormedAddCommGroup E'] {g : α → F} {l : Filter α} {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] [SeminormedAddCommGroup E'] {g : α → F} {l : Filter α} {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] [SeminormedAddCommGroup E'] {g : α → F} {l : Filter α} {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] [SeminormedAddCommGroup E'] {g : α → F} {l : Filter α} {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} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] (g' : α → F') (l : Filter α) : (fun (_x : α) => 0) =o[l] g'

theorem Asymptotics.isBigOWith_zero {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {c : ℝ} (g' : α → F') (l : Filter α) (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] [SeminormedAddCommGroup E'] (g : α → F) (l : Filter α) : 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] [SeminormedAddCommGroup E'] (g : α → F) (l : Filter α) : (fun (_x : α) => 0) =O[l] g

theorem Asymptotics.isBigO_refl_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f' : α → E'} (g' : α → F') (l : Filter α) : (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} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {f' : α → E'} (g' : α → F') (l : Filter α) : (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} [SeminormedAddCommGroup F'] [NormedAddCommGroup E''] {c : ℝ} {f'' : α → E''} {l : Filter α} : (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} [SeminormedAddCommGroup F'] [NormedAddCommGroup E''] {f'' : α → E''} {l : Filter α} : (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} [SeminormedAddCommGroup F'] [NormedAddCommGroup E''] {f'' : α → E''} {l : Filter α} : (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] [NormedAddCommGroup F''] (c : E) {c' : F''} (hc' : c' ≠ 0) (l : Filter α) : 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] [NormedAddCommGroup F''] (c : E) {c' : F''} (hc' : c' ≠ 0) (l : Filter α) : (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} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {c : E''} {c' : F''} (l : Filter α) [l.NeBot] : ((fun (_x : α) => c) =O[l] fun (_x : α) => c') ↔ c' = 0 → c = 0

@[simp]

theorem Asymptotics.isBigO_pure {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {f'' : α → E''} {g'' : α → F''} {x : α} : f'' =O[pure x] g'' ↔ g'' x = 0 → f'' 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 α} : Asymptotics.IsBigOWith c (Filter.principal s) f g ↔ ∀ x ∈ s, ‖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 α} : f =O[Filter.principal s] g ↔ ∃ (c : ℝ), ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖

@[simp]

theorem Asymptotics.isLittleO_principal {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} [SeminormedAddCommGroup F'] [NormedAddCommGroup E''] {g' : α → F'} {f'' : α → E''} {s : Set α} : f'' =o[Filter.principal s] g' ↔ ∀ x ∈ s, 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} : Asymptotics.IsBigOWith c ⊤ f g ↔ ∀ (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} [SeminormedAddCommGroup F'] [NormedAddCommGroup E''] {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] [NormOneClass F] (c : E) (l : Filter α) : 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] [NormOneClass F] (c : E) (l : Filter α) : (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] [NormedAddCommGroup F''] {f : α → E} {l : Filter α} [One F] [NormOneClass 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] [SeminormedAddCommGroup E'] {f' : α → E'} {l : Filter α} [One F] [NormOneClass 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 : Filter α} [One F] [NormOneClass F] : (f =O[l] fun (_x : α) => 1) ↔ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) 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 : Filter α} [One F] [NormOneClass F] : (Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) 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 : Filter α} [One F] [NormOneClass 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] [SeminormedAddCommGroup E'] {f' : α → E'} {l : Filter α} [One F] [NormOneClass 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] [SeminormedAddCommGroup F'] {f : α → E} {g' : α → F'} {l : Filter α} [One F] [NormOneClass 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] [NormOneClass F] [TopologicalSpace α] {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} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {f'' : α → E''} {l : Filter α} {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} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {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] [NormedAddCommGroup F''] {f : α → E} {l : Filter α} (h : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) 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} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {f'' : α → E''} {l : Filter α} {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 : Filter α} {c : F} (h : f =O[l] fun (_x : α) => c) : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l (norm ∘ f)

theorem Asymptotics.isBigO_const_of_ne {α : Type u_1} {E : Type u_3} {F'' : Type u_10} [Norm E] [NormedAddCommGroup F''] {f : α → E} {l : Filter α} {c : F''} (hc : c ≠ 0) : (f =O[l] fun (_x : α) => c) ↔ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l (norm ∘ f)

theorem Asymptotics.isBigO_const_iff {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {f'' : α → E''} {l : Filter α} {c : F''} : (f'' =O[l] fun (_x : α) => c) ↔ (c = 0 → f'' =ᶠ[l] 0) ∧ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) 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] [NormedAddCommGroup F''] {f : α → E} {g'' : α → F''} {l : Filter α} (h : ∀ᶠ (x : α) in l, g'' x ≠ 0) : f =O[l] g'' ↔ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) 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} [SeminormedAddCommGroup E'] [NormedAddCommGroup E''] {f' : α → E'} {l : Filter α} {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} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {f'' : α → E''} {g'' : α → F''} {l : Filter α} (hfg : f'' =O[l] g'') (hg : Filter.Tendsto g'' l (nhds 0)) : Filter.Tendsto f'' l (nhds 0)

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

theorem Asymptotics.isLittleO_id_one {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] [One F''] [NeZero 1] : (fun (x : E'') => x) =o[nhds 0] 1

Multiplication by a constant

theorem Asymptotics.isBigOWith_const_mul_self {α : Type u_1} {R : Type u_13} [SeminormedRing R] (c : R) (f : α → R) (l : Filter α) : Asymptotics.IsBigOWith ‖c‖ l (fun (x : α) => c * f x) f

theorem Asymptotics.isBigO_const_mul_self {α : Type u_1} {R : Type u_13} [SeminormedRing R] (c : R) (f : α → R) (l : Filter α) : (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] [SeminormedRing R] {c : ℝ} {g : α → F} {l : Filter α} {f : α → R} (h : Asymptotics.IsBigOWith c l f g) (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] [SeminormedRing R] {g : α → F} {l : Filter α} {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} [SeminormedRing R] (u : Rˣ) (f : α → R) (l : Filter α) : Asymptotics.IsBigOWith ‖↑u⁻¹‖ l f fun (x : α) => ↑u * f x

theorem Asymptotics.isBigOWith_self_const_mul {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] (c : 𝕜) (hc : c ≠ 0) (f : α → 𝕜) (l : Filter α) : Asymptotics.IsBigOWith ‖c‖⁻¹ l f fun (x : α) => c * f x

theorem Asymptotics.isBigO_self_const_mul' {α : Type u_1} {R : Type u_13} [SeminormedRing R] {c : R} (hc : IsUnit c) (f : α → R) (l : Filter α) : f =O[l] fun (x : α) => c * f x

theorem Asymptotics.isBigO_self_const_mul {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] (c : 𝕜) (hc : c ≠ 0) (f : α → 𝕜) (l : Filter α) : 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] [SeminormedRing R] {g : α → F} {l : Filter α} {f : α → R} {c : R} (hc : IsUnit c) : (fun (x : α) => c * f x) =O[l] g ↔ f =O[l] g

theorem Asymptotics.isBigO_const_mul_left_iff {α : Type u_1} {F : Type u_4} {𝕜 : Type u_15} [Norm F] [NormedDivisionRing 𝕜] {g : α → F} {l : Filter α} {f : α → 𝕜} {c : 𝕜} (hc : c ≠ 0) : (fun (x : α) => c * f x) =O[l] g ↔ f =O[l] g

theorem Asymptotics.IsLittleO.const_mul_left {α : Type u_1} {F : Type u_4} {R : Type u_13} [Norm F] [SeminormedRing R] {g : α → F} {l : Filter α} {f : α → R} (h : f =o[l] g) (c : R) : (fun (x : α) => c * f x) =o[l] g

theorem Asymptotics.isLittleO_const_mul_left_iff' {α : Type u_1} {F : Type u_4} {R : Type u_13} [Norm F] [SeminormedRing R] {g : α → F} {l : Filter α} {f : α → R} {c : R} (hc : IsUnit c) : (fun (x : α) => c * f x) =o[l] g ↔ f =o[l] g

theorem Asymptotics.isLittleO_const_mul_left_iff {α : Type u_1} {F : Type u_4} {𝕜 : Type u_15} [Norm F] [NormedDivisionRing 𝕜] {g : α → F} {l : Filter α} {f : α → 𝕜} {c : 𝕜} (hc : c ≠ 0) : (fun (x : α) => c * f x) =o[l] g ↔ f =o[l] g

theorem Asymptotics.IsBigOWith.of_const_mul_right {α : Type u_1} {E : Type u_3} {R : Type u_13} [Norm E] [SeminormedRing R] {c' : ℝ} {f : α → E} {l : Filter α} {g : α → R} {c : R} (hc' : 0 ≤ c') (h : Asymptotics.IsBigOWith c' l f fun (x : α) => c * g x) : Asymptotics.IsBigOWith (c' * ‖c‖) l f g

theorem Asymptotics.IsBigO.of_const_mul_right {α : Type u_1} {E : Type u_3} {R : Type u_13} [Norm E] [SeminormedRing R] {f : α → E} {l : Filter α} {g : α → R} {c : R} (h : f =O[l] fun (x : α) => c * g x) : f =O[l] g

theorem Asymptotics.IsBigOWith.const_mul_right' {α : Type u_1} {E : Type u_3} {R : Type u_13} [Norm E] [SeminormedRing R] {f : α → E} {l : Filter α} {g : α → R} {u : Rˣ} {c' : ℝ} (hc' : 0 ≤ c') (h : Asymptotics.IsBigOWith c' l f g) : Asymptotics.IsBigOWith (c' * ‖↑u⁻¹‖) l f fun (x : α) => ↑u * g x

theorem Asymptotics.IsBigOWith.const_mul_right {α : Type u_1} {E : Type u_3} {𝕜 : Type u_15} [Norm E] [NormedDivisionRing 𝕜] {f : α → E} {l : Filter α} {g : α → 𝕜} {c : 𝕜} (hc : c ≠ 0) {c' : ℝ} (hc' : 0 ≤ c') (h : Asymptotics.IsBigOWith c' l f g) : Asymptotics.IsBigOWith (c' * ‖c‖⁻¹) l f fun (x : α) => c * g x

theorem Asymptotics.IsBigO.const_mul_right' {α : Type u_1} {E : Type u_3} {R : Type u_13} [Norm E] [SeminormedRing R] {f : α → E} {l : Filter α} {g : α → R} {c : R} (hc : IsUnit c) (h : f =O[l] g) : f =O[l] fun (x : α) => c * g x

theorem Asymptotics.IsBigO.const_mul_right {α : Type u_1} {E : Type u_3} {𝕜 : Type u_15} [Norm E] [NormedDivisionRing 𝕜] {f : α → E} {l : Filter α} {g : α → 𝕜} {c : 𝕜} (hc : c ≠ 0) (h : f =O[l] g) : f =O[l] fun (x : α) => c * g x

theorem Asymptotics.isBigO_const_mul_right_iff' {α : Type u_1} {E : Type u_3} {R : Type u_13} [Norm E] [SeminormedRing R] {f : α → E} {l : Filter α} {g : α → R} {c : R} (hc : IsUnit c) : (f =O[l] fun (x : α) => c * g x) ↔ f =O[l] g

theorem Asymptotics.isBigO_const_mul_right_iff {α : Type u_1} {E : Type u_3} {𝕜 : Type u_15} [Norm E] [NormedDivisionRing 𝕜] {f : α → E} {l : Filter α} {g : α → 𝕜} {c : 𝕜} (hc : c ≠ 0) : (f =O[l] fun (x : α) => c * g x) ↔ f =O[l] g

theorem Asymptotics.IsLittleO.of_const_mul_right {α : Type u_1} {E : Type u_3} {R : Type u_13} [Norm E] [SeminormedRing R] {f : α → E} {l : Filter α} {g : α → R} {c : R} (h : f =o[l] fun (x : α) => c * g x) : f =o[l] g

theorem Asymptotics.IsLittleO.const_mul_right' {α : Type u_1} {E : Type u_3} {R : Type u_13} [Norm E] [SeminormedRing R] {f : α → E} {l : Filter α} {g : α → R} {c : R} (hc : IsUnit c) (h : f =o[l] g) : f =o[l] fun (x : α) => c * g x

theorem Asymptotics.IsLittleO.const_mul_right {α : Type u_1} {E : Type u_3} {𝕜 : Type u_15} [Norm E] [NormedDivisionRing 𝕜] {f : α → E} {l : Filter α} {g : α → 𝕜} {c : 𝕜} (hc : c ≠ 0) (h : f =o[l] g) : f =o[l] fun (x : α) => c * g x

theorem Asymptotics.isLittleO_const_mul_right_iff' {α : Type u_1} {E : Type u_3} {R : Type u_13} [Norm E] [SeminormedRing R] {f : α → E} {l : Filter α} {g : α → R} {c : R} (hc : IsUnit c) : (f =o[l] fun (x : α) => c * g x) ↔ f =o[l] g

theorem Asymptotics.isLittleO_const_mul_right_iff {α : Type u_1} {E : Type u_3} {𝕜 : Type u_15} [Norm E] [NormedDivisionRing 𝕜] {f : α → E} {l : Filter α} {g : α → 𝕜} {c : 𝕜} (hc : c ≠ 0) : (f =o[l] fun (x : α) => c * g x) ↔ f =o[l] g

Multiplication

theorem Asymptotics.IsBigOWith.mul {α : Type u_1} {R : Type u_13} {𝕜 : Type u_15} [SeminormedRing R] [NormedDivisionRing 𝕜] {l : Filter α} {f₁ : α → R} {f₂ : α → R} {g₁ : α → 𝕜} {g₂ : α → 𝕜} {c₁ : ℝ} {c₂ : ℝ} (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) fun (x : α) => g₁ x * g₂ x

theorem Asymptotics.IsBigO.mul {α : Type u_1} {R : Type u_13} {𝕜 : Type u_15} [SeminormedRing R] [NormedDivisionRing 𝕜] {l : Filter α} {f₁ : α → R} {f₂ : α → R} {g₁ : α → 𝕜} {g₂ : α → 𝕜} (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.mul_isLittleO {α : Type u_1} {R : Type u_13} {𝕜 : Type u_15} [SeminormedRing R] [NormedDivisionRing 𝕜] {l : Filter α} {f₁ : α → R} {f₂ : α → R} {g₁ : α → 𝕜} {g₂ : α → 𝕜} (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.IsLittleO.mul_isBigO {α : Type u_1} {R : Type u_13} {𝕜 : Type u_15} [SeminormedRing R] [NormedDivisionRing 𝕜] {l : Filter α} {f₁ : α → R} {f₂ : α → R} {g₁ : α → 𝕜} {g₂ : α → 𝕜} (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.IsLittleO.mul {α : Type u_1} {R : Type u_13} {𝕜 : Type u_15} [SeminormedRing R] [NormedDivisionRing 𝕜] {l : Filter α} {f₁ : α → R} {f₂ : α → R} {g₁ : α → 𝕜} {g₂ : α → 𝕜} (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.IsBigOWith.pow' {α : Type u_1} {R : Type u_13} {𝕜 : Type u_15} [SeminormedRing R] [NormedDivisionRing 𝕜] {c : ℝ} {l : Filter α} {f : α → R} {g : α → 𝕜} (h : Asymptotics.IsBigOWith c l f g) (n : ℕ) : Asymptotics.IsBigOWith (Nat.casesOn n ‖1‖ fun (n : ℕ) => c ^ (n + 1)) l (fun (x : α) => f x ^ n) fun (x : α) => g x ^ n

theorem Asymptotics.IsBigOWith.pow {α : Type u_1} {R : Type u_13} {𝕜 : Type u_15} [SeminormedRing R] [NormedDivisionRing 𝕜] {c : ℝ} {l : Filter α} [NormOneClass R] {f : α → R} {g : α → 𝕜} (h : Asymptotics.IsBigOWith c l f g) (n : ℕ) : Asymptotics.IsBigOWith (c ^ n) l (fun (x : α) => f x ^ n) fun (x : α) => g x ^ n

theorem Asymptotics.IsBigOWith.of_pow {α : Type u_1} {R : Type u_13} {𝕜 : Type u_15} [SeminormedRing R] [NormedDivisionRing 𝕜] {c : ℝ} {c' : ℝ} {l : Filter α} {n : ℕ} {f : α → 𝕜} {g : α → R} (h : Asymptotics.IsBigOWith c l (f ^ n) (g ^ n)) (hn : n ≠ 0) (hc : c ≤ c' ^ n) (hc' : 0 ≤ c') : Asymptotics.IsBigOWith c' l f g

theorem Asymptotics.IsBigO.pow {α : Type u_1} {R : Type u_13} {𝕜 : Type u_15} [SeminormedRing R] [NormedDivisionRing 𝕜] {l : Filter α} {f : α → R} {g : α → 𝕜} (h : f =O[l] g) (n : ℕ) : (fun (x : α) => f x ^ n) =O[l] fun (x : α) => g x ^ n

theorem Asymptotics.IsBigO.of_pow {α : Type u_1} {R : Type u_13} {𝕜 : Type u_15} [SeminormedRing R] [NormedDivisionRing 𝕜] {l : Filter α} {f : α → 𝕜} {g : α → R} {n : ℕ} (hn : n ≠ 0) (h : (f ^ n) =O[l] (g ^ n)) : f =O[l] g

theorem Asymptotics.IsLittleO.pow {α : Type u_1} {R : Type u_13} {𝕜 : Type u_15} [SeminormedRing R] [NormedDivisionRing 𝕜] {l : Filter α} {f : α → R} {g : α → 𝕜} (h : f =o[l] g) {n : ℕ} (hn : 0 < n) : (fun (x : α) => f x ^ n) =o[l] fun (x : α) => g x ^ n

theorem Asymptotics.IsLittleO.of_pow {α : Type u_1} {R : Type u_13} {𝕜 : Type u_15} [SeminormedRing R] [NormedDivisionRing 𝕜] {l : Filter α} {f : α → 𝕜} {g : α → R} {n : ℕ} (h : (f ^ n) =o[l] (g ^ n)) (hn : n ≠ 0) : f =o[l] g

Inverse

theorem Asymptotics.IsBigOWith.inv_rev {α : Type u_1} {𝕜 : Type u_15} {𝕜' : Type u_16} [NormedDivisionRing 𝕜] [NormedDivisionRing 𝕜'] {c : ℝ} {l : Filter α} {f : α → 𝕜} {g : α → 𝕜'} (h : Asymptotics.IsBigOWith c l f g) (h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0) : Asymptotics.IsBigOWith c l (fun (x : α) => (g x)⁻¹) fun (x : α) => (f x)⁻¹

theorem Asymptotics.IsBigO.inv_rev {α : Type u_1} {𝕜 : Type u_15} {𝕜' : Type u_16} [NormedDivisionRing 𝕜] [NormedDivisionRing 𝕜'] {l : Filter α} {f : α → 𝕜} {g : α → 𝕜'} (h : f =O[l] g) (h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0) : (fun (x : α) => (g x)⁻¹) =O[l] fun (x : α) => (f x)⁻¹

theorem Asymptotics.IsLittleO.inv_rev {α : Type u_1} {𝕜 : Type u_15} {𝕜' : Type u_16} [NormedDivisionRing 𝕜] [NormedDivisionRing 𝕜'] {l : Filter α} {f : α → 𝕜} {g : α → 𝕜'} (h : f =o[l] g) (h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0) : (fun (x : α) => (g x)⁻¹) =o[l] fun (x : α) => (f x)⁻¹

Scalar multiplication

theorem Asymptotics.IsBigOWith.const_smul_self {α : Type u_1} {E' : Type u_6} {R : Type u_13} [SeminormedAddCommGroup E'] [SeminormedRing R] {f' : α → E'} {l : Filter α} [Module R E'] [BoundedSMul R E'] (c' : R) : Asymptotics.IsBigOWith ‖c'‖ l (fun (x : α) => c' • f' x) f'

theorem Asymptotics.IsBigO.const_smul_self {α : Type u_1} {E' : Type u_6} {R : Type u_13} [SeminormedAddCommGroup E'] [SeminormedRing R] {f' : α → E'} {l : Filter α} [Module R E'] [BoundedSMul R E'] (c' : R) : (fun (x : α) => c' • f' x) =O[l] f'

theorem Asymptotics.IsBigOWith.const_smul_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} {R : Type u_13} [Norm F] [SeminormedAddCommGroup E'] [SeminormedRing R] {c : ℝ} {g : α → F} {f' : α → E'} {l : Filter α} [Module R E'] [BoundedSMul R E'] (h : Asymptotics.IsBigOWith c l f' g) (c' : R) : Asymptotics.IsBigOWith (‖c'‖ * c) l (fun (x : α) => c' • f' x) g

theorem Asymptotics.IsBigO.const_smul_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} {R : Type u_13} [Norm F] [SeminormedAddCommGroup E'] [SeminormedRing R] {g : α → F} {f' : α → E'} {l : Filter α} [Module R E'] [BoundedSMul R E'] (h : f' =O[l] g) (c : R) : (c • f') =O[l] g

theorem Asymptotics.IsLittleO.const_smul_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} {R : Type u_13} [Norm F] [SeminormedAddCommGroup E'] [SeminormedRing R] {g : α → F} {f' : α → E'} {l : Filter α} [Module R E'] [BoundedSMul R E'] (h : f' =o[l] g) (c : R) : (c • f') =o[l] g

theorem Asymptotics.isBigO_const_smul_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} {𝕜 : Type u_15} [Norm F] [SeminormedAddCommGroup E'] [NormedDivisionRing 𝕜] {g : α → F} {f' : α → E'} {l : Filter α} [Module 𝕜 E'] [BoundedSMul 𝕜 E'] {c : 𝕜} (hc : c ≠ 0) : (fun (x : α) => c • f' x) =O[l] g ↔ f' =O[l] g

theorem Asymptotics.isLittleO_const_smul_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} {𝕜 : Type u_15} [Norm F] [SeminormedAddCommGroup E'] [NormedDivisionRing 𝕜] {g : α → F} {f' : α → E'} {l : Filter α} [Module 𝕜 E'] [BoundedSMul 𝕜 E'] {c : 𝕜} (hc : c ≠ 0) : (fun (x : α) => c • f' x) =o[l] g ↔ f' =o[l] g

theorem Asymptotics.isBigO_const_smul_right {α : Type u_1} {E : Type u_3} {E' : Type u_6} {𝕜 : Type u_15} [Norm E] [SeminormedAddCommGroup E'] [NormedDivisionRing 𝕜] {f : α → E} {f' : α → E'} {l : Filter α} [Module 𝕜 E'] [BoundedSMul 𝕜 E'] {c : 𝕜} (hc : c ≠ 0) : (f =O[l] fun (x : α) => c • f' x) ↔ f =O[l] f'

theorem Asymptotics.isLittleO_const_smul_right {α : Type u_1} {E : Type u_3} {E' : Type u_6} {𝕜 : Type u_15} [Norm E] [SeminormedAddCommGroup E'] [NormedDivisionRing 𝕜] {f : α → E} {f' : α → E'} {l : Filter α} [Module 𝕜 E'] [BoundedSMul 𝕜 E'] {c : 𝕜} (hc : c ≠ 0) : (f =o[l] fun (x : α) => c • f' x) ↔ f =o[l] f'

theorem Asymptotics.IsBigOWith.smul {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {R : Type u_13} {𝕜' : Type u_16} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedRing R] [NormedDivisionRing 𝕜'] {c : ℝ} {c' : ℝ} {f' : α → E'} {g' : α → F'} {l : Filter α} [Module R E'] [BoundedSMul R E'] [Module 𝕜' F'] [BoundedSMul 𝕜' F'] {k₁ : α → R} {k₂ : α → 𝕜'} (h₁ : Asymptotics.IsBigOWith c l k₁ k₂) (h₂ : Asymptotics.IsBigOWith c' l f' g') : Asymptotics.IsBigOWith (c * c') l (fun (x : α) => k₁ x • f' x) fun (x : α) => k₂ x • g' x

theorem Asymptotics.IsBigO.smul {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {R : Type u_13} {𝕜' : Type u_16} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedRing R] [NormedDivisionRing 𝕜'] {f' : α → E'} {g' : α → F'} {l : Filter α} [Module R E'] [BoundedSMul R E'] [Module 𝕜' F'] [BoundedSMul 𝕜' F'] {k₁ : α → R} {k₂ : α → 𝕜'} (h₁ : k₁ =O[l] k₂) (h₂ : f' =O[l] g') : (fun (x : α) => k₁ x • f' x) =O[l] fun (x : α) => k₂ x • g' x

theorem Asymptotics.IsBigO.smul_isLittleO {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {R : Type u_13} {𝕜' : Type u_16} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedRing R] [NormedDivisionRing 𝕜'] {f' : α → E'} {g' : α → F'} {l : Filter α} [Module R E'] [BoundedSMul R E'] [Module 𝕜' F'] [BoundedSMul 𝕜' F'] {k₁ : α → R} {k₂ : α → 𝕜'} (h₁ : k₁ =O[l] k₂) (h₂ : f' =o[l] g') : (fun (x : α) => k₁ x • f' x) =o[l] fun (x : α) => k₂ x • g' x

theorem Asymptotics.IsLittleO.smul_isBigO {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {R : Type u_13} {𝕜' : Type u_16} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedRing R] [NormedDivisionRing 𝕜'] {f' : α → E'} {g' : α → F'} {l : Filter α} [Module R E'] [BoundedSMul R E'] [Module 𝕜' F'] [BoundedSMul 𝕜' F'] {k₁ : α → R} {k₂ : α → 𝕜'} (h₁ : k₁ =o[l] k₂) (h₂ : f' =O[l] g') : (fun (x : α) => k₁ x • f' x) =o[l] fun (x : α) => k₂ x • g' x

theorem Asymptotics.IsLittleO.smul {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {R : Type u_13} {𝕜' : Type u_16} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] [SeminormedRing R] [NormedDivisionRing 𝕜'] {f' : α → E'} {g' : α → F'} {l : Filter α} [Module R E'] [BoundedSMul R E'] [Module 𝕜' F'] [BoundedSMul 𝕜' F'] {k₁ : α → R} {k₂ : α → 𝕜'} (h₁ : k₁ =o[l] k₂) (h₂ : f' =o[l] g') : (fun (x : α) => k₁ x • f' x) =o[l] fun (x : α) => k₂ x • g' x

Sum

theorem Asymptotics.IsBigOWith.sum {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : α → F} {l : Filter α} {ι : Type u_17} {A : ι → α → E'} {C : ι → ℝ} {s : Finset ι} (h : ∀ i ∈ s, Asymptotics.IsBigOWith (C i) l (A i) g) : Asymptotics.IsBigOWith (∑ i ∈ s, C i) l (fun (x : α) => ∑ i ∈ s, A i x) g

theorem Asymptotics.IsBigO.sum {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : α → F} {l : Filter α} {ι : Type u_17} {A : ι → α → E'} {s : Finset ι} (h : ∀ i ∈ s, A i =O[l] g) : (fun (x : α) => ∑ i ∈ s, A i x) =O[l] g

theorem Asymptotics.IsLittleO.sum {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [SeminormedAddCommGroup E'] [SeminormedAddCommGroup F'] {g' : α → F'} {l : Filter α} {ι : Type u_17} {A : ι → α → E'} {s : Finset ι} (h : ∀ i ∈ s, A i =o[l] g') : (fun (x : α) => ∑ i ∈ s, A i x) =o[l] g'

Relation between f = o(g) and f / g → 0

theorem Asymptotics.IsLittleO.tendsto_div_nhds_zero {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {l : Filter α} {f : α → 𝕜} {g : α → 𝕜} (h : f =o[l] g) : Filter.Tendsto (fun (x : α) => f x / g x) l (nhds 0)

theorem Asymptotics.IsLittleO.tendsto_inv_smul_nhds_zero {α : Type u_1} {E' : Type u_6} {𝕜 : Type u_15} [SeminormedAddCommGroup E'] [NormedDivisionRing 𝕜] [Module 𝕜 E'] [BoundedSMul 𝕜 E'] {f : α → E'} {g : α → 𝕜} {l : Filter α} (h : f =o[l] g) : Filter.Tendsto (fun (x : α) => (g x)⁻¹ • f x) l (nhds 0)

theorem Asymptotics.isLittleO_iff_tendsto' {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {l : Filter α} {f : α → 𝕜} {g : α → 𝕜} (hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0) : f =o[l] g ↔ Filter.Tendsto (fun (x : α) => f x / g x) l (nhds 0)

theorem Asymptotics.isLittleO_iff_tendsto {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {l : Filter α} {f : α → 𝕜} {g : α → 𝕜} (hgf : ∀ (x : α), g x = 0 → f x = 0) : f =o[l] g ↔ Filter.Tendsto (fun (x : α) => f x / g x) l (nhds 0)

theorem Asymptotics.isLittleO_of_tendsto' {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {l : Filter α} {f : α → 𝕜} {g : α → 𝕜} (hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0) : Filter.Tendsto (fun (x : α) => f x / g x) l (nhds 0) → f =o[l] g

Alias of the reverse direction of Asymptotics.isLittleO_iff_tendsto'.

theorem Asymptotics.isLittleO_of_tendsto {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {l : Filter α} {f : α → 𝕜} {g : α → 𝕜} (hgf : ∀ (x : α), g x = 0 → f x = 0) : Filter.Tendsto (fun (x : α) => f x / g x) l (nhds 0) → f =o[l] g

Alias of the reverse direction of Asymptotics.isLittleO_iff_tendsto.

theorem Asymptotics.isLittleO_const_left_of_ne {α : Type u_1} {F : Type u_4} {E'' : Type u_9} [Norm F] [NormedAddCommGroup E''] {g : α → F} {l : Filter α} {c : E''} (hc : c ≠ 0) : (fun (_x : α) => c) =o[l] g ↔ Filter.Tendsto (fun (x : α) => ‖g x‖) l Filter.atTop

@[simp]

theorem Asymptotics.isLittleO_const_left {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {g'' : α → F''} {l : Filter α} {c : E''} : (fun (_x : α) => c) =o[l] g'' ↔ c = 0 ∨ Filter.Tendsto (norm ∘ g'') l Filter.atTop

@[simp]

theorem Asymptotics.isLittleO_const_const_iff {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {l : Filter α} [l.NeBot] {d : E''} {c : F''} : ((fun (_x : α) => d) =o[l] fun (_x : α) => c) ↔ d = 0

@[simp]

theorem Asymptotics.isLittleO_pure {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {f'' : α → E''} {g'' : α → F''} {x : α} : f'' =o[pure x] g'' ↔ f'' x = 0

theorem Asymptotics.isLittleO_const_id_cobounded {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] (c : F'') : (fun (x : E'') => c) =o[Bornology.cobounded E''] id

theorem Asymptotics.isLittleO_const_id_atTop {E'' : Type u_9} [NormedAddCommGroup E''] (c : E'') : (fun (_x : ℝ) => c) =o[Filter.atTop] id

theorem Asymptotics.isLittleO_const_id_atBot {E'' : Type u_9} [NormedAddCommGroup E''] (c : E'') : (fun (_x : ℝ) => c) =o[Filter.atBot] id

Eventually (u / v) * v = u

If u and v are linked by an IsBigOWith relation, then we eventually have (u / v) * v = u, even if v vanishes.

theorem Asymptotics.IsBigOWith.eventually_mul_div_cancel {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {c : ℝ} {l : Filter α} {u : α → 𝕜} {v : α → 𝕜} (h : Asymptotics.IsBigOWith c l u v) : u / v * v =ᶠ[l] u

theorem Asymptotics.IsBigO.eventually_mul_div_cancel {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {l : Filter α} {u : α → 𝕜} {v : α → 𝕜} (h : u =O[l] v) : u / v * v =ᶠ[l] u

If u = O(v) along l, then (u / v) * v = u eventually at l.

theorem Asymptotics.IsLittleO.eventually_mul_div_cancel {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {l : Filter α} {u : α → 𝕜} {v : α → 𝕜} (h : u =o[l] v) : u / v * v =ᶠ[l] u

If u = o(v) along l, then (u / v) * v = u eventually at l.

Equivalent definitions of the form ∃ φ, u =ᶠ[l] φ * v in a NormedField.

theorem Asymptotics.isBigOWith_of_eq_mul {α : Type u_1} {R : Type u_13} [SeminormedRing R] {c : ℝ} {l : Filter α} {u : α → R} {v : α → R} (φ : α → R) (hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) (h : u =ᶠ[l] φ * v) : Asymptotics.IsBigOWith c l u v

If ‖φ‖ is eventually bounded by c, and u =ᶠ[l] φ * v, then we have IsBigOWith c u v l. This does not require any assumptions on c, which is why we keep this version along with IsBigOWith_iff_exists_eq_mul.

theorem Asymptotics.isBigOWith_iff_exists_eq_mul {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {c : ℝ} {l : Filter α} {u : α → 𝕜} {v : α → 𝕜} (hc : 0 ≤ c) : Asymptotics.IsBigOWith c l u v ↔ ∃ (φ : α → 𝕜), (∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v

theorem Asymptotics.IsBigOWith.exists_eq_mul {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {c : ℝ} {l : Filter α} {u : α → 𝕜} {v : α → 𝕜} (h : Asymptotics.IsBigOWith c l u v) (hc : 0 ≤ c) : ∃ (φ : α → 𝕜), (∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v

theorem Asymptotics.isBigO_iff_exists_eq_mul {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {l : Filter α} {u : α → 𝕜} {v : α → 𝕜} : u =O[l] v ↔ ∃ (φ : α → 𝕜), Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v

theorem Asymptotics.IsBigO.exists_eq_mul {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {l : Filter α} {u : α → 𝕜} {v : α → 𝕜} : u =O[l] v → ∃ (φ : α → 𝕜), Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v

Alias of the forward direction of Asymptotics.isBigO_iff_exists_eq_mul.

theorem Asymptotics.isLittleO_iff_exists_eq_mul {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {l : Filter α} {u : α → 𝕜} {v : α → 𝕜} : u =o[l] v ↔ ∃ (φ : α → 𝕜), Filter.Tendsto φ l (nhds 0) ∧ u =ᶠ[l] φ * v

theorem Asymptotics.IsLittleO.exists_eq_mul {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {l : Filter α} {u : α → 𝕜} {v : α → 𝕜} : u =o[l] v → ∃ (φ : α → 𝕜), Filter.Tendsto φ l (nhds 0) ∧ u =ᶠ[l] φ * v

Alias of the forward direction of Asymptotics.isLittleO_iff_exists_eq_mul.

Miscellaneous lemmas

theorem Asymptotics.div_isBoundedUnder_of_isBigO {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {α : Type u_17} {l : Filter α} {f : α → 𝕜} {g : α → 𝕜} (h : f =O[l] g) : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l fun (x : α) => ‖f x / g x‖

theorem Asymptotics.isBigO_iff_div_isBoundedUnder {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {α : Type u_17} {l : Filter α} {f : α → 𝕜} {g : α → 𝕜} (hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0) : f =O[l] g ↔ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l fun (x : α) => ‖f x / g x‖

theorem Asymptotics.isBigO_of_div_tendsto_nhds {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {α : Type u_17} {l : Filter α} {f : α → 𝕜} {g : α → 𝕜} (hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0) (c : 𝕜) (H : Filter.Tendsto (f / g) l (nhds c)) : f =O[l] g

theorem Asymptotics.IsLittleO.tendsto_zero_of_tendsto {α : Type u_17} {E : Type u_18} {𝕜 : Type u_19} [NormedAddCommGroup E] [NormedField 𝕜] {u : α → E} {v : α → 𝕜} {l : Filter α} {y : 𝕜} (huv : u =o[l] v) (hv : Filter.Tendsto v l (nhds y)) : Filter.Tendsto u l (nhds 0)

theorem Asymptotics.isLittleO_pow_pow {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {m : ℕ} {n : ℕ} (h : m < n) : (fun (x : 𝕜) => x ^ n) =o[nhds 0] fun (x : 𝕜) => x ^ m

theorem Asymptotics.isLittleO_norm_pow_norm_pow {E' : Type u_6} [SeminormedAddCommGroup E'] {m : ℕ} {n : ℕ} (h : m < n) : (fun (x : E') => ‖x‖ ^ n) =o[nhds 0] fun (x : E') => ‖x‖ ^ m

theorem Asymptotics.isLittleO_pow_id {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {n : ℕ} (h : 1 < n) : (fun (x : 𝕜) => x ^ n) =o[nhds 0] fun (x : 𝕜) => x

theorem Asymptotics.isLittleO_norm_pow_id {E' : Type u_6} [SeminormedAddCommGroup E'] {n : ℕ} (h : 1 < n) : (fun (x : E') => ‖x‖ ^ n) =o[nhds 0] fun (x : E') => x

theorem Asymptotics.IsBigO.eq_zero_of_norm_pow_within {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {f : E'' → F''} {s : Set E''} {x₀ : E''} {n : ℕ} (h : f =O[nhdsWithin x₀ s] fun (x : E'') => ‖x - x₀‖ ^ n) (hx₀ : x₀ ∈ s) (hn : n ≠ 0) : f x₀ = 0

theorem Asymptotics.IsBigO.eq_zero_of_norm_pow {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {f : E'' → F''} {x₀ : E''} {n : ℕ} (h : f =O[nhds x₀] fun (x : E'') => ‖x - x₀‖ ^ n) (hn : n ≠ 0) : f x₀ = 0

theorem Asymptotics.isLittleO_pow_sub_pow_sub {E' : Type u_6} [SeminormedAddCommGroup E'] (x₀ : E') {n : ℕ} {m : ℕ} (h : n < m) : (fun (x : E') => ‖x - x₀‖ ^ m) =o[nhds x₀] fun (x : E') => ‖x - x₀‖ ^ n

theorem Asymptotics.isLittleO_pow_sub_sub {E' : Type u_6} [SeminormedAddCommGroup E'] (x₀ : E') {m : ℕ} (h : 1 < m) : (fun (x : E') => ‖x - x₀‖ ^ m) =o[nhds x₀] fun (x : E') => x - x₀

theorem Asymptotics.IsBigOWith.right_le_sub_of_lt_one {α : Type u_1} {E' : Type u_6} [SeminormedAddCommGroup E'] {c : ℝ} {l : Filter α} {f₁ : α → E'} {f₂ : α → E'} (h : Asymptotics.IsBigOWith c l f₁ f₂) (hc : c < 1) : Asymptotics.IsBigOWith (1 / (1 - c)) l f₂ fun (x : α) => f₂ x - f₁ x

theorem Asymptotics.IsBigOWith.right_le_add_of_lt_one {α : Type u_1} {E' : Type u_6} [SeminormedAddCommGroup E'] {c : ℝ} {l : Filter α} {f₁ : α → E'} {f₂ : α → E'} (h : Asymptotics.IsBigOWith c l f₁ f₂) (hc : c < 1) : Asymptotics.IsBigOWith (1 / (1 - c)) l f₂ fun (x : α) => f₁ x + f₂ x

@[deprecated Asymptotics.IsBigOWith.right_le_sub_of_lt_one]

theorem Asymptotics.IsBigOWith.right_le_sub_of_lt_1 {α : Type u_1} {E' : Type u_6} [SeminormedAddCommGroup E'] {c : ℝ} {l : Filter α} {f₁ : α → E'} {f₂ : α → E'} (h : Asymptotics.IsBigOWith c l f₁ f₂) (hc : c < 1) : Asymptotics.IsBigOWith (1 / (1 - c)) l f₂ fun (x : α) => f₂ x - f₁ x

Alias of Asymptotics.IsBigOWith.right_le_sub_of_lt_one.

@[deprecated Asymptotics.IsBigOWith.right_le_add_of_lt_one]

theorem Asymptotics.IsBigOWith.right_le_add_of_lt_1 {α : Type u_1} {E' : Type u_6} [SeminormedAddCommGroup E'] {c : ℝ} {l : Filter α} {f₁ : α → E'} {f₂ : α → E'} (h : Asymptotics.IsBigOWith c l f₁ f₂) (hc : c < 1) : Asymptotics.IsBigOWith (1 / (1 - c)) l f₂ fun (x : α) => f₁ x + f₂ x

Alias of Asymptotics.IsBigOWith.right_le_add_of_lt_one.

theorem Asymptotics.IsLittleO.right_isBigO_sub {α : Type u_1} {E' : Type u_6} [SeminormedAddCommGroup E'] {l : Filter α} {f₁ : α → E'} {f₂ : α → E'} (h : f₁ =o[l] f₂) : f₂ =O[l] fun (x : α) => f₂ x - f₁ x

theorem Asymptotics.IsLittleO.right_isBigO_add {α : Type u_1} {E' : Type u_6} [SeminormedAddCommGroup E'] {l : Filter α} {f₁ : α → E'} {f₂ : α → E'} (h : f₁ =o[l] f₂) : f₂ =O[l] fun (x : α) => f₁ x + f₂ x

theorem Asymptotics.IsLittleO.right_isBigO_add' {α : Type u_1} {E' : Type u_6} [SeminormedAddCommGroup E'] {l : Filter α} {f₁ : α → E'} {f₂ : α → E'} (h : f₁ =o[l] f₂) : f₂ =O[l] (f₂ + f₁)

theorem Asymptotics.bound_of_isBigO_cofinite {α : Type u_1} {E : Type u_3} {F'' : Type u_10} [Norm E] [NormedAddCommGroup F''] {f : α → E} {g'' : α → F''} (h : f =O[Filter.cofinite] g'') : ∃ C > 0, ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖

If f x = O(g x) along cofinite, then there exists a positive constant C such that ‖f x‖ ≤ C * ‖g x‖ whenever g x ≠ 0.

theorem Asymptotics.isBigO_cofinite_iff {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {f'' : α → E''} {g'' : α → F''} (h : ∀ (x : α), g'' x = 0 → f'' x = 0) : f'' =O[Filter.cofinite] g'' ↔ ∃ (C : ℝ), ∀ (x : α), ‖f'' x‖ ≤ C * ‖g'' x‖

theorem Asymptotics.bound_of_isBigO_nat_atTop {E : Type u_3} {E'' : Type u_9} [Norm E] [NormedAddCommGroup E''] {f : ℕ → E} {g'' : ℕ → E''} (h : f =O[Filter.atTop] g'') : ∃ C > 0, ∀ ⦃x : ℕ⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖

theorem Asymptotics.isBigO_nat_atTop_iff {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] {f : ℕ → E''} {g : ℕ → F''} (h : ∀ (x : ℕ), g x = 0 → f x = 0) : f =O[Filter.atTop] g ↔ ∃ (C : ℝ), ∀ (x : ℕ), ‖f x‖ ≤ C * ‖g x‖

theorem Asymptotics.isBigO_one_nat_atTop_iff {E'' : Type u_9} [NormedAddCommGroup E''] {f : ℕ → E''} : (f =O[Filter.atTop] fun (_n : ℕ) => 1) ↔ ∃ (C : ℝ), ∀ (n : ℕ), ‖f n‖ ≤ C

theorem Asymptotics.isBigOWith_pi {α : Type u_1} {F' : Type u_7} [SeminormedAddCommGroup F'] {g' : α → F'} {l : Filter α} {ι : Type u_17} [Fintype ι] {E' : ι → Type u_18} [(i : ι) → NormedAddCommGroup (E' i)] {f : α → (i : ι) → E' i} {C : ℝ} (hC : 0 ≤ C) : Asymptotics.IsBigOWith C l f g' ↔ ∀ (i : ι), Asymptotics.IsBigOWith C l (fun (x : α) => f x i) g'

@[simp]

theorem Asymptotics.isBigO_pi {α : Type u_1} {F' : Type u_7} [SeminormedAddCommGroup F'] {g' : α → F'} {l : Filter α} {ι : Type u_17} [Fintype ι] {E' : ι → Type u_18} [(i : ι) → NormedAddCommGroup (E' i)] {f : α → (i : ι) → E' i} : f =O[l] g' ↔ ∀ (i : ι), (fun (x : α) => f x i) =O[l] g'

@[simp]

theorem Asymptotics.isLittleO_pi {α : Type u_1} {F' : Type u_7} [SeminormedAddCommGroup F'] {g' : α → F'} {l : Filter α} {ι : Type u_17} [Fintype ι] {E' : ι → Type u_18} [(i : ι) → NormedAddCommGroup (E' i)] {f : α → (i : ι) → E' i} : f =o[l] g' ↔ ∀ (i : ι), (fun (x : α) => f x i) =o[l] g'

theorem Asymptotics.IsBigO.natCast_atTop {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {R : Type u_17} [StrictOrderedSemiring R] [Archimedean R] {f : R → E} {g : R → F} (h : f =O[Filter.atTop] g) : (fun (n : ℕ) => f ↑n) =O[Filter.atTop] fun (n : ℕ) => g ↑n

@[deprecated Asymptotics.IsBigO.natCast_atTop]

theorem Asymptotics.IsBigO.nat_cast_atTop {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {R : Type u_17} [StrictOrderedSemiring R] [Archimedean R] {f : R → E} {g : R → F} (h : f =O[Filter.atTop] g) : (fun (n : ℕ) => f ↑n) =O[Filter.atTop] fun (n : ℕ) => g ↑n

Alias of Asymptotics.IsBigO.natCast_atTop.

theorem Asymptotics.IsLittleO.natCast_atTop {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {R : Type u_17} [StrictOrderedSemiring R] [Archimedean R] {f : R → E} {g : R → F} (h : f =o[Filter.atTop] g) : (fun (n : ℕ) => f ↑n) =o[Filter.atTop] fun (n : ℕ) => g ↑n

@[deprecated Asymptotics.IsLittleO.natCast_atTop]

theorem Asymptotics.IsLittleO.nat_cast_atTop {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {R : Type u_17} [StrictOrderedSemiring R] [Archimedean R] {f : R → E} {g : R → F} (h : f =o[Filter.atTop] g) : (fun (n : ℕ) => f ↑n) =o[Filter.atTop] fun (n : ℕ) => g ↑n

Alias of Asymptotics.IsLittleO.natCast_atTop.

theorem Asymptotics.isBigO_atTop_iff_eventually_exists {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {α : Type u_17} [SemilatticeSup α] [Nonempty α] {f : α → E} {g : α → F} : f =O[Filter.atTop] g ↔ ∀ᶠ (n₀ : α) in Filter.atTop, ∃ (c : ℝ), ∀ n ≥ n₀, ‖f n‖ ≤ c * ‖g n‖

theorem Asymptotics.isBigO_atTop_iff_eventually_exists_pos {G : Type u_5} {G' : Type u_8} [Norm G] [SeminormedAddCommGroup G'] {α : Type u_17} [SemilatticeSup α] [Nonempty α] {f : α → G} {g : α → G'} : f =O[Filter.atTop] g ↔ ∀ᶠ (n₀ : α) in Filter.atTop, ∃ c > 0, ∀ n ≥ n₀, c * ‖f n‖ ≤ ‖g n‖

theorem Asymptotics.isBigO_mul_iff_isBigO_div {α : Type u_1} {𝕜 : Type u_15} [NormedDivisionRing 𝕜] {l : Filter α} {f : α → 𝕜} {g : α → 𝕜} {h : α → 𝕜} (hf : ∀ᶠ (x : α) in l, f x ≠ 0) : (fun (x : α) => f x * g x) =O[l] h ↔ g =O[l] fun (x : α) => h x / f x

theorem summable_of_isBigO {ι : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] [CompleteSpace E] {f : ι → E} {g : ι → ℝ} (hg : Summable g) (h : f =O[Filter.cofinite] g) : Summable f

theorem summable_of_isBigO_nat {E : Type u_1} [SeminormedAddCommGroup E] [CompleteSpace E] {f : ℕ → E} {g : ℕ → ℝ} (hg : Summable g) (h : f =O[Filter.atTop] g) : Summable f

theorem Asymptotics.IsBigO.comp_summable_norm {ι : Type u_1} {E : Type u_2} {F : Type u_3} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] {f : E → F} {g : ι → E} (hf : f =O[nhds 0] id) (hg : Summable fun (x : ι) => ‖g x‖) : Summable fun (x : ι) => ‖f (g x)‖

theorem PartialHomeomorph.isBigOWith_congr {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {E : Type u_3} [Norm E] {F : Type u_4} [Norm F] (e : PartialHomeomorph α β) {b : β} (hb : b ∈ e.target) {f : β → E} {g : β → F} {C : ℝ} : Asymptotics.IsBigOWith C (nhds b) f g ↔ Asymptotics.IsBigOWith C (nhds (↑e.symm b)) (f ∘ ↑e) (g ∘ ↑e)

Transfer IsBigOWith over a PartialHomeomorph.

theorem PartialHomeomorph.isBigO_congr {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {E : Type u_3} [Norm E] {F : Type u_4} [Norm F] (e : PartialHomeomorph α β) {b : β} (hb : b ∈ e.target) {f : β → E} {g : β → F} : f =O[nhds b] g ↔ (f ∘ ↑e) =O[nhds (↑e.symm b)] (g ∘ ↑e)

Transfer IsBigO over a PartialHomeomorph.

theorem PartialHomeomorph.isLittleO_congr {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {E : Type u_3} [Norm E] {F : Type u_4} [Norm F] (e : PartialHomeomorph α β) {b : β} (hb : b ∈ e.target) {f : β → E} {g : β → F} : f =o[nhds b] g ↔ (f ∘ ↑e) =o[nhds (↑e.symm b)] (g ∘ ↑e)

Transfer IsLittleO over a PartialHomeomorph.

theorem Homeomorph.isBigOWith_congr {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {E : Type u_3} [Norm E] {F : Type u_4} [Norm F] (e : α ≃ₜ β) {b : β} {f : β → E} {g : β → F} {C : ℝ} : Asymptotics.IsBigOWith C (nhds b) f g ↔ Asymptotics.IsBigOWith C (nhds (e.symm b)) (f ∘ ⇑e) (g ∘ ⇑e)

Transfer IsBigOWith over a Homeomorph.

theorem Homeomorph.isBigO_congr {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {E : Type u_3} [Norm E] {F : Type u_4} [Norm F] (e : α ≃ₜ β) {b : β} {f : β → E} {g : β → F} : f =O[nhds b] g ↔ (f ∘ ⇑e) =O[nhds (e.symm b)] (g ∘ ⇑e)

Transfer IsBigO over a Homeomorph.

theorem Homeomorph.isLittleO_congr {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {E : Type u_3} [Norm E] {F : Type u_4} [Norm F] (e : α ≃ₜ β) {b : β} {f : β → E} {g : β → F} : f =o[nhds b] g ↔ (f ∘ ⇑e) =o[nhds (e.symm b)] (g ∘ ⇑e)

Transfer IsLittleO over a Homeomorph.

theorem ContinuousOn.isBigOWith_principal {α : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace α] {s : Set α} {f : α → E} {c : F} [SeminormedAddGroup E] [Norm F] (hf : ContinuousOn f s) (hs : IsCompact s) (hc : ‖c‖ ≠ 0) : Asymptotics.IsBigOWith (sSup (norm '' (f '' s)) / ‖c‖) (Filter.principal s) f fun (x : α) => c

theorem ContinuousOn.isBigO_principal {α : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace α] {s : Set α} {f : α → E} {c : F} [SeminormedAddGroup E] [Norm F] (hf : ContinuousOn f s) (hs : IsCompact s) (hc : ‖c‖ ≠ 0) : f =O[Filter.principal s] fun (x : α) => c

theorem ContinuousOn.isBigOWith_rev_principal {α : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace α] {s : Set α} {f : α → E} [NormedAddGroup E] [SeminormedAddGroup F] (hf : ContinuousOn f s) (hs : IsCompact s) (hC : ∀ i ∈ s, f i ≠ 0) (c : F) : Asymptotics.IsBigOWith (‖c‖ / sInf (norm '' (f '' s))) (Filter.principal s) (fun (x : α) => c) f

theorem ContinuousOn.isBigO_rev_principal {α : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace α] {s : Set α} {f : α → E} [NormedAddGroup E] [SeminormedAddGroup F] (hf : ContinuousOn f s) (hs : IsCompact s) (hC : ∀ i ∈ s, f i ≠ 0) (c : F) : (fun (x : α) => c) =O[Filter.principal s] f

theorem NormedField.tendsto_zero_smul_of_tendsto_zero_of_bounded {ι : Type u_1} {𝕜 : Type u_2} {𝔸 : Type u_3} [NormedDivisionRing 𝕜] [NormedAddCommGroup 𝔸] [Module 𝕜 𝔸] [BoundedSMul 𝕜 𝔸] {l : Filter ι} {ε : ι → 𝕜} {f : ι → 𝔸} (hε : Filter.Tendsto ε l (nhds 0)) (hf : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l (norm ∘ f)) : Filter.Tendsto (ε • f) l (nhds 0)

The (scalar) product of a sequence that tends to zero with a bounded one also tends to zero.