mathlibdocumentation

analysis.asymptotics

Asymptotics

We introduce these relations:

• `is_O_with c f g l` : "f is big O of g along l with constant c";
• `is_O f g l` : "f is big O of g along l";
• `is_o f g l` : "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 `is_O_with c` is introduced to factor out common algebraic arguments in the proofs of similar properties of `is_O` and `is_o`. Usually proofs outside of this file should use `is_O` 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

`is_O f g l ↔ is_O (λ x, ∥f x∥) (λ x, ∥g x∥) l`,

and similarly for `is_o`. 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

`is_o f g l ↔ tendsto (λ 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

def asymptotics.is_O_with {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] (c : ) (f : α → E) (g : α → F) (l : filter α) :
Prop

This version of the Landau notation `is_O_with C f g l` 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 `is_O` instead of this relation.

Equations
theorem asymptotics.is_O_with_iff {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {c : } {f : α → E} {g : α → F} {l : filter α} :
l ∀ᶠ (x : α) in l, f x c * g x

Definition of `is_O_with`. We record it in a lemma as we will set `is_O_with` to be irreducible at the end of this file.

theorem asymptotics.is_O_with.of_bound {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {c : } {f : α → E} {g : α → F} {l : filter α} (h : ∀ᶠ (x : α) in l, f x c * g x) :
l

def asymptotics.is_O {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] (f : α → E) (g : α → F) (l : filter α) :
Prop

The Landau notation `is_O f g l` 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
• l = ∃ (c : ), l
theorem asymptotics.is_O_iff_is_O_with {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f : α → E} {g : α → F} {l : filter α} :
l ∃ (c : ), l

Definition of `is_O` in terms of `is_O_with`. We record it in a lemma as we will set `is_O` to be irreducible at the end of this file.

theorem asymptotics.is_O_iff {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f : α → E} {g : α → F} {l : filter α} :
l ∃ (c : ), ∀ᶠ (x : α) in l, f x c * g x

Definition of `is_O` in terms of filters. We record it in a lemma as we will set `is_O` to be irreducible at the end of this file.

theorem asymptotics.is_O.of_bound {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] (c : ) {f : α → E} {g : α → F} {l : filter α} (h : ∀ᶠ (x : α) in l, f x c * g x) :
l

def asymptotics.is_o {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] (f : α → E) (g : α → F) (l : filter α) :
Prop

The Landau notation `is_o f g l` 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
• l = ∀ ⦃c : ⦄, 0 < c l
theorem asymptotics.is_o_iff_forall_is_O_with {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f : α → E} {g : α → F} {l : filter α} :
l ∀ ⦃c : ⦄, 0 < c l

Definition of `is_o` in terms of `is_O_with`. We record it in a lemma as we will set `is_o` to be irreducible at the end of this file.

theorem asymptotics.is_o_iff {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f : α → E} {g : α → F} {l : filter α} :
l ∀ ⦃c : ⦄, 0 < c(∀ᶠ (x : α) in l, f x c * g x)

Definition of `is_o` in terms of filters. We record it in a lemma as we will set `is_o` to be irreducible at the end of this file.

theorem asymptotics.is_o.def {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f : α → E} {g : α → F} {l : filter α} (h : l) {c : } (hc : 0 < c) :
∀ᶠ (x : α) in l, f x c * g x

theorem asymptotics.is_o.def' {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f : α → E} {g : α → F} {l : filter α} (h : l) {c : } (hc : 0 < c) :
l

Conversions

theorem asymptotics.is_O_with.is_O {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {c : } {f : α → E} {g : α → F} {l : filter α} (h : l) :
l

theorem asymptotics.is_o.is_O_with {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f : α → E} {g : α → F} {l : filter α} (hgf : l) :
l

theorem asymptotics.is_o.is_O {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f : α → E} {g : α → F} {l : filter α} (hgf : l) :
l

theorem asymptotics.is_O_with.weaken {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] [normed_group F'] {c c' : } {f : α → E} {g' : α → F'} {l : filter α} (h : g' l) (hc : c c') :
g' l

theorem asymptotics.is_O_with.exists_pos {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] [normed_group F'] {c : } {f : α → E} {g' : α → F'} {l : filter α} (h : g' l) :
∃ (c' : ) (H : 0 < c'), g' l

theorem asymptotics.is_O.exists_pos {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] [normed_group F'] {f : α → E} {g' : α → F'} {l : filter α} (h : g' l) :
∃ (c : ) (H : 0 < c), g' l

theorem asymptotics.is_O_with.exists_nonneg {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] [normed_group F'] {c : } {f : α → E} {g' : α → F'} {l : filter α} (h : g' l) :
∃ (c' : ) (H : 0 c'), g' l

theorem asymptotics.is_O.exists_nonneg {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] [normed_group F'] {f : α → E} {g' : α → F'} {l : filter α} (h : g' l) :
∃ (c : ) (H : 0 c), g' l

Subsingleton

theorem asymptotics.is_o_of_subsingleton {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] {f' : α → E'} {g' : α → F'} {l : filter α} [subsingleton E'] :
g' l

theorem asymptotics.is_O_of_subsingleton {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] {f' : α → E'} {g' : α → F'} {l : filter α} [subsingleton E'] :
g' l

Congruence

theorem asymptotics.is_O_with_congr {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {c₁ c₂ : } {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : filter α} (hc : c₁ = c₂) (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) :
g₁ l g₂ l

theorem asymptotics.is_O_with.congr' {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {c₁ c₂ : } {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : filter α} (hc : c₁ = c₂) (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) :
g₁ l g₂ l

theorem asymptotics.is_O_with.congr {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {c₁ c₂ : } {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : filter α} (hc : c₁ = c₂) (hf : ∀ (x : α), f₁ x = f₂ x) (hg : ∀ (x : α), g₁ x = g₂ x) :
g₁ l g₂ l

theorem asymptotics.is_O_with.congr_left {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {c : } {g : α → F} {f₁ f₂ : α → E} {l : filter α} (hf : ∀ (x : α), f₁ x = f₂ x) :
g l g l

theorem asymptotics.is_O_with.congr_right {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {c : } {f : α → E} {g₁ g₂ : α → F} {l : filter α} (hg : ∀ (x : α), g₁ x = g₂ x) :
g₁ l g₂ l

theorem asymptotics.is_O_with.congr_const {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f : α → E} {g : α → F} {c₁ c₂ : } {l : filter α} (hc : c₁ = c₂) :
g l g l

theorem asymptotics.is_O_congr {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : filter α} (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) :
g₁ l g₂ l

theorem asymptotics.is_O.congr' {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : filter α} (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) :
g₁ l g₂ l

theorem asymptotics.is_O.congr {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : filter α} (hf : ∀ (x : α), f₁ x = f₂ x) (hg : ∀ (x : α), g₁ x = g₂ x) :
g₁ l g₂ l

theorem asymptotics.is_O.congr_left {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {g : α → F} {f₁ f₂ : α → E} {l : filter α} (hf : ∀ (x : α), f₁ x = f₂ x) :
g l g l

theorem asymptotics.is_O.congr_right {α : Type u_1} {E : Type u_3} [has_norm E] {f g₁ g₂ : α → E} {l : filter α} (hg : ∀ (x : α), g₁ x = g₂ x) :
g₁ l g₂ l

theorem asymptotics.is_o_congr {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : filter α} (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) :
g₁ l g₂ l

theorem asymptotics.is_o.congr' {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : filter α} (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) :
g₁ l g₂ l

theorem asymptotics.is_o.congr {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : filter α} (hf : ∀ (x : α), f₁ x = f₂ x) (hg : ∀ (x : α), g₁ x = g₂ x) :
g₁ l g₂ l

theorem asymptotics.is_o.congr_left {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {g : α → F} {f₁ f₂ : α → E} {l : filter α} (hf : ∀ (x : α), f₁ x = f₂ x) :
g l g l

theorem asymptotics.is_o.congr_right {α : Type u_1} {E : Type u_3} [has_norm E] {f g₁ g₂ : α → E} {l : filter α} (hg : ∀ (x : α), g₁ x = g₂ x) :
g₁ l g₂ l

Filter operations and transitivity

theorem asymptotics.is_O_with.comp_tendsto {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {c : } {f : α → E} {g : α → F} {l : filter α} (hcfg : l) {k : β → α} {l' : filter β} (hk : l' l) :
(f k) (g k) l'

theorem asymptotics.is_O.comp_tendsto {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f : α → E} {g : α → F} {l : filter α} (hfg : l) {k : β → α} {l' : filter β} (hk : l' l) :
asymptotics.is_O (f k) (g k) l'

theorem asymptotics.is_o.comp_tendsto {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f : α → E} {g : α → F} {l : filter α} (hfg : l) {k : β → α} {l' : filter β} (hk : l' l) :
asymptotics.is_o (f k) (g k) l'

@[simp]
theorem asymptotics.is_O_with_map {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {c : } {f : α → E} {g : α → F} {k : β → α} {l : filter β} :
l) (f k) (g k) l

@[simp]
theorem asymptotics.is_O_map {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f : α → E} {g : α → F} {k : β → α} {l : filter β} :
l) asymptotics.is_O (f k) (g k) l

@[simp]
theorem asymptotics.is_o_map {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f : α → E} {g : α → F} {k : β → α} {l : filter β} :
l) asymptotics.is_o (f k) (g k) l

theorem asymptotics.is_O_with.mono {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {c : } {f : α → E} {g : α → F} {l l' : filter α} (h : l') (hl : l l') :
l

theorem asymptotics.is_O.mono {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f : α → E} {g : α → F} {l l' : filter α} (h : l') (hl : l l') :
l

theorem asymptotics.is_o.mono {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f : α → E} {g : α → F} {l l' : filter α} (h : l') (hl : l l') :
l

theorem asymptotics.is_O_with.trans {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [has_norm E] [has_norm F] [has_norm G] {c c' : } {f : α → E} {g : α → F} {k : α → G} {l : filter α} (hfg : l) (hgk : k l) (hc : 0 c) :

theorem asymptotics.is_O.trans {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [has_norm E] [has_norm G] [normed_group F'] {f : α → E} {k : α → G} {g' : α → F'} {l : filter α} (hfg : g' l) (hgk : k l) :
l

theorem asymptotics.is_o.trans_is_O_with {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [has_norm E] [has_norm F] [has_norm G] {c : } {f : α → E} {g : α → F} {k : α → G} {l : filter α} (hfg : l) (hgk : l) (hc : 0 < c) :
l

theorem asymptotics.is_o.trans_is_O {α : Type u_1} {E : Type u_3} {F : Type u_4} {G' : Type u_8} [has_norm E] [has_norm F] [normed_group G'] {f : α → E} {g : α → F} {k' : α → G'} {l : filter α} (hfg : l) (hgk : k' l) :
k' l

theorem asymptotics.is_O_with.trans_is_o {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [has_norm E] [has_norm F] [has_norm G] {c : } {f : α → E} {g : α → F} {k : α → G} {l : filter α} (hfg : l) (hgk : l) (hc : 0 < c) :
l

theorem asymptotics.is_O.trans_is_o {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [has_norm E] [has_norm G] [normed_group F'] {f : α → E} {k : α → G} {g' : α → F'} {l : filter α} (hfg : g' l) (hgk : k l) :
l

theorem asymptotics.is_o.trans {α : Type u_1} {E : Type u_3} {F : Type u_4} {G' : Type u_8} [has_norm E] [has_norm F] [normed_group G'] {f : α → E} {g : α → F} {k' : α → G'} {l : filter α} (hfg : l) (hgk : k' l) :
k' l

theorem asymptotics.is_o.trans' {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [has_norm E] [has_norm G] [normed_group F'] {f : α → E} {k : α → G} {g' : α → F'} {l : filter α} (hfg : g' l) (hgk : k l) :
l

theorem asymptotics.is_O_with_of_le' {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {c : } {f : α → E} {g : α → F} (l : filter α) (hfg : ∀ (x : α), f x c * g x) :
l

theorem asymptotics.is_O_with_of_le {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f : α → E} {g : α → F} (l : filter α) (hfg : ∀ (x : α), f x g x) :
l

theorem asymptotics.is_O_of_le' {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {c : } {f : α → E} {g : α → F} (l : filter α) (hfg : ∀ (x : α), f x c * g x) :
l

theorem asymptotics.is_O_of_le {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f : α → E} {g : α → F} (l : filter α) (hfg : ∀ (x : α), f x g x) :
l

theorem asymptotics.is_O_with_refl {α : Type u_1} {E : Type u_3} [has_norm E] (f : α → E) (l : filter α) :
l

theorem asymptotics.is_O_refl {α : Type u_1} {E : Type u_3} [has_norm E] (f : α → E) (l : filter α) :
l

theorem asymptotics.is_O_with.trans_le {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [has_norm E] [has_norm F] [has_norm G] {c : } {f : α → E} {g : α → F} {k : α → G} {l : filter α} (hfg : l) (hgk : ∀ (x : α), g x k x) (hc : 0 c) :
l

theorem asymptotics.is_O.trans_le {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [has_norm E] [has_norm G] [normed_group F'] {f : α → E} {k : α → G} {g' : α → F'} {l : filter α} (hfg : g' l) (hgk : ∀ (x : α), g' x k x) :
l

theorem asymptotics.is_o.trans_le {α : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [has_norm E] [has_norm F] [has_norm G] {f : α → E} {g : α → F} {k : α → G} {l : filter α} (hfg : l) (hgk : ∀ (x : α), g x k x) :
l

@[simp]
theorem asymptotics.is_O_with_bot {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] (c : ) (f : α → E) (g : α → F) :

@[simp]
theorem asymptotics.is_O_bot {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] (f : α → E) (g : α → F) :

@[simp]
theorem asymptotics.is_o_bot {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] (f : α → E) (g : α → F) :

theorem asymptotics.is_O_with.join {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {c : } {f : α → E} {g : α → F} {l l' : filter α} (h : l) (h' : l') :
(l l')

theorem asymptotics.is_O_with.join' {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] [normed_group F'] {c c' : } {f : α → E} {g' : α → F'} {l l' : filter α} (h : g' l) (h' : g' l') :
asymptotics.is_O_with (max c c') f g' (l l')

theorem asymptotics.is_O.join {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] [normed_group F'] {f : α → E} {g' : α → F'} {l l' : filter α} (h : g' l) (h' : g' l') :
g' (l l')

theorem asymptotics.is_o.join {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f : α → E} {g : α → F} {l l' : filter α} (h : l) (h' : l') :
(l l')

Simplification : norm

@[simp]
theorem asymptotics.is_O_with_norm_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] [normed_group F'] {c : } {f : α → E} {g' : α → F'} {l : filter α} :
(λ (x : α), g' x) l g' l

theorem asymptotics.is_O_with.norm_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] [normed_group F'] {c : } {f : α → E} {g' : α → F'} {l : filter α} :
g' l (λ (x : α), g' x) l

Alias of `is_O_with_norm_right`.

theorem asymptotics.is_O_with.of_norm_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] [normed_group F'] {c : } {f : α → E} {g' : α → F'} {l : filter α} :
(λ (x : α), g' x) l g' l

Alias of `is_O_with_norm_right`.

@[simp]
theorem asymptotics.is_O_norm_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] [normed_group F'] {f : α → E} {g' : α → F'} {l : filter α} :
(λ (x : α), g' x) l g' l

theorem asymptotics.is_O.norm_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] [normed_group F'] {f : α → E} {g' : α → F'} {l : filter α} :
g' l (λ (x : α), g' x) l

Alias of `is_O_norm_right`.

theorem asymptotics.is_O.of_norm_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] [normed_group F'] {f : α → E} {g' : α → F'} {l : filter α} :
(λ (x : α), g' x) l g' l

Alias of `is_O_norm_right`.

@[simp]
theorem asymptotics.is_o_norm_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] [normed_group F'] {f : α → E} {g' : α → F'} {l : filter α} :
(λ (x : α), g' x) l g' l

theorem asymptotics.is_o.norm_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] [normed_group F'] {f : α → E} {g' : α → F'} {l : filter α} :
g' l (λ (x : α), g' x) l

Alias of `is_o_norm_right`.

theorem asymptotics.is_o.of_norm_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] [normed_group F'] {f : α → E} {g' : α → F'} {l : filter α} :
(λ (x : α), g' x) l g' l

Alias of `is_o_norm_right`.

@[simp]
theorem asymptotics.is_O_with_norm_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {c : } {g : α → F} {f' : α → E'} {l : filter α} :
(λ (x : α), f' x) g l g l

theorem asymptotics.is_O_with.of_norm_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {c : } {g : α → F} {f' : α → E'} {l : filter α} :
(λ (x : α), f' x) g l g l

Alias of `is_O_with_norm_left`.

theorem asymptotics.is_O_with.norm_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {c : } {g : α → F} {f' : α → E'} {l : filter α} :
g l (λ (x : α), f' x) g l

Alias of `is_O_with_norm_left`.

@[simp]
theorem asymptotics.is_O_norm_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {g : α → F} {f' : α → E'} {l : filter α} :
asymptotics.is_O (λ (x : α), f' x) g l g l

theorem asymptotics.is_O.of_norm_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {g : α → F} {f' : α → E'} {l : filter α} :
asymptotics.is_O (λ (x : α), f' x) g l g l

Alias of `is_O_norm_left`.

theorem asymptotics.is_O.norm_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {g : α → F} {f' : α → E'} {l : filter α} :
g lasymptotics.is_O (λ (x : α), f' x) g l

Alias of `is_O_norm_left`.

@[simp]
theorem asymptotics.is_o_norm_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {g : α → F} {f' : α → E'} {l : filter α} :
asymptotics.is_o (λ (x : α), f' x) g l g l

theorem asymptotics.is_o.norm_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {g : α → F} {f' : α → E'} {l : filter α} :
g lasymptotics.is_o (λ (x : α), f' x) g l

Alias of `is_o_norm_left`.

theorem asymptotics.is_o.of_norm_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {g : α → F} {f' : α → E'} {l : filter α} :
asymptotics.is_o (λ (x : α), f' x) g l g l

Alias of `is_o_norm_left`.

theorem asymptotics.is_O_with_norm_norm {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] {c : } {f' : α → E'} {g' : α → F'} {l : filter α} :
(λ (x : α), f' x) (λ (x : α), g' x) l g' l

theorem asymptotics.is_O_with.of_norm_norm {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] {c : } {f' : α → E'} {g' : α → F'} {l : filter α} :
(λ (x : α), f' x) (λ (x : α), g' x) l g' l

Alias of `is_O_with_norm_norm`.

theorem asymptotics.is_O_with.norm_norm {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] {c : } {f' : α → E'} {g' : α → F'} {l : filter α} :
g' l (λ (x : α), f' x) (λ (x : α), g' x) l

Alias of `is_O_with_norm_norm`.

theorem asymptotics.is_O_norm_norm {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] {f' : α → E'} {g' : α → F'} {l : filter α} :
asymptotics.is_O (λ (x : α), f' x) (λ (x : α), g' x) l g' l

theorem asymptotics.is_O.norm_norm {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] {f' : α → E'} {g' : α → F'} {l : filter α} :
g' lasymptotics.is_O (λ (x : α), f' x) (λ (x : α), g' x) l

Alias of `is_O_norm_norm`.

theorem asymptotics.is_O.of_norm_norm {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] {f' : α → E'} {g' : α → F'} {l : filter α} :
asymptotics.is_O (λ (x : α), f' x) (λ (x : α), g' x) l g' l

Alias of `is_O_norm_norm`.

theorem asymptotics.is_o_norm_norm {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] {f' : α → E'} {g' : α → F'} {l : filter α} :
asymptotics.is_o (λ (x : α), f' x) (λ (x : α), g' x) l g' l

theorem asymptotics.is_o.of_norm_norm {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] {f' : α → E'} {g' : α → F'} {l : filter α} :
asymptotics.is_o (λ (x : α), f' x) (λ (x : α), g' x) l g' l

Alias of `is_o_norm_norm`.

theorem asymptotics.is_o.norm_norm {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] {f' : α → E'} {g' : α → F'} {l : filter α} :
g' lasymptotics.is_o (λ (x : α), f' x) (λ (x : α), g' x) l

Alias of `is_o_norm_norm`.

Simplification: negate

@[simp]
theorem asymptotics.is_O_with_neg_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] [normed_group F'] {c : } {f : α → E} {g' : α → F'} {l : filter α} :
(λ (x : α), -g' x) l g' l

theorem asymptotics.is_O_with.neg_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] [normed_group F'] {c : } {f : α → E} {g' : α → F'} {l : filter α} :
g' l (λ (x : α), -g' x) l

Alias of `is_O_with_neg_right`.

theorem asymptotics.is_O_with.of_neg_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] [normed_group F'] {c : } {f : α → E} {g' : α → F'} {l : filter α} :
(λ (x : α), -g' x) l g' l

Alias of `is_O_with_neg_right`.

@[simp]
theorem asymptotics.is_O_neg_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] [normed_group F'] {f : α → E} {g' : α → F'} {l : filter α} :
(λ (x : α), -g' x) l g' l

theorem asymptotics.is_O.neg_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] [normed_group F'] {f : α → E} {g' : α → F'} {l : filter α} :
g' l (λ (x : α), -g' x) l

Alias of `is_O_neg_right`.

theorem asymptotics.is_O.of_neg_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] [normed_group F'] {f : α → E} {g' : α → F'} {l : filter α} :
(λ (x : α), -g' x) l g' l

Alias of `is_O_neg_right`.

@[simp]
theorem asymptotics.is_o_neg_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] [normed_group F'] {f : α → E} {g' : α → F'} {l : filter α} :
(λ (x : α), -g' x) l g' l

theorem asymptotics.is_o.of_neg_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] [normed_group F'] {f : α → E} {g' : α → F'} {l : filter α} :
(λ (x : α), -g' x) l g' l

Alias of `is_o_neg_right`.

theorem asymptotics.is_o.neg_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] [normed_group F'] {f : α → E} {g' : α → F'} {l : filter α} :
g' l (λ (x : α), -g' x) l

Alias of `is_o_neg_right`.

@[simp]
theorem asymptotics.is_O_with_neg_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {c : } {g : α → F} {f' : α → E'} {l : filter α} :
(λ (x : α), -f' x) g l g l

theorem asymptotics.is_O_with.of_neg_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {c : } {g : α → F} {f' : α → E'} {l : filter α} :
(λ (x : α), -f' x) g l g l

Alias of `is_O_with_neg_left`.

theorem asymptotics.is_O_with.neg_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {c : } {g : α → F} {f' : α → E'} {l : filter α} :
g l (λ (x : α), -f' x) g l

Alias of `is_O_with_neg_left`.

@[simp]
theorem asymptotics.is_O_neg_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {g : α → F} {f' : α → E'} {l : filter α} :
asymptotics.is_O (λ (x : α), -f' x) g l g l

theorem asymptotics.is_O.neg_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {g : α → F} {f' : α → E'} {l : filter α} :
g lasymptotics.is_O (λ (x : α), -f' x) g l

Alias of `is_O_neg_left`.

theorem asymptotics.is_O.of_neg_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {g : α → F} {f' : α → E'} {l : filter α} :
asymptotics.is_O (λ (x : α), -f' x) g l g l

Alias of `is_O_neg_left`.

@[simp]
theorem asymptotics.is_o_neg_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {g : α → F} {f' : α → E'} {l : filter α} :
asymptotics.is_o (λ (x : α), -f' x) g l g l

theorem asymptotics.is_o.neg_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {g : α → F} {f' : α → E'} {l : filter α} :
g lasymptotics.is_o (λ (x : α), -f' x) g l

Alias of `is_o_neg_left`.

Product of functions (right)

theorem asymptotics.is_O_with_fst_prod {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] {f' : α → E'} {g' : α → F'} {l : filter α} :
(λ (x : α), (f' x, g' x)) l

theorem asymptotics.is_O_with_snd_prod {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] {f' : α → E'} {g' : α → F'} {l : filter α} :
(λ (x : α), (f' x, g' x)) l

theorem asymptotics.is_O_fst_prod {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] {f' : α → E'} {g' : α → F'} {l : filter α} :
(λ (x : α), (f' x, g' x)) l

theorem asymptotics.is_O_snd_prod {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] {f' : α → E'} {g' : α → F'} {l : filter α} :
(λ (x : α), (f' x, g' x)) l

theorem asymptotics.is_O_fst_prod' {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] {l : filter α} {f' : α → E' × F'} :
asymptotics.is_O (λ (x : α), (f' x).fst) f' l

theorem asymptotics.is_O_snd_prod' {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] {l : filter α} {f' : α → E' × F'} :
asymptotics.is_O (λ (x : α), (f' x).snd) f' l

theorem asymptotics.is_O_with.prod_rightl {α : Type u_1} {E : Type u_3} {F' : Type u_7} {G' : Type u_8} [has_norm E] [normed_group F'] [normed_group G'] {c : } {f : α → E} {g' : α → F'} (k' : α → G') {l : filter α} (h : g' l) (hc : 0 c) :
(λ (x : α), (g' x, k' x)) l

theorem asymptotics.is_O.prod_rightl {α : Type u_1} {E : Type u_3} {F' : Type u_7} {G' : Type u_8} [has_norm E] [normed_group F'] [normed_group G'] {f : α → E} {g' : α → F'} (k' : α → G') {l : filter α} (h : g' l) :
(λ (x : α), (g' x, k' x)) l

theorem asymptotics.is_o.prod_rightl {α : Type u_1} {E : Type u_3} {F' : Type u_7} {G' : Type u_8} [has_norm E] [normed_group F'] [normed_group G'] {f : α → E} {g' : α → F'} (k' : α → G') {l : filter α} (h : g' l) :
(λ (x : α), (g' x, k' x)) l

theorem asymptotics.is_O_with.prod_rightr {α : Type u_1} {E : Type u_3} {E' : Type u_6} {F' : Type u_7} [has_norm E] [normed_group E'] [normed_group F'] {c : } {f : α → E} (f' : α → E') {g' : α → F'} {l : filter α} (h : g' l) (hc : 0 c) :
(λ (x : α), (f' x, g' x)) l

theorem asymptotics.is_O.prod_rightr {α : Type u_1} {E : Type u_3} {E' : Type u_6} {F' : Type u_7} [has_norm E] [normed_group E'] [normed_group F'] {f : α → E} (f' : α → E') {g' : α → F'} {l : filter α} (h : g' l) :
(λ (x : α), (f' x, g' x)) l

theorem asymptotics.is_o.prod_rightr {α : Type u_1} {E : Type u_3} {E' : Type u_6} {F' : Type u_7} [has_norm E] [normed_group E'] [normed_group F'] {f : α → E} (f' : α → E') {g' : α → F'} {l : filter α} (h : g' l) :
(λ (x : α), (f' x, g' x)) l

theorem asymptotics.is_O_with.prod_left_same {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [normed_group E'] [normed_group F'] [normed_group G'] {c : } {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : filter α} (hf : k' l) (hg : k' l) :
(λ (x : α), (f' x, g' x)) k' l

theorem asymptotics.is_O_with.prod_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [normed_group E'] [normed_group F'] [normed_group G'] {c c' : } {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : filter α} (hf : k' l) (hg : k' l) :
asymptotics.is_O_with (max c c') (λ (x : α), (f' x, g' x)) k' l

theorem asymptotics.is_O_with.prod_left_fst {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [normed_group E'] [normed_group F'] [normed_group G'] {c : } {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : filter α} (h : (λ (x : α), (f' x, g' x)) k' l) :
k' l

theorem asymptotics.is_O_with.prod_left_snd {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [normed_group E'] [normed_group F'] [normed_group G'] {c : } {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : filter α} (h : (λ (x : α), (f' x, g' x)) k' l) :
k' l

theorem asymptotics.is_O_with_prod_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [normed_group E'] [normed_group F'] [normed_group G'] {c : } {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : filter α} :
(λ (x : α), (f' x, g' x)) k' l k' l k' l

theorem asymptotics.is_O.prod_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [normed_group E'] [normed_group F'] [normed_group G'] {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : filter α} (hf : k' l) (hg : k' l) :
asymptotics.is_O (λ (x : α), (f' x, g' x)) k' l

theorem asymptotics.is_O.prod_left_fst {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [normed_group E'] [normed_group F'] [normed_group G'] {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : filter α} (h : asymptotics.is_O (λ (x : α), (f' x, g' x)) k' l) :
k' l

theorem asymptotics.is_O.prod_left_snd {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [normed_group E'] [normed_group F'] [normed_group G'] {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : filter α} (h : asymptotics.is_O (λ (x : α), (f' x, g' x)) k' l) :
k' l

@[simp]
theorem asymptotics.is_O_prod_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [normed_group E'] [normed_group F'] [normed_group G'] {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : filter α} :
asymptotics.is_O (λ (x : α), (f' x, g' x)) k' l k' l k' l

theorem asymptotics.is_o.prod_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [normed_group E'] [normed_group F'] [normed_group G'] {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : filter α} (hf : k' l) (hg : k' l) :
asymptotics.is_o (λ (x : α), (f' x, g' x)) k' l

theorem asymptotics.is_o.prod_left_fst {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [normed_group E'] [normed_group F'] [normed_group G'] {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : filter α} (h : asymptotics.is_o (λ (x : α), (f' x, g' x)) k' l) :
k' l

theorem asymptotics.is_o.prod_left_snd {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [normed_group E'] [normed_group F'] [normed_group G'] {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : filter α} (h : asymptotics.is_o (λ (x : α), (f' x, g' x)) k' l) :
k' l

@[simp]
theorem asymptotics.is_o_prod_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [normed_group E'] [normed_group F'] [normed_group G'] {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : filter α} :
asymptotics.is_o (λ (x : α), (f' x, g' x)) k' l k' l k' l

theorem asymptotics.is_O_with.eq_zero_imp {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] {c : } {f' : α → E'} {g' : α → F'} {l : filter α} (h : g' l) :
∀ᶠ (x : α) in l, g' x = 0f' x = 0

theorem asymptotics.is_O.eq_zero_imp {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] {f' : α → E'} {g' : α → F'} {l : filter α} (h : g' l) :
∀ᶠ (x : α) in l, g' x = 0f' x = 0

theorem asymptotics.is_O_with.add {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {g : α → F} {l : filter α} {c₁ c₂ : } {f₁ f₂ : α → E'} (h₁ : g l) (h₂ : g l) :
asymptotics.is_O_with (c₁ + c₂) (λ (x : α), f₁ x + f₂ x) g l

theorem asymptotics.is_O.add {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {g : α → F} {l : filter α} {f₁ f₂ : α → E'} :
g l g lasymptotics.is_O (λ (x : α), f₁ x + f₂ x) g l

theorem asymptotics.is_o.add {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {g : α → F} {l : filter α} {f₁ f₂ : α → E'} (h₁ : g l) (h₂ : g l) :
asymptotics.is_o (λ (x : α), f₁ x + f₂ x) g l

theorem asymptotics.is_o.add_add {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] {l : filter α} {f₁ f₂ : α → E'} {g₁ g₂ : α → F'} (h₁ : g₁ l) (h₂ : g₂ l) :
asymptotics.is_o (λ (x : α), f₁ x + f₂ x) (λ (x : α), g₁ x + g₂ x) l

theorem asymptotics.is_O.add_is_o {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {g : α → F} {l : filter α} {f₁ f₂ : α → E'} (h₁ : g l) (h₂ : g l) :
asymptotics.is_O (λ (x : α), f₁ x + f₂ x) g l

theorem asymptotics.is_o.add_is_O {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {g : α → F} {l : filter α} {f₁ f₂ : α → E'} (h₁ : g l) (h₂ : g l) :
asymptotics.is_O (λ (x : α), f₁ x + f₂ x) g l

theorem asymptotics.is_O_with.add_is_o {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {g : α → F} {l : filter α} {c₁ c₂ : } {f₁ f₂ : α → E'} (h₁ : g l) (h₂ : g l) (hc : c₁ < c₂) :
(λ (x : α), f₁ x + f₂ x) g l

theorem asymptotics.is_o.add_is_O_with {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {g : α → F} {l : filter α} {c₁ c₂ : } {f₁ f₂ : α → E'} (h₁ : g l) (h₂ : g l) (hc : c₁ < c₂) :
(λ (x : α), f₁ x + f₂ x) g l

theorem asymptotics.is_O_with.sub {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {g : α → F} {l : filter α} {c₁ c₂ : } {f₁ f₂ : α → E'} (h₁ : g l) (h₂ : g l) :
asymptotics.is_O_with (c₁ + c₂) (λ (x : α), f₁ x - f₂ x) g l

theorem asymptotics.is_O_with.sub_is_o {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {g : α → F} {l : filter α} {c₁ c₂ : } {f₁ f₂ : α → E'} (h₁ : g l) (h₂ : g l) (hc : c₁ < c₂) :
(λ (x : α), f₁ x - f₂ x) g l

theorem asymptotics.is_O.sub {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {g : α → F} {l : filter α} {f₁ f₂ : α → E'} (h₁ : g l) (h₂ : g l) :
asymptotics.is_O (λ (x : α), f₁ x - f₂ x) g l

theorem asymptotics.is_o.sub {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {g : α → F} {l : filter α} {f₁ f₂ : α → E'} (h₁ : g l) (h₂ : g l) :
asymptotics.is_o (λ (x : α), f₁ x - f₂ x) g l

Lemmas about `is_O (f₁ - f₂) g l` / `is_o (f₁ - f₂) g l` treated as a binary relation

theorem asymptotics.is_O_with.symm {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {c : } {g : α → F} {l : filter α} {f₁ f₂ : α → E'} (h : (λ (x : α), f₁ x - f₂ x) g l) :
(λ (x : α), f₂ x - f₁ x) g l

theorem asymptotics.is_O_with_comm {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {c : } {g : α → F} {l : filter α} {f₁ f₂ : α → E'} :
(λ (x : α), f₁ x - f₂ x) g l (λ (x : α), f₂ x - f₁ x) g l

theorem asymptotics.is_O.symm {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {g : α → F} {l : filter α} {f₁ f₂ : α → E'} (h : asymptotics.is_O (λ (x : α), f₁ x - f₂ x) g l) :
asymptotics.is_O (λ (x : α), f₂ x - f₁ x) g l

theorem asymptotics.is_O_comm {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {g : α → F} {l : filter α} {f₁ f₂ : α → E'} :
asymptotics.is_O (λ (x : α), f₁ x - f₂ x) g l asymptotics.is_O (λ (x : α), f₂ x - f₁ x) g l

theorem asymptotics.is_o.symm {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {g : α → F} {l : filter α} {f₁ f₂ : α → E'} (h : asymptotics.is_o (λ (x : α), f₁ x - f₂ x) g l) :
asymptotics.is_o (λ (x : α), f₂ x - f₁ x) g l

theorem asymptotics.is_o_comm {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {g : α → F} {l : filter α} {f₁ f₂ : α → E'} :
asymptotics.is_o (λ (x : α), f₁ x - f₂ x) g l asymptotics.is_o (λ (x : α), f₂ x - f₁ x) g l

theorem asymptotics.is_O_with.triangle {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {c c' : } {g : α → F} {l : filter α} {f₁ f₂ f₃ : α → E'} (h₁ : (λ (x : α), f₁ x - f₂ x) g l) (h₂ : (λ (x : α), f₂ x - f₃ x) g l) :
asymptotics.is_O_with (c + c') (λ (x : α), f₁ x - f₃ x) g l

theorem asymptotics.is_O.triangle {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {g : α → F} {l : filter α} {f₁ f₂ f₃ : α → E'} (h₁ : asymptotics.is_O (λ (x : α), f₁ x - f₂ x) g l) (h₂ : asymptotics.is_O (λ (x : α), f₂ x - f₃ x) g l) :
asymptotics.is_O (λ (x : α), f₁ x - f₃ x) g l

theorem asymptotics.is_o.triangle {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {g : α → F} {l : filter α} {f₁ f₂ f₃ : α → E'} (h₁ : asymptotics.is_o (λ (x : α), f₁ x - f₂ x) g l) (h₂ : asymptotics.is_o (λ (x : α), f₂ x - f₃ x) g l) :
asymptotics.is_o (λ (x : α), f₁ x - f₃ x) g l

theorem asymptotics.is_O.congr_of_sub {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {g : α → F} {l : filter α} {f₁ f₂ : α → E'} (h : asymptotics.is_O (λ (x : α), f₁ x - f₂ x) g l) :
g l g l

theorem asymptotics.is_o.congr_of_sub {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {g : α → F} {l : filter α} {f₁ f₂ : α → E'} (h : asymptotics.is_o (λ (x : α), f₁ x - f₂ x) g l) :
g l g l

Zero, one, and other constants

theorem asymptotics.is_o_zero {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] (g' : α → F') (l : filter α) :
asymptotics.is_o (λ (x : α), 0) g' l

theorem asymptotics.is_O_with_zero {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] {c : } (g' : α → F') (l : filter α) (hc : 0 c) :
(λ (x : α), 0) g' l

theorem asymptotics.is_O_with_zero' {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] (g : α → F) (l : filter α) :
(λ (x : α), 0) g l

theorem asymptotics.is_O_zero {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] (g : α → F) (l : filter α) :
asymptotics.is_O (λ (x : α), 0) g l

theorem asymptotics.is_O_refl_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] {f' : α → E'} (g' : α → F') (l : filter α) :
asymptotics.is_O (λ (x : α), f' x - f' x) g' l

theorem asymptotics.is_o_refl_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] {f' : α → E'} (g' : α → F') (l : filter α) :
asymptotics.is_o (λ (x : α), f' x - f' x) g' l

@[simp]
theorem asymptotics.is_O_with_zero_right_iff {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] {c : } {f' : α → E'} {l : filter α} :
(λ (x : α), 0) l ∀ᶠ (x : α) in l, f' x = 0

@[simp]
theorem asymptotics.is_O_zero_right_iff {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] {f' : α → E'} {l : filter α} :
(λ (x : α), 0) l ∀ᶠ (x : α) in l, f' x = 0

@[simp]
theorem asymptotics.is_o_zero_right_iff {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] {f' : α → E'} {l : filter α} :
(λ (x : α), 0) l ∀ᶠ (x : α) in l, f' x = 0

theorem asymptotics.is_O_with_const_const {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] [normed_group F'] (c : E) {c' : F'} (hc' : c' 0) (l : filter α) :
asymptotics.is_O_with (c / c') (λ (x : α), c) (λ (x : α), c') l

theorem asymptotics.is_O_const_const {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] [normed_group F'] (c : E) {c' : F'} (hc' : c' 0) (l : filter α) :
asymptotics.is_O (λ (x : α), c) (λ (x : α), c') l

@[simp]
theorem asymptotics.is_O_with_top {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {c : } {f : α → E} {g : α → F} :
∀ (x : α), f x c * g x

@[simp]
theorem asymptotics.is_O_top {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f : α → E} {g : α → F} :
∃ (C : ), ∀ (x : α), f x C * g x

@[simp]
theorem asymptotics.is_o_top {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] {f' : α → E'} {g' : α → F'} :
g' ∀ (x : α), f' x = 0

@[simp]
theorem asymptotics.is_O_with_principal {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {c : } {f : α → E} {g : α → F} {s : set α} :
(𝓟 s) ∀ (x : α), x sf x c * g x

theorem asymptotics.is_O_principal {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f : α → E} {g : α → F} {s : set α} :
(𝓟 s) ∃ (c : ), ∀ (x : α), x sf x c * g x

theorem asymptotics.is_O_with_const_one {α : Type u_1} {E : Type u_3} {𝕜 : Type u_11} [has_norm E] [normed_field 𝕜] (c : E) (l : filter α) :
(λ (x : α), c) (λ (x : α), 1) l

theorem asymptotics.is_O_const_one {α : Type u_1} {E : Type u_3} {𝕜 : Type u_11} [has_norm E] [normed_field 𝕜] (c : E) (l : filter α) :
asymptotics.is_O (λ (x : α), c) (λ (x : α), 1) l

theorem asymptotics.is_o_const_iff_is_o_one {α : Type u_1} {E : Type u_3} {F' : Type u_7} (𝕜 : Type u_11) [has_norm E] [normed_group F'] [normed_field 𝕜] {f : α → E} {l : filter α} {c : F'} (hc : c 0) :
(λ (x : α), c) l (λ (x : α), 1) l

theorem asymptotics.is_o_const_iff {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] {f' : α → E'} {l : filter α} {c : F'} (hc : c 0) :
(λ (x : α), c) l l (𝓝 0)

theorem asymptotics.is_o_id_const {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] {c : F'} (hc : c 0) :
asymptotics.is_o (λ (x : E'), x) (λ (x : E'), c) (𝓝 0)

theorem asymptotics.is_O_const_of_tendsto {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] {f' : α → E'} {l : filter α} {y : E'} (h : l (𝓝 y)) {c : F'} (hc : c 0) :
(λ (x : α), c) l

theorem asymptotics.is_o_one_iff {α : Type u_1} {E' : Type u_6} (𝕜 : Type u_11) [normed_group E'] [normed_field 𝕜] {f' : α → E'} {l : filter α} :
(λ (x : α), 1) l l (𝓝 0)

theorem asymptotics.is_O_one_of_tendsto {α : Type u_1} {E' : Type u_6} (𝕜 : Type u_11) [normed_group E'] [normed_field 𝕜] {f' : α → E'} {l : filter α} {y : E'} (h : l (𝓝 y)) :
(λ (x : α), 1) l

theorem asymptotics.is_O.trans_tendsto_nhds {α : Type u_1} {E : Type u_3} {F' : Type u_7} (𝕜 : Type u_11) [has_norm E] [normed_group F'] [normed_field 𝕜] {f : α → E} {g' : α → F'} {l : filter α} (hfg : g' l) {y : F'} (hg : l (𝓝 y)) :
(λ (x : α), 1) l

theorem asymptotics.is_O.trans_tendsto {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] {f' : α → E'} {g' : α → F'} {l : filter α} (hfg : g' l) (hg : l (𝓝 0)) :
l (𝓝 0)

theorem asymptotics.is_o.trans_tendsto {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] {f' : α → E'} {g' : α → F'} {l : filter α} (hfg : g' l) (hg : l (𝓝 0)) :
l (𝓝 0)

Multiplication by a constant

theorem asymptotics.is_O_with_const_mul_self {α : Type u_1} {R : Type u_9} [normed_ring R] (c : R) (f : α → R) (l : filter α) :
(λ (x : α), c * f x) f l

theorem asymptotics.is_O_const_mul_self {α : Type u_1} {R : Type u_9} [normed_ring R] (c : R) (f : α → R) (l : filter α) :
asymptotics.is_O (λ (x : α), c * f x) f l

theorem asymptotics.is_O_with.const_mul_left {α : Type u_1} {F : Type u_4} {R : Type u_9} [has_norm F] [normed_ring R] {c : } {g : α → F} {l : filter α} {f : α → R} (h : l) (c' : R) :
asymptotics.is_O_with (c' * c) (λ (x : α), c' * f x) g l

theorem asymptotics.is_O.const_mul_left {α : Type u_1} {F : Type u_4} {R : Type u_9} [has_norm F] [normed_ring R] {g : α → F} {l : filter α} {f : α → R} (h : l) (c' : R) :
asymptotics.is_O (λ (x : α), c' * f x) g l

theorem asymptotics.is_O_with_self_const_mul' {α : Type u_1} {R : Type u_9} [normed_ring R] (u : units R) (f : α → R) (l : filter α) :
(λ (x : α), (u) * f x) l

theorem asymptotics.is_O_with_self_const_mul {α : Type u_1} {𝕜 : Type u_11} [normed_field 𝕜] (c : 𝕜) (hc : c 0) (f : α → 𝕜) (l : filter α) :
(λ (x : α), c * f x) l

theorem asymptotics.is_O_self_const_mul' {α : Type u_1} {R : Type u_9} [normed_ring R] {c : R} (hc : is_unit c) (f : α → R) (l : filter α) :
(λ (x : α), c * f x) l

theorem asymptotics.is_O_self_const_mul {α : Type u_1} {𝕜 : Type u_11} [normed_field 𝕜] (c : 𝕜) (hc : c 0) (f : α → 𝕜) (l : filter α) :
(λ (x : α), c * f x) l

theorem asymptotics.is_O_const_mul_left_iff' {α : Type u_1} {F : Type u_4} {R : Type u_9} [has_norm F] [normed_ring R] {g : α → F} {l : filter α} {f : α → R} {c : R} (hc : is_unit c) :
asymptotics.is_O (λ (x : α), c * f x) g l l

theorem asymptotics.is_O_const_mul_left_iff {α : Type u_1} {F : Type u_4} {𝕜 : Type u_11} [has_norm F] [normed_field 𝕜] {g : α → F} {l : filter α} {f : α → 𝕜} {c : 𝕜} (hc : c 0) :
asymptotics.is_O (λ (x : α), c * f x) g l l

theorem asymptotics.is_o.const_mul_left {α : Type u_1} {F : Type u_4} {R : Type u_9} [has_norm F] [normed_ring R] {g : α → F} {l : filter α} {f : α → R} (h : l) (c : R) :
asymptotics.is_o (λ (x : α), c * f x) g l

theorem asymptotics.is_o_const_mul_left_iff' {α : Type u_1} {F : Type u_4} {R : Type u_9} [has_norm F] [normed_ring R] {g : α → F} {l : filter α} {f : α → R} {c : R} (hc : is_unit c) :
asymptotics.is_o (λ (x : α), c * f x) g l l

theorem asymptotics.is_o_const_mul_left_iff {α : Type u_1} {F : Type u_4} {𝕜 : Type u_11} [has_norm F] [normed_field 𝕜] {g : α → F} {l : filter α} {f : α → 𝕜} {c : 𝕜} (hc : c 0) :
asymptotics.is_o (λ (x : α), c * f x) g l l

theorem asymptotics.is_O_with.of_const_mul_right {α : Type u_1} {E : Type u_3} {R : Type u_9} [has_norm E] [normed_ring R] {c' : } {f : α → E} {l : filter α} {g : α → R} {c : R} (hc' : 0 c') (h : (λ (x : α), c * g x) l) :

theorem asymptotics.is_O.of_const_mul_right {α : Type u_1} {E : Type u_3} {R : Type u_9} [has_norm E] [normed_ring R] {f : α → E} {l : filter α} {g : α → R} {c : R} (h : (λ (x : α), c * g x) l) :
l

theorem asymptotics.is_O_with.const_mul_right' {α : Type u_1} {E : Type u_3} {R : Type u_9} [has_norm E] [normed_ring R] {f : α → E} {l : filter α} {g : α → R} {u : units R} {c' : } (hc' : 0 c') (h : g l) :
asymptotics.is_O_with (c' * u⁻¹) f (λ (x : α), (u) * g x) l

theorem asymptotics.is_O_with.const_mul_right {α : Type u_1} {E : Type u_3} {𝕜 : Type u_11} [has_norm E] [normed_field 𝕜] {f : α → E} {l : filter α} {g : α → 𝕜} {c : 𝕜} (hc : c 0) {c' : } (hc' : 0 c') (h : g l) :
asymptotics.is_O_with (c' * c⁻¹) f (λ (x : α), c * g x) l

theorem asymptotics.is_O.const_mul_right' {α : Type u_1} {E : Type u_3} {R : Type u_9} [has_norm E] [normed_ring R] {f : α → E} {l : filter α} {g : α → R} {c : R} (hc : is_unit c) (h : l) :
(λ (x : α), c * g x) l

theorem asymptotics.is_O.const_mul_right {α : Type u_1} {E : Type u_3} {𝕜 : Type u_11} [has_norm E] [normed_field 𝕜] {f : α → E} {l : filter α} {g : α → 𝕜} {c : 𝕜} (hc : c 0) (h : l) :
(λ (x : α), c * g x) l

theorem asymptotics.is_O_const_mul_right_iff' {α : Type u_1} {E : Type u_3} {R : Type u_9} [has_norm E] [normed_ring R] {f : α → E} {l : filter α} {g : α → R} {c : R} (hc : is_unit c) :
(λ (x : α), c * g x) l l

theorem asymptotics.is_O_const_mul_right_iff {α : Type u_1} {E : Type u_3} {𝕜 : Type u_11} [has_norm E] [normed_field 𝕜] {f : α → E} {l : filter α} {g : α → 𝕜} {c : 𝕜} (hc : c 0) :
(λ (x : α), c * g x) l l

theorem asymptotics.is_o.of_const_mul_right {α : Type u_1} {E : Type u_3} {R : Type u_9} [has_norm E] [normed_ring R] {f : α → E} {l : filter α} {g : α → R} {c : R} (h : (λ (x : α), c * g x) l) :
l

theorem asymptotics.is_o.const_mul_right' {α : Type u_1} {E : Type u_3} {R : Type u_9} [has_norm E] [normed_ring R] {f : α → E} {l : filter α} {g : α → R} {c : R} (hc : is_unit c) (h : l) :
(λ (x : α), c * g x) l

theorem asymptotics.is_o.const_mul_right {α : Type u_1} {E : Type u_3} {𝕜 : Type u_11} [has_norm E] [normed_field 𝕜] {f : α → E} {l : filter α} {g : α → 𝕜} {c : 𝕜} (hc : c 0) (h : l) :
(λ (x : α), c * g x) l

theorem asymptotics.is_o_const_mul_right_iff' {α : Type u_1} {E : Type u_3} {R : Type u_9} [has_norm E] [normed_ring R] {f : α → E} {l : filter α} {g : α → R} {c : R} (hc : is_unit c) :
(λ (x : α), c * g x) l l

theorem asymptotics.is_o_const_mul_right_iff {α : Type u_1} {E : Type u_3} {𝕜 : Type u_11} [has_norm E] [normed_field 𝕜] {f : α → E} {l : filter α} {g : α → 𝕜} {c : 𝕜} (hc : c 0) :
(λ (x : α), c * g x) l l

Multiplication

theorem asymptotics.is_O_with.mul {α : Type u_1} {R : Type u_9} {𝕜 : Type u_11} [normed_ring R] [normed_field 𝕜] {l : filter α} {f₁ f₂ : α → R} {g₁ g₂ : α → 𝕜} {c₁ c₂ : } (h₁ : g₁ l) (h₂ : g₂ l) :
asymptotics.is_O_with (c₁ * c₂) (λ (x : α), (f₁ x) * f₂ x) (λ (x : α), (g₁ x) * g₂ x) l

theorem asymptotics.is_O.mul {α : Type u_1} {R : Type u_9} {𝕜 : Type u_11} [normed_ring R] [normed_field 𝕜] {l : filter α} {f₁ f₂ : α → R} {g₁ g₂ : α → 𝕜} (h₁ : g₁ l) (h₂ : g₂ l) :
asymptotics.is_O (λ (x : α), (f₁ x) * f₂ x) (λ (x : α), (g₁ x) * g₂ x) l

theorem asymptotics.is_O.mul_is_o {α : Type u_1} {R : Type u_9} {𝕜 : Type u_11} [normed_ring R] [normed_field 𝕜] {l : filter α} {f₁ f₂ : α → R} {g₁ g₂ : α → 𝕜} (h₁ : g₁ l) (h₂ : g₂ l) :
asymptotics.is_o (λ (x : α), (f₁ x) * f₂ x) (λ (x : α), (g₁ x) * g₂ x) l

theorem asymptotics.is_o.mul_is_O {α : Type u_1} {R : Type u_9} {𝕜 : Type u_11} [normed_ring R] [normed_field 𝕜] {l : filter α} {f₁ f₂ : α → R} {g₁ g₂ : α → 𝕜} (h₁ : g₁ l) (h₂ : g₂ l) :
asymptotics.is_o (λ (x : α), (f₁ x) * f₂ x) (λ (x : α), (g₁ x) * g₂ x) l

theorem asymptotics.is_o.mul {α : Type u_1} {R : Type u_9} {𝕜 : Type u_11} [normed_ring R] [normed_field 𝕜] {l : filter α} {f₁ f₂ : α → R} {g₁ g₂ : α → 𝕜} (h₁ : g₁ l) (h₂ : g₂ l) :
asymptotics.is_o (λ (x : α), (f₁ x) * f₂ x) (λ (x : α), (g₁ x) * g₂ x) l

theorem asymptotics.is_O_with.pow' {α : Type u_1} {R : Type u_9} {𝕜 : Type u_11} [normed_ring R] [normed_field 𝕜] {c : } {l : filter α} {f : α → R} {g : α → 𝕜} (h : l) (n : ) :
asymptotics.is_O_with (n.cases_on 1 (λ (n : ), c ^ (n + 1))) (λ (x : α), f x ^ n) (λ (x : α), g x ^ n) l

theorem asymptotics.is_O_with.pow {α : Type u_1} {R : Type u_9} {𝕜 : Type u_11} [normed_ring R] [normed_field 𝕜] {c : } {l : filter α} {f : α → R} {g : α → 𝕜} (h : l) (n : ) :
asymptotics.is_O_with (c ^ n) (λ (x : α), f x ^ n) (λ (x : α), g x ^ n) l

theorem asymptotics.is_O.pow {α : Type u_1} {R : Type u_9} {𝕜 : Type u_11} [normed_ring R] [normed_field 𝕜] {l : filter α} {f : α → R} {g : α → 𝕜} (h : l) (n : ) :
asymptotics.is_O (λ (x : α), f x ^ n) (λ (x : α), g x ^ n) l

theorem asymptotics.is_o.pow {α : Type u_1} {R : Type u_9} {𝕜 : Type u_11} [normed_ring R] [normed_field 𝕜] {l : filter α} {f : α → R} {g : α → 𝕜} (h : l) {n : } (hn : 0 < n) :
asymptotics.is_o (λ (x : α), f x ^ n) (λ (x : α), g x ^ n) l

Scalar multiplication

theorem asymptotics.is_O_with.const_smul_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} {𝕜 : Type u_11} [has_norm F] [normed_group E'] [normed_field 𝕜] {c : } {g : α → F} {f' : α → E'} {l : filter α} [ E'] (h : g l) (c' : 𝕜) :
asymptotics.is_O_with (c' * c) (λ (x : α), c' f' x) g l

theorem asymptotics.is_O_const_smul_left_iff {α : Type u_1} {F : Type u_4} {E' : Type u_6} {𝕜 : Type u_11} [has_norm F] [normed_group E'] [normed_field 𝕜] {g : α → F} {f' : α → E'} {l : filter α} [ E'] {c : 𝕜} (hc : c 0) :
asymptotics.is_O (λ (x : α), c f' x) g l g l

theorem asymptotics.is_o_const_smul_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} {𝕜 : Type u_11} [has_norm F] [normed_group E'] [normed_field 𝕜] {g : α → F} {f' : α → E'} {l : filter α} [ E'] (h : g l) (c : 𝕜) :
asymptotics.is_o (λ (x : α), c f' x) g l

theorem asymptotics.is_o_const_smul_left_iff {α : Type u_1} {F : Type u_4} {E' : Type u_6} {𝕜 : Type u_11} [has_norm F] [normed_group E'] [normed_field 𝕜] {g : α → F} {f' : α → E'} {l : filter α} [ E'] {c : 𝕜} (hc : c 0) :
asymptotics.is_o (λ (x : α), c f' x) g l g l

theorem asymptotics.is_O_const_smul_right {α : Type u_1} {E : Type u_3} {E' : Type u_6} {𝕜 : Type u_11} [has_norm E] [normed_group E'] [normed_field 𝕜] {f : α → E} {f' : α → E'} {l : filter α} [ E'] {c : 𝕜} (hc : c 0) :
(λ (x : α), c f' x) l f' l

theorem asymptotics.is_o_const_smul_right {α : Type u_1} {E : Type u_3} {E' : Type u_6} {𝕜 : Type u_11} [has_norm E] [normed_group E'] [normed_field 𝕜] {f : α → E} {f' : α → E'} {l : filter α} [ E'] {c : 𝕜} (hc : c 0) :
(λ (x : α), c f' x) l f' l

theorem asymptotics.is_O_with.smul {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {𝕜 : Type u_11} [normed_group E'] [normed_group F'] [normed_field 𝕜] {c c' : } {f' : α → E'} {g' : α → F'} {l : filter α} [ E'] [ F'] {k₁ k₂ : α → 𝕜} (h₁ : k₂ l) (h₂ : g' l) :
asymptotics.is_O_with (c * c') (λ (x : α), k₁ x f' x) (λ (x : α), k₂ x g' x) l

theorem asymptotics.is_O.smul {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {𝕜 : Type u_11} [normed_group E'] [normed_group F'] [normed_field 𝕜] {f' : α → E'} {g' : α → F'} {l : filter α} [ E'] [ F'] {k₁ k₂ : α → 𝕜} (h₁ : k₂ l) (h₂ : g' l) :
asymptotics.is_O (λ (x : α), k₁ x f' x) (λ (x : α), k₂ x g' x) l

theorem asymptotics.is_O.smul_is_o {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {𝕜 : Type u_11} [normed_group E'] [normed_group F'] [normed_field 𝕜] {f' : α → E'} {g' : α → F'} {l : filter α} [ E'] [ F'] {k₁ k₂ : α → 𝕜} (h₁ : k₂ l) (h₂ : g' l) :
asymptotics.is_o (λ (x : α), k₁ x f' x) (λ (x : α), k₂ x g' x) l

theorem asymptotics.is_o.smul_is_O {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {𝕜 : Type u_11} [normed_group E'] [normed_group F'] [normed_field 𝕜] {f' : α → E'} {g' : α → F'} {l : filter α} [ E'] [ F'] {k₁ k₂ : α → 𝕜} (h₁ : k₂ l) (h₂ : g' l) :
asymptotics.is_o (λ (x : α), k₁ x f' x) (λ (x : α), k₂ x g' x) l

theorem asymptotics.is_o.smul {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {𝕜 : Type u_11} [normed_group E'] [normed_group F'] [normed_field 𝕜] {f' : α → E'} {g' : α → F'} {l : filter α} [ E'] [ F'] {k₁ k₂ : α → 𝕜} (h₁ : k₂ l) (h₂ : g' l) :
asymptotics.is_o (λ (x : α), k₁ x f' x) (λ (x : α), k₂ x g' x) l

Sum

theorem asymptotics.is_O_with.sum {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {g : α → F} {l : filter α} {ι : Type u_13} {A : ι → α → E'} {C : ι → } {s : finset ι} (h : ∀ (i : ι), i s (A i) g l) :
asymptotics.is_O_with (∑ (i : ι) in s, C i) (λ (x : α), ∑ (i : ι) in s, A i x) g l

theorem asymptotics.is_O.sum {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [normed_group E'] {g : α → F} {l : filter α} {ι : Type u_13} {A : ι → α → E'} {s : finset ι} (h : ∀ (i : ι), i sasymptotics.is_O (A i) g l) :
asymptotics.is_O (λ (x : α), ∑ (i : ι) in s, A i x) g l

theorem asymptotics.is_o.sum {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] {g' : α → F'} {l : filter α} {ι : Type u_13} {A : ι → α → E'} {s : finset ι} (h : ∀ (i : ι), i sasymptotics.is_o (A i) g' l) :
asymptotics.is_o (λ (x : α), ∑ (i : ι) in s, A i x) g' l

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

theorem asymptotics.is_o.tendsto_0 {α : Type u_1} {𝕜 : Type u_11} [normed_field 𝕜] {f g : α → 𝕜} {l : filter α} (h : l) :
filter.tendsto (λ (x : α), f x / g x) l (𝓝 0)

theorem asymptotics.is_o_iff_tendsto' {α : Type u_1} {𝕜 : Type u_11} [normed_field 𝕜] {f g : α → 𝕜} {l : filter α} (hgf : ∀ᶠ (x : α) in l, g x = 0f x = 0) :
l filter.tendsto (λ (x : α), f x / g x) l (𝓝 0)

theorem asymptotics.is_o_iff_tendsto {α : Type u_1} {𝕜 : Type u_11} [normed_field 𝕜] {f g : α → 𝕜} {l : filter α} (hgf : ∀ (x : α), g x = 0f x = 0) :
l filter.tendsto (λ (x : α), f x / g x) l (𝓝 0)

theorem asymptotics.is_o_of_tendsto' {α : Type u_1} {𝕜 : Type u_11} [normed_field 𝕜] {f g : α → 𝕜} {l : filter α} (hgf : ∀ᶠ (x : α) in l, g x = 0f x = 0) :
filter.tendsto (λ (x : α), f x / g x) l (𝓝 0) l

Alias of `is_o_iff_tendsto'`.

theorem asymptotics.is_o_of_tendsto {α : Type u_1} {𝕜 : Type u_11} [normed_field 𝕜] {f g : α → 𝕜} {l : filter α} (hgf : ∀ (x : α), g x = 0f x = 0) :
filter.tendsto (λ (x : α), f x / g x) l (𝓝 0) l

Alias of `is_o_iff_tendsto`.

Eventually (u / v) * v = u

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

theorem asymptotics.is_O_with.eventually_mul_div_cancel {α : Type u_1} {𝕜 : Type u_11} [normed_field 𝕜] {c : } {l : filter α} {u v : α → 𝕜} (h : l) :
(u / v) * v =ᶠ[l] u

theorem asymptotics.is_O.eventually_mul_div_cancel {α : Type u_1} {𝕜 : Type u_11} [normed_field 𝕜] {l : filter α} {u v : α → 𝕜} (h : l) :
(u / v) * v =ᶠ[l] u

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

theorem asymptotics.is_o.eventually_mul_div_cancel {α : Type u_1} {𝕜 : Type u_11} [normed_field 𝕜] {l : filter α} {u v : α → 𝕜} (h : l) :
(u / v) * v =ᶠ[l] u

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

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

theorem asymptotics.is_O_with_of_eq_mul {α : Type u_1} {𝕜 : Type u_11} [normed_field 𝕜] {c : } {l : filter α} {u v : α → 𝕜} (φ : α → 𝕜) (hφ : ∀ᶠ (x : α) in l, φ x c) (h : u =ᶠ[l] φ * v) :
l

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

theorem asymptotics.is_O_with_iff_exists_eq_mul {α : Type u_1} {𝕜 : Type u_11} [normed_field 𝕜] {c : } {l : filter α} {u v : α → 𝕜} (hc : 0 c) :
l ∃ (φ : α → 𝕜) (hφ : ∀ᶠ (x : α) in l, φ x c), u =ᶠ[l] φ * v

theorem asymptotics.is_O_with.exists_eq_mul {α : Type u_1} {𝕜 : Type u_11} [normed_field 𝕜] {c : } {l : filter α} {u v : α → 𝕜} (h : l) (hc : 0 c) :
∃ (φ : α → 𝕜) (hφ : ∀ᶠ (x : α) in l, φ x c), u =ᶠ[l] φ * v

theorem asymptotics.is_O_iff_exists_eq_mul {α : Type u_1} {𝕜 : Type u_11} [normed_field 𝕜] {l : filter α} {u v : α → 𝕜} :
l ∃ (φ : α → 𝕜) (hφ : , u =ᶠ[l] φ * v

theorem asymptotics.is_O.exists_eq_mul {α : Type u_1} {𝕜 : Type u_11} [normed_field 𝕜] {l : filter α} {u v : α → 𝕜} :
l(∃ (φ : α → 𝕜) (hφ : , u =ᶠ[l] φ * v)

Alias of `is_O_iff_exists_eq_mul`.

theorem asymptotics.is_o_iff_exists_eq_mul {α : Type u_1} {𝕜 : Type u_11} [normed_field 𝕜] {l : filter α} {u v : α → 𝕜} :
l ∃ (φ : α → 𝕜) (hφ : (𝓝 0)), u =ᶠ[l] φ * v

theorem asymptotics.is_o.exists_eq_mul {α : Type u_1} {𝕜 : Type u_11} [normed_field 𝕜] {l : filter α} {u v : α → 𝕜} :
l(∃ (φ : α → 𝕜) (hφ : (𝓝 0)), u =ᶠ[l] φ * v)

Alias of `is_o_iff_exists_eq_mul`.

Miscellanous lemmas

theorem asymptotics.is_o_pow_pow {𝕜 : Type u_11} [normed_field 𝕜] {m n : } (h : m < n) :
asymptotics.is_o (λ (x : 𝕜), x ^ n) (λ (x : 𝕜), x ^ m) (𝓝 0)

theorem asymptotics.is_o_norm_pow_norm_pow {E' : Type u_6} [normed_group E'] {m n : } (h : m < n) :
asymptotics.is_o (λ (x : E'), x ^ n) (λ (x : E'), x ^ m) (𝓝 0)

theorem asymptotics.is_o_pow_id {𝕜 : Type u_11} [normed_field 𝕜] {n : } (h : 1 < n) :
asymptotics.is_o (λ (x : 𝕜), x ^ n) (λ (x : 𝕜), x) (𝓝 0)

theorem asymptotics.is_o_norm_pow_id {E' : Type u_6} [normed_group E'] {n : } (h : 1 < n) :
asymptotics.is_o (λ (x : E'), x ^ n) (λ (x : E'), x) (𝓝 0)

theorem asymptotics.is_O_with.right_le_sub_of_lt_1 {α : Type u_1} {E' : Type u_6} [normed_group E'] {c : } {l : filter α} {f₁ f₂ : α → E'} (h : f₂ l) (hc : c < 1) :
asymptotics.is_O_with (1 / (1 - c)) f₂ (λ (x : α), f₂ x - f₁ x) l

theorem asymptotics.is_O_with.right_le_add_of_lt_1 {α : Type u_1} {E' : Type u_6} [normed_group E'] {c : } {l : filter α} {f₁ f₂ : α → E'} (h : f₂ l) (hc : c < 1) :
asymptotics.is_O_with (1 / (1 - c)) f₂ (λ (x : α), f₁ x + f₂ x) l

theorem asymptotics.is_o.right_is_O_sub {α : Type u_1} {E' : Type u_6} [normed_group E'] {l : filter α} {f₁ f₂ : α → E'} (h : f₂ l) :
(λ (x : α), f₂ x - f₁ x) l

theorem asymptotics.is_o.right_is_O_add {α : Type u_1} {E' : Type u_6} [normed_group E'] {l : filter α} {f₁ f₂ : α → E'} (h : f₂ l) :
(λ (x : α), f₁ x + f₂ x) l

theorem asymptotics.bound_of_is_O_cofinite {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] [normed_group F'] {f : α → E} {g' : α → F'} (h : g' filter.cofinite) :
∃ (C : ) (H : C > 0), ∀ ⦃x : α⦄, g' x 0f x C * g' x

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

theorem asymptotics.is_O_cofinite_iff {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] {f' : α → E'} {g' : α → F'} (h : ∀ (x : α), g' x = 0f' x = 0) :
∃ (C : ), ∀ (x : α), f' x C * g' x

theorem asymptotics.bound_of_is_O_nat_at_top {E : Type u_3} {E' : Type u_6} [has_norm E] [normed_group E'] {f : → E} {g' : → E'} (h : g' filter.at_top) :
∃ (C : ) (H : C > 0), ∀ ⦃x : ⦄, g' x 0f x C * g' x

theorem asymptotics.is_O_nat_at_top_iff {E' : Type u_6} {F' : Type u_7} [normed_group E'] [normed_group F'] {f : → E'} {g : → F'} (h : ∀ (x : ), g x = 0f x = 0) :
∃ (C : ), ∀ (x : ), f x C * g x

theorem asymptotics.is_O_one_nat_at_top_iff {E' : Type u_6} [normed_group E'] {f : → E'} :
(λ (n : ), 1) filter.at_top ∃ (C : ), ∀ (n : ), f n C

theorem summable_of_is_O {ι : Type u_1} {E : Type u_2} [normed_group E] {f : ι → E} (g : ι → ) (hg : summable g) (h : filter.cofinite) :

theorem summable_of_is_O_nat {E : Type u_1} [normed_group E] {f : → E} (g : ) (hg : summable g) (h : filter.at_top) :

theorem local_homeomorph.is_O_with_congr {α : Type u_1} {β : Type u_2} {E : Type u_3} [has_norm E] {F : Type u_4} [has_norm F] (e : β) {b : β} (hb : b e.to_local_equiv.target) {f : β → E} {g : β → F} {C : } :
(𝓝 b) (f e) (g e) (𝓝 ((e.symm) b))

Transfer `is_O_with` over a `local_homeomorph`.

theorem local_homeomorph.is_O_congr {α : Type u_1} {β : Type u_2} {E : Type u_3} [has_norm E] {F : Type u_4} [has_norm F] (e : β) {b : β} (hb : b e.to_local_equiv.target) {f : β → E} {g : β → F} :
(𝓝 b) asymptotics.is_O (f e) (g e) (𝓝 ((e.symm) b))

Transfer `is_O` over a `local_homeomorph`.

theorem local_homeomorph.is_o_congr {α : Type u_1} {β : Type u_2} {E : Type u_3} [has_norm E] {F : Type u_4} [has_norm F] (e : β) {b : β} (hb : b e.to_local_equiv.target) {f : β → E} {g : β → F} :
(𝓝 b) asymptotics.is_o (f e) (g e) (𝓝 ((e.symm) b))

Transfer `is_o` over a `local_homeomorph`.

theorem homeomorph.is_O_with_congr {α : Type u_1} {β : Type u_2} {E : Type u_3} [has_norm E] {F : Type u_4} [has_norm F] (e : α ≃ₜ β) {b : β} {f : β → E} {g : β → F} {C : } :
(𝓝 b) (f e) (g e) (𝓝 ((e.symm) b))

Transfer `is_O_with` over a `homeomorph`.

theorem homeomorph.is_O_congr {α : Type u_1} {β : Type u_2} {E : Type u_3} [has_norm E] {F : Type u_4} [has_norm F] (e : α ≃ₜ β) {b : β} {f : β → E} {g : β → F} :
(𝓝 b) asymptotics.is_O (f e) (g e) (𝓝 ((e.symm) b))

Transfer `is_O` over a `homeomorph`.

theorem homeomorph.is_o_congr {α : Type u_1} {β : Type u_2} {E : Type u_3} [has_norm E] {F : Type u_4} [has_norm F] (e : α ≃ₜ β) {b : β} {f : β → E} {g : β → F} :
(𝓝 b) asymptotics.is_o (f e) (g e) (𝓝 ((e.symm) b))

Transfer `is_o` over a `homeomorph`.