# mathlibdocumentation

analysis.asymptotics.asymptotic_equivalent

# Asymptotic equivalence #

In this file, we define the relation is_equivalent u v l, which means that u-v is little o of v along the filter l.

Unlike is_[oO] relations, this one requires u and v to have the same codomain β. While the definition only requires β to be a normed_group, most interesting properties require it to be a normed_field.

## Notations #

We introduce the notation u ~[l] v := is_equivalent u v l, which you can use by opening the asymptotics locale.

## Main results #

If β is a normed_group :

• _ ~[l] _ is an equivalence relation
• Equivalent statements for u ~[l] const _ c :
• If c ≠ 0, this is true iff tendsto u l (𝓝 c) (see is_equivalent_const_iff_tendsto)
• For c = 0, this is true iff u =ᶠ[l] 0 (see is_equivalent_zero_iff_eventually_zero)

If β is a normed_field :

• Alternative characterization of the relation (see is_equivalent_iff_exists_eq_mul) :

u ~[l] v ↔ ∃ (φ : α → β) (hφ : tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v

• Provided some non-vanishing hypothesis, this can be seen as u ~[l] v ↔ tendsto (u/v) l (𝓝 1) (see is_equivalent_iff_tendsto_one)

• For any constant c, u ~[l] v implies tendsto u l (𝓝 c) ↔ tendsto v l (𝓝 c) (see is_equivalent.tendsto_nhds_iff)

• * and / are compatible with _ ~[l] _ (see is_equivalent.mul and is_equivalent.div)

If β is a normed_linear_ordered_field :

• If u ~[l] v, we have tendsto u l at_top ↔ tendsto v l at_top (see is_equivalent.tendsto_at_top_iff)
def asymptotics.is_equivalent {α : Type u_1} {β : Type u_2} [normed_group β] (u v : α → β) (l : filter α) :
Prop

Two functions u and v are said to be asymptotically equivalent along a filter l when u x - v x = o(v x) as x converges along l.

Equations
theorem asymptotics.is_equivalent.is_o {α : Type u_1} {β : Type u_2} [normed_group β] {u v : α → β} {l : filter α} (h : u ~[l] v) :
theorem asymptotics.is_equivalent.is_O {α : Type u_1} {β : Type u_2} [normed_group β] {u v : α → β} {l : filter α} (h : u ~[l] v) :
l
theorem asymptotics.is_equivalent.is_O_symm {α : Type u_1} {β : Type u_2} [normed_group β] {u v : α → β} {l : filter α} (h : u ~[l] v) :
l
theorem asymptotics.is_equivalent.refl {α : Type u_1} {β : Type u_2} [normed_group β] {u : α → β} {l : filter α} :
u ~[l] u
theorem asymptotics.is_equivalent.symm {α : Type u_1} {β : Type u_2} [normed_group β] {u v : α → β} {l : filter α} (h : u ~[l] v) :
v ~[l] u
theorem asymptotics.is_equivalent.trans {α : Type u_1} {β : Type u_2} [normed_group β] {u v w : α → β} {l : filter α} (huv : u ~[l] v) (hvw : v ~[l] w) :
u ~[l] w
theorem asymptotics.is_equivalent.congr_left {α : Type u_1} {β : Type u_2} [normed_group β] {u v w : α → β} {l : filter α} (huv : u ~[l] v) (huw : u =ᶠ[l] w) :
w ~[l] v
theorem asymptotics.is_equivalent.congr_right {α : Type u_1} {β : Type u_2} [normed_group β] {u v w : α → β} {l : filter α} (huv : u ~[l] v) (hvw : v =ᶠ[l] w) :
u ~[l] w
theorem asymptotics.is_equivalent_zero_iff_eventually_zero {α : Type u_1} {β : Type u_2} [normed_group β] {u : α → β} {l : filter α} :
u ~[l] 0 u =ᶠ[l] 0
theorem asymptotics.is_equivalent_zero_iff_is_O_zero {α : Type u_1} {β : Type u_2} [normed_group β] {u : α → β} {l : filter α} :
u ~[l] 0 l
theorem asymptotics.is_equivalent_const_iff_tendsto {α : Type u_1} {β : Type u_2} [normed_group β] {u : α → β} {l : filter α} {c : β} (h : c 0) :
u ~[l] (𝓝 c)
theorem asymptotics.is_equivalent.tendsto_const {α : Type u_1} {β : Type u_2} [normed_group β] {u : α → β} {l : filter α} {c : β} (hu : u ~[l] ) :
(𝓝 c)
theorem asymptotics.is_equivalent.tendsto_nhds {α : Type u_1} {β : Type u_2} [normed_group β] {u v : α → β} {l : filter α} {c : β} (huv : u ~[l] v) (hu : (𝓝 c)) :
(𝓝 c)
theorem asymptotics.is_equivalent.tendsto_nhds_iff {α : Type u_1} {β : Type u_2} [normed_group β] {u v : α → β} {l : filter α} {c : β} (huv : u ~[l] v) :
(𝓝 c) (𝓝 c)
theorem asymptotics.is_equivalent.add_is_o {α : Type u_1} {β : Type u_2} [normed_group β] {u v w : α → β} {l : filter α} (huv : u ~[l] v) (hwv : l) :
w + u ~[l] v
theorem asymptotics.is_o.is_equivalent {α : Type u_1} {β : Type u_2} [normed_group β] {u v : α → β} {l : filter α} (huv : asymptotics.is_o (u - v) v l) :
u ~[l] v
theorem asymptotics.is_equivalent.neg {α : Type u_1} {β : Type u_2} [normed_group β] {u v : α → β} {l : filter α} (huv : u ~[l] v) :
(λ (x : α), -u x) ~[l] λ (x : α), -v x
theorem asymptotics.is_equivalent_iff_exists_eq_mul {α : Type u_1} {β : Type u_2} [normed_field β] {u v : α → β} {l : filter α} :
u ~[l] v ∃ (φ : α → β) (hφ : (𝓝 1)), u =ᶠ[l] φ * v
theorem asymptotics.is_equivalent.exists_eq_mul {α : Type u_1} {β : Type u_2} [normed_field β] {u v : α → β} {l : filter α} (huv : u ~[l] v) :
∃ (φ : α → β) (hφ : (𝓝 1)), u =ᶠ[l] φ * v
theorem asymptotics.is_equivalent_of_tendsto_one {α : Type u_1} {β : Type u_2} [normed_field β] {u v : α → β} {l : filter α} (hz : ∀ᶠ (x : α) in l, v x = 0u x = 0) (huv : filter.tendsto (u / v) l (𝓝 1)) :
u ~[l] v
theorem asymptotics.is_equivalent_of_tendsto_one' {α : Type u_1} {β : Type u_2} [normed_field β] {u v : α → β} {l : filter α} (hz : ∀ (x : α), v x = 0u x = 0) (huv : filter.tendsto (u / v) l (𝓝 1)) :
u ~[l] v
theorem asymptotics.is_equivalent_iff_tendsto_one {α : Type u_1} {β : Type u_2} [normed_field β] {u v : α → β} {l : filter α} (hz : ∀ᶠ (x : α) in l, v x 0) :
u ~[l] v filter.tendsto (u / v) l (𝓝 1)
theorem asymptotics.is_equivalent.smul {α : Type u_1} {E : Type u_2} {𝕜 : Type u_3} [normed_field 𝕜] [normed_group E] [ E] {a b : α → 𝕜} {u v : α → E} {l : filter α} (hab : a ~[l] b) (huv : u ~[l] v) :
(λ (x : α), a x u x) ~[l] λ (x : α), b x v x
theorem asymptotics.is_equivalent.mul {α : Type u_1} {β : Type u_2} [normed_field β] {t u v w : α → β} {l : filter α} (htu : t ~[l] u) (hvw : v ~[l] w) :
t * v ~[l] u * w
theorem asymptotics.is_equivalent.inv {α : Type u_1} {β : Type u_2} [normed_field β] {u v : α → β} {l : filter α} (huv : u ~[l] v) :
(λ (x : α), (u x)⁻¹) ~[l] λ (x : α), (v x)⁻¹
theorem asymptotics.is_equivalent.div {α : Type u_1} {β : Type u_2} [normed_field β] {t u v w : α → β} {l : filter α} (htu : t ~[l] u) (hvw : v ~[l] w) :
(λ (x : α), t x / v x) ~[l] λ (x : α), u x / w x
theorem asymptotics.is_equivalent.tendsto_at_top {α : Type u_1} {β : Type u_2} {u v : α → β} {l : filter α} (huv : u ~[l] v) (hu : filter.at_top) :
theorem asymptotics.is_equivalent.tendsto_at_top_iff {α : Type u_1} {β : Type u_2} {u v : α → β} {l : filter α} (huv : u ~[l] v) :
theorem asymptotics.is_equivalent.tendsto_at_bot {α : Type u_1} {β : Type u_2} {u v : α → β} {l : filter α} (huv : u ~[l] v) (hu : filter.at_bot) :
theorem asymptotics.is_equivalent.tendsto_at_bot_iff {α : Type u_1} {β : Type u_2} {u v : α → β} {l : filter α} (huv : u ~[l] v) :
theorem filter.eventually_eq.is_equivalent {α : Type u_1} {β : Type u_2} [normed_group β] {u v : α → β} {l : filter α} (h : u =ᶠ[l] v) :
u ~[l] v