# 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 is that there is a norm associated with these types, and it is the norm that is compared asymptotically.

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

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

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

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

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

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

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

### Definitions #

source
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‖
source
@[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‖

Instances For

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

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

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

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

Instances For

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

Instances For

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

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

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

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

source
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
source
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
source
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‖
source
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`.

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

Instances For

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

Instances For

source
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`.

source
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`.

source
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`.

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

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

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

source
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‖
source
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
source
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 #

source
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
source
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
source
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
source
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
source
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'
source
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'
source
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'
source
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'
source
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'
source
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`.

source
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`.

source
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‖
source
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‖
source
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‖
source
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‖
source
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 #

source
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'
source
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 #

source
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₂
source
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₂
source
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₂
source
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
source
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₂
source
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
source
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₂
source
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₂
source
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₂
source
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
source
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₂
source
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₂
source
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₂
source
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₂
source
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
source
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₂
source
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
source
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 := ⋯ }

source
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
source
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 := ⋯ }

source
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₂
source
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 := ⋯ }

source
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₂
source
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 #

source
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)
source
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)
source
theorem Asymptotics.IsBigO.comp_neg_int {E : Type u_3} {F : Type u_4} [Norm E] [Norm F] {f : ℤ → E} {g : ℤ → F} (hf : f =O[Filter.cofinite] g) :
(fun (n : ℤ) => f (-n)) =O[Filter.cofinite] fun (n : ℤ) => g (-n)
source
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)
source
@[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)
source
@[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)
source
@[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)
source
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
source
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
source
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
source
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
source
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
source
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 := ⋯ }

source
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
source
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
source
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 := ⋯ }

source
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
source
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
source
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 := ⋯ }

source
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
source
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 := ⋯ }

source
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
source
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`.

source
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
source
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
source
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
source
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
source
theorem Asymptotics.isBigOWith_refl {α : Type u_1} {E : Type u_3} [Norm E] (f : α → E) (l : Filter α) :
IsBigOWith 1 l f f
source
theorem Asymptotics.isBigO_refl {α : Type u_1} {E : Type u_3} [Norm E] (f : α → E) (l : Filter α) :
f =O[l] f
source
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₂
source
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
source
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
source
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
source
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'
source
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''
source
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''
source
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''
source
@[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
source
@[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
source
@[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
source
@[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‖
source
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
source
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'
source
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'
source
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
source
@[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'
source
@[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
source
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'
source
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'
source
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'
source
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 #

source
@[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'
source
@[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
source
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`.

source
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`.

source
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`.

source
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`.

source
@[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'
source
@[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
source
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`.

source
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`.

source
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`.

source
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`.

source
@[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'
source
@[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
source
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`.

source
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`.

source
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`.

source
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`.

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

source
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`.

source
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`.

source
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`.

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

source
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`.

source
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`.

source
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`.

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

source
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`.

source
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`.

source
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`.

source
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'
source
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
source
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`.

source
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`.

source
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`.

source
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`.

source
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'
source
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
source
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`.

source
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`.

source
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`.

source
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`.

source
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'
source
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
source
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`.

source
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`.

source
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`.

source
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 #

source
@[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'
source
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`.

source
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`.

source
@[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'
source
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`.

source
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`.

source
@[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'
source
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`.

source
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`.

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

source
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`.

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

source
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`.

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

source
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) #

source
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)
source
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)
source
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)
source
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)
source
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'
source
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'
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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'
source
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'
source
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'
source
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'
source
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'
source
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'
source
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'
source
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'
source
@[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'
source
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'
source
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'
source
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'
source
@[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'
source
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
source
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 #

source
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
source
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
source
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
source
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‖
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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 #

source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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 #

source
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'
source
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'
source
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
source
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
source
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'
source
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'
source
@[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
source
@[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
source
@[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
source
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'
source
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'
source
@[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
source
@[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 #

source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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 #

source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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 #

source
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)⁻¹
source
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)⁻¹
source
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 #

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

source
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
source
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`.

source
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`.