Asymptotic equivalence #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 :
_ ~[l] _is an equivalence relation- Equivalent statements for
u ~[l] const _ c:- If
c ≠ 0, this is true ifftendsto u l (𝓝 c)(seeis_equivalent_const_iff_tendsto) - For
c = 0, this is true iffu =ᶠ[l] 0(seeis_equivalent_zero_iff_eventually_zero)
- If
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)(seeis_equivalent_iff_tendsto_one) -
For any constant
c,u ~[l] vimpliestendsto u l (𝓝 c) ↔ tendsto v l (𝓝 c)(seeis_equivalent.tendsto_nhds_iff) -
*and/are compatible with_ ~[l] _(seeis_equivalent.mulandis_equivalent.div)
If β is a normed_linear_ordered_field :
- If
u ~[l] v, we havetendsto u l at_top ↔ tendsto v l at_top(seeis_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_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
- 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) :
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) :
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) :
@[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 α} :
asymptotics.is_equivalent l u 0 ↔ u =ᶠ[l] 0
theorem
asymptotics.is_equivalent_zero_iff_is_O_zero
{α : Type u_1}
{β : Type u_2}
[normed_add_comm_group β]
{u : α → β}
{l : filter α} :
asymptotics.is_equivalent l u 0 ↔ u =O[l] 0
theorem
asymptotics.is_equivalent_const_iff_tendsto
{α : Type u_1}
{β : Type u_2}
[normed_add_comm_group β]
{u : α → β}
{l : filter α}
{c : β}
(h : c ≠ 0) :
asymptotics.is_equivalent l u (function.const α c) ↔ filter.tendsto u l (nhds c)
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)) :
filter.tendsto u l (nhds 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)) :
filter.tendsto v 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) :
filter.tendsto u l (nhds c) ↔ filter.tendsto v l (nhds c)
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) :
asymptotics.is_equivalent l (u + w) 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) :
asymptotics.is_equivalent l (u - w) 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) :
asymptotics.is_equivalent l (u + 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) :
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 = 0 → u 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 = 0 → u 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) :
asymptotics.is_equivalent l u v ↔ 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_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) :
asymptotics.is_equivalent l (t * v) (u * 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_top_iff
{α : Type u_1}
{β : Type u_2}
[normed_linear_ordered_field β]
{u v : α → β}
{l : filter α}
[order_topology β]
(huv : asymptotics.is_equivalent l u 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 : asymptotics.is_equivalent l u 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 : asymptotics.is_equivalent l u v) :
theorem
filter.eventually_eq.is_equivalent
{α : Type u_1}
{β : Type u_2}
[normed_add_comm_group β]
{u v : α → β}
{l : filter α}
(h : u =ᶠ[l] v) :