mathlib documentation

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_add_comm_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_add_comm_group :

If β is a normed_field :

If β is a normed_linear_ordered_field :

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_add_comm_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_add_comm_group β] {u v : α → β} {l : filter α} (h : asymptotics.is_equivalent l u v) :
(u - v) =o[l] v
theorem asymptotics.is_equivalent.is_O {α : Type u_1} {β : Type u_2} [normed_add_comm_group β] {u v : α → β} {l : filter α} (h : asymptotics.is_equivalent l u v) :
u =O[l] v
theorem asymptotics.is_equivalent.is_O_symm {α : Type u_1} {β : Type u_2} [normed_add_comm_group β] {u v : α → β} {l : filter α} (h : asymptotics.is_equivalent l u v) :
v =O[l] u
@[refl]
theorem asymptotics.is_equivalent.refl {α : Type u_1} {β : Type u_2} [normed_add_comm_group β] {u : α → β} {l : filter α} :
@[symm]
theorem asymptotics.is_equivalent.symm {α : Type u_1} {β : Type u_2} [normed_add_comm_group β] {u v : α → β} {l : filter α} (h : asymptotics.is_equivalent l u v) :
@[trans]
theorem asymptotics.is_equivalent.trans {α : Type u_1} {β : Type u_2} [normed_add_comm_group β] {l : filter α} {u v w : α → β} (huv : asymptotics.is_equivalent l u v) (hvw : asymptotics.is_equivalent l v w) :
theorem asymptotics.is_equivalent.congr_left {α : Type u_1} {β : Type u_2} [normed_add_comm_group β] {u v w : α → β} {l : filter α} (huv : asymptotics.is_equivalent l u v) (huw : u =ᶠ[l] w) :
theorem asymptotics.is_equivalent.congr_right {α : Type u_1} {β : Type u_2} [normed_add_comm_group β] {u v w : α → β} {l : filter α} (huv : asymptotics.is_equivalent l u v) (hvw : v =ᶠ[l] w) :
theorem asymptotics.is_equivalent_zero_iff_eventually_zero {α : Type u_1} {β : Type u_2} [normed_add_comm_group β] {u : α → β} {l : filter α} :
theorem asymptotics.is_equivalent_zero_iff_is_O_zero {α : Type u_1} {β : Type u_2} [normed_add_comm_group β] {u : α → β} {l : filter α} :
theorem asymptotics.is_equivalent_const_iff_tendsto {α : Type u_1} {β : Type u_2} [normed_add_comm_group β] {u : α → β} {l : filter α} {c : β} (h : c 0) :
theorem asymptotics.is_equivalent.tendsto_const {α : Type u_1} {β : Type u_2} [normed_add_comm_group β] {u : α → β} {l : filter α} {c : β} (hu : asymptotics.is_equivalent l u (function.const α c)) :
theorem asymptotics.is_equivalent.tendsto_nhds {α : Type u_1} {β : Type u_2} [normed_add_comm_group β] {u v : α → β} {l : filter α} {c : β} (huv : asymptotics.is_equivalent l u v) (hu : filter.tendsto u l (nhds c)) :
theorem asymptotics.is_equivalent.tendsto_nhds_iff {α : Type u_1} {β : Type u_2} [normed_add_comm_group β] {u v : α → β} {l : filter α} {c : β} (huv : asymptotics.is_equivalent l u v) :
theorem asymptotics.is_equivalent.add_is_o {α : Type u_1} {β : Type u_2} [normed_add_comm_group β] {u v w : α → β} {l : filter α} (huv : asymptotics.is_equivalent l u v) (hwv : w =o[l] v) :
theorem asymptotics.is_equivalent.sub_is_o {α : Type u_1} {β : Type u_2} [normed_add_comm_group β] {u v w : α → β} {l : filter α} (huv : asymptotics.is_equivalent l u v) (hwv : w =o[l] v) :
theorem asymptotics.is_o.add_is_equivalent {α : Type u_1} {β : Type u_2} [normed_add_comm_group β] {u v w : α → β} {l : filter α} (hu : u =o[l] w) (hv : asymptotics.is_equivalent l v w) :
theorem asymptotics.is_o.is_equivalent {α : Type u_1} {β : Type u_2} [normed_add_comm_group β] {u v : α → β} {l : filter α} (huv : (u - v) =o[l] v) :
theorem asymptotics.is_equivalent.neg {α : Type u_1} {β : Type u_2} [normed_add_comm_group β] {u v : α → β} {l : filter α} (huv : asymptotics.is_equivalent l u v) :
asymptotics.is_equivalent l (λ (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 α} :
asymptotics.is_equivalent l u v ∃ (φ : α → β) (hφ : filter.tendsto φ l (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 : asymptotics.is_equivalent l u v) :
∃ (φ : α → β) (hφ : filter.tendsto φ l (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) :
theorem asymptotics.is_equivalent.smul {α : Type u_1} {E : Type u_2} {𝕜 : Type u_3} [normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] {a b : α → 𝕜} {u v : α → E} {l : filter α} (hab : asymptotics.is_equivalent l a b) (huv : asymptotics.is_equivalent l u v) :
asymptotics.is_equivalent l (λ (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 : asymptotics.is_equivalent l t u) (hvw : asymptotics.is_equivalent l v w) :
theorem asymptotics.is_equivalent.inv {α : Type u_1} {β : Type u_2} [normed_field β] {u v : α → β} {l : filter α} (huv : asymptotics.is_equivalent l u v) :
asymptotics.is_equivalent l (λ (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 : asymptotics.is_equivalent l t u) (hvw : asymptotics.is_equivalent l v w) :
asymptotics.is_equivalent l (λ (x : α), t x / v x) (λ (x : α), u x / w x)
theorem asymptotics.is_equivalent.tendsto_at_top {α : Type u_1} {β : Type u_2} [normed_linear_ordered_field β] {u v : α → β} {l : filter α} [order_topology β] (huv : asymptotics.is_equivalent l u v) (hu : filter.tendsto u l filter.at_top) :
theorem asymptotics.is_equivalent.tendsto_at_bot {α : Type u_1} {β : Type u_2} [normed_linear_ordered_field β] {u v : α → β} {l : filter α} [order_topology β] (huv : asymptotics.is_equivalent l u v) (hu : filter.tendsto u l filter.at_bot) :
theorem filter.eventually_eq.is_equivalent {α : Type u_1} {β : Type u_2} [normed_add_comm_group β] {u v : α → β} {l : filter α} (h : u =ᶠ[l] v) :