# mathlibdocumentation

analysis.asymptotics.asymptotics

# Asymptotics #

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.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[l] g' β βαΆ  (c : β) in filter.at_top, g'

`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β) :
l fβ gβ β l 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 : l fβ gβ) (hc : cβ = cβ) (hf : fβ =αΆ [l] fβ) (hg : gβ =αΆ [l] gβ) :
l 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 : l fβ gβ) (hc : cβ = cβ) (hf : β (x : Ξ±), fβ x = fβ x) (hg : β (x : Ξ±), gβ x = gβ x) :
l 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 : l f g) (hc : cβ = cβ) :
l 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 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 : Ξ±} :
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

### 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 Ξ±} (h : (Ξ» (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 Ξ±} (h : (Ξ» (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 Ξ±} (h : (Ξ» (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 Ξ±} (h : (Ξ» (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β : l fβ g) (hβ : l 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β : l fβ g) (hβ : fβ =o[l] g) (hc : cβ < cβ) :
l (Ξ» (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β : l fβ g) (hc : cβ < cβ) :
l (Ξ» (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β : l fβ g) (hβ : l 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β : l fβ g) (hβ : fβ =o[l] g) (hc : cβ < cβ) :
l (Ξ» (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 Ξ±) :
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 filter.is_bounded_under.is_O_const {Ξ± : Type u_1} {E : Type u_3} {F'' : Type u_10} [has_norm E] {f : Ξ± β E} {l : filter Ξ±} (h : ) {c : F''} (hc : c β  0) :
f =O[l] Ξ» (x : Ξ±), c
theorem asymptotics.is_O_const_of_tendsto {Ξ± : Type u_1} {E'' : Type u_9} {F'' : Type u_10} {f'' : Ξ± β E''} {l : filter Ξ±} {y : E''} (h : l (nhds y)) {c : F''} (hc : c β  0) :
f'' =O[l] Ξ» (x : Ξ±), c
theorem asymptotics.is_O.is_bounded_under_le {Ξ± : Type u_1} {E : Type u_3} {F : Type u_4} [has_norm E] [has_norm F] {f : Ξ± β E} {l : filter Ξ±} {c : F} (h : f =O[l] Ξ» (x : Ξ±), c) :
theorem asymptotics.is_O_const_of_ne {Ξ± : Type u_1} {E : Type u_3} {F'' : Type u_10} [has_norm E] {f : Ξ± β E} {l : filter Ξ±} {c : F''} (hc : c β  0) :
(f =O[l] Ξ» (x : Ξ±), c) β
theorem asymptotics.is_O_const_iff {Ξ± : Type u_1} {E'' : Type u_9} {F'' : Type u_10} {f'' : Ξ± β E''} {l : filter Ξ±} {c : F''} :
(f'' =O[l] Ξ» (x : Ξ±), c) β (c = 0 β f'' =αΆ [l] 0) β§ (Ξ» (x : Ξ±), β₯f'' xβ₯)
theorem asymptotics.is_O_iff_is_bounded_under_le_div {Ξ± : Type u_1} {E : Type u_3} {F'' : Type u_10} [has_norm E] {f : Ξ± β E} {g'' : Ξ± β F''} {l : filter Ξ±} (h : βαΆ  (x : Ξ±) in l, g'' x β  0) :
f =O[l] g'' β (Ξ» (x : Ξ±), β₯f xβ₯ / β₯g'' xβ₯)
theorem asymptotics.is_O_const_left_iff_pos_le_norm {Ξ± : Type u_1} {E' : Type u_6} {E'' : Type u_9} {f' : Ξ± β E'} {l : filter Ξ±} {c : E''} (hc : c β  0) :
(Ξ» (x : Ξ±), c) =O[l] f' β β (b : β), 0 < b β§ βαΆ  (x : Ξ±) in l, b β€ β₯f' xβ₯

`(Ξ» x, c) =O[l] f` if and only if `f` is bounded away from zero.

theorem asymptotics.is_O.trans_tendsto {Ξ± : Type u_1} {E'' : Type u_9} {F'' : Type u_10} {f'' : Ξ± β E''} {g'' : Ξ± β F''} {l : filter Ξ±} (hfg : f'' =O[l] g'') (hg : l (nhds 0)) :
l (nhds 0)
theorem asymptotics.is_o.trans_tendsto {Ξ± : Type u_1} {E'' : Type u_9} {F'' : Type u_10} {f'' : Ξ± β E''} {g'' : Ξ± β F''} {l : filter Ξ±} (hfg : f'' =o[l] g'') (hg : l (nhds 0)) :
l (nhds 0)

### Multiplication by a constant #

theorem asymptotics.is_O_with_const_mul_self {Ξ± : Type u_1} {R : Type u_12} (c : R) (f : Ξ± β R) (l : filter Ξ±) :
(Ξ» (x : Ξ±), c * f x) f
theorem asymptotics.is_O_const_mul_self {Ξ± : Type u_1} {R : Type u_12} (c : R) (f : Ξ± β R) (l : filter Ξ±) :
(Ξ» (x : Ξ±), c * f x) =O[l] f
theorem asymptotics.is_O_with.const_mul_left {Ξ± : Type u_1} {F : Type u_4} {R : Type u_12} [has_norm F] {c : β} {g : Ξ± β F} {l : filter Ξ±} {f : Ξ± β R} (h : g) (c' : R) :
asymptotics.is_O_with (β₯c'β₯ * c) l (Ξ» (x : Ξ±), c' * f x) g
theorem asymptotics.is_O.const_mul_left {Ξ± : Type u_1} {F : Type u_4} {R : Type u_12} [has_norm F] {g : Ξ± β F} {l : filter Ξ±} {f : Ξ± β R} (h : f =O[l] g) (c' : R) :
(Ξ» (x : Ξ±), c' * f x) =O[l] g
theorem asymptotics.is_O_with_self_const_mul' {Ξ± : Type u_1} {R : Type u_12} (u : RΛ£) (f : Ξ± β R) (l : filter Ξ±) :
(Ξ» (x : Ξ±), βu * f x)
theorem asymptotics.is_O_with_self_const_mul {Ξ± : Type u_1} {π : Type u_14} [normed_field π] (c : π) (hc : c β  0) (f : Ξ± β π) (l : filter Ξ±) :
(Ξ» (x : Ξ±), c * f x)
theorem asymptotics.is_O_self_const_mul' {Ξ± : Type u_1} {R : Type u_12} {c : R} (hc : is_unit c) (f : Ξ± β R) (l : filter Ξ±) :
f =O[l] Ξ» (x : Ξ±), c * f x
theorem asymptotics.is_O_self_const_mul {Ξ± : Type u_1} {π : Type u_14} [normed_field π] (c : π) (hc : c β  0) (f : Ξ± β π) (l : filter Ξ±) :
f =O[l] Ξ» (x : Ξ±), c * f x
theorem asymptotics.is_O_const_mul_left_iff' {Ξ± : Type u_1} {F : Type u_4} {R : Type u_12} [has_norm F] {g : Ξ± β F} {l : filter Ξ±} {f : Ξ± β R} {c : R} (hc : is_unit c) :
(Ξ» (x : Ξ±), c * f x) =O[l] g β f =O[l] g
theorem asymptotics.is_O_const_mul_left_iff {Ξ± : Type u_1} {F : Type u_4} {π : Type u_14} [has_norm F] [normed_field π] {g : Ξ± β F} {l : filter Ξ±} {f : Ξ± β π} {c : π} (hc : c β  0) :
(Ξ» (x : Ξ±), c * f x) =O[l] g β f =O[l] g
theorem asymptotics.is_o.const_mul_left {Ξ± : Type u_1} {F : Type u_4} {R : Type u_12} [has_norm F] {g : Ξ± β F} {l : filter Ξ±} {f : Ξ± β R} (h : f =o[l] g) (c : R) :
(Ξ» (x : Ξ±), c * f x) =o[l] g
theorem asymptotics.is_o_const_mul_left_iff' {Ξ± : Type u_1} {F : Type u_4} {R : Type u_12} [has_norm F] {g : Ξ± β F} {l : filter Ξ±} {f : Ξ± β R} {c : R} (hc : is_unit c) :
(Ξ» (x : Ξ±), c * f x) =o[l] g β f =o[l] g
theorem asymptotics.is_o_const_mul_left_iff {Ξ± : Type u_1} {F : Type u_4} {π : Type u_14} [has_norm F] [normed_field π] {g : Ξ± β F} {l : filter Ξ±} {f : Ξ± β π} {c : π} (hc : c β  0) :
(Ξ» (x : Ξ±), c * f x) =o[l] g β f =o[l] g
theorem asymptotics.is_O_with.of_const_mul_right {Ξ± : Type u_1} {E : Type u_3} {R : Type u_12} [has_norm E] {c' : β} {f : Ξ± β E} {l : filter Ξ±} {g : Ξ± β R} {c : R} (hc' : 0 β€ c') (h : f (Ξ» (x : Ξ±), c * g x)) :
theorem asymptotics.is_O.of_const_mul_right {Ξ± : Type u_1} {E : Type u_3} {R : Type u_12} [has_norm E] {f : Ξ± β E} {l : filter Ξ±} {g : Ξ± β R} {c : R} (h : f =O[l] Ξ» (x : Ξ±), c * g x) :
f =O[l] g
theorem asymptotics.is_O_with.const_mul_right' {Ξ± : Type u_1} {E : Type u_3} {R : Type u_12} [has_norm E] {f : Ξ± β E} {l : filter Ξ±} {g : Ξ± β R} {u : RΛ£} {c' : β} (hc' : 0 β€ c') (h : f g) :
l f (Ξ» (x : Ξ±), βu * g x)
theorem asymptotics.is_O_with.const_mul_right {Ξ± : Type u_1} {E : Type u_3} {π : Type u_14} [has_norm E] [normed_field π] {f : Ξ± β E} {l : filter Ξ±} {g : Ξ± β π} {c : π} (hc : c β  0) {c' : β} (hc' : 0 β€ c') (h : f g) :
l f (Ξ» (x : Ξ±), c * g x)
theorem asymptotics.is_O.const_mul_right' {Ξ± : Type u_1} {E : Type u_3} {R : Type u_12} [has_norm E] {f : Ξ± β E} {l : filter Ξ±} {g : Ξ± β R} {c : R} (hc : is_unit c) (h : f =O[l] g) :
f =O[l] Ξ» (x : Ξ±), c * g x
theorem asymptotics.is_O.const_mul_right {Ξ± : Type u_1} {E : Type u_3} {π : Type u_14} [has_norm E] [normed_field π] {f : Ξ± β E} {l : filter Ξ±} {g : Ξ± β π} {c : π} (hc : c β  0) (h : f =O[l] g) :
f =O[l] Ξ» (x : Ξ±), c * g x
theorem asymptotics.is_O_const_mul_right_iff' {Ξ± : Type u_1} {E : Type u_3} {R : Type u_12} [has_norm E] {f : Ξ± β E} {l : filter Ξ±} {g : Ξ± β R} {c : R} (hc : is_unit c) :
(f =O[l] Ξ» (x : Ξ±), c * g x) β f =O[l] g
theorem asymptotics.is_O_const_mul_right_iff {Ξ± : Type u_1} {E : Type u_3} {π : Type u_14} [has_norm E] [normed_field π] {f : Ξ± β E} {l : filter Ξ±} {g : Ξ± β π} {c : π} (hc : c β  0) :
(f =O[l] Ξ» (x : Ξ±), c * g x) β f =O[l] g
theorem asymptotics.is_o.of_const_mul_right {Ξ± : Type u_1} {E : Type u_3} {R : Type u_12} [has_norm E] {f : Ξ± β E} {l : filter Ξ±} {g : Ξ± β R} {c : R} (h : f =o[l] Ξ» (x : Ξ±), c * g x) :
f =o[l] g
theorem asymptotics.is_o.const_mul_right' {Ξ± : Type u_1} {E : Type u_3} {R : Type u_12} [has_norm E] {f : Ξ± β E} {l : filter Ξ±} {g : Ξ± β R} {c : R} (hc : is_unit c) (h : f =o[l] g) :
f =o[l] Ξ» (x : Ξ±), c * g x
theorem asymptotics.is_o.const_mul_right {Ξ± : Type u_1} {E : Type u_3} {π : Type u_14} [has_norm E] [normed_field π] {f : Ξ± β E} {l : filter Ξ±} {g : Ξ± β π} {c : π} (hc : c β  0) (h : f =o[l] g) :
f =o[l] Ξ» (x : Ξ±), c * g x
theorem asymptotics.is_o_const_mul_right_iff' {Ξ± : Type u_1} {E : Type u_3} {R : Type u_12} [has_norm E] {f : Ξ± β E} {l : filter Ξ±} {g : Ξ± β R} {c : R} (hc : is_unit c) :
(f =o[l] Ξ» (x : Ξ±), c * g x) β f =o[l] g
theorem asymptotics.is_o_const_mul_right_iff {Ξ± : Type u_1} {E : Type u_3} {π : Type u_14} [has_norm E] [normed_field π] {f : Ξ± β E} {l : filter Ξ±} {g : Ξ± β π} {c : π} (hc : c β  0) :
(f =o[l] Ξ» (x : Ξ±), c * g x) β f =o[l] g

### Multiplication #

theorem asymptotics.is_O_with.mul {Ξ± : Type u_1} {R : Type u_12} {π : Type u_14} [normed_field π] {l : filter Ξ±} {fβ fβ : Ξ± β R} {gβ gβ : Ξ± β π} {cβ cβ : β} (hβ : l fβ gβ) (hβ : l fβ gβ) :
asymptotics.is_O_with (cβ * cβ) l (Ξ» (x : Ξ±), fβ x * fβ x) (Ξ» (x : Ξ±), gβ x * gβ x)
theorem asymptotics.is_O.mul {Ξ± : Type u_1} {R : Type u_12} {π : Type u_14} [normed_field π] {l : filter Ξ±} {fβ fβ : Ξ± β R} {gβ gβ : Ξ± β π} (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.mul_is_o {Ξ± : Type u_1} {R : Type u_12} {π : Type u_14} [normed_field π] {l : filter Ξ±} {fβ fβ : Ξ± β R} {gβ gβ : Ξ± β π} (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.mul_is_O {Ξ± : Type u_1} {R : Type u_12} {π : Type u_14} [normed_field π] {l : filter Ξ±} {fβ fβ : Ξ± β R} {gβ gβ : Ξ± β π} (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.mul {Ξ± : Type u_1} {R : Type u_12} {π : Type u_14} [normed_field π] {l : filter Ξ±} {fβ fβ : Ξ± β R} {gβ gβ : Ξ± β π} (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_with.pow' {Ξ± : Type u_1} {R : Type u_12} {π : Type u_14} [normed_field π] {c : β} {l : filter Ξ±} {f : Ξ± β R} {g : Ξ± β π} (h : g) (n : β) :
asymptotics.is_O_with (n.cases_on β₯1β₯ (Ξ» (n : β), c ^ (n + 1))) l (Ξ» (x : Ξ±), f x ^ n) (Ξ» (x : Ξ±), g x ^ n)
theorem asymptotics.is_O_with.pow {Ξ± : Type u_1} {R : Type u_12} {π : Type u_14} [normed_field π] {c : β} {l : filter Ξ±} {f : Ξ± β R} {g : Ξ± β π} (h : g) (n : β) :
asymptotics.is_O_with (c ^ n) l (Ξ» (x : Ξ±), f x ^ n) (Ξ» (x : Ξ±), g x ^ n)
theorem asymptotics.is_O_with.of_pow {Ξ± : Type u_1} {R : Type u_12} {π : Type u_14} [normed_field π] {c c' : β} {l : filter Ξ±} {n : β} {f : Ξ± β π} {g : Ξ± β R} (h : (f ^ n) (g ^ n)) (hn : n β  0) (hc : c β€ c' ^ n) (hc' : 0 β€ c') :
f g
theorem asymptotics.is_O.pow {Ξ± : Type u_1} {R : Type u_12} {π : Type u_14} [normed_field π] {l : filter Ξ±} {f : Ξ± β R} {g : Ξ± β π} (h : f =O[l] g) (n : β) :
(Ξ» (x : Ξ±), f x ^ n) =O[l] Ξ» (x : Ξ±), g x ^ n
theorem asymptotics.is_O.of_pow {Ξ± : Type u_1} {R : Type u_12} {π : Type u_14} [normed_field π] {l : filter Ξ±} {f : Ξ± β π} {g : Ξ± β R} {n : β} (hn : n β  0) (h : (f ^ n) =O[l] (g ^ n)) :
f =O[l] g
theorem asymptotics.is_o.pow {Ξ± : Type u_1} {R : Type u_12} {π : Type u_14} [normed_field π] {l : filter Ξ±} {f : Ξ± β R} {g : Ξ± β π} (h : f =o[l] g) {n : β} (hn : 0 < n) :
(Ξ» (x : Ξ±), f x ^ n) =o[l] Ξ» (x : Ξ±), g x ^ n
theorem asymptotics.is_o.of_pow {Ξ± : Type u_1} {R : Type u_12} {π : Type u_14} [normed_field π] {l : filter Ξ±} {f : Ξ± β π} {g : Ξ± β R} {n : β} (h : (f ^ n) =o[l] (g ^ n)) (hn : n β  0) :
f =o[l] g

### Inverse #

theorem asymptotics.is_O_with.inv_rev {Ξ± : Type u_1} {π : Type u_14} {π' : Type u_15} [normed_field π] [normed_field π'] {c : β} {l : filter Ξ±} {f : Ξ± β π} {g : Ξ± β π'} (h : g) (hβ : βαΆ  (x : Ξ±) in l, f x = 0 β g x = 0) :
(Ξ» (x : Ξ±), (g x)β»ΒΉ) (Ξ» (x : Ξ±), (f x)β»ΒΉ)
theorem asymptotics.is_O.inv_rev {Ξ± : Type u_1} {π : Type u_14} {π' : Type u_15} [normed_field π] [normed_field π'] {l : filter Ξ±} {f : Ξ± β π} {g : Ξ± β π'} (h : f =O[l] g) (hβ : βαΆ  (x : Ξ±) in l, f x = 0 β g x = 0) :
(Ξ» (x : Ξ±), (g x)β»ΒΉ) =O[l] Ξ» (x : Ξ±), (f x)β»ΒΉ
theorem asymptotics.is_o.inv_rev {Ξ± : Type u_1} {π : Type u_14} {π' : Type u_15} [normed_field π] [normed_field π'] {l : filter Ξ±} {f : Ξ± β π} {g : Ξ± β π'} (h : f =o[l] g) (hβ : βαΆ  (x : Ξ±) in l, f x = 0 β g x = 0) :
(Ξ» (x : Ξ±), (g x)β»ΒΉ) =o[l] Ξ» (x : Ξ±), (f x)β»ΒΉ

### Scalar multiplication #

theorem asymptotics.is_O_with.const_smul_left {Ξ± : Type u_1} {F : Type u_4} {E' : Type u_6} {π : Type u_14} [has_norm F] [normed_field π] {c : β} {g : Ξ± β F} {f' : Ξ± β E'} {l : filter Ξ±} [normed_space π E'] (h : f' g) (c' : π) :
asymptotics.is_O_with (β₯c'β₯ * c) l (Ξ» (x : Ξ±), c' β’ f' x) g
theorem asymptotics.is_O.const_smul_left {Ξ± : Type u_1} {F : Type u_4} {E' : Type u_6} {π : Type u_14} [has_norm F] [normed_field π] {g : Ξ± β F} {f' : Ξ± β E'} {l : filter Ξ±} [normed_space π E'] (h : f' =O[l] g) (c : π) :
(c β’ f') =O[l] g
theorem asymptotics.is_o.const_smul_left {Ξ± : Type u_1} {F : Type u_4} {E' : Type u_6} {π : Type u_14} [has_norm F] [normed_field π] {g : Ξ± β F} {f' : Ξ± β E'} {l : filter Ξ±} [normed_space π E'] (h : f' =o[l] g) (c : π) :
(c β’ f') =o[l] g
theorem asymptotics.is_O_const_smul_left {Ξ± : Type u_1} {F : Type u_4} {E' : Type u_6} {π : Type u_14} [has_norm F] [normed_field π] {g : Ξ± β F} {f' : Ξ± β E'} {l : filter Ξ±} [normed_space π E'] {c : π} (hc : c β  0) :
(Ξ» (x : Ξ±), c β’ f' x) =O[l] g β f' =O[l] g
theorem asymptotics.is_o_const_smul_left {Ξ± : Type u_1} {F : Type u_4} {E' : Type u_6} {π : Type u_14} [has_norm F] [normed_field π] {g : Ξ± β F} {f' : Ξ± β E'} {l : filter Ξ±} [normed_space π E'] {c : π} (hc : c β  0) :
(Ξ» (x : Ξ±), c β’ f' x) =o[l] g β f' =o[l] g
theorem asymptotics.is_O_const_smul_right {Ξ± : Type u_1} {E : Type u_3} {E' : Type u_6} {π : Type u_14} [has_norm E] [normed_field π] {f : Ξ± β E} {f' : Ξ± β E'} {l : filter Ξ±} [normed_space π E'] {c : π} (hc : c β  0) :
(f =O[l] Ξ» (x : Ξ±), c β’ f' x) β f =O[l] f'
theorem asymptotics.is_o_const_smul_right {Ξ± : Type u_1} {E : Type u_3} {E' : Type u_6} {π : Type u_14} [has_norm E] [normed_field π] {f : Ξ± β E} {f' : Ξ± β E'} {l : filter Ξ±} [normed_space π E'] {c : π} (hc : c β  0) :
(f =o[l] Ξ» (x : Ξ±), c β’ f' x) β f =o[l] f'
theorem asymptotics.is_O_with.smul {Ξ± : Type u_1} {E' : Type u_6} {F' : Type u_7} {π : Type u_14} {π' : Type u_15} [normed_field π] [normed_field π'] {c c' : β} {f' : Ξ± β E'} {g' : Ξ± β F'} {l : filter Ξ±} [normed_space π E'] [normed_space π' F'] {kβ : Ξ± β π} {kβ : Ξ± β π'} (hβ : kβ kβ) (hβ : f' g') :
asymptotics.is_O_with (c * c') l (Ξ» (x : Ξ±), kβ x β’ f' x) (Ξ» (x : Ξ±), kβ x β’ g' x)
theorem asymptotics.is_O.smul {Ξ± : Type u_1} {E' : Type u_6} {F' : Type u_7} {π : Type u_14} {π' : Type u_15} [normed_field π] [normed_field π'] {f' : Ξ± β E'} {g' : Ξ± β F'} {l : filter Ξ±} [normed_space π E'] [normed_space π' F'] {kβ : Ξ± β π} {kβ : Ξ± β π'} (hβ : kβ =O[l] kβ) (hβ : f' =O[l] g') :
(Ξ» (x : Ξ±), kβ x β’ f' x) =O[l] Ξ» (x : Ξ±), kβ x β’ g' x
theorem asymptotics.is_O.smul_is_o {Ξ± : Type u_1} {E' : Type u_6} {F' : Type u_7} {π : Type u_14} {π' : Type u_15} [normed_field π] [normed_field π'] {f' : Ξ± β E'} {g' : Ξ± β F'} {l : filter Ξ±} [normed_space π E'] [normed_space π' F'] {kβ : Ξ± β π} {kβ : Ξ± β π'} (hβ : kβ =O[l] kβ) (hβ : f' =o[l] g') :
(Ξ» (x : Ξ±), kβ x β’ f' x) =o[l] Ξ» (x : Ξ±), kβ x β’ g' x
theorem asymptotics.is_o.smul_is_O {Ξ± : Type u_1} {E' : Type u_6} {F' : Type u_7} {π : Type u_14} {π' : Type u_15} [normed_field π] [normed_field π'] {f' : Ξ± β E'} {g' : Ξ± β F'} {l : filter Ξ±} [normed_space π E'] [normed_space π' F'] {kβ : Ξ± β π} {kβ : Ξ± β π'} (hβ : kβ =o[l] kβ) (hβ : f' =O[l] g') :
(Ξ» (x : Ξ±), kβ x β’ f' x) =o[l] Ξ» (x : Ξ±), kβ x β’ g' x
theorem asymptotics.is_o.smul {Ξ± : Type u_1} {E' : Type u_6} {F' : Type u_7} {π : Type u_14} {π' : Type u_15} [normed_field π] [normed_field π'] {f' : Ξ± β E'} {g' : Ξ± β F'} {l : filter Ξ±} [normed_space π E'] [normed_space π' F'] {kβ : Ξ± β π} {kβ : Ξ± β π'} (hβ : kβ =o[l] kβ) (hβ : f' =o[l] g') :
(Ξ» (x : Ξ±), kβ x β’ f' x) =o[l] Ξ» (x : Ξ±), kβ x β’ g' x

### Sum #

theorem asymptotics.is_O_with.sum {Ξ± : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] {g : Ξ± β F} {l : filter Ξ±} {ΞΉ : Type u_16} {A : ΞΉ β Ξ± β E'} {C : ΞΉ β β} {s : finset ΞΉ} (h : β (i : ΞΉ), i β s β l (A i) g) :
asymptotics.is_O_with (s.sum (Ξ» (i : ΞΉ), C i)) l (Ξ» (x : Ξ±), s.sum (Ξ» (i : ΞΉ), A i x)) g
theorem asymptotics.is_O.sum {Ξ± : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] {g : Ξ± β F} {l : filter Ξ±} {ΞΉ : Type u_16} {A : ΞΉ β Ξ± β E'} {s : finset ΞΉ} (h : β (i : ΞΉ), i β s β A i =O[l] g) :
(Ξ» (x : Ξ±), s.sum (Ξ» (i : ΞΉ), A i x)) =O[l] g
theorem asymptotics.is_o.sum {Ξ± : Type u_1} {E' : Type u_6} {F' : Type u_7} {g' : Ξ± β F'} {l : filter Ξ±} {ΞΉ : Type u_16} {A : ΞΉ β Ξ± β E'} {s : finset ΞΉ} (h : β (i : ΞΉ), i β s β A i =o[l] g') :
(Ξ» (x : Ξ±), s.sum (Ξ» (i : ΞΉ), A i x)) =o[l] g'

### Relation between `f = o(g)` and `f / g β 0`#

theorem asymptotics.is_o.tendsto_div_nhds_zero {Ξ± : Type u_1} {π : Type u_14} [normed_field π] {l : filter Ξ±} {f g : Ξ± β π} (h : f =o[l] g) :
filter.tendsto (Ξ» (x : Ξ±), f x / g x) l (nhds 0)
theorem asymptotics.is_o.tendsto_inv_smul_nhds_zero {Ξ± : Type u_1} {E' : Type u_6} {π : Type u_14} [normed_field π] [normed_space π E'] {f : Ξ± β E'} {g : Ξ± β π} {l : filter Ξ±} (h : f =o[l] g) :
filter.tendsto (Ξ» (x : Ξ±), (g x)β»ΒΉ β’ f x) l (nhds 0)
theorem asymptotics.is_o_iff_tendsto' {Ξ± : Type u_1} {π : Type u_14} [normed_field π] {l : filter Ξ±} {f g : Ξ± β π} (hgf : βαΆ  (x : Ξ±) in l, g x = 0 β f x = 0) :
f =o[l] g β filter.tendsto (Ξ» (x : Ξ±), f x / g x) l (nhds 0)
theorem asymptotics.is_o_iff_tendsto {Ξ± : Type u_1} {π : Type u_14} [normed_field π] {l : filter Ξ±} {f g : Ξ± β π} (hgf : β (x : Ξ±), g x = 0 β f x = 0) :
f =o[l] g β filter.tendsto (Ξ» (x : Ξ±), f x / g x) l (nhds 0)
theorem asymptotics.is_o_of_tendsto' {Ξ± : Type u_1} {π : Type u_14} [normed_field π] {l : filter Ξ±} {f g : Ξ± β π} (hgf : βαΆ  (x : Ξ±) in l, g x = 0 β f x = 0) :
filter.tendsto (Ξ» (x : Ξ±), f x / g x) l (nhds 0) β f =o[l] g

Alias of the reverse direction of `asymptotics.is_o_iff_tendsto'`.

theorem asymptotics.is_o_of_tendsto {Ξ± : Type u_1} {π : Type u_14} [normed_field π] {l : filter Ξ±} {f g : Ξ± β π} (hgf : β (x : Ξ±), g x = 0 β f x = 0) :
filter.tendsto (Ξ» (x : Ξ±), f x / g x) l (nhds 0) β f =o[l] g

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

theorem asymptotics.is_o_const_left_of_ne {Ξ± : Type u_1}