mathlib3 documentation

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

asymptotics.is_O_with c l f g = ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

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 α} :

asymptotics.is_O_with c l f 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 α} :

asymptotics.is_O_with c l f 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‖) → asymptotics.is_O_with c l f 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

f =O[l] g = ∃ (c : ℝ), asymptotics.is_O_with c l f g

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 : ℝ), asymptotics.is_O_with c l f 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

f =o[l] g = ∀ ⦃c : ℝ⦄, 0 < c → asymptotics.is_O_with c l f g

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 → asymptotics.is_O_with c l f 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 → asymptotics.is_O_with c l f 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 → asymptotics.is_O_with c l f 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) :

asymptotics.is_O_with c l f 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 : asymptotics.is_O_with c l f 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) :

asymptotics.is_O_with 1 l f 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 : ℝ), asymptotics.is_O_with c l f g)

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

asymptotics.is_O_with c' l f g'

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

∃ (c' : ℝ) (H : 0 < c'), asymptotics.is_O_with c' l f g'

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

∃ (c : ℝ) (H : 0 < c), asymptotics.is_O_with c l f g'

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

∃ (c' : ℝ) (H : 0 ≤ c'), asymptotics.is_O_with c' l f g'

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

∃ (c : ℝ) (H : 0 ≤ c), asymptotics.is_O_with c l f g'

theorem asymptotics.is_O_iff_eventually_is_O_with {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] [seminormed_add_comm_group F'] {f : α → E} {g' : α → F'} {l : filter α} :

f =O[l] g' ↔ ∀ᶠ (c : ℝ) in filter.at_top , asymptotics.is_O_with c l f 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] [seminormed_add_comm_group F'] {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] [seminormed_add_comm_group F'] {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) :

asymptotics.is_O_with c⁻¹ l f 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] [seminormed_add_comm_group F'] {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] [seminormed_add_comm_group E'] {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} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] {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} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] {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₂) :

asymptotics.is_O_with c₁ l f₁ g₁ ↔ asymptotics.is_O_with c₂ 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 : asymptotics.is_O_with c₁ l f₁ g₁) (hc : c₁ = c₂) (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) :

asymptotics.is_O_with c₂ 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 : asymptotics.is_O_with c₁ l f₁ g₁) (hc : c₁ = c₂) (hf : ∀ (x : α), f₁ x = f₂ x) (hg : ∀ (x : α), g₁ x = g₂ x) :

asymptotics.is_O_with c₂ 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 : asymptotics.is_O_with c l f₁ g) (hf : ∀ (x : α), f₁ x = f₂ x) :

asymptotics.is_O_with c l 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 : asymptotics.is_O_with c l f g₁) (hg : ∀ (x : α), g₁ x = g₂ x) :

asymptotics.is_O_with c l f 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 : asymptotics.is_O_with c₁ l f g) (hc : c₁ = c₂) :

asymptotics.is_O_with 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 : asymptotics.is_O_with c l f g) {k : β → α} {l' : filter β} (hk : filter.tendsto k l' l) :

asymptotics.is_O_with c 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 : filter.tendsto k 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 : filter.tendsto k 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 β} :

asymptotics.is_O_with c (filter.map k l) f g ↔ asymptotics.is_O_with c l (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[filter.map k 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[filter.map k 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 : asymptotics.is_O_with c l' f g) (hl : l ≤ l') :

asymptotics.is_O_with c l f 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 : asymptotics.is_O_with c l f g) (hgk : asymptotics.is_O_with c' l g k) (hc : 0 ≤ c) :

asymptotics.is_O_with (c * c') l f k

@[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] [seminormed_add_comm_group 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.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 : asymptotics.is_O_with c l g 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] [seminormed_add_comm_group 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.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 : asymptotics.is_O_with c l f 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] [seminormed_add_comm_group F'] {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] [seminormed_add_comm_group F'] {l : filter α} {f : α → E} {g : α → F'} {k : α → G} (hfg : ∀ᶠ (x : α) in l, ‖f x‖ ≤ ‖g x‖) (hgk : g =O[l] k) :

f =O[l] k

theorem filter.eventually.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‖) :

asymptotics.is_O_with c l f 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‖) :

asymptotics.is_O_with 1 l f 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 α) :

asymptotics.is_O_with 1 l f 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 : asymptotics.is_O_with c l f g) (hgk : ∀ (x : α), ‖g x‖ ≤ ‖k x‖) (hc : 0 ≤ c) :

asymptotics.is_O_with c l f 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] [seminormed_add_comm_group F'] {f : α → E} {k : α → G} {g' : α → F'} {l : filter α} (hfg : f =O[l] g') (hgk : ∀ (x : α), ‖g' x‖ ≤ ‖k x‖) :

f =O[l] k

theorem asymptotics.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} [seminormed_add_comm_group E'] {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} [normed_add_comm_group E''] {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} [seminormed_add_comm_group F'] [normed_add_comm_group E''] {g' : α → F'} {f'' : α → E''} {l : filter α} (h : f'' =O[l] g') (hf : ∃ᶠ (x : α) in l, f'' x ≠ 0) :

¬g' =o[l] f''

theorem asymptotics.is_o.not_is_O {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} [seminormed_add_comm_group F'] [normed_add_comm_group E''] {g' : α → F'} {f'' : α → E''} {l : filter α} (h : f'' =o[l] g') (hf : ∃ᶠ (x : α) in l, f'' x ≠ 0) :

¬g' =O[l] f''

@[simp]

theorem asymptotics.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) :

asymptotics.is_O_with c ⊥ 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 : α} :

asymptotics.is_O_with c (has_pure.pure x) f 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 : asymptotics.is_O_with c l f g) (h' : asymptotics.is_O_with c l' f g) :

asymptotics.is_O_with c (l ⊔ l') f g

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

asymptotics.is_O_with (linear_order.max c c') (l ⊔ l') f g'

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

f =O[l ⊔ l'] g'

theorem asymptotics.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] [seminormed_add_comm_group F'] {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] [topological_space α] {x : α} {s : set α} {C : ℝ} {g : α → E} {g' : α → F} (h : ‖g x‖ ≤ C * ‖g' x‖) :

asymptotics.is_O_with C (nhds_within x (has_insert.insert x s)) g g' ↔ asymptotics.is_O_with C (nhds_within x 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] [topological_space α] {x : α} {s : set α} {C : ℝ} {g : α → E} {g' : α → F} (h1 : asymptotics.is_O_with C (nhds_within x s) g g') (h2 : ‖g x‖ ≤ C * ‖g' x‖) :

asymptotics.is_O_with C (nhds_within x (has_insert.insert x s)) g g'

theorem asymptotics.is_o_insert {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] [topological_space α] {x : α} {s : set α} {g : α → E'} {g' : α → F'} (h : g x = 0) :

g =o[nhds_within x (has_insert.insert x s)] g' ↔ g =o[nhds_within x s] g'

theorem asymptotics.is_o.insert {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] [topological_space α] {x : α} {s : set α} {g : α → E'} {g' : α → F'} (h1 : g =o[nhds_within x s] g') (h2 : g x = 0) :

g =o[nhds_within x (has_insert.insert x 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] [seminormed_add_comm_group F'] {c : ℝ} {f : α → E} {g' : α → F'} {l : filter α} :

asymptotics.is_O_with c l f (λ (x : α), ‖g' x‖) ↔ asymptotics.is_O_with c l f 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 : α → ℝ} :

asymptotics.is_O_with c l f (λ (x : α), |u x|) ↔ asymptotics.is_O_with c l f u

theorem asymptotics.is_O_with.norm_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] [seminormed_add_comm_group F'] {c : ℝ} {f : α → E} {g' : α → F'} {l : filter α} :

asymptotics.is_O_with c l f g' → asymptotics.is_O_with c l f (λ (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] [seminormed_add_comm_group F'] {c : ℝ} {f : α → E} {g' : α → F'} {l : filter α} :

asymptotics.is_O_with c l f (λ (x : α), ‖g' x‖) → asymptotics.is_O_with c l f 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 : α → ℝ} :

asymptotics.is_O_with c l f (λ (x : α), |u x|) → asymptotics.is_O_with c l f 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 : α → ℝ} :

asymptotics.is_O_with c l f u → asymptotics.is_O_with c l f (λ (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] [seminormed_add_comm_group F'] {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] [seminormed_add_comm_group F'] {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] [seminormed_add_comm_group F'] {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] [seminormed_add_comm_group F'] {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] [seminormed_add_comm_group F'] {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] [seminormed_add_comm_group F'] {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] [seminormed_add_comm_group E'] {c : ℝ} {g : α → F} {f' : α → E'} {l : filter α} :

asymptotics.is_O_with c l (λ (x : α), ‖f' x‖) g ↔ asymptotics.is_O_with c l 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 : α → ℝ} :

asymptotics.is_O_with c l (λ (x : α), |u x|) g ↔ asymptotics.is_O_with c l u g

theorem asymptotics.is_O_with.of_norm_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [seminormed_add_comm_group E'] {c : ℝ} {g : α → F} {f' : α → E'} {l : filter α} :

asymptotics.is_O_with c l (λ (x : α), ‖f' x‖) g → asymptotics.is_O_with c l 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] [seminormed_add_comm_group E'] {c : ℝ} {g : α → F} {f' : α → E'} {l : filter α} :

asymptotics.is_O_with c l f' g → asymptotics.is_O_with c l (λ (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 : α → ℝ} :

asymptotics.is_O_with c l (λ (x : α), |u x|) g → asymptotics.is_O_with c l u 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 : α → ℝ} :

asymptotics.is_O_with c l u g → asymptotics.is_O_with c l (λ (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] [seminormed_add_comm_group E'] {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] [seminormed_add_comm_group E'] {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] [seminormed_add_comm_group E'] {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] [seminormed_add_comm_group E'] {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] [seminormed_add_comm_group E'] {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] [seminormed_add_comm_group E'] {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} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] {c : ℝ} {f' : α → E'} {g' : α → F'} {l : filter α} :

asymptotics.is_O_with c l (λ (x : α), ‖f' x‖) (λ (x : α), ‖g' x‖) ↔ asymptotics.is_O_with c l f' g'

theorem asymptotics.is_O_with_abs_abs {α : Type u_1} {c : ℝ} {l : filter α} {u v : α → ℝ} :

asymptotics.is_O_with c l (λ (x : α), |u x|) (λ (x : α), |v x|) ↔ asymptotics.is_O_with c l u v

theorem asymptotics.is_O_with.of_norm_norm {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] {c : ℝ} {f' : α → E'} {g' : α → F'} {l : filter α} :

asymptotics.is_O_with c l (λ (x : α), ‖f' x‖) (λ (x : α), ‖g' x‖) → asymptotics.is_O_with c l 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} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] {c : ℝ} {f' : α → E'} {g' : α → F'} {l : filter α} :

asymptotics.is_O_with c l f' g' → asymptotics.is_O_with c l (λ (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 : α → ℝ} :

asymptotics.is_O_with c l (λ (x : α), |u x|) (λ (x : α), |v x|) → asymptotics.is_O_with c l u 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 : α → ℝ} :

asymptotics.is_O_with c l u v → asymptotics.is_O_with c l (λ (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} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] {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} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] {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} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] {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} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] {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} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] {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} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] {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] [seminormed_add_comm_group F'] {c : ℝ} {f : α → E} {g' : α → F'} {l : filter α} :

asymptotics.is_O_with c l f (λ (x : α), -g' x) ↔ asymptotics.is_O_with c l f g'

theorem asymptotics.is_O_with.neg_right {α : Type u_1} {E : Type u_3} {F' : Type u_7} [has_norm E] [seminormed_add_comm_group F'] {c : ℝ} {f : α → E} {g' : α → F'} {l : filter α} :

asymptotics.is_O_with c l f g' → asymptotics.is_O_with c l f (λ (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] [seminormed_add_comm_group F'] {c : ℝ} {f : α → E} {g' : α → F'} {l : filter α} :

asymptotics.is_O_with c l f (λ (x : α), -g' x) → asymptotics.is_O_with c l f 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] [seminormed_add_comm_group F'] {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] [seminormed_add_comm_group F'] {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] [seminormed_add_comm_group F'] {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] [seminormed_add_comm_group F'] {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] [seminormed_add_comm_group F'] {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] [seminormed_add_comm_group F'] {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] [seminormed_add_comm_group E'] {c : ℝ} {g : α → F} {f' : α → E'} {l : filter α} :

asymptotics.is_O_with c l (λ (x : α), -f' x) g ↔ asymptotics.is_O_with c l f' g

theorem asymptotics.is_O_with.of_neg_left {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [seminormed_add_comm_group E'] {c : ℝ} {g : α → F} {f' : α → E'} {l : filter α} :

asymptotics.is_O_with c l (λ (x : α), -f' x) g → asymptotics.is_O_with c l 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] [seminormed_add_comm_group E'] {c : ℝ} {g : α → F} {f' : α → E'} {l : filter α} :

asymptotics.is_O_with c l f' g → asymptotics.is_O_with c l (λ (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] [seminormed_add_comm_group E'] {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] [seminormed_add_comm_group E'] {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] [seminormed_add_comm_group E'] {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] [seminormed_add_comm_group E'] {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] [seminormed_add_comm_group E'] {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} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] {f' : α → E'} {g' : α → F'} {l : filter α} :

asymptotics.is_O_with 1 l f' (λ (x : α), (f' x, g' x))

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

asymptotics.is_O_with 1 l g' (λ (x : α), (f' x, g' x))

theorem asymptotics.is_O_fst_prod {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] {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} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] {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} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] {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} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] {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] [seminormed_add_comm_group F'] [seminormed_add_comm_group G'] {c : ℝ} {f : α → E} {g' : α → F'} (k' : α → G') {l : filter α} (h : asymptotics.is_O_with c l f g') (hc : 0 ≤ c) :

asymptotics.is_O_with c l f (λ (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] [seminormed_add_comm_group F'] [seminormed_add_comm_group G'] {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] [seminormed_add_comm_group F'] [seminormed_add_comm_group G'] {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] [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] {c : ℝ} {f : α → E} (f' : α → E') {g' : α → F'} {l : filter α} (h : asymptotics.is_O_with c l f g') (hc : 0 ≤ c) :

asymptotics.is_O_with c l f (λ (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] [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] {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] [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] {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} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] [seminormed_add_comm_group G'] {c : ℝ} {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : filter α} (hf : asymptotics.is_O_with c l f' k') (hg : asymptotics.is_O_with c l g' k') :

asymptotics.is_O_with c l (λ (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} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] [seminormed_add_comm_group G'] {c c' : ℝ} {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : filter α} (hf : asymptotics.is_O_with c l f' k') (hg : asymptotics.is_O_with c' l g' k') :

asymptotics.is_O_with (linear_order.max c c') l (λ (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} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] [seminormed_add_comm_group G'] {c : ℝ} {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : filter α} (h : asymptotics.is_O_with c l (λ (x : α), (f' x, g' x)) k') :

asymptotics.is_O_with c l 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} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] [seminormed_add_comm_group G'] {c : ℝ} {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : filter α} (h : asymptotics.is_O_with c l (λ (x : α), (f' x, g' x)) k') :

asymptotics.is_O_with c l g' k'

theorem asymptotics.is_O_with_prod_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] [seminormed_add_comm_group G'] {c : ℝ} {f' : α → E'} {g' : α → F'} {k' : α → G'} {l : filter α} :

asymptotics.is_O_with c l (λ (x : α), (f' x, g' x)) k' ↔ asymptotics.is_O_with c l f' k' ∧ asymptotics.is_O_with c l g' k'

theorem asymptotics.is_O.prod_left {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] [seminormed_add_comm_group G'] {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} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] [seminormed_add_comm_group G'] {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} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] [seminormed_add_comm_group G'] {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} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] [seminormed_add_comm_group G'] {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} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] [seminormed_add_comm_group G'] {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} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] [seminormed_add_comm_group G'] {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} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] [seminormed_add_comm_group G'] {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} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] [seminormed_add_comm_group G'] {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} [normed_add_comm_group E''] [normed_add_comm_group F''] {c : ℝ} {f'' : α → E''} {g'' : α → F''} {l : filter α} (h : asymptotics.is_O_with c l 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} [normed_add_comm_group E''] [normed_add_comm_group F''] {f'' : α → E''} {g'' : α → F''} {l : filter α} (h : f'' =O[l] g'') :

∀ᶠ (x : α) in l, g'' x = 0 → f'' x = 0

Addition and subtraction #

theorem asymptotics.is_O_with.add {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [seminormed_add_comm_group E'] {c₁ c₂ : ℝ} {g : α → F} {l : filter α} {f₁ f₂ : α → E'} (h₁ : asymptotics.is_O_with c₁ l f₁ g) (h₂ : asymptotics.is_O_with c₂ 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] [seminormed_add_comm_group E'] {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] [seminormed_add_comm_group E'] {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} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] {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] [seminormed_add_comm_group E'] {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] [seminormed_add_comm_group E'] {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] [seminormed_add_comm_group E'] {c₁ c₂ : ℝ} {g : α → F} {l : filter α} {f₁ f₂ : α → E'} (h₁ : asymptotics.is_O_with c₁ l f₁ g) (h₂ : f₂ =o[l] g) (hc : c₁ < c₂) :

asymptotics.is_O_with 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] [seminormed_add_comm_group E'] {c₁ c₂ : ℝ} {g : α → F} {l : filter α} {f₁ f₂ : α → E'} (h₁ : f₁ =o[l] g) (h₂ : asymptotics.is_O_with c₁ l f₂ g) (hc : c₁ < c₂) :

asymptotics.is_O_with 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] [seminormed_add_comm_group E'] {c₁ c₂ : ℝ} {g : α → F} {l : filter α} {f₁ f₂ : α → E'} (h₁ : asymptotics.is_O_with c₁ l f₁ g) (h₂ : asymptotics.is_O_with c₂ 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] [seminormed_add_comm_group E'] {c₁ c₂ : ℝ} {g : α → F} {l : filter α} {f₁ f₂ : α → E'} (h₁ : asymptotics.is_O_with c₁ l f₁ g) (h₂ : f₂ =o[l] g) (hc : c₁ < c₂) :

asymptotics.is_O_with 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] [seminormed_add_comm_group E'] {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] [seminormed_add_comm_group E'] {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] [seminormed_add_comm_group E'] {c : ℝ} {g : α → F} {l : filter α} {f₁ f₂ : α → E'} (h : asymptotics.is_O_with c l (λ (x : α), f₁ x - f₂ x) g) :

asymptotics.is_O_with c l (λ (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] [seminormed_add_comm_group E'] {c : ℝ} {g : α → F} {l : filter α} {f₁ f₂ : α → E'} :

asymptotics.is_O_with c l (λ (x : α), f₁ x - f₂ x) g ↔ asymptotics.is_O_with c l (λ (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] [seminormed_add_comm_group E'] {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] [seminormed_add_comm_group E'] {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] [seminormed_add_comm_group E'] {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] [seminormed_add_comm_group E'] {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] [seminormed_add_comm_group E'] {c c' : ℝ} {g : α → F} {l : filter α} {f₁ f₂ f₃ : α → E'} (h₁ : asymptotics.is_O_with c l (λ (x : α), f₁ x - f₂ x) g) (h₂ : asymptotics.is_O_with c' l (λ (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] [seminormed_add_comm_group E'] {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] [seminormed_add_comm_group E'] {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] [seminormed_add_comm_group E'] {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] [seminormed_add_comm_group E'] {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} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] (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} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] {c : ℝ} (g' : α → F') (l : filter α) (hc : 0 ≤ c) :

asymptotics.is_O_with c l (λ (x : α), 0) g'

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

asymptotics.is_O_with 0 l (λ (x : α), 0) g

theorem asymptotics.is_O_zero {α : Type u_1} {F : Type u_4} {E' : Type u_6} [has_norm F] [seminormed_add_comm_group E'] (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} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] {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} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] {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} [seminormed_add_comm_group F'] [normed_add_comm_group E''] {c : ℝ} {f'' : α → E''} {l : filter α} :

asymptotics.is_O_with c l 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} [seminormed_add_comm_group F'] [normed_add_comm_group E''] {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} [seminormed_add_comm_group F'] [normed_add_comm_group E''] {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] [normed_add_comm_group F''] (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] [normed_add_comm_group F''] (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} [normed_add_comm_group E''] [normed_add_comm_group F''] {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} [normed_add_comm_group E''] [normed_add_comm_group F''] {f'' : α → E''} {g'' : α → F''} {x : α} :

f'' =O[has_pure.pure x] 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} :

asymptotics.is_O_with c ⊤ 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} [normed_add_comm_group E''] [normed_add_comm_group F''] {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 α} :

asymptotics.is_O_with c (filter.principal s) f 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 α} :

f =O[filter.principal s] g ↔ ∃ (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] [norm_one_class F] (c : E) (l : filter α) :

asymptotics.is_O_with ‖c‖ l (λ (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] [norm_one_class 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] [normed_add_comm_group F''] {f : α → E} {l : filter α} [has_one F] [norm_one_class 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] [seminormed_add_comm_group E'] {f' : α → E'} {l : filter α} [has_one F] [norm_one_class F] :

(f' =o[l] λ (x : α), 1) ↔ filter.tendsto f' 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] [norm_one_class F] :

(f =O[l] λ (x : α), 1) ↔ filter.is_bounded_under has_le.le l (λ (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] [norm_one_class F] :

filter.is_bounded_under has_le.le l (λ (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] [norm_one_class 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] [seminormed_add_comm_group E'] {f' : α → E'} {l : filter α} [has_one F] [norm_one_class F] {c : E'} (h : filter.tendsto f' 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] [seminormed_add_comm_group F'] {f : α → E} {g' : α → F'} {l : filter α} [has_one F] [norm_one_class F] (hfg : f =O[l] g') {y : F'} (hg : filter.tendsto g' 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} [normed_add_comm_group E''] [normed_add_comm_group F''] {f'' : α → E''} {l : filter α} {c : F''} (hc : c ≠ 0) :

(f'' =o[l] λ (x : α), c) ↔ filter.tendsto f'' l (nhds 0)

theorem asymptotics.is_o_id_const {E'' : Type u_9} {F'' : Type u_10} [normed_add_comm_group E''] [normed_add_comm_group F''] {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] [normed_add_comm_group F''] {f : α → E} {l : filter α} (h : filter.is_bounded_under has_le.le l (has_norm.norm ∘ f)) {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} [normed_add_comm_group E''] [normed_add_comm_group F''] {f'' : α → E''} {l : filter α} {y : E''} (h : filter.tendsto f'' 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) :

filter.is_bounded_under has_le.le l (has_norm.norm ∘ f)

theorem asymptotics.is_O_const_of_ne {α : Type u_1} {E : Type u_3} {F'' : Type u_10} [has_norm E] [normed_add_comm_group F''] {f : α → E} {l : filter α} {c : F''} (hc : c ≠ 0) :

(f =O[l] λ (x : α), c) ↔ filter.is_bounded_under has_le.le l (has_norm.norm ∘ f)

theorem asymptotics.is_O_const_iff {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [normed_add_comm_group E''] [normed_add_comm_group F''] {f'' : α → E''} {l : filter α} {c : F''} :

(f'' =O[l] λ (x : α), c) ↔ (c = 0 → f'' =ᶠ[l] 0) ∧ filter.is_bounded_under has_le.le l (λ (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] [normed_add_comm_group F''] {f : α → E} {g'' : α → F''} {l : filter α} (h : ∀ᶠ (x : α) in l, g'' x ≠ 0) :

f =O[l] g'' ↔ filter.is_bounded_under has_le.le l (λ (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} [seminormed_add_comm_group E'] [normed_add_comm_group E''] {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} [normed_add_comm_group E''] [normed_add_comm_group F''] {f'' : α → E''} {g'' : α → F''} {l : filter α} (hfg : f'' =O[l] g'') (hg : filter.tendsto g'' l (nhds 0)) :

filter.tendsto f'' l (nhds 0)

theorem asymptotics.is_o.trans_tendsto {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [normed_add_comm_group E''] [normed_add_comm_group F''] {f'' : α → E''} {g'' : α → F''} {l : filter α} (hfg : f'' =o[l] g'') (hg : filter.tendsto g'' l (nhds 0)) :

filter.tendsto f'' l (nhds 0)

Multiplication by a constant #

theorem asymptotics.is_O_with_const_mul_self {α : Type u_1} {R : Type u_12} [semi_normed_ring R] (c : R) (f : α → R) (l : filter α) :

asymptotics.is_O_with ‖c‖ l (λ (x : α), c * f x) f

theorem asymptotics.is_O_const_mul_self {α : Type u_1} {R : Type u_12} [semi_normed_ring R] (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] [semi_normed_ring R] {c : ℝ} {g : α → F} {l : filter α} {f : α → R} (h : asymptotics.is_O_with c l f 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] [semi_normed_ring R] {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} [semi_normed_ring R] (u : Rˣ) (f : α → R) (l : filter α) :

asymptotics.is_O_with ‖↑u⁻¹ ‖ l f (λ (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 α) :

asymptotics.is_O_with ‖c‖⁻¹ l f (λ (x : α), c * f x)

theorem asymptotics.is_O_self_const_mul' {α : Type u_1} {R : Type u_12} [semi_normed_ring R] {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] [semi_normed_ring R] {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] [semi_normed_ring R] {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] [semi_normed_ring R] {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] [semi_normed_ring R] {c' : ℝ} {f : α → E} {l : filter α} {g : α → R} {c : R} (hc' : 0 ≤ c') (h : asymptotics.is_O_with c' l f (λ (x : α), c * g x)) :

asymptotics.is_O_with (c' * ‖c‖) l f g

theorem asymptotics.is_O.of_const_mul_right {α : Type u_1} {E : Type u_3} {R : Type u_12} [has_norm E] [semi_normed_ring R] {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] [semi_normed_ring R] {f : α → E} {l : filter α} {g : α → R} {u : Rˣ} {c' : ℝ} (hc' : 0 ≤ c') (h : asymptotics.is_O_with c' l f g) :

asymptotics.is_O_with (c' * ‖↑u⁻¹ ‖) 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 : asymptotics.is_O_with c' l f g) :

asymptotics.is_O_with (c' * ‖c‖⁻¹) 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] [semi_normed_ring R] {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] [semi_normed_ring R] {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] [semi_normed_ring R] {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] [semi_normed_ring R] {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] [semi_normed_ring R] {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} [semi_normed_ring R] [normed_field 𝕜] {l : filter α} {f₁ f₂ : α → R} {g₁ g₂ : α → 𝕜} {c₁ c₂ : ℝ} (h₁ : asymptotics.is_O_with c₁ l f₁ g₁) (h₂ : asymptotics.is_O_with c₂ 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} [semi_normed_ring R] [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} [semi_normed_ring R] [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} [semi_normed_ring R] [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} [semi_normed_ring R] [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} [semi_normed_ring R] [normed_field 𝕜] {c : ℝ} {l : filter α} {f : α → R} {g : α → 𝕜} (h : asymptotics.is_O_with c l f 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} [semi_normed_ring R] [normed_field 𝕜] {c : ℝ} {l : filter α} [norm_one_class R] {f : α → R} {g : α → 𝕜} (h : asymptotics.is_O_with c l f 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} [semi_normed_ring R] [normed_field 𝕜] {c c' : ℝ} {l : filter α} {n : ℕ} {f : α → 𝕜} {g : α → R} (h : asymptotics.is_O_with c l (f ^ n) (g ^ n)) (hn : n ≠ 0) (hc : c ≤ c' ^ n) (hc' : 0 ≤ c') :

asymptotics.is_O_with c' l f g

theorem asymptotics.is_O.pow {α : Type u_1} {R : Type u_12} {𝕜 : Type u_14} [semi_normed_ring R] [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} [semi_normed_ring R] [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} [semi_normed_ring R] [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} [semi_normed_ring R] [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 : asymptotics.is_O_with c l f g) (h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0) :

asymptotics.is_O_with c l (λ (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] [seminormed_add_comm_group E'] [normed_field 𝕜] {c : ℝ} {g : α → F} {f' : α → E'} {l : filter α} [normed_space 𝕜 E'] (h : asymptotics.is_O_with c l 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] [seminormed_add_comm_group E'] [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] [seminormed_add_comm_group E'] [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] [seminormed_add_comm_group E'] [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] [seminormed_add_comm_group E'] [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] [seminormed_add_comm_group 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] [seminormed_add_comm_group 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} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] [normed_field 𝕜] [normed_field 𝕜'] {c c' : ℝ} {f' : α → E'} {g' : α → F'} {l : filter α} [normed_space 𝕜 E'] [normed_space 𝕜' F'] {k₁ : α → 𝕜} {k₂ : α → 𝕜'} (h₁ : asymptotics.is_O_with c l k₁ k₂) (h₂ : asymptotics.is_O_with c' l 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} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] [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} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] [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} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] [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} [seminormed_add_comm_group E'] [seminormed_add_comm_group F'] [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] [seminormed_add_comm_group E'] {g : α → F} {l : filter α} {ι : Type u_16} {A : ι → α → E'} {C : ι → ℝ} {s : finset ι} (h : ∀ (i : ι), i ∈ s → asymptotics.is_O_with (C i) 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] [seminormed_add_comm_group E'] {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} [seminormed_add_comm_group E'] [seminormed_add_comm_group 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'

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} [seminormed_add_comm_group E'] [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} {F : Type u_4} {E'' : Type u_9} [has_norm F] [normed_add_comm_group E''] {g : α → F} {l : filter α} {c : E''} (hc : c ≠ 0) :

(λ (x : α), c) =o[l] g ↔ filter.tendsto (λ (x : α), ‖g x‖) l filter.at_top

@[simp]

theorem asymptotics.is_o_const_left {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [normed_add_comm_group E''] [normed_add_comm_group F''] {g'' : α → F''} {l : filter α} {c : E''} :

(λ (x : α), c) =o[l] g'' ↔ c = 0 ∨ filter.tendsto (has_norm.norm ∘ g'') l filter.at_top

@[simp]

theorem asymptotics.is_o_const_const_iff {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [normed_add_comm_group E''] [normed_add_comm_group F''] {l : filter α} [l.ne_bot] {d : E''} {c : F''} :

((λ (x : α), d) =o[l] λ (x : α), c) ↔ d = 0

@[simp]

theorem asymptotics.is_o_pure {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [normed_add_comm_group E''] [normed_add_comm_group F''] {f'' : α → E''} {g'' : α → F''} {x : α} :

f'' =o[has_pure.pure x] g'' ↔ f'' x = 0

theorem asymptotics.is_o_const_id_comap_norm_at_top {E'' : Type u_9} {F'' : Type u_10} [normed_add_comm_group E''] [normed_add_comm_group F''] (c : F'') :

(λ (x : E''), c) =o[filter.comap has_norm.norm filter.at_top] id

theorem asymptotics.is_o_const_id_at_top {E'' : Type u_9} [normed_add_comm_group E''] (c : E'') :

(λ (x : ℝ), c) =o[filter.at_top ] id

theorem asymptotics.is_o_const_id_at_bot {E'' : Type u_9} [normed_add_comm_group E''] (c : E'') :

(λ (x : ℝ), c) =o[filter.at_bot ] id

Eventually (u / v) * v = u #

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

theorem asymptotics.is_O_with.eventually_mul_div_cancel {α : Type u_1} {𝕜 : Type u_14} [normed_field 𝕜] {c : ℝ} {l : filter α} {u v : α → 𝕜} (h : asymptotics.is_O_with c l u v) :

u / v * v =ᶠ[l] u

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

u / v * v =ᶠ[l] u

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

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

u / v * v =ᶠ[l] u

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

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

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

asymptotics.is_O_with c l u v

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

theorem asymptotics.is_O_with_iff_exists_eq_mul {α : Type u_1} {𝕜 : Type u_14} [normed_field 𝕜] {c : ℝ} {l : filter α} {u v : α → 𝕜} (hc : 0 ≤ c) :

asymptotics.is_O_with c l u v ↔ ∃ (φ : α → 𝕜) (hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c), u =ᶠ[l] φ * v

theorem asymptotics.is_O_with.exists_eq_mul {α : Type u_1} {𝕜 : Type u_14} [normed_field 𝕜] {c : ℝ} {l : filter α} {u v : α → 𝕜} (h : asymptotics.is_O_with c l u v) (hc : 0 ≤ c) :

∃ (φ : α → 𝕜) (hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c), u =ᶠ[l] φ * v

theorem asymptotics.is_O_iff_exists_eq_mul {α : Type u_1} {𝕜 : Type u_14} [normed_field 𝕜] {l : filter α} {u v : α → 𝕜} :

u =O[l] v ↔ ∃ (φ : α → 𝕜) (hφ : filter.is_bounded_under has_le.le l (has_norm.norm ∘ φ)), u =ᶠ[l] φ * v

theorem asymptotics.is_O.exists_eq_mul {α : Type u_1} {𝕜 : Type u_14} [normed_field 𝕜] {l : filter α} {u v : α → 𝕜} :

u =O[l] v → (∃ (φ : α → 𝕜) (hφ : filter.is_bounded_under has_le.le l (has_norm.norm ∘ φ)), u =ᶠ[l] φ * v)

Alias of the forward direction of asymptotics.is_O_iff_exists_eq_mul.

theorem asymptotics.is_o_iff_exists_eq_mul {α : Type u_1} {𝕜 : Type u_14} [normed_field 𝕜] {l : filter α} {u v : α → 𝕜} :

u =o[l] v ↔ ∃ (φ : α → 𝕜) (hφ : filter.tendsto φ l (nhds 0)), u =ᶠ[l] φ * v

theorem asymptotics.is_o.exists_eq_mul {α : Type u_1} {𝕜 : Type u_14} [normed_field 𝕜] {l : filter α} {u v : α → 𝕜} :

u =o[l] v → (∃ (φ : α → 𝕜) (hφ : filter.tendsto φ l (nhds 0)), u =ᶠ[l] φ * v)

Alias of the forward direction of asymptotics.is_o_iff_exists_eq_mul.

Miscellanous lemmas #

theorem asymptotics.div_is_bounded_under_of_is_O {𝕜 : Type u_14} [normed_field 𝕜] {α : Type u_1} {l : filter α} {f g : α → 𝕜} (h : f =O[l] g) :

filter.is_bounded_under has_le.le l (λ (x : α), ‖f x / g x‖)

theorem asymptotics.is_O_iff_div_is_bounded_under {𝕜 : Type u_14} [normed_field 𝕜] {α : Type u_1} {l : filter α} {f g : α → 𝕜} (hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0) :

f =O[l] g ↔ filter.is_bounded_under has_le.le l (λ (x : α), ‖f x / g x‖)

theorem asymptotics.is_O_of_div_tendsto_nhds {𝕜 : Type u_14} [normed_field 𝕜] {α : Type u_1} {l : filter α} {f g : α → 𝕜} (hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0) (c : 𝕜) (H : filter.tendsto (f / g) l (nhds c)) :

f =O[l] g

theorem asymptotics.is_o.tendsto_zero_of_tendsto {α : Type u_1} {E : Type u_2} {𝕜 : Type u_3} [normed_add_comm_group E] [normed_field 𝕜] {u : α → E} {v : α → 𝕜} {l : filter α} {y : 𝕜} (huv : u =o[l] v) (hv : filter.tendsto v l (nhds y)) :

filter.tendsto u l (nhds 0)

theorem asymptotics.is_o_pow_pow {𝕜 : Type u_14} [normed_field 𝕜] {m n : ℕ} (h : m < n) :

(λ (x : 𝕜), x ^ n) =o[nhds 0] λ (x : 𝕜), x ^ m

theorem asymptotics.is_o_norm_pow_norm_pow {E' : Type u_6} [seminormed_add_comm_group E'] {m n : ℕ} (h : m < n) :

(λ (x : E'), ‖x‖ ^ n) =o[nhds 0] λ (x : E'), ‖x‖ ^ m

theorem asymptotics.is_o_pow_id {𝕜 : Type u_14} [normed_field 𝕜] {n : ℕ} (h : 1 < n) :

(λ (x : 𝕜), x ^ n) =o[nhds 0] λ (x : 𝕜), x

theorem asymptotics.is_o_norm_pow_id {E' : Type u_6} [seminormed_add_comm_group E'] {n : ℕ} (h : 1 < n) :

(λ (x : E'), ‖x‖ ^ n) =o[nhds 0] λ (x : E'), x

theorem asymptotics.is_O.eq_zero_of_norm_pow_within {E'' : Type u_9} {F'' : Type u_10} [normed_add_comm_group E''] [normed_add_comm_group F''] {f : E'' → F''} {s : set E''} {x₀ : E''} {n : ℕ} (h : f =O[nhds_within x₀ s] λ (x : E''), ‖x - x₀‖ ^ n) (hx₀ : x₀ ∈ s) (hn : 0 < n) :

f x₀ = 0

theorem asymptotics.is_O.eq_zero_of_norm_pow {E'' : Type u_9} {F'' : Type u_10} [normed_add_comm_group E''] [normed_add_comm_group F''] {f : E'' → F''} {x₀ : E''} {n : ℕ} (h : f =O[nhds x₀] λ (x : E''), ‖x - x₀‖ ^ n) (hn : 0 < n) :

f x₀ = 0

theorem asymptotics.is_o_pow_sub_pow_sub {E' : Type u_6} [seminormed_add_comm_group E'] (x₀ : E') {n m : ℕ} (h : n < m) :

(λ (x : E'), ‖x - x₀‖ ^ m) =o[nhds x₀] λ (x : E'), ‖x - x₀‖ ^ n

theorem asymptotics.is_o_pow_sub_sub {E' : Type u_6} [seminormed_add_comm_group E'] (x₀ : E') {m : ℕ} (h : 1 < m) :

(λ (x : E'), ‖x - x₀‖ ^ m) =o[nhds x₀] λ (x : E'), x - x₀

theorem asymptotics.is_O_with.right_le_sub_of_lt_1 {α : Type u_1} {E' : Type u_6} [seminormed_add_comm_group E'] {c : ℝ} {l : filter α} {f₁ f₂ : α → E'} (h : asymptotics.is_O_with c l f₁ f₂) (hc : c < 1) :

asymptotics.is_O_with (1 / (1 - c)) l f₂ (λ (x : α), f₂ x - f₁ x)

theorem asymptotics.is_O_with.right_le_add_of_lt_1 {α : Type u_1} {E' : Type u_6} [seminormed_add_comm_group E'] {c : ℝ} {l : filter α} {f₁ f₂ : α → E'} (h : asymptotics.is_O_with c l f₁ f₂) (hc : c < 1) :

asymptotics.is_O_with (1 / (1 - c)) l f₂ (λ (x : α), f₁ x + f₂ x)

theorem asymptotics.is_o.right_is_O_sub {α : Type u_1} {E' : Type u_6} [seminormed_add_comm_group E'] {l : filter α} {f₁ f₂ : α → E'} (h : f₁ =o[l] f₂) :

f₂ =O[l] λ (x : α), f₂ x - f₁ x

theorem asymptotics.is_o.right_is_O_add {α : Type u_1} {E' : Type u_6} [seminormed_add_comm_group E'] {l : filter α} {f₁ f₂ : α → E'} (h : f₁ =o[l] f₂) :

f₂ =O[l] λ (x : α), f₁ x + f₂ x

theorem asymptotics.bound_of_is_O_cofinite {α : Type u_1} {E : Type u_3} {F'' : Type u_10} [has_norm E] [normed_add_comm_group F''] {f : α → E} {g'' : α → F''} (h : f =O[filter.cofinite ] g'') :

∃ (C : ℝ) (H : C > 0), ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖

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

theorem asymptotics.is_O_cofinite_iff {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [normed_add_comm_group E''] [normed_add_comm_group F''] {f'' : α → E''} {g'' : α → F''} (h : ∀ (x : α), g'' x = 0 → f'' x = 0) :

f'' =O[filter.cofinite ] g'' ↔ ∃ (C : ℝ), ∀ (x : α), ‖f'' x‖ ≤ C * ‖g'' x‖

theorem asymptotics.bound_of_is_O_nat_at_top {E : Type u_3} {E'' : Type u_9} [has_norm E] [normed_add_comm_group E''] {f : ℕ → E} {g'' : ℕ → E''} (h : f =O[filter.at_top ] g'') :

∃ (C : ℝ) (H : C > 0), ∀ ⦃x : ℕ⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖

theorem asymptotics.is_O_nat_at_top_iff {E'' : Type u_9} {F'' : Type u_10} [normed_add_comm_group E''] [normed_add_comm_group F''] {f : ℕ → E''} {g : ℕ → F''} (h : ∀ (x : ℕ), g x = 0 → f x = 0) :

f =O[filter.at_top ] g ↔ ∃ (C : ℝ), ∀ (x : ℕ), ‖f x‖ ≤ C * ‖g x‖

theorem asymptotics.is_O_one_nat_at_top_iff {E'' : Type u_9} [normed_add_comm_group E''] {f : ℕ → E''} :

(f =O[filter.at_top ] λ (n : ℕ), 1) ↔ ∃ (C : ℝ), ∀ (n : ℕ), ‖f n‖ ≤ C

theorem asymptotics.is_O_with_pi {α : Type u_1} {F' : Type u_7} [seminormed_add_comm_group F'] {g' : α → F'} {l : filter α} {ι : Type u_2} [fintype ι] {E' : ι → Type u_3} [Π (i : ι), normed_add_comm_group (E' i)] {f : α → Π (i : ι), E' i} {C : ℝ} (hC : 0 ≤ C) :

asymptotics.is_O_with C l f g' ↔ ∀ (i : ι), asymptotics.is_O_with C l (λ (x : α), f x i) g'

@[simp]

theorem asymptotics.is_O_pi {α : Type u_1} {F' : Type u_7} [seminormed_add_comm_group F'] {g' : α → F'} {l : filter α} {ι : Type u_2} [fintype ι] {E' : ι → Type u_3} [Π (i : ι), normed_add_comm_group (E' i)] {f : α → Π (i : ι), E' i} :

f =O[l] g' ↔ ∀ (i : ι), (λ (x : α), f x i) =O[l] g'

@[simp]

theorem asymptotics.is_o_pi {α : Type u_1} {F' : Type u_7} [seminormed_add_comm_group F'] {g' : α → F'} {l : filter α} {ι : Type u_2} [fintype ι] {E' : ι → Type u_3} [Π (i : ι), normed_add_comm_group (E' i)] {f : α → Π (i : ι), E' i} :

f =o[l] g' ↔ ∀ (i : ι), (λ (x : α), f x i) =o[l] g'

theorem summable_of_is_O {ι : Type u_1} {E : Type u_2} [normed_add_comm_group E] [complete_space E] {f : ι → E} {g : ι → ℝ} (hg : summable g) (h : f =O[filter.cofinite ] g) :

theorem summable_of_is_O_nat {E : Type u_1} [normed_add_comm_group E] [complete_space E] {f : ℕ → E} {g : ℕ → ℝ} (hg : summable g) (h : f =O[filter.at_top ] g) :

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

asymptotics.is_O_with C (nhds b) f g ↔ asymptotics.is_O_with C (nhds (⇑(e.symm) b)) (f ∘ ⇑e) (g ∘ ⇑e)

Transfer is_O_with over a local_homeomorph.

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

f =O[nhds b] g ↔ (f ∘ ⇑e) =O[nhds (⇑(e.symm) b)] (g ∘ ⇑e)

Transfer is_O over a local_homeomorph.

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

f =o[nhds b] g ↔ (f ∘ ⇑e) =o[nhds (⇑(e.symm) b)] (g ∘ ⇑e)

Transfer is_o over a local_homeomorph.

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

asymptotics.is_O_with C (nhds b) f g ↔ asymptotics.is_O_with C (nhds (⇑(e.symm) b)) (f ∘ ⇑e) (g ∘ ⇑e)

Transfer is_O_with over a homeomorph.

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

f =O[nhds b] g ↔ (f ∘ ⇑e) =O[nhds (⇑(e.symm) b)] (g ∘ ⇑e)

Transfer is_O over a homeomorph.

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

f =o[nhds b] g ↔ (f ∘ ⇑e) =o[nhds (⇑(e.symm) b)] (g ∘ ⇑e)

Transfer is_o over a homeomorph.