mathlib documentation

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 codomaine β. 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 :

If β is a normed_field :

If β is a normed_linear_ordered_field :

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) :
theorem asymptotics.is_equivalent.is_O_symm {α : Type u_1} {β : Type u_2} [normed_group β] {u v : α → β} {l : filter α} (h : u ~[l] v) :
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_const_iff_tendsto {α : Type u_1} {β : Type u_2} [normed_group β] {u : α → β} {l : filter α} {c : β} (h : c 0) :
theorem asymptotics.is_equivalent.tendsto_const {α : Type u_1} {β : Type u_2} [normed_group β] {u : α → β} {l : filter α} {c : β} (hu : u ~[l] function.const α 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 : filter.tendsto u l (𝓝 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) :
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 : asymptotics.is_o w v 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φ : filter.tendsto φ l (𝓝 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φ : filter.tendsto φ 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 : α) 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] [normed_space 𝕜 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} [normed_linear_ordered_field β] {u v : α → β} {l : filter α} [order_topology β] (huv : u ~[l] v) (hu : filter.tendsto u l filter.at_top) :
theorem asymptotics.is_equivalent.tendsto_at_top_iff {α : Type u_1} {β : Type u_2} [normed_linear_ordered_field β] {u v : α → β} {l : filter α} [order_topology β] (huv : u ~[l] v) :
theorem asymptotics.is_equivalent.tendsto_at_bot {α : Type u_1} {β : Type u_2} [normed_linear_ordered_field β] {u v : α → β} {l : filter α} [order_topology β] (huv : u ~[l] v) (hu : filter.tendsto u l filter.at_bot) :
theorem asymptotics.is_equivalent.tendsto_at_bot_iff {α : Type u_1} {β : Type u_2} [normed_linear_ordered_field β] {u v : α → β} {l : filter α} [order_topology β] (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