# mathlib3documentation

analysis.asymptotics.asymptotics

# Asymptotics #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We introduce these relations:

• `is_O_with c l f g` : "f is big O of g along l with constant c";
• `f =O[l] g` : "f is big O of g along l";
• `f =o[l] g` : "f is little o of g along l".

Here `l` is any filter on the domain of `f` and `g`, which are assumed to be the same. The codomains of `f` and `g` do not need to be the same; all that is needed that there is a norm associated with these types, and it is the norm that is compared asymptotically.

The relation `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

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

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

`f =o[l] g ↔ 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 #

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

This version of the Landau notation `is_O_with 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 `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 α} :
g ∀ᶠ (x : α) in l, f x c * g x

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

theorem asymptotics.is_O_with.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 α} :
g (∀ᶠ (x : α) in l, f x c * g x)

Alias of the forward direction of `asymptotics.is_O_with_iff`.

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 α} :
(∀ᶠ (x : α) in l, f x c * g x) g

Alias of the reverse direction of `asymptotics.is_O_with_iff`.

@[irreducible]
def asymptotics.is_O {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_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
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 α} :
f =O[l] g (c : ), g

Definition of `is_O` in terms of `is_O_with`. We record it in a lemma as `is_O` is irreducible.

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 α} :
f =O[l] g (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] {f : α E} {g : α F} {l : filter α} (c : ) (h : ∀ᶠ (x : α) in l, f x c * g x) :
f =O[l] g
theorem asymptotics.is_O.of_bound' {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f : α E} {g : α F} {l : filter α} (h : ∀ᶠ (x : α) in l, f x g x) :
f =O[l] g
theorem asymptotics.is_O.bound {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f : α E} {g : α F} {l : filter α} :
f =O[l] g ( (c : ), ∀ᶠ (x : α) in l, f x c * g x)
@[irreducible]
def asymptotics.is_o {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_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
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 α} :
f =o[l] g ⦃c : ⦄, 0 < c g

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.of_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 α} :
( ⦃c : ⦄, 0 < c g) f =o[l] g

Alias of the reverse direction of `asymptotics.is_o_iff_forall_is_O_with`.

theorem asymptotics.is_o.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 α} :
f =o[l] g ⦃c : ⦄, 0 < c g

Alias of the forward direction of `asymptotics.is_o_iff_forall_is_O_with`.

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 α} :
f =o[l] g ⦃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.bound {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_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.is_o_iff`.

theorem asymptotics.is_o.of_bound {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_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.is_o_iff`.

theorem asymptotics.is_o.def {α : 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 : f =o[l] g) (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] {c : } {f : α E} {g : α F} {l : filter α} (h : f =o[l] g) (hc : 0 < c) :
g

### 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 : g) :
f =O[l] g
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 : f =o[l] g) :
g
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 : f =o[l] g) :
f =O[l] g
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 α} :
f =O[l] g ( (c : ), g)
theorem asymptotics.is_O_with.weaken {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] {c c' : } {f : α E} {g' : α F'} {l : filter α} (h : g') (hc : c c') :
f g'
theorem asymptotics.is_O_with.exists_pos {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] {c : } {f : α E} {g' : α F'} {l : filter α} (h : g') :
(c' : ) (H : 0 < c'), f g'
theorem asymptotics.is_O.exists_pos {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] {f : α E} {g' : α F'} {l : filter α} (h : f =O[l] g') :
(c : ) (H : 0 < c), g'
theorem asymptotics.is_O_with.exists_nonneg {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] {c : } {f : α E} {g' : α F'} {l : filter α} (h : g') :
(c' : ) (H : 0 c'), f g'
theorem asymptotics.is_O.exists_nonneg {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] {f : α E} {g' : α F'} {l : filter α} (h : f =O[l] g') :
(c : ) (H : 0 c), g'
theorem asymptotics.is_O_iff_eventually_is_O_with {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] {f : α E} {g' : α F'} {l : filter α} :

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

theorem asymptotics.is_O_iff_eventually {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] {f : α E} {g' : α F'} {l : filter α} :
f =O[l] g' ∀ᶠ (c : ) in filter.at_top, ∀ᶠ (x : α) in l, f x c * g' x

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

theorem asymptotics.is_O.exists_mem_basis {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] {f : α E} {g' : α F'} {l : filter α} {ι : Sort u_2} {p : ι Prop} {s : ι set α} (h : f =O[l] g') (hb : l.has_basis p s) :
(c : ) (hc : 0 < c) (i : ι) (hi : p i), (x : α), x s i f x c * g' x
theorem asymptotics.is_O_with_inv {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {c : } {f : α E} {g : α F} {l : filter α} (hc : 0 < c) :
g ∀ᶠ (x : α) in l, c * f x g x
theorem asymptotics.is_o_iff_nat_mul_le_aux {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f : α E} {g : α F} {l : filter α} (h₀ : ( (x : α), 0 f x) (x : α), 0 g x) :
f =o[l] g (n : ), ∀ᶠ (x : α) in l, n * f x g x
theorem asymptotics.is_o_iff_nat_mul_le {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] {f : α E} {g' : α F'} {l : filter α} :
f =o[l] g' (n : ), ∀ᶠ (x : α) in l, n * f x g' x
theorem asymptotics.is_o_iff_nat_mul_le' {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] {g : α F} {f' : α E'} {l : filter α} :
f' =o[l] g (n : ), ∀ᶠ (x : α) in l, n * f' x g x

### Subsingleton #

theorem asymptotics.is_o_of_subsingleton {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {f' : α E'} {g' : α F'} {l : filter α} [subsingleton E'] :
f' =o[l] g'
theorem asymptotics.is_O_of_subsingleton {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {f' : α E'} {g' : α F'} {l : filter α} [subsingleton E'] :
f' =O[l] g'

### 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₂ : } {l : filter α} {f₁ f₂ : α E} {g₁ g₂ : α F} (hc : c₁ = c₂) (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) :
f₁ g₁ f₂ g₂
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₂ : } {l : filter α} {f₁ f₂ : α E} {g₁ g₂ : α F} (h : f₁ g₁) (hc : c₁ = c₂) (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) :
f₂ g₂
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₂ : } {l : filter α} {f₁ f₂ : α E} {g₁ g₂ : α F} (h : f₁ g₁) (hc : c₁ = c₂) (hf : (x : α), f₁ x = f₂ x) (hg : (x : α), g₁ x = g₂ x) :
f₂ g₂
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} {l : filter α} {f₁ f₂ : α E} (h : f₁ g) (hf : (x : α), f₁ x = f₂ x) :
f₂ g
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} {l : filter α} {g₁ g₂ : α F} (h : g₁) (hg : (x : α), g₁ x = g₂ x) :
g₂
theorem asymptotics.is_O_with.congr_const {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {c₁ c₂ : } {f : α E} {g : α F} {l : filter α} (h : f g) (hc : c₁ = c₂) :
f g
theorem asymptotics.is_O_congr {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {l : filter α} {f₁ f₂ : α E} {g₁ g₂ : α F} (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) :
f₁ =O[l] g₁ f₂ =O[l] g₂
theorem asymptotics.is_O.congr' {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {l : filter α} {f₁ f₂ : α E} {g₁ g₂ : α F} (h : f₁ =O[l] g₁) (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) :
f₂ =O[l] g₂
theorem asymptotics.is_O.congr {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {l : filter α} {f₁ f₂ : α E} {g₁ g₂ : α F} (h : f₁ =O[l] g₁) (hf : (x : α), f₁ x = f₂ x) (hg : (x : α), g₁ x = g₂ x) :
f₂ =O[l] g₂
theorem asymptotics.is_O.congr_left {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {g : α F} {l : filter α} {f₁ f₂ : α E} (h : f₁ =O[l] g) (hf : (x : α), f₁ x = f₂ x) :
f₂ =O[l] g
theorem asymptotics.is_O.congr_right {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f : α E} {l : filter α} {g₁ g₂ : α F} (h : f =O[l] g₁) (hg : (x : α), g₁ x = g₂ x) :
f =O[l] g₂
theorem asymptotics.is_o_congr {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {l : filter α} {f₁ f₂ : α E} {g₁ g₂ : α F} (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) :
f₁ =o[l] g₁ f₂ =o[l] g₂
theorem asymptotics.is_o.congr' {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {l : filter α} {f₁ f₂ : α E} {g₁ g₂ : α F} (h : f₁ =o[l] g₁) (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) :
f₂ =o[l] g₂
theorem asymptotics.is_o.congr {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {l : filter α} {f₁ f₂ : α E} {g₁ g₂ : α F} (h : f₁ =o[l] g₁) (hf : (x : α), f₁ x = f₂ x) (hg : (x : α), g₁ x = g₂ x) :
f₂ =o[l] g₂
theorem asymptotics.is_o.congr_left {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {g : α F} {l : filter α} {f₁ f₂ : α E} (h : f₁ =o[l] g) (hf : (x : α), f₁ x = f₂ x) :
f₂ =o[l] g
theorem asymptotics.is_o.congr_right {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f : α E} {l : filter α} {g₁ g₂ : α F} (h : f =o[l] g₁) (hg : (x : α), g₁ x = g₂ x) :
f =o[l] g₂
@[trans]
theorem filter.eventually_eq.trans_is_O {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {l : filter α} {f₁ f₂ : α E} {g : α F} (hf : f₁ =ᶠ[l] f₂) (h : f₂ =O[l] g) :
f₁ =O[l] g
@[trans]
theorem filter.eventually_eq.trans_is_o {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {l : filter α} {f₁ f₂ : α E} {g : α F} (hf : f₁ =ᶠ[l] f₂) (h : f₂ =o[l] g) :
f₁ =o[l] g
@[trans]
theorem asymptotics.is_O.trans_eventually_eq {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {l : filter α} {f : α E} {g₁ g₂ : α F} (h : f =O[l] g₁) (hg : g₁ =ᶠ[l] g₂) :
f =O[l] g₂
@[trans]
theorem asymptotics.is_o.trans_eventually_eq {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {l : filter α} {f : α E} {g₁ g₂ : α F} (h : f =o[l] g₁) (hg : g₁ =ᶠ[l] g₂) :
f =o[l] g₂

### 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 : g) {k : β α} {l' : filter β} (hk : l' l) :
(f k) (g k)
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 : f =O[l] g) {k : β α} {l' : filter β} (hk : l' l) :
(f k) =O[l'] (g k)
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 : f =o[l] g) {k : β α} {l' : filter β} (hk : l' l) :
(f k) =o[l'] (g k)
@[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 g (f k) (g k)
@[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 β} :
f =O[ l] g (f k) =O[l] (g k)
@[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 β} :
f =o[ l] g (f k) =o[l] (g k)
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 : f g) (hl : l l') :
g
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 : f =O[l'] g) (hl : l l') :
f =O[l] g
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 : f =o[l'] g) (hl : l l') :
f =o[l] g
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 : g) (hgk : g k) (hc : 0 c) :
@[trans]
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] {l : filter α} {f : α E} {g : α F'} {k : α G} (hfg : f =O[l] g) (hgk : g =O[l] k) :
f =O[l] k
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 : f =o[l] g) (hgk : k) (hc : 0 < c) :
f =o[l] k
@[trans]
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] {l : filter α} {f : α E} {g : α F} {k : α G'} (hfg : f =o[l] g) (hgk : g =O[l] k) :
f =o[l] k
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 : g) (hgk : g =o[l] k) (hc : 0 < c) :
f =o[l] k
@[trans]
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] {l : filter α} {f : α E} {g : α F'} {k : α G} (hfg : f =O[l] g) (hgk : g =o[l] k) :
f =o[l] k
@[trans]
theorem asymptotics.is_o.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] {l : filter α} {f : α E} {g : α F} {k : α G} (hfg : f =o[l] g) (hgk : g =o[l] k) :
f =o[l] k
theorem filter.eventually.trans_is_O {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [has_norm E] [has_norm G] {l : filter α} {f : α E} {g : α F'} {k : α G} (hfg : ∀ᶠ (x : α) in l, f x g x) (hgk : g =O[l] k) :
f =O[l] k
theorem filter.eventually.is_O {α : Type u_1} {E : Type u_3} [has_norm E] {f : α E} {g : α } {l : filter α} (hfg : ∀ᶠ (x : α) in l, f x g x) :
f =O[l] g
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) :
g
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) :
g
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) :
f =O[l] g
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) :
f =O[l] g
theorem asymptotics.is_O_with_refl {α : Type u_1} {E : Type u_3} [has_norm E] (f : α E) (l : filter α) :
f
theorem asymptotics.is_O_refl {α : Type u_1} {E : Type u_3} [has_norm E] (f : α E) (l : filter α) :
f =O[l] f
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 : g) (hgk : (x : α), g x k x) (hc : 0 c) :
k
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] {f : α E} {k : α G} {g' : α F'} {l : filter α} (hfg : f =O[l] g') (hgk : (x : α), g' x k x) :
f =O[l] k
theorem asymptotics.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 : f =o[l] g) (hgk : (x : α), g x k x) :
f =o[l] k
theorem asymptotics.is_o_irrefl' {α : Type u_1} {E' : Type u_6} {f' : α E'} {l : filter α} (h : ∃ᶠ (x : α) in l, f' x 0) :
¬f' =o[l] f'
theorem asymptotics.is_o_irrefl {α : Type u_1} {E'' : Type u_9} {f'' : α E''} {l : filter α} (h : ∃ᶠ (x : α) in l, f'' x 0) :
¬f'' =o[l] f''
theorem asymptotics.is_O.not_is_o {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} {g' : α F'} {f'' : α E''} {l : filter α} (h : f'' =O[l] g') (hf : ∃ᶠ (x : α) in l, f'' x 0) :
¬g' =o[l] f''
theorem asymptotics.is_o.not_is_O {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} {g' : α F'} {f'' : α E''} {l : filter α} (h : f'' =o[l] g') (hf : ∃ᶠ (x : α) in l, f'' x 0) :
¬g' =O[l] f''
@[simp]
theorem asymptotics.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) :
g
@[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) :
@[simp]
theorem asymptotics.is_O_with_pure {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {c : } {f : α E} {g : α F} {x : α} :
g f x c * g x
theorem asymptotics.is_O_with.sup {α : 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 : g) (h' : f g) :
(l l') f g
theorem asymptotics.is_O_with.sup' {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] {c c' : } {f : α E} {g' : α F'} {l l' : filter α} (h : g') (h' : f g') :
(l l') f g'
theorem asymptotics.is_O.sup {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] {f : α E} {g' : α F'} {l l' : filter α} (h : f =O[l] g') (h' : f =O[l'] g') :
f =O[l l'] g'
theorem asymptotics.is_o.sup {α : 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 : f =o[l] g) (h' : f =o[l'] g) :
f =o[l l'] g
@[simp]
theorem asymptotics.is_O_sup {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] {f : α E} {g' : α F'} {l l' : filter α} :
f =O[l l'] g' f =O[l] g' f =O[l'] g'
@[simp]
theorem asymptotics.is_o_sup {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f : α E} {g : α F} {l l' : filter α} :
f =o[l l'] g f =o[l] g f =o[l'] g
theorem asymptotics.is_O_with_insert {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {x : α} {s : set α} {C : } {g : α E} {g' : α F} (h : g x C * g' x) :
s)) g g' s) g g'
theorem asymptotics.is_O_with.insert {α : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {x : α} {s : set α} {C : } {g : α E} {g' : α F} (h1 : s) g g') (h2 : g x C * g' x) :
s)) g g'
theorem asymptotics.is_o_insert {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {x : α} {s : set α} {g : α E'} {g' : α F'} (h : g x = 0) :
g =o[ s)] g' g =o[ s] g'
theorem asymptotics.is_o.insert {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {x : α} {s : set α} {g : α E'} {g' : α F'} (h1 : g =o[ s] g') (h2 : g x = 0) :
g =o[ s)] g'

### Simplification : norm, abs #

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

Alias of the reverse direction of `asymptotics.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] {c : } {f : α E} {g' : α F'} {l : filter α} :
(λ (x : α), g' x) g'

Alias of the forward direction of `asymptotics.is_O_with_norm_right`.

theorem asymptotics.is_O_with.of_abs_right {α : Type u_1} {E : Type u_3} [has_norm E] {c : } {f : α E} {l : filter α} {u : α } :
(λ (x : α), |u x|) u

Alias of the forward direction of `asymptotics.is_O_with_abs_right`.

theorem asymptotics.is_O_with.abs_right {α : Type u_1} {E : Type u_3} [has_norm E] {c : } {f : α E} {l : filter α} {u : α } :
u (λ (x : α), |u x|)

Alias of the reverse direction of `asymptotics.is_O_with_abs_right`.

@[simp]
theorem asymptotics.is_O_norm_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] {f : α E} {g' : α F'} {l : filter α} :
(f =O[l] λ (x : α), g' x) f =O[l] g'
@[simp]
theorem asymptotics.is_O_abs_right {α : Type u_1} {E : Type u_3} [has_norm E] {f : α E} {l : filter α} {u : α } :
(f =O[l] λ (x : α), |u x|) f =O[l] u
theorem asymptotics.is_O.norm_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] {f : α E} {g' : α F'} {l : filter α} :
f =O[l] g' (f =O[l] λ (x : α), g' x)

Alias of the reverse direction of `asymptotics.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] {f : α E} {g' : α F'} {l : filter α} :
(f =O[l] λ (x : α), g' x) f =O[l] g'

Alias of the forward direction of `asymptotics.is_O_norm_right`.

theorem asymptotics.is_O.of_abs_right {α : Type u_1} {E : Type u_3} [has_norm E] {f : α E} {l : filter α} {u : α } :
(f =O[l] λ (x : α), |u x|) f =O[l] u

Alias of the forward direction of `asymptotics.is_O_abs_right`.

theorem asymptotics.is_O.abs_right {α : Type u_1} {E : Type u_3} [has_norm E] {f : α E} {l : filter α} {u : α } :
f =O[l] u (f =O[l] λ (x : α), |u x|)

Alias of the reverse direction of `asymptotics.is_O_abs_right`.

@[simp]
theorem asymptotics.is_o_norm_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] {f : α E} {g' : α F'} {l : filter α} :
(f =o[l] λ (x : α), g' x) f =o[l] g'
@[simp]
theorem asymptotics.is_o_abs_right {α : Type u_1} {E : Type u_3} [has_norm E] {f : α E} {l : filter α} {u : α } :
(f =o[l] λ (x : α), |u x|) f =o[l] u
theorem asymptotics.is_o.norm_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] {f : α E} {g' : α F'} {l : filter α} :
f =o[l] g' (f =o[l] λ (x : α), g' x)

Alias of the reverse direction of `asymptotics.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] {f : α E} {g' : α F'} {l : filter α} :
(f =o[l] λ (x : α), g' x) f =o[l] g'

Alias of the forward direction of `asymptotics.is_o_norm_right`.

theorem asymptotics.is_o.of_abs_right {α : Type u_1} {E : Type u_3} [has_norm E] {f : α E} {l : filter α} {u : α } :
(f =o[l] λ (x : α), |u x|) f =o[l] u

Alias of the forward direction of `asymptotics.is_o_abs_right`.

theorem asymptotics.is_o.abs_right {α : Type u_1} {E : Type u_3} [has_norm E] {f : α E} {l : filter α} {u : α } :
f =o[l] u (f =o[l] λ (x : α), |u x|)

Alias of the reverse direction of `asymptotics.is_o_abs_right`.

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

Alias of the forward direction of `asymptotics.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] {c : } {g : α F} {f' : α E'} {l : filter α} :
f' g (λ (x : α), f' x) g

Alias of the reverse direction of `asymptotics.is_O_with_norm_left`.

theorem asymptotics.is_O_with.of_abs_left {α : Type u_1} {F : Type u_4} [has_norm F] {c : } {g : α F} {l : filter α} {u : α } :
(λ (x : α), |u x|) g g

Alias of the forward direction of `asymptotics.is_O_with_abs_left`.

theorem asymptotics.is_O_with.abs_left {α : Type u_1} {F : Type u_4} [has_norm F] {c : } {g : α F} {l : filter α} {u : α } :
g (λ (x : α), |u x|) g

Alias of the reverse direction of `asymptotics.is_O_with_abs_left`.

@[simp]
theorem asymptotics.is_O_norm_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] {g : α F} {f' : α E'} {l : filter α} :
(λ (x : α), f' x) =O[l] g f' =O[l] g
@[simp]
theorem asymptotics.is_O_abs_left {α : Type u_1} {F : Type u_4} [has_norm F] {g : α F} {l : filter α} {u : α } :
(λ (x : α), |u x|) =O[l] g u =O[l] g
theorem asymptotics.is_O.of_norm_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] {g : α F} {f' : α E'} {l : filter α} :
(λ (x : α), f' x) =O[l] g f' =O[l] g

Alias of the forward direction of `asymptotics.is_O_norm_left`.

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

Alias of the reverse direction of `asymptotics.is_O_norm_left`.

theorem asymptotics.is_O.of_abs_left {α : Type u_1} {F : Type u_4} [has_norm F] {g : α F} {l : filter α} {u : α } :
(λ (x : α), |u x|) =O[l] g u =O[l] g

Alias of the forward direction of `asymptotics.is_O_abs_left`.

theorem asymptotics.is_O.abs_left {α : Type u_1} {F : Type u_4} [has_norm F] {g : α F} {l : filter α} {u : α } :
u =O[l] g (λ (x : α), |u x|) =O[l] g

Alias of the reverse direction of `asymptotics.is_O_abs_left`.

@[simp]
theorem asymptotics.is_o_norm_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] {g : α F} {f' : α E'} {l : filter α} :
(λ (x : α), f' x) =o[l] g f' =o[l] g
@[simp]
theorem asymptotics.is_o_abs_left {α : Type u_1} {F : Type u_4} [has_norm F] {g : α F} {l : filter α} {u : α } :
(λ (x : α), |u x|) =o[l] g u =o[l] g
theorem asymptotics.is_o.norm_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] {g : α F} {f' : α E'} {l : filter α} :
f' =o[l] g (λ (x : α), f' x) =o[l] g

Alias of the reverse direction of `asymptotics.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] {g : α F} {f' : α E'} {l : filter α} :
(λ (x : α), f' x) =o[l] g f' =o[l] g

Alias of the forward direction of `asymptotics.is_o_norm_left`.

theorem asymptotics.is_o.of_abs_left {α : Type u_1} {F : Type u_4} [has_norm F] {g : α F} {l : filter α} {u : α } :
(λ (x : α), |u x|) =o[l] g u =o[l] g

Alias of the forward direction of `asymptotics.is_o_abs_left`.

theorem asymptotics.is_o.abs_left {α : Type u_1} {F : Type u_4} [has_norm F] {g : α F} {l : filter α} {u : α } :
u =o[l] g (λ (x : α), |u x|) =o[l] g

Alias of the reverse direction of `asymptotics.is_o_abs_left`.

theorem asymptotics.is_O_with_norm_norm {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {c : } {f' : α E'} {g' : α F'} {l : filter α} :
(λ (x : α), f' x) (λ (x : α), g' x) f' g'
theorem asymptotics.is_O_with_abs_abs {α : Type u_1} {c : } {l : filter α} {u v : α } :
(λ (x : α), |u x|) (λ (x : α), |v x|) v
theorem asymptotics.is_O_with.of_norm_norm {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {c : } {f' : α E'} {g' : α F'} {l : filter α} :
(λ (x : α), f' x) (λ (x : α), g' x) f' g'

Alias of the forward direction of `asymptotics.is_O_with_norm_norm`.

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

Alias of the reverse direction of `asymptotics.is_O_with_norm_norm`.

theorem asymptotics.is_O_with.of_abs_abs {α : Type u_1} {c : } {l : filter α} {u v : α } :
(λ (x : α), |u x|) (λ (x : α), |v x|) v

Alias of the forward direction of `asymptotics.is_O_with_abs_abs`.

theorem asymptotics.is_O_with.abs_abs {α : Type u_1} {c : } {l : filter α} {u v : α } :
v (λ (x : α), |u x|) (λ (x : α), |v x|)

Alias of the reverse direction of `asymptotics.is_O_with_abs_abs`.

theorem asymptotics.is_O_norm_norm {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {f' : α E'} {g' : α F'} {l : filter α} :
((λ (x : α), f' x) =O[l] λ (x : α), g' x) f' =O[l] g'
theorem asymptotics.is_O_abs_abs {α : Type u_1} {l : filter α} {u v : α } :
((λ (x : α), |u x|) =O[l] λ (x : α), |v x|) u =O[l] v
theorem asymptotics.is_O.norm_norm {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {f' : α E'} {g' : α F'} {l : filter α} :
f' =O[l] g' ((λ (x : α), f' x) =O[l] λ (x : α), g' x)

Alias of the reverse direction of `asymptotics.is_O_norm_norm`.

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

Alias of the forward direction of `asymptotics.is_O_norm_norm`.

theorem asymptotics.is_O.abs_abs {α : Type u_1} {l : filter α} {u v : α } :
u =O[l] v ((λ (x : α), |u x|) =O[l] λ (x : α), |v x|)

Alias of the reverse direction of `asymptotics.is_O_abs_abs`.

theorem asymptotics.is_O.of_abs_abs {α : Type u_1} {l : filter α} {u v : α } :
((λ (x : α), |u x|) =O[l] λ (x : α), |v x|) u =O[l] v

Alias of the forward direction of `asymptotics.is_O_abs_abs`.

theorem asymptotics.is_o_norm_norm {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {f' : α E'} {g' : α F'} {l : filter α} :
((λ (x : α), f' x) =o[l] λ (x : α), g' x) f' =o[l] g'
theorem asymptotics.is_o_abs_abs {α : Type u_1} {l : filter α} {u v : α } :
((λ (x : α), |u x|) =o[l] λ (x : α), |v x|) u =o[l] v
theorem asymptotics.is_o.of_norm_norm {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {f' : α E'} {g' : α F'} {l : filter α} :
((λ (x : α), f' x) =o[l] λ (x : α), g' x) f' =o[l] g'

Alias of the forward direction of `asymptotics.is_o_norm_norm`.

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

Alias of the reverse direction of `asymptotics.is_o_norm_norm`.

theorem asymptotics.is_o.of_abs_abs {α : Type u_1} {l : filter α} {u v : α } :
((λ (x : α), |u x|) =o[l] λ (x : α), |v x|) u =o[l] v

Alias of the forward direction of `asymptotics.is_o_abs_abs`.

theorem asymptotics.is_o.abs_abs {α : Type u_1} {l : filter α} {u v : α } :
u =o[l] v ((λ (x : α), |u x|) =o[l] λ (x : α), |v x|)

Alias of the reverse direction of `asymptotics.is_o_abs_abs`.

### Simplification: negate #

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

Alias of the reverse direction of `asymptotics.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] {c : } {f : α E} {g' : α F'} {l : filter α} :
(λ (x : α), -g' x) g'

Alias of the forward direction of `asymptotics.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] {f : α E} {g' : α F'} {l : filter α} :
(f =O[l] λ (x : α), -g' x) f =O[l] g'
theorem asymptotics.is_O.neg_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] {f : α E} {g' : α F'} {l : filter α} :
f =O[l] g' (f =O[l] λ (x : α), -g' x)

Alias of the reverse direction of `asymptotics.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] {f : α E} {g' : α F'} {l : filter α} :
(f =O[l] λ (x : α), -g' x) f =O[l] g'

Alias of the forward direction of `asymptotics.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] {f : α E} {g' : α F'} {l : filter α} :
(f =o[l] λ (x : α), -g' x) f =o[l] g'
theorem asymptotics.is_o.of_neg_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] {f : α E} {g' : α F'} {l : filter α} :
(f =o[l] λ (x : α), -g' x) f =o[l] g'

Alias of the forward direction of `asymptotics.is_o_neg_right`.

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

Alias of the reverse direction of `asymptotics.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] {c : } {g : α F} {f' : α E'} {l : filter α} :
(λ (x : α), -f' x) g f' g
theorem asymptotics.is_O_with.of_neg_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] {c : } {g : α F} {f' : α E'} {l : filter α} :
(λ (x : α), -f' x) g f' g

Alias of the forward direction of `asymptotics.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] {c : } {g : α F} {f' : α E'} {l : filter α} :
f' g (λ (x : α), -f' x) g

Alias of the reverse direction of `asymptotics.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] {g : α F} {f' : α E'} {l : filter α} :
(λ (x : α), -f' x) =O[l] g f' =O[l] g
theorem asymptotics.is_O.neg_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] {g : α F} {f' : α E'} {l : filter α} :
f' =O[l] g (λ (x : α), -f' x) =O[l] g

Alias of the reverse direction of `asymptotics.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] {g : α F} {f' : α E'} {l : filter α} :
(λ (x : α), -f' x) =O[l] g f' =O[l] g

Alias of the forward direction of `asymptotics.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] {g : α F} {f' : α E'} {l : filter α} :
(λ (x : α), -f' x) =o[l] g f' =o[l] g
theorem asymptotics.is_o.neg_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] {g : α F} {f' : α E'} {l : filter α} :
f' =o[l] g (λ (x : α), -f' x) =o[l] g

Alias of the reverse direction of `asymptotics.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} {f' : α E'} {g' : α F'} {l : filter α} :
f' (λ (x : α), (f' x, g' x))
theorem asymptotics.is_O_with_snd_prod {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {f' : α E'} {g' : α F'} {l : filter α} :
g' (λ (x : α), (f' x, g' x))
theorem asymptotics.is_O_fst_prod {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {f' : α E'} {g' : α F'} {l : filter α} :
f' =O[l] λ (x : α), (f' x, g' x)
theorem asymptotics.is_O_snd_prod {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {f' : α E'} {g' : α F'} {l : filter α} :
g' =O[l] λ (x : α), (f' x, g' x)
theorem asymptotics.is_O_fst_prod' {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {l : filter α} {f' : α E' × F'} :
(λ (x : α), (f' x).fst) =O[l] f'
theorem asymptotics.is_O_snd_prod' {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {l : filter α} {f' : α E' × F'} :
(λ (x : α), (f' x).snd) =O[l] f'
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] {c : } {f : α E} {g' : α F'} (k' : α G') {l : filter α} (h : g') (hc : 0 c) :
(λ (x : α), (g' x, k' x))
theorem asymptotics.is_O.prod_rightl {α : Type u_1} {E : Type u_3} {F' : Type u_7} {G' : Type u_8} [has_norm E] {f : α E} {g' : α F'} (k' : α G') {l : filter α} (h : f =O[l] g') :
f =O[l] λ (x : α), (g' x, k' x)
theorem asymptotics.is_o.prod_rightl {α : Type u_1} {E : Type u_3} {F' : Type u_7} {G' : Type u_8} [has_norm E] {f : α E} {g' : α F'} (k' : α G') {l : filter α} (h : f =o[l] g') :
f =o[l] λ (x : α), (g' x, k' x)
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] {c : } {f : α E} (f' : α E') {g' : α F'} {l : filter α} (h : g') (hc : 0 c) :
(λ (x : α), (f' x, g' x))
theorem asymptotics.is_O.prod_rightr {α : Type u_1} {E : Type u_3} {E' : Type u_6} {F' : Type u_7} [has_norm E] {f : α E} (f' : α E') {g' : α F'} {l : filter α} (h : f =O[l] g') :
f =O[l] λ (x : α), (f' x, g' x)
theorem asymptotics.is_o.prod_rightr {α : Type u_1} {E : Type u_3} {E' : Type u_6} {F' : Type u_7} [has_norm E] {f : α E} (f' : α E') {g' : α F'} {l : filter α} (h : f =o[l] g') :
f =o[l] λ (x : α), (f' x, g' x)
theorem asymptotics.is_O_with.prod_left_same {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} {c : } {f' : α E'} {g' : α F'} {k' : α G'} {l : filter α} (hf : f' k') (hg : g' k') :
(λ (x : α), (f' x, g' x)) k'
theorem asymptotics.is_O_with.prod_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} {c c' : } {f' : α E'} {g' : α F'} {k' : α G'} {l : filter α} (hf : f' k') (hg : g' k') :
(λ (x : α), (f' x, g' x)) k'
theorem asymptotics.is_O_with.prod_left_fst {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} {c : } {f' : α E'} {g' : α F'} {k' : α G'} {l : filter α} (h : (λ (x : α), (f' x, g' x)) k') :
f' k'
theorem asymptotics.is_O_with.prod_left_snd {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} {c : } {f' : α E'} {g' : α F'} {k' : α G'} {l : filter α} (h : (λ (x : α), (f' x, g' x)) k') :
g' k'
theorem asymptotics.is_O_with_prod_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} {c : } {f' : α E'} {g' : α F'} {k' : α G'} {l : filter α} :
(λ (x : α), (f' x, g' x)) k' f' k' g' k'
theorem asymptotics.is_O.prod_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} {f' : α E'} {g' : α F'} {k' : α G'} {l : filter α} (hf : f' =O[l] k') (hg : g' =O[l] k') :
(λ (x : α), (f' x, g' x)) =O[l] k'
theorem asymptotics.is_O.prod_left_fst {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} {f' : α E'} {g' : α F'} {k' : α G'} {l : filter α} :
(λ (x : α), (f' x, g' x)) =O[l] k' f' =O[l] k'
theorem asymptotics.is_O.prod_left_snd {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} {f' : α E'} {g' : α F'} {k' : α G'} {l : filter α} :
(λ (x : α), (f' x, g' x)) =O[l] k' g' =O[l] k'
@[simp]
theorem asymptotics.is_O_prod_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} {f' : α E'} {g' : α F'} {k' : α G'} {l : filter α} :
(λ (x : α), (f' x, g' x)) =O[l] k' f' =O[l] k' g' =O[l] k'
theorem asymptotics.is_o.prod_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} {f' : α E'} {g' : α F'} {k' : α G'} {l : filter α} (hf : f' =o[l] k') (hg : g' =o[l] k') :
(λ (x : α), (f' x, g' x)) =o[l] k'
theorem asymptotics.is_o.prod_left_fst {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} {f' : α E'} {g' : α F'} {k' : α G'} {l : filter α} :
(λ (x : α), (f' x, g' x)) =o[l] k' f' =o[l] k'
theorem asymptotics.is_o.prod_left_snd {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} {f' : α E'} {g' : α F'} {k' : α G'} {l : filter α} :
(λ (x : α), (f' x, g' x)) =o[l] k' g' =o[l] k'
@[simp]
theorem asymptotics.is_o_prod_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} {f' : α E'} {g' : α F'} {k' : α G'} {l : filter α} :
(λ (x : α), (f' x, g' x)) =o[l] k' f' =o[l] k' g' =o[l] k'
theorem asymptotics.is_O_with.eq_zero_imp {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} {c : } {f'' : α E''} {g'' : α F''} {l : filter α} (h : f'' g'') :
∀ᶠ (x : α) in l, g'' x = 0 f'' x = 0
theorem asymptotics.is_O.eq_zero_imp {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} {f'' : α E''} {g'' : α F''} {l : filter α} (h : f'' =O[l] g'') :
∀ᶠ (x : α) in l, g'' x = 0 f'' x = 0

theorem asymptotics.is_O_with.add {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] {c₁ c₂ : } {g : α F} {l : filter α} {f₁ f₂ : α E'} (h₁ : f₁ g) (h₂ : f₂ g) :
asymptotics.is_O_with (c₁ + c₂) l (λ (x : α), f₁ x + f₂ x) g
theorem asymptotics.is_O.add {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] {g : α F} {l : filter α} {f₁ f₂ : α E'} (h₁ : f₁ =O[l] g) (h₂ : f₂ =O[l] g) :
(λ (x : α), f₁ x + f₂ x) =O[l] g
theorem asymptotics.is_o.add {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] {g : α F} {l : filter α} {f₁ f₂ : α E'} (h₁ : f₁ =o[l] g) (h₂ : f₂ =o[l] g) :
(λ (x : α), f₁ x + f₂ x) =o[l] g
theorem asymptotics.is_o.add_add {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {l : filter α} {f₁ f₂ : α E'} {g₁ g₂ : α F'} (h₁ : f₁ =o[l] g₁) (h₂ : f₂ =o[l] g₂) :
(λ (x : α), f₁ x + f₂ x) =o[l] λ (x : α), g₁ x + g₂ x
theorem asymptotics.is_O.add_is_o {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] {g : α F} {l : filter α} {f₁ f₂ : α E'} (h₁ : f₁ =O[l] g) (h₂ : f₂ =o[l] g) :
(λ (x : α), f₁ x + f₂ x) =O[l] g
theorem asymptotics.is_o.add_is_O {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] {g : α F} {l : filter α} {f₁ f₂ : α E'} (h₁ : f₁ =o[l] g) (h₂ : f₂ =O[l] g) :
(λ (x : α), f₁ x + f₂ x) =O[l] g
theorem asymptotics.is_O_with.add_is_o {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] {c₁ c₂ : } {g : α F} {l : filter α} {f₁ f₂ : α E'} (h₁ : f₁ g) (h₂ : f₂ =o[l] g) (hc : c₁ < c₂) :
(λ (x : α), f₁ x + f₂ x) g
theorem asymptotics.is_o.add_is_O_with {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] {c₁ c₂ : } {g : α F} {l : filter α} {f₁ f₂ : α E'} (h₁ : f₁ =o[l] g) (h₂ : f₂ g) (hc : c₁ < c₂) :
(λ (x : α), f₁ x + f₂ x) g
theorem asymptotics.is_O_with.sub {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] {c₁ c₂ : } {g : α F} {l : filter α} {f₁ f₂ : α E'} (h₁ : f₁ g) (h₂ : f₂ g) :
asymptotics.is_O_with (c₁ + c₂) l (λ (x : α), f₁ x - f₂ x) g
theorem asymptotics.is_O_with.sub_is_o {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] {c₁ c₂ : } {g : α F} {l : filter α} {f₁ f₂ : α E'} (h₁ : f₁ g) (h₂ : f₂ =o[l] g) (hc : c₁ < c₂) :
(λ (x : α), f₁ x - f₂ x) g
theorem asymptotics.is_O.sub {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] {g : α F} {l : filter α} {f₁ f₂ : α E'} (h₁ : f₁ =O[l] g) (h₂ : f₂ =O[l] g) :
(λ (x : α), f₁ x - f₂ x) =O[l] g
theorem asymptotics.is_o.sub {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] {g : α F} {l : filter α} {f₁ f₂ : α E'} (h₁ : f₁ =o[l] g) (h₂ : f₂ =o[l] g) :
(λ (x : α), f₁ x - f₂ x) =o[l] g

### 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] {c : } {g : α F} {l : filter α} {f₁ f₂ : α E'} (h : (λ (x : α), f₁ x - f₂ x) g) :
(λ (x : α), f₂ x - f₁ x) g
theorem asymptotics.is_O_with_comm {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] {c : } {g : α F} {l : filter α} {f₁ f₂ : α E'} :
(λ (x : α), f₁ x - f₂ x) g (λ (x : α), f₂ x - f₁ x) g
theorem asymptotics.is_O.symm {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] {g : α F} {l : filter α} {f₁ f₂ : α E'} (h : (λ (x : α), f₁ x - f₂ x) =O[l] g) :
(λ (x : α), f₂ x - f₁ x) =O[l] g
theorem asymptotics.is_O_comm {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] {g : α F} {l : filter α} {f₁ f₂ : α E'} :
(λ (x : α), f₁ x - f₂ x) =O[l] g (λ (x : α), f₂ x - f₁ x) =O[l] g
theorem asymptotics.is_o.symm {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] {g : α F} {l : filter α} {f₁ f₂ : α E'} (h : (λ (x : α), f₁ x - f₂ x) =o[l] g) :
(λ (x : α), f₂ x - f₁ x) =o[l] g
theorem asymptotics.is_o_comm {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] {g : α F} {l : filter α} {f₁ f₂ : α E'} :
(λ (x : α), f₁ x - f₂ x) =o[l] g (λ (x : α), f₂ x - f₁ x) =o[l] g
theorem asymptotics.is_O_with.triangle {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] {c c' : } {g : α F} {l : filter α} {f₁ f₂ f₃ : α E'} (h₁ : (λ (x : α), f₁ x - f₂ x) g) (h₂ : (λ (x : α), f₂ x - f₃ x) g) :
asymptotics.is_O_with (c + c') l (λ (x : α), f₁ x - f₃ x) g
theorem asymptotics.is_O.triangle {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] {g : α F} {l : filter α} {f₁ f₂ f₃ : α E'} (h₁ : (λ (x : α), f₁ x - f₂ x) =O[l] g) (h₂ : (λ (x : α), f₂ x - f₃ x) =O[l] g) :
(λ (x : α), f₁ x - f₃ x) =O[l] g
theorem asymptotics.is_o.triangle {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] {g : α F} {l : filter α} {f₁ f₂ f₃ : α E'} (h₁ : (λ (x : α), f₁ x - f₂ x) =o[l] g) (h₂ : (λ (x : α), f₂ x - f₃ x) =o[l] g) :
(λ (x : α), f₁ x - f₃ x) =o[l] g
theorem asymptotics.is_O.congr_of_sub {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] {g : α F} {l : filter α} {f₁ f₂ : α E'} (h : (λ (x : α), f₁ x - f₂ x) =O[l] g) :
f₁ =O[l] g f₂ =O[l] g
theorem asymptotics.is_o.congr_of_sub {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] {g : α F} {l : filter α} {f₁ f₂ : α E'} (h : (λ (x : α), f₁ x - f₂ x) =o[l] g) :
f₁ =o[l] g f₂ =o[l] g

### Zero, one, and other constants #

theorem asymptotics.is_o_zero {α : Type u_1} {E' : Type u_6} {F' : Type u_7} (g' : α F') (l : filter α) :
(λ (x : α), 0) =o[l] g'
theorem asymptotics.is_O_with_zero {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {c : } (g' : α F') (l : filter α) (hc : 0 c) :
(λ (x : α), 0) g'
theorem asymptotics.is_O_with_zero' {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] (g : α F) (l : filter α) :
(λ (x : α), 0) g
theorem asymptotics.is_O_zero {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] (g : α F) (l : filter α) :
(λ (x : α), 0) =O[l] g
theorem asymptotics.is_O_refl_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {f' : α E'} (g' : α F') (l : filter α) :
(λ (x : α), f' x - f' x) =O[l] g'
theorem asymptotics.is_o_refl_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {f' : α E'} (g' : α F') (l : filter α) :
(λ (x : α), f' x - f' x) =o[l] g'
@[simp]
theorem asymptotics.is_O_with_zero_right_iff {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} {c : } {f'' : α E''} {l : filter α} :
f'' (λ (x : α), 0) f'' =ᶠ[l] 0
@[simp]
theorem asymptotics.is_O_zero_right_iff {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} {f'' : α E''} {l : filter α} :
(f'' =O[l] λ (x : α), 0) f'' =ᶠ[l] 0
@[simp]
theorem asymptotics.is_o_zero_right_iff {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} {f'' : α E''} {l : filter α} :
(f'' =o[l] λ (x : α), 0) f'' =ᶠ[l] 0
theorem asymptotics.is_O_with_const_const {α : Type u_1} {E : Type u_3} {F'' : Type u_10} [has_norm E] (c : E) {c' : F''} (hc' : c' 0) (l : filter α) :
asymptotics.is_O_with (c / c') l (λ (x : α), c) (λ (x : α), c')
theorem asymptotics.is_O_const_const {α : Type u_1} {E : Type u_3} {F'' : Type u_10} [has_norm E] (c : E) {c' : F''} (hc' : c' 0) (l : filter α) :
(λ (x : α), c) =O[l] λ (x : α), c'
@[simp]
theorem asymptotics.is_O_const_const_iff {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} {c : E''} {c' : F''} (l : filter α) [l.ne_bot] :
((λ (x : α), c) =O[l] λ (x : α), c') c' = 0 c = 0
@[simp]
theorem asymptotics.is_O_pure {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} {f'' : α E''} {g'' : α F''} {x : α} :
f'' =O[] g'' g'' x = 0 f'' x = 0
@[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} :
g (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} :
f =O[] g (C : ), (x : α), f x C * g x
@[simp]
theorem asymptotics.is_o_top {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} {f'' : α E''} {g'' : α F''} :
f'' =o[] 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 α} :
g (x : α), x s f 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 α} :
(c : ), (x : α), x s f x c * g x
theorem asymptotics.is_O_with_const_one {α : Type u_1} {E : Type u_3} (F : Type u_4) [has_norm E] [has_norm F] [has_one F] (c : E) (l : filter α) :
(λ (x : α), c) (λ (x : α), 1)
theorem asymptotics.is_O_const_one {α : Type u_1} {E : Type u_3} (F : Type u_4) [has_norm E] [has_norm F] [has_one F] (c : E) (l : filter α) :
(λ (x : α), c) =O[l] λ (x : α), 1
theorem asymptotics.is_o_const_iff_is_o_one {α : Type u_1} {E : Type u_3} (F : Type u_4) {F'' : Type u_10} [has_norm E] [has_norm F] {f : α E} {l : filter α} [has_one F] {c : F''} (hc : c 0) :
(f =o[l] λ (x : α), c) f =o[l] λ (x : α), 1
@[simp]
theorem asymptotics.is_o_one_iff {α : Type u_1} (F : Type u_4) {E' : Type u_6} [has_norm F] {f' : α E'} {l : filter α} [has_one F]  :
(f' =o[l] λ (x : α), 1) l (nhds 0)
@[simp]
theorem asymptotics.is_O_one_iff {α : Type u_1} {E : Type u_3} (F : Type u_4) [has_norm E] [has_norm F] {f : α E} {l : filter α} [has_one F]  :
(f =O[l] λ (x : α), 1) (λ (x : α), f x)
theorem filter.is_bounded_under.is_O_one {α : Type u_1} {E : Type u_3} (F : Type u_4) [has_norm E] [has_norm F] {f : α E} {l : filter α} [has_one F]  :
(λ (x : α), f x) (f =O[l] λ (x : α), 1)

Alias of the reverse direction of `asymptotics.is_O_one_iff`.

@[simp]
theorem asymptotics.is_o_one_left_iff {α : Type u_1} {E : Type u_3} (F : Type u_4) [has_norm E] [has_norm F] {f : α E} {l : filter α} [has_one F]  :
(λ (x : α), 1) =o[l] f filter.tendsto (λ (x : α), f x) l filter.at_top
theorem filter.tendsto.is_O_one {α : Type u_1} (F : Type u_4) {E' : Type u_6} [has_norm F] {f' : α E'} {l : filter α} [has_one F] {c : E'} (h : l (nhds c)) :
f' =O[l] λ (x : α), 1
theorem asymptotics.is_O.trans_tendsto_nhds {α : Type u_1} {E : Type u_3} (F : Type u_4) {F' : Type u_7} [has_norm E] [has_norm F] {f : α E} {g' : α F'} {l : filter α} [has_one F] (hfg : f =O[l] g') {y : F'} (hg : l (nhds y)) :
f =O[l] λ (x : α), 1
theorem asymptotics.is_o_const_iff {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} {f'' : α E''} {l : filter α} {c : F''} (hc : c 0) :
(f'' =o[l] λ (x : α), c) l (nhds 0)
theorem asymptotics.is_o_id_const {E'' : Type u_9} {F'' : Type u_10} {c : F''} (hc : c 0) :
(λ (x : E''), x) =o[nhds 0] λ (x : E''), c
theorem