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_18} {E : Type u_19} {F : Type u_20} [Norm E] [Norm F] (c : ℝ) (l : Filter α) (f : α → E) (g : α → F) : IsBigOWith c l f g = ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

@[irreducible]

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

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

Equations

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

theorem Asymptotics.isBigOWith_iff {α : Type u_1} {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {c : ℝ} {f : α → E} {g : α → F} {l : Filter α} : 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 α} : 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‖) → 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_18} {E : Type u_19} {F : Type u_20} [Norm E] [Norm F] (l : Filter α) (f : α → E) (g : α → F) : Prop

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

Equations

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

theorem Asymptotics.IsBigO_def {α : Type u_18} {E : Type u_19} {F : Type u_20} [Norm E] [Norm F] (l : Filter α) (f : α → E) (g : α → F) : f =O[l] g = ∃ (c : ℝ), 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 : ℝ), 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.IsBigO.of_norm_eventuallyLE {α : Type u_1} {E : Type u_3} [Norm E] {f : α → E} {l : Filter α} {g : α → ℝ} (h : (fun (x : α) => ‖f x‖) ≤ᶠ[l] g) : f =O[l] g

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

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

@[irreducible]

def Asymptotics.IsLittleO {α : Type u_18} {E : Type u_19} {F : Type u_20} [Norm E] [Norm F] (l : Filter α) (f : α → E) (g : α → F) : Prop

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

Equations

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

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

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

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

Equations

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

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

Definition of IsLittleO in terms of IsBigOWith.

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

Alias of the forward direction of Asymptotics.isLittleO_iff_forall_isBigOWith.

---

Definition of IsLittleO in terms of IsBigOWith.

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

Alias of the reverse direction of Asymptotics.isLittleO_iff_forall_isBigOWith.

---

Definition of IsLittleO in terms of IsBigOWith.

theorem Asymptotics.isLittleO_iff {α : Type u_1} {E : Type u_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) : 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 : 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) : 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 : ℝ), 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 : IsBigOWith c l f g') (hc : c ≤ c') : 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 : IsBigOWith c l f g') : ∃ c' > 0, 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, 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 : IsBigOWith c l f g') : ∃ c' ≥ 0, 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, 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, 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_18} {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) : 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₁ f₂ : α → E} {g₁ g₂ : α → F} (hc : c₁ = c₂) (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) : IsBigOWith c₁ l f₁ g₁ ↔ 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₁ f₂ : α → E} {g₁ g₂ : α → F} (h : IsBigOWith c₁ l f₁ g₁) (hc : c₁ = c₂) (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) : 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₁ f₂ : α → E} {g₁ g₂ : α → F} (h : IsBigOWith c₁ l f₁ g₁) (hc : c₁ = c₂) (hf : ∀ (x : α), f₁ x = f₂ x) (hg : ∀ (x : α), g₁ x = g₂ x) : 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₁ f₂ : α → E} (h : IsBigOWith c l f₁ g) (hf : ∀ (x : α), f₁ x = f₂ x) : 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₁ g₂ : α → F} (h : IsBigOWith c l f g₁) (hg : ∀ (x : α), g₁ x = g₂ x) : 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 : IsBigOWith c₁ l f g) (hc : c₁ = c₂) : 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₁ f₂ : α → E} {g₁ 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₁ f₂ : α → E} {g₁ 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₁ f₂ : α → E} {g₁ 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₁ 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₁ 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₁ f₂ : α → E} {g₁ 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₁ f₂ : α → E} {g₁ 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₁ f₂ : α → E} {g₁ 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₁ 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₁ 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₁ 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₁ 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₁ 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₁ 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 : IsBigOWith c l f g) {k : β → α} {l' : Filter β} (hk : Filter.Tendsto k l' l) : 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 β} : IsBigOWith c (Filter.map k l) f g ↔ 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 l' : Filter α} (h : IsBigOWith c l' f g) (hl : l ≤ l') : 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 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 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 : IsBigOWith c l f g) (hgk : IsBigOWith c' l g k) (hc : 0 ≤ c) : 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 : 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 : 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

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

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‖) : 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‖) : 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 α) : 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₁ 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 : IsBigOWith c l f g) (hgk : ∀ (x : α), ‖g x‖ ≤ ‖k x‖) (hc : 0 ≤ c) : 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) : 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 : α} : 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 l' : Filter α} (h : IsBigOWith c l f g) (h' : IsBigOWith c l' f g) : 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 l' : Filter α} (h : IsBigOWith c l f g') (h' : IsBigOWith c' l' f g') : 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 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 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 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 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‖) : IsBigOWith C (nhdsWithin x (insert x s)) g g' ↔ 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 : IsBigOWith C (nhdsWithin x s) g g') (h2 : ‖g x‖ ≤ C * ‖g' x‖) : 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 α} : (IsBigOWith c l f fun (x : α) => ‖g' x‖) ↔ 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 : α → ℝ} : (IsBigOWith c l f fun (x : α) => |u x|) ↔ 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 α} : IsBigOWith c l f g' → 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 α} : (IsBigOWith c l f fun (x : α) => ‖g' x‖) → IsBigOWith c l f g'

Alias of the forward direction of Asymptotics.isBigOWith_norm_right.

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

Alias of the forward direction of Asymptotics.isBigOWith_abs_right.

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

Alias of the reverse direction of Asymptotics.isBigOWith_abs_right.

@[simp]

theorem Asymptotics.isBigO_norm_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] [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.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.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.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.

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.

@[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 α} : IsBigOWith c l (fun (x : α) => ‖f' x‖) g ↔ 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 : α → ℝ} : IsBigOWith c l (fun (x : α) => |u x|) g ↔ IsBigOWith c l u g

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 α} : IsBigOWith c l (fun (x : α) => ‖f' x‖) g → IsBigOWith c l f' g

Alias of the forward direction of Asymptotics.isBigOWith_norm_left.

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 α} : IsBigOWith c l f' g → IsBigOWith c l (fun (x : α) => ‖f' x‖) g

Alias of the reverse 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 : α → ℝ} : IsBigOWith c l (fun (x : α) => |u x|) g → 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 : α → ℝ} : IsBigOWith c l u g → 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.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_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.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 α} : (IsBigOWith c l (fun (x : α) => ‖f' x‖) fun (x : α) => ‖g' x‖) ↔ IsBigOWith c l f' g'

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

Alias of the reverse direction of Asymptotics.isBigOWith_norm_norm.

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

Alias of the reverse direction of Asymptotics.isBigOWith_abs_abs.

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

Alias of the forward 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.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.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.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.

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.

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 α} : (IsBigOWith c l f fun (x : α) => -g' x) ↔ IsBigOWith c l f g'

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 α} : IsBigOWith c l f g' → IsBigOWith c l f fun (x : α) => -g' x

Alias of the reverse direction of Asymptotics.isBigOWith_neg_right.

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

Alias of the forward direction of Asymptotics.isBigOWith_neg_right.

@[simp]

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

theorem Asymptotics.IsBigO.of_neg_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] [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.

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.

@[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 α} : IsBigOWith c l (fun (x : α) => -f' x) g ↔ 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 α} : IsBigOWith c l f' g → 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 α} : IsBigOWith c l (fun (x : α) => -f' x) g → 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.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.

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.

@[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.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.

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.

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 α} : 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 α} : 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 : IsBigOWith c l f g') (hc : 0 ≤ c) : 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 : IsBigOWith c l f g') (hc : 0 ≤ c) : 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 : IsBigOWith c l f' k') (hg : IsBigOWith c l g' k') : 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 : IsBigOWith c l f' k') (hg : IsBigOWith c' l g' k') : 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 : IsBigOWith c l (fun (x : α) => (f' x, g' x)) k') : 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 : IsBigOWith c l (fun (x : α) => (f' x, g' x)) k') : 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 α} : IsBigOWith c l (fun (x : α) => (f' x, g' x)) k' ↔ IsBigOWith c l f' k' ∧ 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 : 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₁ f₂ : α → E'} (h₁ : IsBigOWith c₁ l f₁ g) (h₂ : IsBigOWith c₂ l f₂ g) : 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₁ 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₁ 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₁ f₂ : α → E'} {g₁ 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₁ 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₁ 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₁ f₂ : α → E'} (h₁ : IsBigOWith c₁ l f₁ g) (h₂ : f₂ =o[l] g) (hc : c₁ < c₂) : 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₁ f₂ : α → E'} (h₁ : f₁ =o[l] g) (h₂ : IsBigOWith c₁ l f₂ g) (hc : c₁ < c₂) : 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₁ f₂ : α → E'} (h₁ : IsBigOWith c₁ l f₁ g) (h₂ : IsBigOWith c₂ l f₂ g) : 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₁ f₂ : α → E'} (h₁ : IsBigOWith c₁ l f₁ g) (h₂ : f₂ =o[l] g) (hc : c₁ < c₂) : 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₁ 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₁ f₂ : α → E'} (h₁ : f₁ =o[l] g) (h₂ : f₂ =o[l] g) : (fun (x : α) => f₁ x - f₂ x) =o[l] g

theorem Asymptotics.IsBigO.add_iff_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : α → F} {l : Filter α} {f₁ f₂ : α → E'} (h₂ : f₂ =O[l] g) : (fun (x : α) => f₁ x + f₂ x) =O[l] g ↔ f₁ =O[l] g

theorem Asymptotics.IsBigO.add_iff_right {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : α → F} {l : Filter α} {f₁ f₂ : α → E'} (h₁ : f₁ =O[l] g) : (fun (x : α) => f₁ x + f₂ x) =O[l] g ↔ f₂ =O[l] g

theorem Asymptotics.IsLittleO.add_iff_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : α → F} {l : Filter α} {f₁ f₂ : α → E'} (h₂ : f₂ =o[l] g) : (fun (x : α) => f₁ x + f₂ x) =o[l] g ↔ f₁ =o[l] g

theorem Asymptotics.IsLittleO.add_iff_right {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : α → F} {l : Filter α} {f₁ f₂ : α → E'} (h₁ : f₁ =o[l] g) : (fun (x : α) => f₁ x + f₂ x) =o[l] g ↔ f₂ =o[l] g

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

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

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

theorem Asymptotics.IsLittleO.sub_iff_right {α : Type u_1} {F : Type u_4} {E' : Type u_6} [Norm F] [SeminormedAddCommGroup E'] {g : α → F} {l : Filter α} {f₁ f₂ : α → E'} (h₁ : f₁ =o[l] g) : (fun (x : α) => f₁ x - f₂ x) =o[l] g ↔ f₂ =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₁ f₂ : α → E'} (h : IsBigOWith c l (fun (x : α) => f₁ x - f₂ x) g) : 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₁ f₂ : α → E'} : IsBigOWith c l (fun (x : α) => f₁ x - f₂ x) g ↔ 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₁ 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₁ 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₁ 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₁ 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₁ f₂ f₃ : α → E'} (h₁ : IsBigOWith c l (fun (x : α) => f₁ x - f₂ x) g) (h₂ : IsBigOWith c' l (fun (x : α) => f₂ x - f₃ x) g) : 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₁ f₂ 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₁ f₂ 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₁ 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₁ 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) : 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 α) : 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 α} : (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 α) : 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

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 α) : 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 : IsBigOWith c l f g) (c' : R) : 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 α) : IsBigOWith ‖↑u⁻¹‖ l f fun (x : α) => ↑u * f x

theorem Asymptotics.isBigOWith_self_const_mul {α : Type u_1} {S : Type u_17} [NormedRing S] [NormMulClass S] {c : S} (hc : c ≠ 0) (f : α → S) (l : Filter α) : 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} {S : Type u_17} [NormedRing S] [NormMulClass S] {c : S} (hc : c ≠ 0) (f : α → S) (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} [Norm F] {S : Type u_17} [NormedRing S] [NormMulClass S] {g : α → F} {l : Filter α} {f : α → S} {c : S} (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} [Norm F] {S : Type u_17} [NormedRing S] [NormMulClass S] {g : α → F} {l : Filter α} {f : α → S} {c : S} (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 : IsBigOWith c' l f fun (x : α) => c * g x) : 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 : IsBigOWith c' l f g) : IsBigOWith (c' * ‖↑u⁻¹‖) l f fun (x : α) => ↑u * g x

theorem Asymptotics.IsBigOWith.const_mul_right {α : Type u_1} {E : Type u_3} [Norm E] {S : Type u_17} [NormedRing S] [NormMulClass S] {f : α → E} {l : Filter α} {g : α → S} {c : S} (hc : c ≠ 0) {c' : ℝ} (hc' : 0 ≤ c') (h : IsBigOWith c' l f g) : 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} [Norm E] {S : Type u_17} [NormedRing S] [NormMulClass S] {f : α → E} {l : Filter α} {g : α → S} {c : S} (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} [Norm E] {S : Type u_17} [NormedRing S] [NormMulClass S] {f : α → E} {l : Filter α} {g : α → S} {c : S} (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} [Norm E] {S : Type u_17} [NormedRing S] [NormMulClass S] {f : α → E} {l : Filter α} {g : α → S} {c : S} (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} [Norm E] {S : Type u_17} [NormedRing S] [NormMulClass S] {f : α → E} {l : Filter α} {g : α → S} {c : S} (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} [SeminormedRing R] {S : Type u_17} [NormedRing S] [NormMulClass S] {l : Filter α} {f₁ f₂ : α → R} {g₁ g₂ : α → S} {c₁ c₂ : ℝ} (h₁ : IsBigOWith c₁ l f₁ g₁) (h₂ : IsBigOWith c₂ l f₂ g₂) : 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} [SeminormedRing R] {S : Type u_17} [NormedRing S] [NormMulClass S] {l : Filter α} {f₁ f₂ : α → R} {g₁ g₂ : α → S} (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} [SeminormedRing R] {S : Type u_17} [NormedRing S] [NormMulClass S] {l : Filter α} {f₁ f₂ : α → R} {g₁ g₂ : α → S} (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} [SeminormedRing R] {S : Type u_17} [NormedRing S] [NormMulClass S] {l : Filter α} {f₁ f₂ : α → R} {g₁ g₂ : α → S} (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} [SeminormedRing R] {S : Type u_17} [NormedRing S] [NormMulClass S] {l : Filter α} {f₁ f₂ : α → R} {g₁ g₂ : α → S} (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} [SeminormedRing R] {S : Type u_17} [NormedRing S] [NormMulClass S] {c : ℝ} {l : Filter α} [NormOneClass S] {f : α → R} {g : α → S} (h : IsBigOWith c l f g) (n : ℕ) : 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} [SeminormedRing R] {S : Type u_17} [NormedRing S] [NormMulClass S] {c : ℝ} {l : Filter α} [NormOneClass R] [NormOneClass S] {f : α → R} {g : α → S} (h : IsBigOWith c l f g) (n : ℕ) : 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} [SeminormedRing R] {S : Type u_17} [NormedRing S] [NormMulClass S] {c c' : ℝ} {l : Filter α} [NormOneClass S] {n : ℕ} {f : α → S} {g : α → R} (h : IsBigOWith c l (f ^ n) (g ^ n)) (hn : n ≠ 0) (hc : c ≤ c' ^ n) (hc' : 0 ≤ c') : IsBigOWith c' l f g

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

theorem Asymptotics.IsLittleO.pow {α : Type u_1} {R : Type u_13} [SeminormedRing R] {S : Type u_17} [NormedRing S] [NormMulClass S] {l : Filter α} {f : α → R} {g : α → S} (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} [SeminormedRing R] {S : Type u_17} [NormedRing S] [NormMulClass S] {l : Filter α} [NormOneClass S] {f : α → S} {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 : IsBigOWith c l f g) (h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0) : 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)⁻¹

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_18} {A : ι → α → E'} {C : ι → ℝ} {s : Finset ι} (h : ∀ i ∈ s, IsBigOWith (C i) l (A i) g) : 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_18} {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_18} {A : ι → α → E'} {s : Finset ι} (h : ∀ i ∈ s, A i =o[l] g') : (fun (x : α) => ∑ i ∈ s, A i x) =o[l] g'

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