# mathlibdocumentation

analysis.asymptotics.asymptotic_equivalent

# Asymptotic equivalence #

In this file, we define the relation is_equivalent l u v, 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 l u v, 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)

## Implementation Notes #

Note that is_equivalent takes the parameters (l : filter α) (u v : α → β) in that order. This is to enable calc support, as calc requires that the last two explicit arguments are u v.

def asymptotics.is_equivalent {α : Type u_1} {β : Type u_2} [normed_group β] (l : filter α) (u v : α → β) :
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 : v) :
(u - v) =o[l] v
theorem asymptotics.is_equivalent.is_O {α : Type u_1} {β : Type u_2} [normed_group β] {u v : α → β} {l : filter α} (h : v) :
u =O[l] v
theorem asymptotics.is_equivalent.is_O_symm {α : Type u_1} {β : Type u_2} [normed_group β] {u v : α → β} {l : filter α} (h : v) :
v =O[l] u
theorem asymptotics.is_equivalent.refl {α : Type u_1} {β : Type u_2} [normed_group β] {u : α → β} {l : filter α} :
theorem asymptotics.is_equivalent.symm {α : Type u_1} {β : Type u_2} [normed_group β] {u v : α → β} {l : filter α} (h : v) :
theorem asymptotics.is_equivalent.trans {α : Type u_1} {β : Type u_2} [normed_group β] {l : filter α} {u v w : α → β} (huv : v) (hvw : w) :
theorem asymptotics.is_equivalent.congr_left {α : Type u_1} {β : Type u_2} [normed_group β] {u v w : α → β} {l : filter α} (huv : v) (huw : u =ᶠ[l] w) :
theorem asymptotics.is_equivalent.congr_right {α : Type u_1} {β : Type u_2} [normed_group β] {u v w : α → β} {l : filter α} (huv : v) (hvw : v =ᶠ[l] w) :
theorem asymptotics.is_equivalent_zero_iff_eventually_zero {α : Type u_1} {β : Type u_2} [normed_group β] {u : α → β} {l : filter α} :
u =ᶠ[l] 0
theorem asymptotics.is_equivalent_zero_iff_is_O_zero {α : Type u_1} {β : Type u_2} [normed_group β] {u : α → β} {l : filter α} :
u =O[l] 0
theorem asymptotics.is_equivalent_const_iff_tendsto {α : Type u_1} {β : Type u_2} [normed_group β] {u : α → β} {l : filter α} {c : β} (h : c 0) :
c) (nhds c)
theorem asymptotics.is_equivalent.tendsto_const {α : Type u_1} {β : Type u_2} [normed_group β] {u : α → β} {l : filter α} {c : β} (hu : c)) :
(nhds c)
theorem asymptotics.is_equivalent.tendsto_nhds {α : Type u_1} {β : Type u_2} [normed_group β] {u v : α → β} {l : filter α} {c : β} (huv : v) (hu : (nhds c)) :
(nhds c)
theorem asymptotics.is_equivalent.tendsto_nhds_iff {α : Type u_1} {β : Type u_2} [normed_group β] {u v : α → β} {l : filter α} {c : β} (huv : v) :
(nhds c) (nhds c)
theorem asymptotics.is_equivalent.add_is_o {α : Type u_1} {β : Type u_2} [normed_group β] {u v w : α → β} {l : filter α} (huv : v) (hwv : w =o[l] v) :
(w + u) v
theorem asymptotics.is_o.add_is_equivalent {α : Type u_1} {β : Type u_2} [normed_group β] {u v w : α → β} {l : filter α} (hu : u =o[l] w) (hv : w) :
(u + v) w
theorem asymptotics.is_o.is_equivalent {α : Type u_1} {β : Type u_2} [normed_group β] {u v : α → β} {l : filter α} (huv : (u - v) =o[l] v) :
theorem asymptotics.is_equivalent.neg {α : Type u_1} {β : Type u_2} [normed_group β] {u v : α → β} {l : filter α} (huv : v) :
(λ (x : α), -u x) (λ (x : α), -v x)
theorem asymptotics.is_equivalent_iff_exists_eq_mul {α : Type u_1} {β : Type u_2} [normed_field β] {u v : α → β} {l : filter α} :
∃ (φ : α → β) (hφ : (nhds 1)), u =ᶠ[l] φ * v
theorem asymptotics.is_equivalent.exists_eq_mul {α : Type u_1} {β : Type u_2} [normed_field β] {u v : α → β} {l : filter α} (huv : v) :
∃ (φ : α → β) (hφ : (nhds 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 (nhds 1)) :
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 (nhds 1)) :
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) :
filter.tendsto (u / v) l (nhds 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 : b) (huv : v) :
(λ (x : α), a x u x) (λ (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 : u) (hvw : w) :
(t * v) (u * w)
theorem asymptotics.is_equivalent.inv {α : Type u_1} {β : Type u_2} [normed_field β] {u v : α → β} {l : filter α} (huv : v) :
(λ (x : α), (u x)⁻¹) (λ (x : α), (v x)⁻¹)
theorem asymptotics.is_equivalent.div {α : Type u_1} {β : Type u_2} [normed_field β] {t u v w : α → β} {l : filter α} (htu : u) (hvw : w) :
(λ (x : α), t x / v x) (λ (x : α), u x / w x)
theorem asymptotics.is_equivalent.tendsto_at_top {α : Type u_1} {β : Type u_2} {u v : α → β} {l : filter α} (huv : v) (hu : filter.at_top) :
theorem asymptotics.is_equivalent.tendsto_at_top_iff {α : Type u_1} {β : Type u_2} {u v : α → β} {l : filter α} (huv : v) :
theorem asymptotics.is_equivalent.tendsto_at_bot {α : Type u_1} {β : Type u_2} {u v : α → β} {l : filter α} (huv : v) (hu : filter.at_bot) :
theorem asymptotics.is_equivalent.tendsto_at_bot_iff {α : Type u_1} {β : Type u_2} {u v : α → β} {l : filter α} (huv : v) :
theorem filter.eventually_eq.is_equivalent {α : Type u_1} {β : Type u_2} [normed_group β] {u v : α → β} {l : filter α} (h : u =ᶠ[l] v) :