Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Asymptotics.IsEquivalent definition

(l : Filter α) (u v : α → β)

Full source

/-- Two functions `u` and `v` are said to be asymptotically equivalent along a filter `l`
  (denoted as `u ~[l] v` in the `Asymptotics` namespace)
  when `u x - v x = o(v x)` as `x` converges along `l`. -/
def IsEquivalent (l : Filter α) (u v : α → β) :=
  (u - v) =o[l] v

Asymptotic equivalence of functions

Informal description

Two functions $ u, v : \alpha \to \beta $ are said to be asymptotically equivalent along a filter $ l $ (denoted $ u \sim[l] v $) if their difference $ u - v $ is little-o of $ v $ as $ x $ converges along $ l $, i.e., $ u(x) - v(x) = o(v(x)) $ as $ x \to l $.

Asymptotics.term_~[_]_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc] scoped notation:50 u " ~[" l:50 "] " v:50 => Asymptotics.IsEquivalent l u v

Asymptotic equivalence notation

Informal description

The notation $ u \sim[l] v $ denotes that the difference $ u - v $ is asymptotically negligible compared to $ v $ along the filter $ l $, i.e., $ u - v = o(v) $ as $ l $ approaches its limit.

Asymptotics.IsEquivalent.isLittleO theorem

(h : u ~[l] v) : (u - v) =o[l] v

Full source

theorem IsEquivalent.isLittleO (h : u ~[l] v) : (u - v) =o[l] v := h

Difference of Asymptotically Equivalent Functions is Little-o

Informal description

If two functions $u$ and $v$ are asymptotically equivalent along a filter $l$ (denoted $u \sim[l] v$), then their difference $u - v$ is little-o of $v$ along $l$, i.e., $u(x) - v(x) = o(v(x))$ as $x \to l$.

Asymptotics.IsEquivalent.isBigO theorem

(h : u ~[l] v) : u =O[l] v

Full source

nonrec theorem IsEquivalent.isBigO (h : u ~[l] v) : u =O[l] v :=
  (IsBigO.congr_of_sub h.isBigO.symm).mp (isBigO_refl _ _)

Asymptotic equivalence implies big-O: $u \sim[l] v \Rightarrow u = O(v)$

Informal description

If two functions $u, v : \alpha \to \beta$ are asymptotically equivalent along a filter $l$ (denoted $u \sim[l] v$), then $u$ is big-O of $v$ along $l$, i.e., $u = O(v)$ as $x \to l$.

Asymptotics.IsEquivalent.isBigO_symm theorem

(h : u ~[l] v) : v =O[l] u

Full source

theorem IsEquivalent.isBigO_symm (h : u ~[l] v) : v =O[l] u := by
  convert h.isLittleO.right_isBigO_add
  simp

Asymptotic equivalence implies big-O symmetry: $u \sim[l] v \Rightarrow v = O(u)$

Informal description

If two functions $u, v : \alpha \to \beta$ are asymptotically equivalent along a filter $l$ (denoted $u \sim[l] v$), then $v$ is big-O of $u$ along $l$, i.e., $v = O(u)$ as $x \to l$.

Asymptotics.IsEquivalent.isTheta theorem

(h : u ~[l] v) : u =Θ[l] v

Full source

theorem IsEquivalent.isTheta (h : u ~[l] v) : u =Θ[l] v :=
  ⟨h.isBigO, h.isBigO_symm⟩

Asymptotic equivalence implies big-Theta equivalence: $ u \sim[l] v \Rightarrow u = \Theta[l] v $

Informal description

If two functions $ u, v : \alpha \to \beta $ are asymptotically equivalent along a filter $ l $ (denoted $ u \sim[l] v $), then $ u $ and $ v $ are big-Theta equivalent along $ l $, i.e., $ u = \Theta[l] v $.

Asymptotics.IsEquivalent.isTheta_symm theorem

(h : u ~[l] v) : v =Θ[l] u

Full source

theorem IsEquivalent.isTheta_symm (h : u ~[l] v) : v =Θ[l] u :=
  ⟨h.isBigO_symm, h.isBigO⟩

Asymptotic Equivalence Implies Big-Theta Symmetry: $ u \sim[l] v \Rightarrow v = \Theta(u) $

Informal description

If two functions $ u, v : \alpha \to \beta $ are asymptotically equivalent along a filter $ l $ (denoted $ u \sim[l] v $), then $ v $ is big-Theta of $ u $ along $ l $, i.e., $ v = \Theta[l] u $.

Asymptotics.IsEquivalent.refl theorem

: u ~[l] u

Full source

@[refl]
theorem IsEquivalent.refl : u ~[l] u := by
  rw [IsEquivalent, sub_self]
  exact isLittleO_zero _ _

Reflexivity of Asymptotic Equivalence

Informal description

For any function $u : \alpha \to \beta$ and any filter $l$ on $\alpha$, the function $u$ is asymptotically equivalent to itself along $l$, i.e., $u \sim[l] u$.

Asymptotics.IsEquivalent.symm theorem

(h : u ~[l] v) : v ~[l] u

Full source

@[symm]
theorem IsEquivalent.symm (h : u ~[l] v) : v ~[l] u :=
  (h.isLittleO.trans_isBigO h.isBigO_symm).symm

Symmetry of Asymptotic Equivalence: $u \sim[l] v \Rightarrow v \sim[l] u$

Informal description

If two functions $u, v : \alpha \to \beta$ are asymptotically equivalent along a filter $l$ (i.e., $u \sim[l] v$), then $v \sim[l] u$.

Asymptotics.IsEquivalent.trans theorem

{l : Filter α} {u v w : α → β} (huv : u ~[l] v) (hvw : v ~[l] w) : u ~[l] w

Full source

@[trans]
theorem IsEquivalent.trans {l : Filter α} {u v w : α → β} (huv : u ~[l] v) (hvw : v ~[l] w) :
    u ~[l] w :=
  (huv.isLittleO.trans_isBigO hvw.isBigO).triangle hvw.isLittleO

Transitivity of Asymptotic Equivalence: $u \sim[l] v \land v \sim[l] w \Rightarrow u \sim[l] w$

Informal description

Let $u, v, w : \alpha \to \beta$ be functions from a type $\alpha$ to a normed additive commutative group $\beta$, and let $l$ be a filter on $\alpha$. If $u$ is asymptotically equivalent to $v$ along $l$ (i.e., $u \sim[l] v$) and $v$ is asymptotically equivalent to $w$ along $l$ (i.e., $v \sim[l] w$), then $u$ is asymptotically equivalent to $w$ along $l$ (i.e., $u \sim[l] w$).

Asymptotics.IsEquivalent.congr_left theorem

{u v w : α → β} {l : Filter α} (huv : u ~[l] v) (huw : u =ᶠ[l] w) : w ~[l] v

Full source

theorem IsEquivalent.congr_left {u v w : α → β} {l : Filter α} (huv : u ~[l] v) (huw : u =ᶠ[l] w) :
    w ~[l] v :=
  huv.congr' (huw.sub (EventuallyEq.refl _ _)) (EventuallyEq.refl _ _)

Left Congruence of Asymptotic Equivalence under Eventual Equality

Informal description

Let $u, v, w : \alpha \to \beta$ be functions and $l$ be a filter on $\alpha$. If $u$ is asymptotically equivalent to $v$ along $l$ (i.e., $u \sim[l] v$) and $u$ is eventually equal to $w$ along $l$, then $w$ is asymptotically equivalent to $v$ along $l$ (i.e., $w \sim[l] v$).

Asymptotics.IsEquivalent.congr_right theorem

{u v w : α → β} {l : Filter α} (huv : u ~[l] v) (hvw : v =ᶠ[l] w) : u ~[l] w

Full source

theorem IsEquivalent.congr_right {u v w : α → β} {l : Filter α} (huv : u ~[l] v) (hvw : v =ᶠ[l] w) :
    u ~[l] w :=
  (huv.symm.congr_left hvw).symm

Right Congruence of Asymptotic Equivalence under Eventual Equality

Informal description

Let $u, v, w : \alpha \to \beta$ be functions from a type $\alpha$ to a normed additive commutative group $\beta$, and let $l$ be a filter on $\alpha$. If $u$ is asymptotically equivalent to $v$ along $l$ (i.e., $u \sim[l] v$) and $v$ is eventually equal to $w$ along $l$, then $u$ is asymptotically equivalent to $w$ along $l$ (i.e., $u \sim[l] w$).

Asymptotics.isEquivalent_zero_iff_eventually_zero theorem

: u ~[l] 0 ↔ u =ᶠ[l] 0

Full source

theorem isEquivalent_zero_iff_eventually_zero : u ~[l] 0u ~[l] 0 ↔ u =ᶠ[l] 0 := by
  rw [IsEquivalent, sub_zero]
  exact isLittleO_zero_right_iff

Asymptotic equivalence to zero iff eventually zero

Informal description

For a function $u : \alpha \to \beta$ and a filter $l$ on $\alpha$, the asymptotic equivalence $u \sim[l] 0$ holds if and only if $u$ is eventually equal to zero along the filter $l$.

Asymptotics.isEquivalent_zero_iff_isBigO_zero theorem

: u ~[l] 0 ↔ u =O[l] (0 : α → β)

Full source

theorem isEquivalent_zero_iff_isBigO_zero : u ~[l] 0u ~[l] 0 ↔ u =O[l] (0 : α → β) := by
  refine ⟨IsEquivalent.isBigO, fun h ↦ ?_⟩
  rw [isEquivalent_zero_iff_eventually_zero, eventuallyEq_iff_exists_mem]
  exact ⟨{ x : α | u x = 0 }, isBigO_zero_right_iff.mp h, fun x hx ↦ hx⟩

Asymptotic equivalence to zero iff big-O of zero: $u \sim[l] 0 \leftrightarrow u = O(0)$

Informal description

For a function $u : \alpha \to \beta$ and a filter $l$ on $\alpha$, the asymptotic equivalence $u \sim[l] 0$ holds if and only if $u$ is big-O of the zero function along $l$, i.e., $u = O(0)$ as $x \to l$.

Asymptotics.isEquivalent_const_iff_tendsto theorem

{c : β} (h : c ≠ 0) : u ~[l] const _ c ↔ Tendsto u l (𝓝 c)

Full source

theorem isEquivalent_const_iff_tendsto {c : β} (h : c ≠ 0) :
    u ~[l] const _ cu ~[l] const _ c ↔ Tendsto u l (𝓝 c) := by
  simp +unfoldPartialApp only [IsEquivalent, const, isLittleO_const_iff h]
  constructor <;> intro h
  · have := h.sub (tendsto_const_nhds (x := -c))
    simp only [Pi.sub_apply, sub_neg_eq_add, sub_add_cancel, zero_add] at this
    exact this
  · have := h.sub (tendsto_const_nhds (x := c))
    rwa [sub_self] at this

Asymptotic equivalence to nonzero constant iff tends to that constant

Informal description

For a function $u : \alpha \to \beta$ and a nonzero constant $c \in \beta$, the asymptotic equivalence $u \sim[l] c$ holds if and only if $u$ tends to $c$ along the filter $l$, i.e., $\lim_{x \to l} u(x) = c$.

Asymptotics.IsEquivalent.tendsto_const theorem

{c : β} (hu : u ~[l] const _ c) : Tendsto u l (𝓝 c)

Full source

theorem IsEquivalent.tendsto_const {c : β} (hu : u ~[l] const _ c) : Tendsto u l (𝓝 c) := by
  rcases em <| c = 0 with rfl | h
  · exact (tendsto_congr' <| isEquivalent_zero_iff_eventually_zero.mp hu).mpr tendsto_const_nhds
  · exact (isEquivalent_const_iff_tendsto h).mp hu

Asymptotic equivalence to constant implies convergence to that constant

Informal description

Let $u : \alpha \to \beta$ be a function and $c \in \beta$ a constant. If $u$ is asymptotically equivalent to the constant function $x \mapsto c$ along the filter $l$ (denoted $u \sim[l] c$), then $u$ tends to $c$ along $l$, i.e., $\lim_{x \to l} u(x) = c$.

Asymptotics.IsEquivalent.tendsto_nhds theorem

{c : β} (huv : u ~[l] v) (hu : Tendsto u l (𝓝 c)) : Tendsto v l (𝓝 c)

Full source

theorem IsEquivalent.tendsto_nhds {c : β} (huv : u ~[l] v) (hu : Tendsto u l (𝓝 c)) :
    Tendsto v l (𝓝 c) := by
  by_cases h : c = 0
  · subst c
    rw [← isLittleO_one_iff ℝ] at hu ⊢
    simpa using (huv.symm.isLittleO.trans hu).add hu
  · rw [← isEquivalent_const_iff_tendsto h] at hu ⊢
    exact huv.symm.trans hu

Asymptotic equivalence preserves limits: $u \sim[l] v$ and $u \to c$ implies $v \to c$

Informal description

Let $u, v : \alpha \to \beta$ be functions from a type $\alpha$ to a normed additive commutative group $\beta$, and let $l$ be a filter on $\alpha$. If $u$ is asymptotically equivalent to $v$ along $l$ (i.e., $u \sim[l] v$) and $u$ tends to $c \in \beta$ along $l$, then $v$ also tends to $c$ along $l$.

Asymptotics.IsEquivalent.tendsto_nhds_iff theorem

{c : β} (huv : u ~[l] v) : Tendsto u l (𝓝 c) ↔ Tendsto v l (𝓝 c)

Full source

theorem IsEquivalent.tendsto_nhds_iff {c : β} (huv : u ~[l] v) :
    TendstoTendsto u l (𝓝 c) ↔ Tendsto v l (𝓝 c) :=
  ⟨huv.tendsto_nhds, huv.symm.tendsto_nhds⟩

Asymptotic equivalence preserves limit points: $u \sim[l] v \Rightarrow (\lim_{x \to l} u(x) = c \leftrightarrow \lim_{x \to l} v(x) = c)$

Informal description

Let $u, v : \alpha \to \beta$ be functions from a type $\alpha$ to a normed additive commutative group $\beta$, and let $l$ be a filter on $\alpha$. If $u$ is asymptotically equivalent to $v$ along $l$ (i.e., $u \sim[l] v$), then for any $c \in \beta$, the function $u$ tends to $c$ along $l$ if and only if $v$ tends to $c$ along $l$.

Asymptotics.IsEquivalent.add_isLittleO theorem

(huv : u ~[l] v) (hwv : w =o[l] v) : u + w ~[l] v

Full source

theorem IsEquivalent.add_isLittleO (huv : u ~[l] v) (hwv : w =o[l] v) : u + w ~[l] v := by
  simpa only [IsEquivalent, add_sub_right_comm] using huv.add hwv

Asymptotic equivalence is preserved under addition of a little-o term

Informal description

Let $u, v, w : \alpha \to \beta$ be functions from a type $\alpha$ to a normed additive commutative group $\beta$, and let $l$ be a filter on $\alpha$. If $u$ is asymptotically equivalent to $v$ along $l$ (i.e., $u \sim[l] v$) and $w$ is little-o of $v$ along $l$ (i.e., $w = o[l] v$), then the sum $u + w$ is asymptotically equivalent to $v$ along $l$ (i.e., $u + w \sim[l] v$).

Asymptotics.IsEquivalent.sub_isLittleO theorem

(huv : u ~[l] v) (hwv : w =o[l] v) : u - w ~[l] v

Full source

theorem IsEquivalent.sub_isLittleO (huv : u ~[l] v) (hwv : w =o[l] v) : u - w ~[l] v := by
  simpa only [sub_eq_add_neg] using huv.add_isLittleO hwv.neg_left

Asymptotic equivalence is preserved under subtraction of a little-o term

Informal description

Let $u, v, w : \alpha \to \beta$ be functions from a type $\alpha$ to a normed additive commutative group $\beta$, and let $l$ be a filter on $\alpha$. If $u$ is asymptotically equivalent to $v$ along $l$ (i.e., $u \sim[l] v$) and $w$ is little-o of $v$ along $l$ (i.e., $w = o[l] v$), then the difference $u - w$ is asymptotically equivalent to $v$ along $l$ (i.e., $u - w \sim[l] v$).

Asymptotics.IsLittleO.add_isEquivalent theorem

(hu : u =o[l] w) (hv : v ~[l] w) : u + v ~[l] w

Full source

theorem IsLittleO.add_isEquivalent (hu : u =o[l] w) (hv : v ~[l] w) : u + v ~[l] w :=
  add_comm v u ▸ hv.add_isLittleO hu

Sum of Little-o and Asymptotically Equivalent Functions is Asymptotically Equivalent

Informal description

Let $u, v, w : \alpha \to \beta$ be functions from a type $\alpha$ to a normed additive commutative group $\beta$, and let $l$ be a filter on $\alpha$. If $u$ is little-o of $w$ along $l$ (i.e., $u = o[l] w$) and $v$ is asymptotically equivalent to $w$ along $l$ (i.e., $v \sim[l] w$), then the sum $u + v$ is asymptotically equivalent to $w$ along $l$ (i.e., $u + v \sim[l] w$).

Asymptotics.IsLittleO.isEquivalent theorem

(huv : (u - v) =o[l] v) : u ~[l] v

Full source

theorem IsLittleO.isEquivalent (huv : (u - v) =o[l] v) : u ~[l] v := huv

Little-o condition implies asymptotic equivalence

Informal description

For functions $u, v : \alpha \to \beta$ and a filter $l$ on $\alpha$, if the difference $u - v$ is little-o of $v$ along $l$ (i.e., $u - v = o(v)$ as $x \to l$), then $u$ is asymptotically equivalent to $v$ along $l$ (denoted $u \sim[l] v$).

Asymptotics.IsEquivalent.neg theorem

(huv : u ~[l] v) : (fun x ↦ -u x) ~[l] fun x ↦ -v x

Full source

theorem IsEquivalent.neg (huv : u ~[l] v) : (fun x ↦ -u x) ~[l] fun x ↦ -v x := by
  rw [IsEquivalent]
  convert huv.isLittleO.neg_left.neg_right
  simp [neg_add_eq_sub]

Negation Preserves Asymptotic Equivalence

Informal description

If two functions $u, v : \alpha \to \beta$ are asymptotically equivalent along a filter $l$ (i.e., $u \sim[l] v$), then their negations $-u$ and $-v$ are also asymptotically equivalent along $l$ (i.e., $-u \sim[l] -v$).

Asymptotics.isEquivalent_iff_exists_eq_mul theorem

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

Full source

theorem isEquivalent_iff_exists_eq_mul :
    u ~[l] vu ~[l] v ↔ ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v := by
  rw [IsEquivalent, isLittleO_iff_exists_eq_mul]
  constructor <;> rintro ⟨φ, hφ, h⟩ <;> [refine ⟨φ + 1, ?_, ?_⟩; refine ⟨φ - 1, ?_, ?_⟩]
  · conv in 𝓝 _ => rw [← zero_add (1 : β)]
    exact hφ.add tendsto_const_nhds
  · convert h.add (EventuallyEq.refl l v) <;> simp [add_mul]
  · conv in 𝓝 _ => rw [← sub_self (1 : β)]
    exact hφ.sub tendsto_const_nhds
  · convert h.sub (EventuallyEq.refl l v); simp [sub_mul]

Characterization of Asymptotic Equivalence via Multiplicative Perturbation

Informal description

Two functions $u, v : \alpha \to \beta$ are asymptotically equivalent along a filter $l$ (denoted $u \sim[l] v$) if and only if there exists a function $\varphi : \alpha \to \beta$ such that $\varphi$ tends to $1$ along $l$ and $u$ is eventually equal to $\varphi \cdot v$ along $l$.

Asymptotics.IsEquivalent.exists_eq_mul theorem

(huv : u ~[l] v) : ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v

Full source

theorem IsEquivalent.exists_eq_mul (huv : u ~[l] v) :
    ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v :=
  isEquivalent_iff_exists_eq_mul.mp huv

Existence of Multiplicative Perturbation for Asymptotically Equivalent Functions

Informal description

If two functions $u, v : \alpha \to \beta$ are asymptotically equivalent along a filter $l$ (i.e., $u \sim[l] v$), then there exists a function $\varphi : \alpha \to \beta$ such that $\varphi$ tends to $1$ along $l$ and $u$ is eventually equal to $\varphi \cdot v$ along $l$.

Asymptotics.isEquivalent_of_tendsto_one theorem

(hz : ∀ᶠ x in l, v x = 0 → u x = 0) (huv : Tendsto (u / v) l (𝓝 1)) : u ~[l] v

Full source

theorem isEquivalent_of_tendsto_one (hz : ∀ᶠ x in l, v x = 0 → u x = 0)
    (huv : Tendsto (u / v) l (𝓝 1)) : u ~[l] v := by
  rw [isEquivalent_iff_exists_eq_mul]
  exact ⟨u / v, huv, hz.mono fun x hz' ↦ (div_mul_cancel_of_imp hz').symm⟩

Asymptotic equivalence via ratio tending to one

Informal description

Let $u, v : \alpha \to \beta$ be functions where $\beta$ is a normed field. Suppose that for all $x$ in a neighborhood of the filter $l$, if $v(x) = 0$ then $u(x) = 0$. If the ratio $u/v$ tends to $1$ along $l$, then $u$ is asymptotically equivalent to $v$ along $l$, denoted $u \sim[l] v$.

Asymptotics.isEquivalent_of_tendsto_one' theorem

(hz : ∀ x, v x = 0 → u x = 0) (huv : Tendsto (u / v) l (𝓝 1)) : u ~[l] v

Full source

theorem isEquivalent_of_tendsto_one' (hz : ∀ x, v x = 0 → u x = 0) (huv : Tendsto (u / v) l (𝓝 1)) :
    u ~[l] v :=
  isEquivalent_of_tendsto_one (Eventually.of_forall hz) huv

Asymptotic equivalence via pointwise ratio tending to one

Informal description

Let $u, v : \alpha \to \beta$ be functions where $\beta$ is a normed field. Suppose that for all $x \in \alpha$, if $v(x) = 0$ then $u(x) = 0$. If the ratio $u(x)/v(x)$ tends to $1$ as $x$ converges along the filter $l$, then $u$ is asymptotically equivalent to $v$ along $l$, denoted $u \sim[l] v$.

Asymptotics.isEquivalent_iff_tendsto_one theorem

(hz : ∀ᶠ x in l, v x ≠ 0) : u ~[l] v ↔ Tendsto (u / v) l (𝓝 1)

Full source

theorem isEquivalent_iff_tendsto_one (hz : ∀ᶠ x in l, v x ≠ 0) :
    u ~[l] vu ~[l] v ↔ Tendsto (u / v) l (𝓝 1) := by
  constructor
  · intro hequiv
    have := hequiv.isLittleO.tendsto_div_nhds_zero
    simp only [Pi.sub_apply, sub_div] at this
    have key : Tendsto (fun x ↦ v x / v x) l (𝓝 1) :=
      (tendsto_congr' <| hz.mono fun x hnz ↦ @div_self _ _ (v x) hnz).mpr tendsto_const_nhds
    convert this.add key
    · simp
    · norm_num
  · exact isEquivalent_of_tendsto_one (hz.mono fun x hnvz hz ↦ (hnvz hz).elim)

Asymptotic equivalence via non-vanishing ratio tending to one

Informal description

Let $u, v : \alpha \to \beta$ be functions where $\beta$ is a normed field, and let $l$ be a filter on $\alpha$. Suppose that $v(x) \neq 0$ for all $x$ in a neighborhood of $l$. Then $u$ is asymptotically equivalent to $v$ along $l$ (denoted $u \sim[l] v$) if and only if the ratio $u/v$ tends to $1$ along $l$, i.e., $\lim_{x \to l} \frac{u(x)}{v(x)} = 1$.

Asymptotics.IsEquivalent.smul theorem

 {α E 𝕜 : Type*} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {a b : α → 𝕜} {u v : α → E} {l : Filter α}
  (hab : a ~[l] b) (huv : u ~[l] v) : (fun x ↦ a x • u x) ~[l] fun x ↦ b x • v x

Full source

theorem IsEquivalent.smul {α E 𝕜 : Type*} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
    {a b : α → 𝕜} {u v : α → E} {l : Filter α} (hab : a ~[l] b) (huv : u ~[l] v) :
    (fun x ↦ a x • u x) ~[l] fun x ↦ b x • v x := by
  rcases hab.exists_eq_mul with ⟨φ, hφ, habφ⟩
  have : ((fun x ↦ a x • u x) - (fun x ↦ b x • v x)) =ᶠ[l] fun x ↦ b x • (φ x • u x - v x) := by
    convert (habφ.comp₂ (· • ·) <| EventuallyEq.refl _ u).sub
      (EventuallyEq.refl _ fun x ↦ b x • v x) using 1
    ext
    rw [Pi.mul_apply, mul_comm, mul_smul, ← smul_sub]
  refine (isLittleO_congr this.symm <| EventuallyEq.rfl).mp ((isBigO_refl b l).smul_isLittleO ?_)
  rcases huv.isBigO.exists_pos with ⟨C, hC, hCuv⟩
  rw [IsEquivalent] at *
  rw [isLittleO_iff] at *
  rw [IsBigOWith] at hCuv
  simp only [Metric.tendsto_nhds, dist_eq_norm] at hφ
  intro c hc
  specialize hφ (c / 2 / C) (div_pos (div_pos hc zero_lt_two) hC)
  specialize huv (div_pos hc zero_lt_two)
  refine hφ.mp (huv.mp <| hCuv.mono fun x hCuvx huvx hφx ↦ ?_)
  have key :=
    calc
      ‖φ x - 1‖ * ‖u x‖ ≤ c / 2 / C * ‖u x‖ := by gcongr
      _ ≤ c / 2 / C * (C * ‖v x‖) := by gcongr
      _ = c / 2 * ‖v x‖ := by
        field_simp [hC.ne.symm]
        ring
  calc
    ‖((fun x : α ↦ φ x • u x) - v) x‖ = ‖(φ x - 1) • u x + (u x - v x)‖ := by
      simp [sub_smul, sub_add]
    _ ≤ ‖(φ x - 1) • u x‖ + ‖u x - v x‖ := norm_add_le _ _
    _ = ‖φ x - 1‖ * ‖u x‖ + ‖u x - v x‖ := by rw [norm_smul]
    _ ≤ c / 2 * ‖v x‖ + ‖u x - v x‖ := by gcongr
    _ ≤ c / 2 * ‖v x‖ + c / 2 * ‖v x‖ := by gcongr; exact huvx
    _ = c * ‖v x‖ := by ring

Asymptotic equivalence is preserved under scalar multiplication: $a \sim[l] b$ and $u \sim[l] v$ implies $a \cdot u \sim[l] b \cdot v$

Informal description

Let $\alpha$ be a type, $E$ a normed additive commutative group, and $\mathbb{K}$ a normed field. Suppose $E$ is a normed space over $\mathbb{K}$. For functions $a, b : \alpha \to \mathbb{K}$ and $u, v : \alpha \to E$, and a filter $l$ on $\alpha$, if $a$ is asymptotically equivalent to $b$ along $l$ (denoted $a \sim[l] b$) and $u$ is asymptotically equivalent to $v$ along $l$ (denoted $u \sim[l] v$), then the function $x \mapsto a(x) \cdot u(x)$ is asymptotically equivalent to $x \mapsto b(x) \cdot v(x)$ along $l$.

Asymptotics.IsEquivalent.mul theorem

(htu : t ~[l] u) (hvw : v ~[l] w) : t * v ~[l] u * w

Full source

protected theorem IsEquivalent.mul (htu : t ~[l] u) (hvw : v ~[l] w) : t * v ~[l] u * w :=
  htu.smul hvw

Asymptotic equivalence is preserved under multiplication: $t \sim[l] u$ and $v \sim[l] w$ implies $t v \sim[l] u w$

Informal description

Let $\alpha$ be a type, $\beta$ a normed field, and $l$ a filter on $\alpha$. For functions $t, u, v, w : \alpha \to \beta$, if $t$ is asymptotically equivalent to $u$ along $l$ (denoted $t \sim[l] u$) and $v$ is asymptotically equivalent to $w$ along $l$ (denoted $v \sim[l] w$), then the product function $t \cdot v$ is asymptotically equivalent to $u \cdot w$ along $l$ (i.e., $t v \sim[l] u w$).

Asymptotics.IsEquivalent.listProd theorem

 {L : List ι} {f g : ι → α → β} (h : ∀ i ∈ L, f i ~[l] g i) :
  (fun x ↦ (L.map (f · x)).prod) ~[l] (fun x ↦ (L.map (g · x)).prod)

Full source

theorem IsEquivalent.listProd {L : List ι} {f g : ι → α → β} (h : ∀ i ∈ L, f i ~[l] g i) :
    (fun x ↦ (L.map (f · x)).prod) ~[l] (fun x ↦ (L.map (g · x)).prod) := by
  induction L with
  | nil => simp [IsEquivalent.refl]
  | cons i L ihL =>
    simp only [List.forall_mem_cons, List.map_cons, List.prod_cons] at h ⊢
    exact h.1.mul (ihL h.2)

Asymptotic equivalence of list products: $\prod_{i \in L} f_i \sim[l] \prod_{i \in L} g_i$ when $f_i \sim[l] g_i$ for all $i \in L$

Informal description

Let $\alpha$ be a type, $\beta$ a normed field, and $l$ a filter on $\alpha$. Given a list $L$ of indices and functions $f, g : \iota \to \alpha \to \beta$ such that for every $i \in L$, $f_i$ is asymptotically equivalent to $g_i$ along $l$ (denoted $f_i \sim[l] g_i$), then the product function $\prod_{i \in L} f_i(\cdot)$ is asymptotically equivalent to $\prod_{i \in L} g_i(\cdot)$ along $l$.

Asymptotics.IsEquivalent.multisetProd theorem

 {s : Multiset ι} {f g : ι → α → β} (h : ∀ i ∈ s, f i ~[l] g i) :
  (fun x ↦ (s.map (f · x)).prod) ~[l] (fun x ↦ (s.map (g · x)).prod)

Full source

theorem IsEquivalent.multisetProd {s : Multiset ι} {f g : ι → α → β} (h : ∀ i ∈ s, f i ~[l] g i) :
    (fun x ↦ (s.map (f · x)).prod) ~[l] (fun x ↦ (s.map (g · x)).prod) := by
  obtain ⟨l, rfl⟩ : ∃ l : List ι, ↑l = s := Quotient.mk_surjective s
  exact listProd h

Asymptotic equivalence of multiset products: $\prod_{i \in s} f_i \sim[l] \prod_{i \in s} g_i$ when $f_i \sim[l] g_i$ for all $i \in s$

Informal description

Let $\alpha$ be a type, $\beta$ a normed field, and $l$ a filter on $\alpha$. Given a multiset $s$ of indices and functions $f, g : \iota \to \alpha \to \beta$ such that for every $i \in s$, $f_i$ is asymptotically equivalent to $g_i$ along $l$ (i.e., $f_i \sim[l] g_i$), then the product function $\prod_{i \in s} f_i(\cdot)$ is asymptotically equivalent to $\prod_{i \in s} g_i(\cdot)$ along $l$.

Asymptotics.IsEquivalent.finsetProd theorem

 {s : Finset ι} {f g : ι → α → β} (h : ∀ i ∈ s, f i ~[l] g i) : (∏ i ∈ s, f i ·) ~[l] (∏ i ∈ s, g i ·)

Full source

theorem IsEquivalent.finsetProd {s : Finset ι} {f g : ι → α → β} (h : ∀ i ∈ s, f i ~[l] g i) :
    (∏ i ∈ s, f i ·) ~[l] (∏ i ∈ s, g i ·) :=
  multisetProd h

Asymptotic equivalence of finite products: $\prod_{i \in s} f_i \sim[l] \prod_{i \in s} g_i$ when $f_i \sim[l] g_i$ for all $i \in s$

Informal description

Let $\alpha$ be a type, $\beta$ a normed field, and $l$ a filter on $\alpha$. Given a finite set $s$ of indices and functions $f, g : \iota \to \alpha \to \beta$ such that for every $i \in s$, $f_i$ is asymptotically equivalent to $g_i$ along $l$ (i.e., $f_i \sim[l] g_i$), then the product function $\prod_{i \in s} f_i(\cdot)$ is asymptotically equivalent to $\prod_{i \in s} g_i(\cdot)$ along $l$.

Asymptotics.IsEquivalent.inv theorem

(huv : u ~[l] v) : (fun x ↦ (u x)⁻¹) ~[l] fun x ↦ (v x)⁻¹

Full source

protected theorem IsEquivalent.inv (huv : u ~[l] v) : (fun x ↦ (u x)⁻¹) ~[l] fun x ↦ (v x)⁻¹ := by
  rw [isEquivalent_iff_exists_eq_mul] at *
  rcases huv with ⟨φ, hφ, h⟩
  rw [← inv_one]
  refine ⟨fun x ↦ (φ x)⁻¹, Tendsto.inv₀ hφ (by norm_num), ?_⟩
  convert h.inv
  simp [mul_comm]

Asymptotic equivalence is preserved under pointwise inversion: $u \sim[l] v$ implies $u^{-1} \sim[l] v^{-1}$

Informal description

Let $u, v : \alpha \to \beta$ be functions from a type $\alpha$ to a normed field $\beta$, and let $l$ be a filter on $\alpha$. If $u$ is asymptotically equivalent to $v$ along $l$ (denoted $u \sim[l] v$), then the pointwise inverses $x \mapsto (u x)^{-1}$ and $x \mapsto (v x)^{-1}$ are also asymptotically equivalent along $l$.

Asymptotics.IsEquivalent.div theorem

(htu : t ~[l] u) (hvw : v ~[l] w) : (fun x ↦ t x / v x) ~[l] fun x ↦ u x / w x

Full source

protected theorem IsEquivalent.div (htu : t ~[l] u) (hvw : v ~[l] w) :
    (fun x ↦ t x / v x) ~[l] fun x ↦ u x / w x := by
  simpa only [div_eq_mul_inv] using htu.mul hvw.inv

Asymptotic equivalence is preserved under division: $t \sim[l] u$ and $v \sim[l] w$ implies $t/v \sim[l] u/w$

Informal description

Let $\alpha$ be a type, $\beta$ a normed field, and $l$ a filter on $\alpha$. For functions $t, u, v, w : \alpha \to \beta$, if $t$ is asymptotically equivalent to $u$ along $l$ (denoted $t \sim[l] u$) and $v$ is asymptotically equivalent to $w$ along $l$ (denoted $v \sim[l] w$), then the quotient function $x \mapsto t(x)/v(x)$ is asymptotically equivalent to $x \mapsto u(x)/w(x)$ along $l$ (i.e., $t/v \sim[l] u/w$).

Asymptotics.IsEquivalent.pow theorem

(h : t ~[l] u) (n : ℕ) : t ^ n ~[l] u ^ n

Full source

protected theorem IsEquivalent.pow (h : t ~[l] u) (n : ℕ) : t ^ n ~[l] u ^ n := by
  induction n with
  | zero => simpa using IsEquivalent.refl
  | succ _ ih => simpa [pow_succ] using ih.mul h

Asymptotic equivalence is preserved under natural number powers: $t \sim[l] u$ implies $t^n \sim[l] u^n$ for $n \in \mathbb{N}$

Informal description

Let $\alpha$ be a type, $\beta$ a normed field, and $l$ a filter on $\alpha$. For functions $t, u : \alpha \to \beta$, if $t$ is asymptotically equivalent to $u$ along $l$ (denoted $t \sim[l] u$), then for any natural number $n$, the $n$-th power functions $t^n$ and $u^n$ are also asymptotically equivalent along $l$ (i.e., $t^n \sim[l] u^n$).

Asymptotics.IsEquivalent.zpow theorem

(h : t ~[l] u) (z : ℤ) : t ^ z ~[l] u ^ z

Full source

protected theorem IsEquivalent.zpow (h : t ~[l] u) (z : ℤ) : t ^ z ~[l] u ^ z := by
  match z with
  | Int.ofNat _ => simpa using h.pow _
  | Int.negSucc _ => simpa using (h.pow _).inv

Asymptotic equivalence is preserved under integer powers: $t \sim[l] u$ implies $t^z \sim[l] u^z$ for $z \in \mathbb{Z}$

Informal description

Let $\alpha$ be a type, $\beta$ a normed field, and $l$ a filter on $\alpha$. For functions $t, u : \alpha \to \beta$, if $t$ is asymptotically equivalent to $u$ along $l$ (denoted $t \sim[l] u$), then for any integer $z$, the $z$-th power functions $t^z$ and $u^z$ are also asymptotically equivalent along $l$ (i.e., $t^z \sim[l] u^z$).

Asymptotics.IsEquivalent.tendsto_atTop theorem

[OrderTopology β] (huv : u ~[l] v) (hu : Tendsto u l atTop) : Tendsto v l atTop

Full source

theorem IsEquivalent.tendsto_atTop [OrderTopology β] (huv : u ~[l] v) (hu : Tendsto u l atTop) :
    Tendsto v l atTop :=
  let ⟨φ, hφ, h⟩ := huv.symm.exists_eq_mul
  Tendsto.congr' h.symm (mul_comm u φ ▸ hu.atTop_mul_pos zero_lt_one hφ)

Asymptotic equivalence preserves divergence to $+\infty$

Informal description

Let $\beta$ be a normed field with an order topology. If two functions $u, v : \alpha \to \beta$ are asymptotically equivalent along a filter $l$ (i.e., $u \sim[l] v$) and $u$ tends to $+\infty$ along $l$, then $v$ also tends to $+\infty$ along $l$.

Asymptotics.IsEquivalent.tendsto_atTop_iff theorem

[OrderTopology β] (huv : u ~[l] v) : Tendsto u l atTop ↔ Tendsto v l atTop

Full source

theorem IsEquivalent.tendsto_atTop_iff [OrderTopology β] (huv : u ~[l] v) :
    TendstoTendsto u l atTop ↔ Tendsto v l atTop :=
  ⟨huv.tendsto_atTop, huv.symm.tendsto_atTop⟩

Asymptotic equivalence preserves divergence to $+\infty$ (iff version)

Informal description

Let $\beta$ be a normed field with an order topology. For two functions $u, v : \alpha \to \beta$ that are asymptotically equivalent along a filter $l$ (i.e., $u \sim[l] v$), the function $u$ tends to $+\infty$ along $l$ if and only if $v$ tends to $+\infty$ along $l$.

Asymptotics.IsEquivalent.tendsto_atBot theorem

[OrderTopology β] (huv : u ~[l] v) (hu : Tendsto u l atBot) : Tendsto v l atBot

Full source

theorem IsEquivalent.tendsto_atBot [OrderTopology β] (huv : u ~[l] v) (hu : Tendsto u l atBot) :
    Tendsto v l atBot := by
  convert tendsto_neg_atTop_atBot.comp (huv.neg.tendsto_atTop <| tendsto_neg_atBot_atTop.comp hu)
  ext
  simp

Asymptotic equivalence preserves divergence to $-\infty$

Informal description

Let $\beta$ be a normed field with an order topology. If two functions $u, v : \alpha \to \beta$ are asymptotically equivalent along a filter $l$ (i.e., $u \sim[l] v$) and $u$ tends to $-\infty$ along $l$, then $v$ also tends to $-\infty$ along $l$.

Asymptotics.IsEquivalent.tendsto_atBot_iff theorem

[OrderTopology β] (huv : u ~[l] v) : Tendsto u l atBot ↔ Tendsto v l atBot

Full source

theorem IsEquivalent.tendsto_atBot_iff [OrderTopology β] (huv : u ~[l] v) :
    TendstoTendsto u l atBot ↔ Tendsto v l atBot :=
  ⟨huv.tendsto_atBot, huv.symm.tendsto_atBot⟩

Asymptotic equivalence preserves divergence to $-\infty$ (iff version)

Informal description

Let $\beta$ be a normed field with an order topology. For two functions $u, v : \alpha \to \beta$ that are asymptotically equivalent along a filter $l$ (i.e., $u \sim[l] v$), the function $u$ tends to $-\infty$ along $l$ if and only if $v$ tends to $-\infty$ along $l$.

Filter.EventuallyEq.isEquivalent theorem

{u v : α → β} (h : u =ᶠ[l] v) : u ~[l] v

Full source

theorem Filter.EventuallyEq.isEquivalent {u v : α → β} (h : u =ᶠ[l] v) : u ~[l] v :=
  IsEquivalent.congr_right (isLittleO_refl_left _ _) h

Eventual equality implies asymptotic equivalence

Informal description

For any two functions $u, v : \alpha \to \beta$ from a type $\alpha$ to a normed additive commutative group $\beta$, if $u$ is eventually equal to $v$ along a filter $l$ (i.e., $u(x) = v(x)$ for all $x$ in a set that is eventually in $l$), then $u$ is asymptotically equivalent to $v$ along $l$ (denoted $u \sim[l] v$).

Filter.EventuallyEq.trans_isEquivalent theorem

{f g₁ g₂ : α → β} (h : f =ᶠ[l] g₁) (h₂ : g₁ ~[l] g₂) : f ~[l] g₂

Full source

@[trans]
theorem Filter.EventuallyEq.trans_isEquivalent {f g₁ g₂ : α → β} (h : f =ᶠ[l] g₁)
    (h₂ : g₁ ~[l] g₂) : f ~[l] g₂ :=
  h.isEquivalent.trans h₂

Transitivity of Asymptotic Equivalence via Eventual Equality: $f =ᶠ[l] g_1 \land g_1 \sim[l] g_2 \Rightarrow f \sim[l] g_2$

Informal description

Let $f, g_1, g_2 : \alpha \to \beta$ be functions from a type $\alpha$ to a normed additive commutative group $\beta$, and let $l$ be a filter on $\alpha$. If $f$ is eventually equal to $g_1$ along $l$ (i.e., $f(x) = g_1(x)$ for all $x$ in a set that is eventually in $l$) and $g_1$ is asymptotically equivalent to $g_2$ along $l$ (i.e., $g_1 \sim[l] g_2$), then $f$ is asymptotically equivalent to $g_2$ along $l$ (i.e., $f \sim[l] g_2$).

Asymptotics.transIsEquivalentIsEquivalent instance

: @Trans (α → β) (α → β) (α → β) (IsEquivalent l) (IsEquivalent l) (IsEquivalent l)

Full source

instance transIsEquivalentIsEquivalent :
    @Trans (α → β) (α → β) (α → β) (IsEquivalent l) (IsEquivalent l) (IsEquivalent l) where
  trans := IsEquivalent.trans

Transitivity of Asymptotic Equivalence

Informal description

The relation of asymptotic equivalence $u \sim[l] v$ is transitive. That is, for functions $u, v, w : \alpha \to \beta$ where $\beta$ is a normed additive commutative group, if $u \sim[l] v$ and $v \sim[l] w$ along a filter $l$, then $u \sim[l] w$.

Asymptotics.transEventuallyEqIsEquivalent instance

: @Trans (α → β) (α → β) (α → β) (EventuallyEq l) (IsEquivalent l) (IsEquivalent l)

Full source

instance transEventuallyEqIsEquivalent :
    @Trans (α → β) (α → β) (α → β) (EventuallyEq l) (IsEquivalent l) (IsEquivalent l) where
  trans := EventuallyEq.trans_isEquivalent

Transitivity of Eventual Equality and Asymptotic Equivalence

Informal description

The relation of eventual equality between functions is transitive with asymptotic equivalence. That is, for functions $f, g_1, g_2 : \alpha \to \beta$ where $\beta$ is a normed additive commutative group, if $f$ is eventually equal to $g_1$ along a filter $l$ and $g_1$ is asymptotically equivalent to $g_2$ along $l$, then $f$ is asymptotically equivalent to $g_2$ along $l$.

Asymptotics.IsEquivalent.trans_eventuallyEq theorem

{f g₁ g₂ : α → β} (h : f ~[l] g₁) (h₂ : g₁ =ᶠ[l] g₂) : f ~[l] g₂

Full source

@[trans]
theorem IsEquivalent.trans_eventuallyEq {f g₁ g₂ : α → β} (h : f ~[l] g₁)
    (h₂ : g₁ =ᶠ[l] g₂) : f ~[l] g₂ :=
  h.trans h₂.isEquivalent

Transitivity of Asymptotic Equivalence with Eventual Equality: $f \sim[l] g_1 \land g_1 =ᶠ[l] g_2 \Rightarrow f \sim[l] g_2$

Informal description

Let $f, g_1, g_2 : \alpha \to \beta$ be functions from a type $\alpha$ to a normed additive commutative group $\beta$, and let $l$ be a filter on $\alpha$. If $f$ is asymptotically equivalent to $g_1$ along $l$ (i.e., $f \sim[l] g_1$) and $g_1$ is eventually equal to $g_2$ along $l$ (i.e., $g_1(x) = g_2(x)$ for all $x$ in a set that is eventually in $l$), then $f$ is asymptotically equivalent to $g_2$ along $l$ (i.e., $f \sim[l] g_2$).

Asymptotics.transIsEquivalentEventuallyEq instance

: @Trans (α → β) (α → β) (α → β) (IsEquivalent l) (EventuallyEq l) (IsEquivalent l)

Full source

instance transIsEquivalentEventuallyEq :
    @Trans (α → β) (α → β) (α → β) (IsEquivalent l) (EventuallyEq l) (IsEquivalent l) where
  trans := IsEquivalent.trans_eventuallyEq

Transitivity of Asymptotic Equivalence with Eventual Equality

Informal description

The relation of asymptotic equivalence $u \sim[l] v$ between functions $u, v : \alpha \to \beta$ is transitive with respect to eventual equality. That is, if $u \sim[l] v$ and $v$ is eventually equal to $w$ along $l$, then $u \sim[l] w$.

Asymptotics.IsEquivalent.trans_isBigO theorem

{f g₁ : α → β} {g₂ : α → β₂} (h : f ~[l] g₁) (h₂ : g₁ =O[l] g₂) : f =O[l] g₂

Full source

@[trans]
theorem IsEquivalent.trans_isBigO {f g₁ : α → β} {g₂ : α → β₂} (h : f ~[l] g₁) (h₂ : g₁ =O[l] g₂) :
    f =O[l] g₂ :=
  IsBigO.trans h.isBigO h₂

Transitivity of Asymptotic Equivalence and Big-O: $f \sim[l] g_1 \land g_1 = O(g_2) \Rightarrow f = O(g_2)$

Informal description

Let $f, g_1 : \alpha \to \beta$ and $g_2 : \alpha \to \beta_2$ be functions, and let $l$ be a filter on $\alpha$. If $f$ is asymptotically equivalent to $g_1$ along $l$ (i.e., $f \sim[l] g_1$) and $g_1$ is big-O of $g_2$ along $l$ (i.e., $g_1 = O(g_2)$ at $l$), then $f$ is big-O of $g_2$ along $l$ (i.e., $f = O(g_2)$ at $l$).

Asymptotics.transIsEquivalentIsBigO instance

: @Trans (α → β) (α → β) (α → β₂) (IsEquivalent l) (IsBigO l) (IsBigO l)

Full source

instance transIsEquivalentIsBigO :
    @Trans (α → β) (α → β) (α → β₂) (IsEquivalent l) (IsBigO l) (IsBigO l) where
  trans := IsEquivalent.trans_isBigO

Transitivity of Asymptotic Equivalence and Big-O

Informal description

The relation of asymptotic equivalence $u \sim[l] v$ between functions $u, v : \alpha \to \beta$ is transitive with respect to the big-O relation. That is, if $u \sim[l] v$ and $v = O[l] w$ for some function $w : \alpha \to \beta_2$, then $u = O[l] w$.

Asymptotics.IsBigO.trans_isEquivalent theorem

{f : α → β₂} {g₁ g₂ : α → β} (h : f =O[l] g₁) (h₂ : g₁ ~[l] g₂) : f =O[l] g₂

Full source

@[trans]
theorem IsBigO.trans_isEquivalent {f : α → β₂} {g₁ g₂ : α → β} (h : f =O[l] g₁) (h₂ : g₁ ~[l] g₂) :
    f =O[l] g₂ :=
  IsBigO.trans h h₂.isBigO

Transitivity of Big-O and Asymptotic Equivalence: $f = O(g_1) \land g_1 \sim g_2 \Rightarrow f = O(g_2)$

Informal description

Let $f : \alpha \to \beta_2$ and $g_1, g_2 : \alpha \to \beta$ be functions, where $\beta$ is a normed additive commutative group and $\beta_2$ is a normed space. If $f$ is big-O of $g_1$ along the filter $l$ (i.e., $f = O[l] g_1$) and $g_1$ is asymptotically equivalent to $g_2$ along $l$ (i.e., $g_1 \sim[l] g_2$), then $f$ is big-O of $g_2$ along $l$ (i.e., $f = O[l] g_2$).

Asymptotics.transIsBigOIsEquivalent instance

: @Trans (α → β₂) (α → β) (α → β) (IsBigO l) (IsEquivalent l) (IsBigO l)

Full source

instance transIsBigOIsEquivalent :
    @Trans (α → β₂) (α → β) (α → β) (IsBigO l) (IsEquivalent l) (IsBigO l) where
  trans := IsBigO.trans_isEquivalent

Transitivity of Big-O and Asymptotic Equivalence

Informal description

The relation of big-O is transitive with respect to asymptotic equivalence. Specifically, for functions $f : \alpha \to \beta_2$, $g : \alpha \to \beta$, and $h : \alpha \to \beta$, if $f = O[l] g$ (i.e., $f$ is big-O of $g$ along the filter $l$) and $g \sim[l] h$ (i.e., $g$ is asymptotically equivalent to $h$ along $l$), then $f = O[l] h$ (i.e., $f$ is big-O of $h$ along $l$).

Asymptotics.IsEquivalent.trans_isLittleO theorem

{f g₁ : α → β} {g₂ : α → β₂} (h : f ~[l] g₁) (h₂ : g₁ =o[l] g₂) : f =o[l] g₂

Full source

@[trans]
theorem IsEquivalent.trans_isLittleO {f g₁ : α → β} {g₂ : α → β₂} (h : f ~[l] g₁)
    (h₂ : g₁ =o[l] g₂) : f =o[l] g₂ :=
  IsBigO.trans_isLittleO h.isBigO h₂

Transitivity of asymptotic equivalence and little-o: $f \sim[l] g_1 \land g_1 = o[l] g_2 \Rightarrow f = o[l] g_2$

Informal description

Let $f, g_1 : \alpha \to \beta$ and $g_2 : \alpha \to \beta_2$ be functions, where $\beta$ is a normed additive commutative group and $\beta_2$ is a normed space. If $f$ is asymptotically equivalent to $g_1$ along the filter $l$ (i.e., $f \sim[l] g_1$) and $g_1$ is little-o of $g_2$ along $l$ (i.e., $g_1 = o[l] g_2$), then $f$ is little-o of $g_2$ along $l$ (i.e., $f = o[l] g_2$).

Asymptotics.transIsEquivalentIsLittleO instance

: @Trans (α → β) (α → β) (α → β₂) (IsEquivalent l) (IsLittleO l) (IsLittleO l)

Full source

instance transIsEquivalentIsLittleO :
    @Trans (α → β) (α → β) (α → β₂) (IsEquivalent l) (IsLittleO l) (IsLittleO l) where
  trans := IsEquivalent.trans_isLittleO

Transitivity of Asymptotic Equivalence and Little-o

Informal description

The relation of asymptotic equivalence is transitive with respect to the little-o relation. Specifically, for functions $f, g : \alpha \to \beta$ and $h : \alpha \to \beta_2$, if $f \sim[l] g$ (i.e., $f$ is asymptotically equivalent to $g$ along the filter $l$) and $g = o[l] h$ (i.e., $g$ is little-o of $h$ along $l$), then $f = o[l] h$ (i.e., $f$ is little-o of $h$ along $l$).

Asymptotics.IsLittleO.trans_isEquivalent theorem

{f : α → β₂} {g₁ g₂ : α → β} (h : f =o[l] g₁) (h₂ : g₁ ~[l] g₂) : f =o[l] g₂

Full source

@[trans]
theorem IsLittleO.trans_isEquivalent {f : α → β₂} {g₁ g₂ : α → β} (h : f =o[l] g₁)
    (h₂ : g₁ ~[l] g₂) : f =o[l] g₂ :=
  IsLittleO.trans_isBigO h h₂.isBigO

Transitivity of Little-o and Asymptotic Equivalence: $f = o(g_1) \land g_1 \sim g_2 \Rightarrow f = o(g_2)$

Informal description

Let $f : \alpha \to \beta_2$ and $g_1, g_2 : \alpha \to \beta$ be functions to normed spaces, and let $l$ be a filter on $\alpha$. If $f$ is little-o of $g_1$ with respect to $l$ (i.e., $f = o[l] g_1$) and $g_1$ is asymptotically equivalent to $g_2$ with respect to $l$ (i.e., $g_1 \sim[l] g_2$), then $f$ is little-o of $g_2$ with respect to $l$ (i.e., $f = o[l] g_2$).

Asymptotics.transIsLittleOIsEquivalent instance

: @Trans (α → β₂) (α → β) (α → β) (IsLittleO l) (IsEquivalent l) (IsLittleO l)

Full source

instance transIsLittleOIsEquivalent :
    @Trans (α → β₂) (α → β) (α → β) (IsLittleO l) (IsEquivalent l) (IsLittleO l) where
  trans := IsLittleO.trans_isEquivalent

Transitivity of Little-o through Asymptotic Equivalence

Informal description

For any filter $l$ on a type $\alpha$ and functions $f : \alpha \to \beta_2$, $g_1 : \alpha \to \beta$, and $g_2 : \alpha \to \beta$ where $\beta$ and $\beta_2$ are normed additive commutative groups, the relation $f = o[l] g_1$ and $g_1 \sim[l] g_2$ implies $f = o[l] g_2$. This establishes the transitivity of the little-o relation through asymptotic equivalence.

Asymptotics.IsEquivalent.trans_isTheta theorem

{f g₁ : α → β} {g₂ : α → β₂} (h : f ~[l] g₁) (h₂ : g₁ =Θ[l] g₂) : f =Θ[l] g₂

Full source

@[trans]
theorem IsEquivalent.trans_isTheta {f g₁ : α → β} {g₂ : α → β₂} (h : f ~[l] g₁)
    (h₂ : g₁ =Θ[l] g₂) : f =Θ[l] g₂ :=
  IsTheta.trans h.isTheta h₂

Transitivity of Asymptotic Equivalence through Big-Theta: $f \sim g_1 \land g_1 = \Theta g_2 \Rightarrow f = \Theta g_2$

Informal description

Let $f, g_1 : \alpha \to \beta$ and $g_2 : \alpha \to \beta_2$ be functions where $\beta$ and $\beta_2$ are normed additive commutative groups. If $f$ is asymptotically equivalent to $g_1$ along the filter $l$ (i.e., $f \sim[l] g_1$) and $g_1$ is big-Theta equivalent to $g_2$ along $l$ (i.e., $g_1 = \Theta[l] g_2$), then $f$ is big-Theta equivalent to $g_2$ along $l$ (i.e., $f = \Theta[l] g_2$).

Asymptotics.transIsEquivalentIsTheta instance

: @Trans (α → β) (α → β) (α → β₂) (IsEquivalent l) (IsTheta l) (IsTheta l)

Full source

instance transIsEquivalentIsTheta :
    @Trans (α → β) (α → β) (α → β₂) (IsEquivalent l) (IsTheta l) (IsTheta l) where
  trans := IsEquivalent.trans_isTheta

Transitivity of Asymptotic Equivalence via Big-Theta

Informal description

The relation of asymptotic equivalence $u \sim[l] v$ is transitive with respect to the big-Theta relation. That is, for functions $f, g_1 : \alpha \to \beta$ and $g_2 : \alpha \to \beta_2$ where $\beta$ and $\beta_2$ are normed additive commutative groups, if $f \sim[l] g_1$ and $g_1 = \Theta[l] g_2$, then $f = \Theta[l] g_2$.

Asymptotics.IsTheta.trans_isEquivalent theorem

{f : α → β₂} {g₁ g₂ : α → β} (h : f =Θ[l] g₁) (h₂ : g₁ ~[l] g₂) : f =Θ[l] g₂

Full source

@[trans]
theorem IsTheta.trans_isEquivalent {f : α → β₂} {g₁ g₂ : α → β} (h : f =Θ[l] g₁)
    (h₂ : g₁ ~[l] g₂) : f =Θ[l] g₂ :=
  IsTheta.trans h h₂.isTheta

Transitivity of Big-Theta via Asymptotic Equivalence: $f = \Theta[l] g_1$ and $g_1 \sim[l] g_2$ implies $f = \Theta[l] g_2$

Informal description

Let $f : \alpha \to \beta_2$ and $g_1, g_2 : \alpha \to \beta$ be functions. If $f$ is big-Theta equivalent to $g_1$ along the filter $l$ (i.e., $f = \Theta[l] g_1$) and $g_1$ is asymptotically equivalent to $g_2$ along $l$ (i.e., $g_1 \sim[l] g_2$), then $f$ is big-Theta equivalent to $g_2$ along $l$ (i.e., $f = \Theta[l] g_2$).

Asymptotics.transIsThetaIsEquivalent instance

: @Trans (α → β₂) (α → β) (α → β) (IsTheta l) (IsEquivalent l) (IsTheta l)

Full source

instance transIsThetaIsEquivalent :
    @Trans (α → β₂) (α → β) (α → β) (IsTheta l) (IsEquivalent l) (IsTheta l) where
  trans := IsTheta.trans_isEquivalent

Transitivity of Big-Theta via Asymptotic Equivalence

Informal description

The relation of being big-Theta (`IsTheta`) followed by asymptotic equivalence (`IsEquivalent`) implies big-Theta. That is, for functions $f : \alpha \to \beta_2$, $g_1 : \alpha \to \beta$, and $g_2 : \alpha \to \beta$, if $f$ is big-Theta equivalent to $g_1$ along the filter $l$ and $g_1$ is asymptotically equivalent to $g_2$ along $l$, then $f$ is big-Theta equivalent to $g_2$ along $l$.

Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Notations

Main results

Implementation Notes