Mathlib.Analysis.Asymptotics.Theta

Asymptotics.IsTheta definition

(l : Filter α) (f : α → E) (g : α → F) : Prop

Full source

/-- We say that `f` is `Θ(g)` along a filter `l` (notation: `f =Θ[l] g`) if `f =O[l] g` and
`g =O[l] f`. -/
def IsTheta (l : Filter α) (f : α → E) (g : α → F) : Prop :=
  IsBigOIsBigO l f g ∧ IsBigO l g f

Asymptotic equivalence up to a constant factor

Informal description

Given a filter $ l $ on a type $ \alpha $, and two functions $ f : \alpha \to E $ and $ g : \alpha \to F $, we say $ f $ is asymptotically equivalent to $ g $ up to a constant factor (denoted $ f = \Theta[l] g $) if both $ f = O[l] g $ and $ g = O[l] f $ hold. This means there exist positive constants $ C_1, C_2 $ such that for all $ x $ in some neighborhood determined by $ l $, we have $ C_1 \|g(x)\| \leq \|f(x)\| \leq C_2 \|g(x)\| $.

Asymptotics.term_=Θ[_]_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
notation:100 f " =Θ[" l "] " g:100 => IsTheta l f g

Asymptotic equivalence up to a constant factor

Informal description

The notation $ f = \Theta[l] g $ denotes that the functions $ f $ and $ g $ are asymptotically equivalent up to a constant factor with respect to the filter $ l $. This means that $ f $ is big-O of $ g $ and $ g $ is big-O of $ f $ under the filter $ l $, i.e., $ f = O[l] g $ and $ g = O[l] f $.

Asymptotics.IsBigO.antisymm theorem

(h₁ : f =O[l] g) (h₂ : g =O[l] f) : f =Θ[l] g

Full source

theorem IsBigO.antisymm (h₁ : f =O[l] g) (h₂ : g =O[l] f) : f =Θ[l] g :=
  ⟨h₁, h₂⟩

Antisymmetry of Asymptotic Equivalence: $f = O[l] g \land g = O[l] f \Rightarrow f = \Theta[l] g$

Informal description

Given two functions $f : \alpha \to E$ and $g : \alpha \to F$ and a filter $l$ on $\alpha$, if $f$ is asymptotically bounded above by $g$ (i.e., $f = O[l] g$) and $g$ is asymptotically bounded above by $f$ (i.e., $g = O[l] f$), then $f$ is asymptotically equivalent to $g$ up to a constant factor (i.e., $f = \Theta[l] g$).

Asymptotics.IsTheta.isBigO theorem

(h : f =Θ[l] g) : f =O[l] g

Full source

lemma IsTheta.isBigO (h : f =Θ[l] g) : f =O[l] g := h.1

Asymptotic equivalence implies big-O bound: $f = \Theta[l] g \Rightarrow f = O[l] g$

Informal description

Given two functions $f : \alpha \to E$ and $g : \alpha \to F$ and a filter $l$ on $\alpha$, if $f$ is asymptotically equivalent to $g$ up to a constant factor (i.e., $f = \Theta[l] g$), then $f$ is asymptotically bounded above by $g$ (i.e., $f = O[l] g$).

Asymptotics.IsTheta.isBigO_symm theorem

(h : f =Θ[l] g) : g =O[l] f

Full source

lemma IsTheta.isBigO_symm (h : f =Θ[l] g) : g =O[l] f := h.2

Asymptotic equivalence implies symmetric big-O bound: $f = \Theta[l] g \Rightarrow g = O[l] f$

Informal description

Given two functions $f : \alpha \to E$ and $g : \alpha \to F$ and a filter $l$ on $\alpha$, if $f$ is asymptotically equivalent to $g$ up to a constant factor (i.e., $f = \Theta[l] g$), then $g$ is asymptotically bounded above by $f$ (i.e., $g = O[l] f$).

Asymptotics.isTheta_refl theorem

(f : α → E) (l : Filter α) : f =Θ[l] f

Full source

@[refl]
theorem isTheta_refl (f : α → E) (l : Filter α) : f =Θ[l] f :=
  ⟨isBigO_refl _ _, isBigO_refl _ _⟩

Reflexivity of Asymptotic Equivalence: $f = \Theta[l] f$

Informal description

For any function $f \colon \alpha \to E$ mapping to a normed space $E$ and any filter $l$ on $\alpha$, the function $f$ is asymptotically equivalent to itself up to a constant factor along $l$, i.e., $f = \Theta[l] f$.

Asymptotics.isTheta_rfl theorem

: f =Θ[l] f

Full source

theorem isTheta_rfl : f =Θ[l] f :=
  isTheta_refl _ _

Reflexivity of Asymptotic Equivalence: $f = \Theta[l] f$

Informal description

For any function $f \colon \alpha \to E$ and any filter $l$ on $\alpha$, the function $f$ is asymptotically equivalent to itself up to a constant factor along $l$, i.e., $f = \Theta[l] f$.

Asymptotics.IsTheta.symm theorem

(h : f =Θ[l] g) : g =Θ[l] f

Full source

@[symm]
nonrec theorem IsTheta.symm (h : f =Θ[l] g) : g =Θ[l] f :=
  h.symm

Symmetry of Asymptotic Equivalence up to a Constant Factor

Informal description

For any functions $f : \alpha \to E$ and $g : \alpha \to F$ and a filter $l$ on $\alpha$, if $f$ is asymptotically equivalent to $g$ up to a constant factor (i.e., $f = \Theta[l] g$), then $g$ is also asymptotically equivalent to $f$ up to a constant factor (i.e., $g = \Theta[l] f$).

Asymptotics.isTheta_comm theorem

: f =Θ[l] g ↔ g =Θ[l] f

Full source

theorem isTheta_comm : f =Θ[l] gf =Θ[l] g ↔ g =Θ[l] f :=
  ⟨fun h ↦ h.symm, fun h ↦ h.symm⟩

Commutativity of Asymptotic Equivalence: $f = \Theta[l] g \leftrightarrow g = \Theta[l] f$

Informal description

For any functions $f : \alpha \to E$ and $g : \alpha \to F$ and a filter $l$ on $\alpha$, the asymptotic equivalence $f = \Theta[l] g$ holds if and only if $g = \Theta[l] f$ holds. In other words, $f$ is asymptotically equivalent to $g$ up to a constant factor if and only if $g$ is asymptotically equivalent to $f$ up to a constant factor.

Asymptotics.IsTheta.trans theorem

{f : α → E} {g : α → F'} {k : α → G} (h₁ : f =Θ[l] g) (h₂ : g =Θ[l] k) : f =Θ[l] k

Full source

@[trans]
theorem IsTheta.trans {f : α → E} {g : α → F'} {k : α → G} (h₁ : f =Θ[l] g) (h₂ : g =Θ[l] k) :
    f =Θ[l] k :=
  ⟨h₁.1.trans h₂.1, h₂.2.trans h₁.2⟩

Transitivity of Asymptotic Equivalence: $f = \Theta(g) \land g = \Theta(k) \Rightarrow f = \Theta(k)$

Informal description

Let $f : \alpha \to E$, $g : \alpha \to F'$, and $k : \alpha \to G$ be functions to normed spaces, and let $l$ be a filter on $\alpha$. If $f$ is asymptotically equivalent to $g$ up to a constant factor (i.e., $f = \Theta[l] g$) and $g$ is asymptotically equivalent to $k$ up to a constant factor (i.e., $g = \Theta[l] k$), then $f$ is asymptotically equivalent to $k$ up to a constant factor (i.e., $f = \Theta[l] k$).

Asymptotics.instTransForallIsTheta instance

: Trans (α := α → E) (β := α → F') (γ := α → G) (IsTheta l) (IsTheta l) (IsTheta l)

Full source

instance : Trans (α := α → E) (β := α → F') (γ := α → G) (IsTheta l) (IsTheta l) (IsTheta l) :=
  ⟨IsTheta.trans⟩

Transitivity of Asymptotic Equivalence ($\Theta$)

Informal description

The relation of asymptotic equivalence up to a constant factor ($f = \Theta[l] g$) is transitive. That is, for functions $f : \alpha \to E$, $g : \alpha \to F'$, and $k : \alpha \to G$ and a filter $l$ on $\alpha$, if $f = \Theta[l] g$ and $g = \Theta[l] k$, then $f = \Theta[l] k$.

Asymptotics.IsBigO.trans_isTheta theorem

{f : α → E} {g : α → F'} {k : α → G} (h₁ : f =O[l] g) (h₂ : g =Θ[l] k) : f =O[l] k

Full source

@[trans]
theorem IsBigO.trans_isTheta {f : α → E} {g : α → F'} {k : α → G} (h₁ : f =O[l] g)
    (h₂ : g =Θ[l] k) : f =O[l] k :=
  h₁.trans h₂.1

Transitivity of Big-O with Theta: $f = O(g) \land g = \Theta(k) \Rightarrow f = O(k)$

Informal description

Let $f : \alpha \to E$, $g : \alpha \to F'$, and $k : \alpha \to G$ be functions to normed spaces, and let $l$ be a filter on $\alpha$. If $f = O(g)$ along $l$ and $g = \Theta(k)$ along $l$, then $f = O(k)$ along $l$.

Asymptotics.instTransForallIsBigOIsTheta instance

: Trans (α := α → E) (β := α → F') (γ := α → G) (IsBigO l) (IsTheta l) (IsBigO l)

Full source

instance : Trans (α := α → E) (β := α → F') (γ := α → G) (IsBigO l) (IsTheta l) (IsBigO l) :=
  ⟨IsBigO.trans_isTheta⟩

Transitivity of Big-O through Theta

Informal description

For any functions $f : \alpha \to E$, $g : \alpha \to F'$, and $k : \alpha \to G$ to normed spaces and a filter $l$ on $\alpha$, the relation $f = O[l] g$ and $g = \Theta[l] k$ implies $f = O[l] k$. In other words, the big-O relation is transitive through asymptotic equivalence up to a constant factor.

Asymptotics.IsTheta.trans_isBigO theorem

{f : α → E} {g : α → F'} {k : α → G} (h₁ : f =Θ[l] g) (h₂ : g =O[l] k) : f =O[l] k

Full source

@[trans]
theorem IsTheta.trans_isBigO {f : α → E} {g : α → F'} {k : α → G} (h₁ : f =Θ[l] g)
    (h₂ : g =O[l] k) : f =O[l] k :=
  h₁.1.trans h₂

Transitivity of Theta and Big-O: $f = \Theta(g) \land g = O(k) \Rightarrow f = O(k)$

Informal description

Let $f : \alpha \to E$, $g : \alpha \to F'$, and $k : \alpha \to G$ be functions to normed spaces, and let $l$ be a filter on $\alpha$. If $f$ is asymptotically equivalent to $g$ up to a constant factor (i.e., $f = \Theta[l] g$) and $g$ is big-O of $k$ along $l$ (i.e., $g = O[l] k$), then $f$ is big-O of $k$ along $l$ (i.e., $f = O[l] k$).

Asymptotics.instTransForallIsThetaIsBigO instance

: Trans (α := α → E) (β := α → F') (γ := α → G) (IsTheta l) (IsBigO l) (IsBigO l)

Full source

instance : Trans (α := α → E) (β := α → F') (γ := α → G) (IsTheta l) (IsBigO l) (IsBigO l) :=
  ⟨IsTheta.trans_isBigO⟩

Transitivity of Theta and Big-O Relations

Informal description

For any filter $l$ on a type $\alpha$, and functions $f : \alpha \to E$, $g : \alpha \to F'$, and $k : \alpha \to G$, if $f$ is asymptotically equivalent to $g$ up to a constant factor (i.e., $f = \Theta[l] g$) and $g$ is big-O of $k$ along $l$ (i.e., $g = O[l] k$), then $f$ is big-O of $k$ along $l$ (i.e., $f = O[l] k$).

Asymptotics.IsLittleO.trans_isTheta theorem

{f : α → E} {g : α → F} {k : α → G'} (h₁ : f =o[l] g) (h₂ : g =Θ[l] k) : f =o[l] k

Full source

@[trans]
theorem IsLittleO.trans_isTheta {f : α → E} {g : α → F} {k : α → G'} (h₁ : f =o[l] g)
    (h₂ : g =Θ[l] k) : f =o[l] k :=
  h₁.trans_isBigO h₂.1

Transitivity of Little-o and Theta: $f = o(g) \land g = \Theta(k) \Rightarrow f = o(k)$

Informal description

Let $f : \alpha \to E$, $g : \alpha \to F$, and $k : \alpha \to G'$ be functions to normed spaces, and let $l$ be a filter on $\alpha$. If $f = o[l] g$ (i.e., $f$ is asymptotically dominated by $g$) and $g = \Theta[l] k$ (i.e., $g$ and $k$ are asymptotically equivalent up to a constant factor), then $f = o[l] k$ (i.e., $f$ is asymptotically dominated by $k$).

Asymptotics.instTransForallIsLittleOIsTheta instance

: Trans (α := α → E) (β := α → F') (γ := α → G') (IsLittleO l) (IsTheta l) (IsLittleO l)

Full source

instance : Trans (α := α → E) (β := α → F') (γ := α → G') (IsLittleO l) (IsTheta l) (IsLittleO l) :=
  ⟨IsLittleO.trans_isTheta⟩

Transitivity of Little-o and Theta Asymptotic Relations

Informal description

For any filter $l$ on a type $\alpha$, and functions $f : \alpha \to E$, $g : \alpha \to F'$, and $k : \alpha \to G'$, if $f = o[l] g$ and $g = \Theta[l] k$, then $f = o[l] k$. This means that if $f$ grows asymptotically strictly slower than $g$, and $g$ is asymptotically equivalent to $k$ up to a constant factor, then $f$ grows asymptotically strictly slower than $k$ as well.

Asymptotics.IsTheta.trans_isLittleO theorem

{f : α → E} {g : α → F'} {k : α → G} (h₁ : f =Θ[l] g) (h₂ : g =o[l] k) : f =o[l] k

Full source

@[trans]
theorem IsTheta.trans_isLittleO {f : α → E} {g : α → F'} {k : α → G} (h₁ : f =Θ[l] g)
    (h₂ : g =o[l] k) : f =o[l] k :=
  h₁.1.trans_isLittleO h₂

Transitivity of Theta and Little-o: $f = \Theta(g) \land g = o(k) \Rightarrow f = o(k)$

Informal description

Let $f : \alpha \to E$, $g : \alpha \to F'$, and $k : \alpha \to G$ be functions mapping to normed spaces, and let $l$ be a filter on $\alpha$. If $f$ is asymptotically equivalent to $g$ up to a constant factor along $l$ (i.e., $f = \Theta[l] g$) and $g$ is asymptotically strictly smaller than $k$ along $l$ (i.e., $g = o[l] k$), then $f$ is asymptotically strictly smaller than $k$ along $l$ (i.e., $f = o[l] k$).

Asymptotics.instTransForallIsThetaIsLittleO instance

: Trans (α := α → E) (β := α → F') (γ := α → G) (IsTheta l) (IsLittleO l) (IsLittleO l)

Full source

instance : Trans (α := α → E) (β := α → F') (γ := α → G) (IsTheta l) (IsLittleO l) (IsLittleO l) :=
  ⟨IsTheta.trans_isLittleO⟩

Transitivity of Theta and Little-o Asymptotic Relations

Informal description

For any filter $l$ on a type $\alpha$, and functions $f : \alpha \to E$, $g : \alpha \to F'$, and $k : \alpha \to G$, if $f$ is asymptotically equivalent to $g$ up to a constant factor along $l$ (i.e., $f = \Theta[l] g$) and $g$ is asymptotically strictly smaller than $k$ along $l$ (i.e., $g = o[l] k$), then $f$ is asymptotically strictly smaller than $k$ along $l$ (i.e., $f = o[l] k$).

Asymptotics.IsTheta.trans_eventuallyEq theorem

{f : α → E} {g₁ g₂ : α → F} (h : f =Θ[l] g₁) (hg : g₁ =ᶠ[l] g₂) : f =Θ[l] g₂

Full source

@[trans]
theorem IsTheta.trans_eventuallyEq {f : α → E} {g₁ g₂ : α → F} (h : f =Θ[l] g₁) (hg : g₁ =ᶠ[l] g₂) :
    f =Θ[l] g₂ :=
  ⟨h.1.trans_eventuallyEq hg, hg.symm.trans_isBigO h.2⟩

Preservation of Asymptotic Equivalence under Eventual Equality

Informal description

Let $f : \alpha \to E$ and $g_1, g_2 : \alpha \to F$ be functions, and let $l$ be a filter on $\alpha$. If $f$ is asymptotically equivalent to $g_1$ up to a constant factor along $l$ (i.e., $f = \Theta[l] g_1$) and $g_1$ is eventually equal to $g_2$ along $l$ (i.e., $g_1 =_{l} g_2$), then $f$ is asymptotically equivalent to $g_2$ up to a constant factor along $l$ (i.e., $f = \Theta[l] g_2$).

Asymptotics.instTransForallIsThetaEventuallyEq instance

: Trans (α := α → E) (β := α → F) (γ := α → F) (IsTheta l) (EventuallyEq l) (IsTheta l)

Full source

instance : Trans (α := α → E) (β := α → F) (γ := α → F) (IsTheta l) (EventuallyEq l) (IsTheta l) :=
  ⟨IsTheta.trans_eventuallyEq⟩

Transitivity of Asymptotic Equivalence under Eventual Equality

Informal description

For any filter $l$ on a type $\alpha$, the relation $\Theta[l]$ (asymptotic equivalence up to a constant factor) is transitive with respect to eventual equality. That is, if $f : \alpha \to E$ is asymptotically equivalent to $g_1 : \alpha \to F$ up to a constant factor along $l$, and $g_1$ is eventually equal to $g_2 : \alpha \to F$ along $l$, then $f$ is also asymptotically equivalent to $g_2$ up to a constant factor along $l$.

Filter.EventuallyEq.trans_isTheta theorem

{f₁ f₂ : α → E} {g : α → F} (hf : f₁ =ᶠ[l] f₂) (h : f₂ =Θ[l] g) : f₁ =Θ[l] g

Full source

@[trans]
theorem _root_.Filter.EventuallyEq.trans_isTheta {f₁ f₂ : α → E} {g : α → F} (hf : f₁ =ᶠ[l] f₂)
    (h : f₂ =Θ[l] g) : f₁ =Θ[l] g :=
  ⟨hf.trans_isBigO h.1, h.2.trans_eventuallyEq hf.symm⟩

Preservation of Asymptotic Equivalence under Eventual Equality

Informal description

Let $f_1, f_2 : \alpha \to E$ and $g : \alpha \to F$ be functions, and let $l$ be a filter on $\alpha$. If $f_1$ is eventually equal to $f_2$ along $l$ (i.e., $f_1(x) = f_2(x)$ for all $x$ in some neighborhood determined by $l$) and $f_2$ is asymptotically equivalent to $g$ up to a constant factor along $l$ (i.e., $f_2 = \Theta[l] g$), then $f_1$ is also asymptotically equivalent to $g$ up to a constant factor along $l$ (i.e., $f_1 = \Theta[l] g$).

Asymptotics.instTransForallEventuallyEqIsTheta instance

: Trans (α := α → E) (β := α → E) (γ := α → F) (EventuallyEq l) (IsTheta l) (IsTheta l)

Full source

instance : Trans (α := α → E) (β := α → E) (γ := α → F) (EventuallyEq l) (IsTheta l) (IsTheta l) :=
  ⟨EventuallyEq.trans_isTheta⟩

Transitivity of Asymptotic Equivalence under Eventual Equality

Informal description

For any functions $f, g : \alpha \to E$ and $h : \alpha \to F$, if $f$ is eventually equal to $g$ along the filter $l$ (i.e., $f(x) = g(x)$ for all $x$ in some neighborhood determined by $l$) and $g$ is asymptotically equivalent to $h$ up to a constant factor along $l$ (i.e., $g = \Theta[l] h$), then $f$ is also asymptotically equivalent to $h$ up to a constant factor along $l$ (i.e., $f = \Theta[l] h$).

Filter.EventuallyEq.isTheta theorem

{f g : α → E} (h : f =ᶠ[l] g) : f =Θ[l] g

Full source

lemma _root_.Filter.EventuallyEq.isTheta {f g : α → E} (h : f =ᶠ[l] g) : f =Θ[l] g :=
  h.trans_isTheta isTheta_rfl

Eventual equality implies asymptotic equivalence: $f =ᶠ[l] g \Rightarrow f = \Theta[l] g$

Informal description

For any functions $f, g : \alpha \to E$ and a filter $l$ on $\alpha$, if $f$ is eventually equal to $g$ along $l$ (i.e., $f(x) = g(x)$ for all $x$ in some neighborhood determined by $l$), then $f$ is asymptotically equivalent to $g$ up to a constant factor along $l$, denoted $f = \Theta[l] g$.

Asymptotics.isTheta_bot theorem

: f =Θ[⊥] g

Full source

@[simp]
theorem isTheta_bot : f =Θ[⊥] g := by simp [IsTheta]

Asymptotic equivalence up to a constant factor holds trivially for the bottom filter

Informal description

For any functions $f, g : \alpha \to E$, the relation $f = \Theta[\bot] g$ holds, where $\bot$ denotes the bottom filter. This means that $f$ and $g$ are asymptotically equivalent up to a constant factor in the context of the bottom filter.

Asymptotics.isTheta_norm_left theorem

: (fun x ↦ ‖f' x‖) =Θ[l] g ↔ f' =Θ[l] g

Full source

@[simp]
theorem isTheta_norm_left : (fun x ↦ ‖f' x‖) =Θ[l] g(fun x ↦ ‖f' x‖) =Θ[l] g ↔ f' =Θ[l] g := by simp [IsTheta]

Norm Equivalence in Asymptotic Comparison: $\|\cdot\|f' = \Theta[l] g \leftrightarrow f' = \Theta[l] g$

Informal description

For functions $f' : \alpha \to E$ and $g : \alpha \to F$ and a filter $l$ on $\alpha$, the function $x \mapsto \|f'(x)\|$ is asymptotically equivalent to $g$ up to a constant factor (i.e., $x \mapsto \|f'(x)\| = \Theta[l] g$) if and only if $f'$ itself is asymptotically equivalent to $g$ up to a constant factor (i.e., $f' = \Theta[l] g$).

Asymptotics.isTheta_norm_right theorem

: (f =Θ[l] fun x ↦ ‖g' x‖) ↔ f =Θ[l] g'

Full source

@[simp]
theorem isTheta_norm_right : (f =Θ[l] fun x ↦ ‖g' x‖) ↔ f =Θ[l] g' := by simp [IsTheta]

Norm Equivalence in Asymptotic Comparison: $f = \Theta[l] \|g'\| \leftrightarrow f = \Theta[l] g'$

Informal description

For functions $f : \alpha \to E$ and $g' : \alpha \to F$ and a filter $l$ on $\alpha$, the relation $f = \Theta[l] (x \mapsto \|g'(x)\|)$ holds if and only if $f = \Theta[l] g'$. In other words, $f$ is asymptotically equivalent to the norm of $g'$ up to a constant factor if and only if $f$ is asymptotically equivalent to $g'$ itself up to a constant factor.

Asymptotics.IsTheta.of_norm_eventuallyEq_norm theorem

(h : (fun x ↦ ‖f x‖) =ᶠ[l] fun x ↦ ‖g x‖) : f =Θ[l] g

Full source

theorem IsTheta.of_norm_eventuallyEq_norm (h : (fun x ↦ ‖f x‖) =ᶠ[l] fun x ↦ ‖g x‖) : f =Θ[l] g :=
  ⟨.of_bound' h.le, .of_bound' h.symm.le⟩

Asymptotic equivalence via eventual norm equality: $\|f\| \sim_l \|g\| \Rightarrow f = \Theta[l] g$

Informal description

Let $f : \alpha \to E$ and $g : \alpha \to F$ be functions, and let $l$ be a filter on $\alpha$. If the norms $\|f(x)\|$ and $\|g(x)\|$ are eventually equal along $l$, then $f$ is asymptotically equivalent to $g$ up to a constant factor, i.e., $f = \Theta[l] g$.

Asymptotics.IsTheta.of_norm_eventuallyEq theorem

{g : α → ℝ} (h : (fun x ↦ ‖f' x‖) =ᶠ[l] g) : f' =Θ[l] g

Full source

theorem IsTheta.of_norm_eventuallyEq {g : α → ℝ} (h : (fun x ↦ ‖f' x‖) =ᶠ[l] g) : f' =Θ[l] g :=
  of_norm_eventuallyEq_norm <| h.mono fun x hx ↦ by simp only [← hx, norm_norm]

Asymptotic equivalence via eventual norm equality: $\|f'\| \sim_l g \Rightarrow f' = \Theta[l] g$

Informal description

Let $f' : \alpha \to E$ be a function and $g : \alpha \to \mathbb{R}$ be another function, where $l$ is a filter on $\alpha$. If the norm $\|f'(x)\|$ is eventually equal to $g(x)$ along $l$, then $f'$ is asymptotically equivalent to $g$ up to a constant factor, i.e., $f' = \Theta[l] g$.

Asymptotics.IsTheta.isLittleO_congr_left theorem

(h : f' =Θ[l] g') : f' =o[l] k ↔ g' =o[l] k

Full source

theorem IsTheta.isLittleO_congr_left (h : f' =Θ[l] g') : f' =o[l] kf' =o[l] k ↔ g' =o[l] k :=
  ⟨h.symm.trans_isLittleO, h.trans_isLittleO⟩

Equivalence of Little-o Relations under Theta Asymptotic Equivalence

Informal description

Let $f', g' : \alpha \to E$ and $k : \alpha \to F$ be functions, and let $l$ be a filter on $\alpha$. If $f'$ is asymptotically equivalent to $g'$ up to a constant factor along $l$ (i.e., $f' = \Theta[l] g'$), then $f'$ is asymptotically strictly smaller than $k$ along $l$ if and only if $g'$ is asymptotically strictly smaller than $k$ along $l$. In other words: $$ f' = o[l] k \leftrightarrow g' = o[l] k. $$

Asymptotics.IsTheta.isLittleO_congr_right theorem

(h : g' =Θ[l] k') : f =o[l] g' ↔ f =o[l] k'

Full source

theorem IsTheta.isLittleO_congr_right (h : g' =Θ[l] k') : f =o[l] g'f =o[l] g' ↔ f =o[l] k' :=
  ⟨fun H ↦ H.trans_isTheta h, fun H ↦ H.trans_isTheta h.symm⟩

Little-o Congruence under Asymptotic Equivalence: $g' = \Theta[k'] \Rightarrow (f = o[g'] \leftrightarrow f = o[k'])$

Informal description

Let $f : \alpha \to E$, $g' : \alpha \to F$, and $k' : \alpha \to G$ be functions to normed spaces, and let $l$ be a filter on $\alpha$. If $g'$ is asymptotically equivalent to $k'$ up to a constant factor (i.e., $g' = \Theta[l] k'$), then $f$ is asymptotically dominated by $g'$ (i.e., $f = o[l] g'$) if and only if $f$ is asymptotically dominated by $k'$ (i.e., $f = o[l] k'$).

Asymptotics.IsTheta.isBigO_congr_left theorem

(h : f' =Θ[l] g') : f' =O[l] k ↔ g' =O[l] k

Full source

theorem IsTheta.isBigO_congr_left (h : f' =Θ[l] g') : f' =O[l] kf' =O[l] k ↔ g' =O[l] k :=
  ⟨h.symm.trans_isBigO, h.trans_isBigO⟩

Big-O Congruence under Theta Asymptotic Equivalence: Left Version

Informal description

Let $f', g' : \alpha \to E$ and $k : \alpha \to F$ be functions to normed spaces, and let $l$ be a filter on $\alpha$. If $f'$ is asymptotically equivalent to $g'$ up to a constant factor along $l$ (i.e., $f' = \Theta[l] g'$), then $f'$ is asymptotically bounded above by $k$ along $l$ if and only if $g'$ is asymptotically bounded above by $k$ along $l$. In other words: $$ f' = O[l] k \leftrightarrow g' = O[l] k. $$

Asymptotics.IsTheta.isBigO_congr_right theorem

(h : g' =Θ[l] k') : f =O[l] g' ↔ f =O[l] k'

Full source

theorem IsTheta.isBigO_congr_right (h : g' =Θ[l] k') : f =O[l] g'f =O[l] g' ↔ f =O[l] k' :=
  ⟨fun H ↦ H.trans_isTheta h, fun H ↦ H.trans_isTheta h.symm⟩

Big-O Congruence under Asymptotic Equivalence: $g' = \Theta[k'] \Rightarrow (f = O[g'] \leftrightarrow f = O[k'])$

Informal description

Let $f : \alpha \to E$, $g' : \alpha \to F$, and $k' : \alpha \to G$ be functions to normed spaces, and let $l$ be a filter on $\alpha$. If $g'$ is asymptotically equivalent to $k'$ up to a constant factor (i.e., $g' = \Theta[l] k'$), then $f$ is asymptotically bounded by $g'$ (i.e., $f = O[l] g'$) if and only if $f$ is asymptotically bounded by $k'$ (i.e., $f = O[l] k'$).

Asymptotics.IsTheta.isTheta_congr_left theorem

(h : f' =Θ[l] g') : f' =Θ[l] k ↔ g' =Θ[l] k

Full source

lemma IsTheta.isTheta_congr_left (h : f' =Θ[l] g') : f' =Θ[l] kf' =Θ[l] k ↔ g' =Θ[l] k :=
  h.isBigO_congr_left.and h.isBigO_congr_right

Theta Asymptotic Equivalence Congruence: Left Version

Informal description

Let $f', g' : \alpha \to E$ and $k : \alpha \to F$ be functions to normed spaces, and let $l$ be a filter on $\alpha$. If $f'$ is asymptotically equivalent to $g'$ up to a constant factor along $l$ (i.e., $f' = \Theta[l] g'$), then $f'$ is asymptotically equivalent to $k$ along $l$ if and only if $g'$ is asymptotically equivalent to $k$ along $l$. In other words: $$ f' = \Theta[l] k \leftrightarrow g' = \Theta[l] k. $$

Asymptotics.IsTheta.isTheta_congr_right theorem

(h : f' =Θ[l] g') : k =Θ[l] f' ↔ k =Θ[l] g'

Full source

lemma IsTheta.isTheta_congr_right (h : f' =Θ[l] g') : k =Θ[l] f'k =Θ[l] f' ↔ k =Θ[l] g' :=
  h.isBigO_congr_right.and h.isBigO_congr_left

Asymptotic Equivalence Congruence: Right Version ($k = \Theta[f'] \leftrightarrow k = \Theta[g']$ when $f' = \Theta[g']$)

Informal description

Let $f', g' : \alpha \to E$ and $k : \alpha \to F$ be functions to normed spaces, and let $l$ be a filter on $\alpha$. If $f'$ is asymptotically equivalent to $g'$ up to a constant factor along $l$ (i.e., $f' = \Theta[l] g'$), then $k$ is asymptotically equivalent to $f'$ along $l$ if and only if $k$ is asymptotically equivalent to $g'$ along $l$. In other words: $$ k = \Theta[l] f' \leftrightarrow k = \Theta[l] g'. $$

Asymptotics.IsTheta.mono theorem

(h : f =Θ[l] g) (hl : l' ≤ l) : f =Θ[l'] g

Full source

theorem IsTheta.mono (h : f =Θ[l] g) (hl : l' ≤ l) : f =Θ[l'] g :=
  ⟨h.1.mono hl, h.2.mono hl⟩

Asymptotic Equivalence is Preserved Under Filter Refinement

Informal description

Let $f : \alpha \to E$ and $g : \alpha \to F$ be functions to normed spaces, and let $l, l'$ be filters on $\alpha$. If $f$ is asymptotically equivalent to $g$ up to a constant factor along $l$ (i.e., $f = \Theta[l] g$) and $l'$ is a finer filter than $l$ (i.e., $l' \leq l$), then $f$ is asymptotically equivalent to $g$ up to a constant factor along $l'$ (i.e., $f = \Theta[l'] g$).

Asymptotics.IsTheta.sup theorem

(h : f' =Θ[l] g') (h' : f' =Θ[l'] g') : f' =Θ[l ⊔ l'] g'

Full source

theorem IsTheta.sup (h : f' =Θ[l] g') (h' : f' =Θ[l'] g') : f' =Θ[l ⊔ l'] g' :=
  ⟨h.1.sup h'.1, h.2.sup h'.2⟩

Asymptotic Equivalence Preserved under Filter Supremum

Informal description

Let $f' : \alpha \to E$ and $g' : \alpha \to F$ be functions from a type $\alpha$ to normed spaces $E$ and $F$ respectively, and let $l$ and $l'$ be filters on $\alpha$. If $f'$ is asymptotically equivalent to $g'$ up to a constant factor along $l$ (i.e., $f' = \Theta[l] g'$) and $f'$ is asymptotically equivalent to $g'$ up to a constant factor along $l'$ (i.e., $f' = \Theta[l'] g'$), then $f'$ is asymptotically equivalent to $g'$ up to a constant factor along the supremum filter $l \sqcup l'$ (i.e., $f' = \Theta[l \sqcup l'] g'$).

Asymptotics.isTheta_sup theorem

: f' =Θ[l ⊔ l'] g' ↔ f' =Θ[l] g' ∧ f' =Θ[l'] g'

Full source

@[simp]
theorem isTheta_sup : f' =Θ[l ⊔ l'] g'f' =Θ[l ⊔ l'] g' ↔ f' =Θ[l] g' ∧ f' =Θ[l'] g' :=
  ⟨fun h ↦ ⟨h.mono le_sup_left, h.mono le_sup_right⟩, fun h ↦ h.1.sup h.2⟩

Asymptotic Equivalence Characterization via Filter Supremum: $f' = \Theta[l \sqcup l'] g' \leftrightarrow f' = \Theta[l] g' \land f' = \Theta[l'] g'$

Informal description

For functions $f', g' : \alpha \to E$ and filters $l, l'$ on $\alpha$, the asymptotic equivalence $f' = \Theta[l \sqcup l'] g'$ holds if and only if both $f' = \Theta[l] g'$ and $f' = \Theta[l'] g'$ hold. In other words, $f'$ is asymptotically equivalent to $g'$ up to constant factors along the supremum filter $l \sqcup l'$ if and only if $f'$ is asymptotically equivalent to $g'$ up to constant factors along both $l$ and $l'$ individually.

Asymptotics.IsTheta.tendsto_zero_iff theorem

(h : f'' =Θ[l] g'') : Tendsto f'' l (𝓝 0) ↔ Tendsto g'' l (𝓝 0)

Full source

theorem IsTheta.tendsto_zero_iff (h : f'' =Θ[l] g'') :
    TendstoTendsto f'' l (𝓝 0) ↔ Tendsto g'' l (𝓝 0) := by
  simp only [← isLittleO_one_iff ℝ, h.isLittleO_congr_left]

Equivalence of Tendency to Zero under Theta Asymptotic Equivalence

Informal description

Let $f''$ and $g''$ be functions from a type $\alpha$ to normed spaces, and let $l$ be a filter on $\alpha$. If $f''$ is asymptotically equivalent to $g''$ up to a constant factor along $l$ (i.e., $f'' = \Theta[l] g''$), then $f''$ tends to $0$ along $l$ if and only if $g''$ tends to $0$ along $l$. In other words: $$ f'' \to_{l} 0 \leftrightarrow g'' \to_{l} 0. $$

Asymptotics.IsTheta.tendsto_norm_atTop_iff theorem

(h : f' =Θ[l] g') : Tendsto (norm ∘ f') l atTop ↔ Tendsto (norm ∘ g') l atTop

Full source

theorem IsTheta.tendsto_norm_atTop_iff (h : f' =Θ[l] g') :
    TendstoTendsto (norm ∘ f') l atTop ↔ Tendsto (norm ∘ g') l atTop := by
  simp only [Function.comp_def, ← isLittleO_const_left_of_ne (one_ne_zero' ℝ),
    h.isLittleO_congr_right]

Equivalence of Norm Divergence under Asymptotic Equivalence: $\|f'\| \to \infty \leftrightarrow \|g'\| \to \infty$ when $f' = \Theta[l] g'$

Informal description

Let $f', g' : \alpha \to E$ be functions to a normed space $E$, and let $l$ be a filter on $\alpha$. If $f'$ is asymptotically equivalent to $g'$ up to a constant factor (i.e., $f' = \Theta[l] g'$), then the norm of $f'$ tends to infinity along $l$ if and only if the norm of $g'$ tends to infinity along $l$. In other words, $\lim_{l} \|f'(x)\| = \infty \leftrightarrow \lim_{l} \|g'(x)\| = \infty$.

Asymptotics.IsTheta.smul theorem

 [NormedSpace 𝕜 E'] [NormedSpace 𝕜' F'] {f₁ : α → 𝕜} {f₂ : α → 𝕜'} {g₁ : α → E'} {g₂ : α → F'} (hf : f₁ =Θ[l] f₂)
  (hg : g₁ =Θ[l] g₂) : (fun x ↦ f₁ x • g₁ x) =Θ[l] fun x ↦ f₂ x • g₂ x

Full source

theorem IsTheta.smul [NormedSpace 𝕜 E'] [NormedSpace 𝕜' F'] {f₁ : α → 𝕜} {f₂ : α → 𝕜'} {g₁ : α → E'}
    {g₂ : α → F'} (hf : f₁ =Θ[l] f₂) (hg : g₁ =Θ[l] g₂) :
    (fun x ↦ f₁ x • g₁ x) =Θ[l] fun x ↦ f₂ x • g₂ x :=
  ⟨hf.1.smul hg.1, hf.2.smul hg.2⟩

Preservation of asymptotic equivalence under scalar multiplication: $f_1 = \Theta f_2$ and $g_1 = \Theta g_2$ implies $f_1 \cdot g_1 = \Theta f_2 \cdot g_2$

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields, and $E'$ and $F'$ be normed spaces over $\mathbb{K}$ and $\mathbb{K}'$ respectively. Given functions $f_1, f_2 : \alpha \to \mathbb{K}$ and $g_1, g_2 : \alpha \to E'$ such that $f_1$ and $f_2$ are asymptotically equivalent up to a constant factor (denoted $f_1 = \Theta[l] f_2$) and $g_1$ and $g_2$ are asymptotically equivalent up to a constant factor (denoted $g_1 = \Theta[l] g_2$), then the scalar multiplication functions $x \mapsto f_1(x) \cdot g_1(x)$ and $x \mapsto f_2(x) \cdot g_2(x)$ are also asymptotically equivalent up to a constant factor along the filter $l$.

Asymptotics.IsTheta.mul theorem

 {f₁ f₂ : α → 𝕜} {g₁ g₂ : α → 𝕜'} (h₁ : f₁ =Θ[l] g₁) (h₂ : f₂ =Θ[l] g₂) :
  (fun x ↦ f₁ x * f₂ x) =Θ[l] fun x ↦ g₁ x * g₂ x

Full source

theorem IsTheta.mul {f₁ f₂ : α → 𝕜} {g₁ g₂ : α → 𝕜'} (h₁ : f₁ =Θ[l] g₁) (h₂ : f₂ =Θ[l] g₂) :
    (fun x ↦ f₁ x * f₂ x) =Θ[l] fun x ↦ g₁ x * g₂ x :=
  h₁.smul h₂

Preservation of Asymptotic Equivalence under Multiplication: $f_1 = \Theta g_1$ and $f_2 = \Theta g_2$ implies $f_1 f_2 = \Theta g_1 g_2$

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields, and let $f_1, f_2 : \alpha \to \mathbb{K}$ and $g_1, g_2 : \alpha \to \mathbb{K}'$ be functions. If $f_1$ is asymptotically equivalent to $g_1$ up to a constant factor along the filter $l$ (denoted $f_1 = \Theta[l] g_1$) and $f_2$ is asymptotically equivalent to $g_2$ up to a constant factor along $l$ (denoted $f_2 = \Theta[l] g_2$), then the product functions $x \mapsto f_1(x) * f_2(x)$ and $x \mapsto g_1(x) * g_2(x)$ are also asymptotically equivalent up to a constant factor along $l$.

Asymptotics.IsTheta.listProd theorem

 {ι : Type*} {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 IsTheta.listProd {ι : Type*} {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) :=
  ⟨.listProd fun i hi ↦ (h i hi).isBigO, .listProd fun i hi ↦ (h i hi).symm.isBigO⟩

Asymptotic Equivalence of List Products: $\prod_{i \in L} f_i(\cdot) = \Theta[l] \prod_{i \in L} g_i(\cdot)$ when $f_i = \Theta[l] g_i$ for all $i \in L$

Informal description

Let $\iota$ be a type, $L$ a list of elements of $\iota$, and $f_i, g_i : \alpha \to \mathbb{K}$ functions for each $i \in L$, where $\mathbb{K}$ is a normed field. If for every $i \in L$, the functions $f_i$ and $g_i$ are asymptotically equivalent up to a constant factor along a filter $l$ (i.e., $f_i = \Theta[l] g_i$), then the product function $x \mapsto \prod_{i \in L} f_i(x)$ is asymptotically equivalent to the product function $x \mapsto \prod_{i \in L} g_i(x)$ along $l$ (i.e., $\prod_{i \in L} f_i(\cdot) = \Theta[l] \prod_{i \in L} g_i(\cdot)$).

Asymptotics.IsTheta.multisetProd theorem

 {ι : Type*} {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 IsTheta.multisetProd {ι : Type*} {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) :=
  ⟨.multisetProd fun i hi ↦ (h i hi).isBigO, .multisetProd fun i hi ↦ (h i hi).symm.isBigO⟩

Asymptotic Equivalence of Multiset Products: $\prod_{i \in s} f_i(\cdot) = \Theta[l] \prod_{i \in s} g_i(\cdot)$ when $f_i = \Theta[l] g_i$ for all $i \in s$

Informal description

Let $\iota$ be a type, $s$ a multiset of elements of $\iota$, and $f_i, g_i : \alpha \to \mathbb{K}$ functions for each $i \in s$, where $\mathbb{K}$ is a normed field. If for every $i \in s$, the functions $f_i$ and $g_i$ are asymptotically equivalent up to a constant factor along a filter $l$ (i.e., $f_i = \Theta[l] g_i$), then the product function $x \mapsto \prod_{i \in s} f_i(x)$ is asymptotically equivalent to the product function $x \mapsto \prod_{i \in s} g_i(x)$ along $l$ (i.e., $\prod_{i \in s} f_i(\cdot) = \Theta[l] \prod_{i \in s} g_i(\cdot)$).

Asymptotics.IsTheta.finsetProd theorem

 {ι : Type*} {s : Finset ι} {f : ι → α → 𝕜} {g : ι → α → 𝕜'} (h : ∀ i ∈ s, f i =Θ[l] g i) :
  (∏ i ∈ s, f i ·) =Θ[l] (∏ i ∈ s, g i ·)

Full source

theorem IsTheta.finsetProd {ι : Type*} {s : Finset ι} {f : ι → α → 𝕜} {g : ι → α → 𝕜'}
    (h : ∀ i ∈ s, f i =Θ[l] g i) : (∏ i ∈ s, f i ·) =Θ[l] (∏ i ∈ s, g i ·) :=
  ⟨.finsetProd fun i hi ↦ (h i hi).isBigO, .finsetProd fun i hi ↦ (h i hi).symm.isBigO⟩

Asymptotic Equivalence of Finite Products: $\prod_{i \in s} f_i(\cdot) = \Theta[l] \prod_{i \in s} g_i(\cdot)$ when $f_i = \Theta[l] g_i$ for all $i \in s$

Informal description

Let $\iota$ be a type, $s$ a finite set of elements of $\iota$, and $f_i, g_i : \alpha \to \mathbb{K}$ functions for each $i \in s$, where $\mathbb{K}$ is a normed field. If for every $i \in s$, the functions $f_i$ and $g_i$ are asymptotically equivalent up to a constant factor along a filter $l$ (i.e., $f_i = \Theta[l] g_i$), then the product function $x \mapsto \prod_{i \in s} f_i(x)$ is asymptotically equivalent to the product function $x \mapsto \prod_{i \in s} g_i(x)$ along $l$ (i.e., $\prod_{i \in s} f_i(\cdot) = \Theta[l] \prod_{i \in s} g_i(\cdot)$).

Asymptotics.IsTheta.inv theorem

{f : α → 𝕜} {g : α → 𝕜'} (h : f =Θ[l] g) : (fun x ↦ (f x)⁻¹) =Θ[l] fun x ↦ (g x)⁻¹

Full source

theorem IsTheta.inv {f : α → 𝕜} {g : α → 𝕜'} (h : f =Θ[l] g) :
    (fun x ↦ (f x)⁻¹) =Θ[l] fun x ↦ (g x)⁻¹ :=
  ⟨h.2.inv_rev h.1.eq_zero_imp, h.1.inv_rev h.2.eq_zero_imp⟩

Reciprocal Preservation under Asymptotic Equivalence: $f^{-1} = \Theta[l] g^{-1}$ given $f = \Theta[l] g$

Informal description

Let $f : \alpha \to \mathbb{K}$ and $g : \alpha \to \mathbb{K}'$ be functions where $\mathbb{K}$ and $\mathbb{K}'$ are normed division rings, and let $l$ be a filter on $\alpha$. If $f$ is asymptotically equivalent to $g$ up to a constant factor along $l$ (i.e., $f = \Theta[l] g$), then the reciprocal function $x \mapsto (f(x))^{-1}$ is asymptotically equivalent to the reciprocal function $x \mapsto (g(x))^{-1}$ along $l$.

Asymptotics.isTheta_inv theorem

{f : α → 𝕜} {g : α → 𝕜'} : ((fun x ↦ (f x)⁻¹) =Θ[l] fun x ↦ (g x)⁻¹) ↔ f =Θ[l] g

Full source

@[simp]
theorem isTheta_inv {f : α → 𝕜} {g : α → 𝕜'} :
    ((fun x ↦ (f x)⁻¹) =Θ[l] fun x ↦ (g x)⁻¹) ↔ f =Θ[l] g :=
  ⟨fun h ↦ by simpa only [inv_inv] using h.inv, IsTheta.inv⟩

Reciprocal Asymptotic Equivalence: $f^{-1} = \Theta[l] g^{-1} \leftrightarrow f = \Theta[l] g$

Informal description

For functions $f : \alpha \to \mathbb{K}$ and $g : \alpha \to \mathbb{K}'$ where $\mathbb{K}$ and $\mathbb{K}'$ are normed division rings, and a filter $l$ on $\alpha$, the reciprocal functions $x \mapsto (f(x))^{-1}$ and $x \mapsto (g(x))^{-1}$ are asymptotically equivalent up to a constant factor along $l$ (i.e., $f^{-1} = \Theta[l] g^{-1}$) if and only if $f$ and $g$ are asymptotically equivalent up to a constant factor along $l$ (i.e., $f = \Theta[l] g$).

Asymptotics.IsTheta.div theorem

 {f₁ f₂ : α → 𝕜} {g₁ g₂ : α → 𝕜'} (h₁ : f₁ =Θ[l] g₁) (h₂ : f₂ =Θ[l] g₂) :
  (fun x ↦ f₁ x / f₂ x) =Θ[l] fun x ↦ g₁ x / g₂ x

Full source

theorem IsTheta.div {f₁ f₂ : α → 𝕜} {g₁ g₂ : α → 𝕜'} (h₁ : f₁ =Θ[l] g₁) (h₂ : f₂ =Θ[l] g₂) :
    (fun x ↦ f₁ x / f₂ x) =Θ[l] fun x ↦ g₁ x / g₂ x := by
  simpa only [div_eq_mul_inv] using h₁.mul h₂.inv

Preservation of Asymptotic Equivalence under Division: $f_1 = \Theta g_1$ and $f_2 = \Theta g_2$ implies $f_1/f_2 = \Theta g_1/g_2$

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields, and let $f_1, f_2 : \alpha \to \mathbb{K}$ and $g_1, g_2 : \alpha \to \mathbb{K}'$ be functions. If $f_1$ is asymptotically equivalent to $g_1$ up to a constant factor along the filter $l$ (i.e., $f_1 = \Theta[l] g_1$) and $f_2$ is asymptotically equivalent to $g_2$ up to a constant factor along $l$ (i.e., $f_2 = \Theta[l] g_2$), then the quotient functions $x \mapsto f_1(x) / f_2(x)$ and $x \mapsto g_1(x) / g_2(x)$ are also asymptotically equivalent up to a constant factor along $l$.

Asymptotics.IsTheta.pow theorem

{f : α → 𝕜} {g : α → 𝕜'} (h : f =Θ[l] g) (n : ℕ) : (fun x ↦ f x ^ n) =Θ[l] fun x ↦ g x ^ n

Full source

theorem IsTheta.pow {f : α → 𝕜} {g : α → 𝕜'} (h : f =Θ[l] g) (n : ℕ) :
    (fun x ↦ f x ^ n) =Θ[l] fun x ↦ g x ^ n :=
  ⟨h.1.pow n, h.2.pow n⟩

Preservation of Asymptotic Equivalence under Powers: $f = \Theta[l] g \implies f^n = \Theta[l] g^n$

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields, and let $f : \alpha \to \mathbb{K}$ and $g : \alpha \to \mathbb{K}'$ be functions. If $f$ is asymptotically equivalent to $g$ up to a constant factor along a filter $l$ (i.e., $f = \Theta[l] g$), then for any natural number $n$, the function $x \mapsto f(x)^n$ is asymptotically equivalent to $x \mapsto g(x)^n$ along $l$ (i.e., $f^n = \Theta[l] g^n$).

Asymptotics.IsTheta.zpow theorem

{f : α → 𝕜} {g : α → 𝕜'} (h : f =Θ[l] g) (n : ℤ) : (fun x ↦ f x ^ n) =Θ[l] fun x ↦ g x ^ n

Full source

theorem IsTheta.zpow {f : α → 𝕜} {g : α → 𝕜'} (h : f =Θ[l] g) (n : ℤ) :
    (fun x ↦ f x ^ n) =Θ[l] fun x ↦ g x ^ n := by
  cases n
  · simpa only [Int.ofNat_eq_coe, zpow_natCast] using h.pow _
  · simpa only [zpow_negSucc] using (h.pow _).inv

Preservation of Asymptotic Equivalence under Integer Powers: $f = \Theta[l] g \implies f^n = \Theta[l] g^n$ for $n \in \mathbb{Z}$

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields, and let $f : \alpha \to \mathbb{K}$ and $g : \alpha \to \mathbb{K}'$ be functions. If $f$ is asymptotically equivalent to $g$ up to a constant factor along a filter $l$ (i.e., $f = \Theta[l] g$), then for any integer $n$, the function $x \mapsto f(x)^n$ is asymptotically equivalent to $x \mapsto g(x)^n$ along $l$ (i.e., $f^n = \Theta[l] g^n$).

Asymptotics.isTheta_const_const theorem

{c₁ : E''} {c₂ : F''} (h₁ : c₁ ≠ 0) (h₂ : c₂ ≠ 0) : (fun _ : α ↦ c₁) =Θ[l] fun _ ↦ c₂

Full source

theorem isTheta_const_const {c₁ : E''} {c₂ : F''} (h₁ : c₁ ≠ 0) (h₂ : c₂ ≠ 0) :
    (fun _ : α ↦ c₁) =Θ[l] fun _ ↦ c₂ :=
  ⟨isBigO_const_const _ h₂ _, isBigO_const_const _ h₁ _⟩

Asymptotic Equivalence of Nonzero Constant Functions: $c_1 = \Theta[l] c_2$ for $c_1, c_2 \neq 0$

Informal description

Let $E''$ and $F''$ be normed spaces, and let $c_1 \in E''$ and $c_2 \in F''$ be nonzero constants. For any filter $l$ on a type $\alpha$, the constant functions $x \mapsto c_1$ and $x \mapsto c_2$ are asymptotically equivalent up to a constant factor, i.e., $c_1 = \Theta[l] c_2$.

Asymptotics.isTheta_const_const_iff theorem

[NeBot l] {c₁ : E''} {c₂ : F''} : ((fun _ : α ↦ c₁) =Θ[l] fun _ ↦ c₂) ↔ (c₁ = 0 ↔ c₂ = 0)

Full source

@[simp]
theorem isTheta_const_const_iff [NeBot l] {c₁ : E''} {c₂ : F''} :
    ((fun _ : α ↦ c₁) =Θ[l] fun _ ↦ c₂) ↔ (c₁ = 0 ↔ c₂ = 0) := by
  simpa only [IsTheta, isBigO_const_const_iff, ← iff_def] using Iff.comm

Asymptotic Equivalence of Constant Functions: $c_1 = \Theta[l] c_2 \iff (c_1 = 0 \iff c_2 = 0)$

Informal description

Let $l$ be a non-trivial filter on a type $\alpha$, and let $c_1 \in E''$ and $c_2 \in F''$ be constants. Then the constant functions $x \mapsto c_1$ and $x \mapsto c_2$ are asymptotically equivalent up to a constant factor (denoted $c_1 = \Theta[l] c_2$) if and only if $c_1 = 0$ if and only if $c_2 = 0$.

Asymptotics.isTheta_zero_left theorem

: (fun _ ↦ (0 : E')) =Θ[l] g'' ↔ g'' =ᶠ[l] 0

Full source

@[simp]
theorem isTheta_zero_left : (fun _ ↦ (0 : E')) =Θ[l] g''(fun _ ↦ (0 : E')) =Θ[l] g'' ↔ g'' =ᶠ[l] 0 := by
  simp only [IsTheta, isBigO_zero, isBigO_zero_right_iff, true_and]

Zero Function Asymptotic Equivalence Criterion: $0 = \Theta[l] g'' \leftrightarrow g'' \to_{l} 0$

Informal description

The zero function is asymptotically equivalent to a function $g''$ along a filter $l$ if and only if $g''$ is eventually equal to zero along $l$. In other words, $0 = \Theta[l] g'' \leftrightarrow g'' \to_{l} 0$.

Asymptotics.isTheta_zero_right theorem

: (f'' =Θ[l] fun _ ↦ (0 : F')) ↔ f'' =ᶠ[l] 0

Full source

@[simp]
theorem isTheta_zero_right : (f'' =Θ[l] fun _ ↦ (0 : F')) ↔ f'' =ᶠ[l] 0 :=
  isTheta_comm.trans isTheta_zero_left

Zero Function Asymptotic Equivalence Criterion: $f'' = \Theta[l] 0 \leftrightarrow f'' \to_{l} 0$

Informal description

For a function $f'' : \alpha \to E'$ and a filter $l$ on $\alpha$, the asymptotic equivalence $f'' = \Theta[l] 0$ holds if and only if $f''$ is eventually equal to zero along $l$, i.e., $f'' \to_{l} 0$.

Asymptotics.isTheta_const_smul_left theorem

[NormedSpace 𝕜 E'] {c : 𝕜} (hc : c ≠ 0) : (fun x ↦ c • f' x) =Θ[l] g ↔ f' =Θ[l] g

Full source

theorem isTheta_const_smul_left [NormedSpace 𝕜 E'] {c : 𝕜} (hc : c ≠ 0) :
    (fun x ↦ c • f' x) =Θ[l] g(fun x ↦ c • f' x) =Θ[l] g ↔ f' =Θ[l] g :=
  and_congr (isBigO_const_smul_left hc) (isBigO_const_smul_right hc)

Asymptotic Equivalence Under Left Scalar Multiplication: $(c \cdot f') = \Theta[l] g \leftrightarrow f' = \Theta[l] g$ for $c \neq 0$

Informal description

Let $\mathbb{K}$ be a normed field, $E'$ be a normed space over $\mathbb{K}$, and $f' \colon \alpha \to E'$ and $g \colon \alpha \to F$ be functions. For a nonzero scalar $c \in \mathbb{K}$ and a filter $l$ on $\alpha$, the function $x \mapsto c \cdot f'(x)$ is asymptotically equivalent to $g$ up to a constant factor along $l$ if and only if $f'$ is asymptotically equivalent to $g$ along $l$. In other words: $$(c \cdot f') = \Theta[l] g \leftrightarrow f' = \Theta[l] g.$$

Asymptotics.isTheta_const_smul_right theorem

[NormedSpace 𝕜 F'] {c : 𝕜} (hc : c ≠ 0) : (f =Θ[l] fun x ↦ c • g' x) ↔ f =Θ[l] g'

Full source

theorem isTheta_const_smul_right [NormedSpace 𝕜 F'] {c : 𝕜} (hc : c ≠ 0) :
    (f =Θ[l] fun x ↦ c • g' x) ↔ f =Θ[l] g' :=
  and_congr (isBigO_const_smul_right hc) (isBigO_const_smul_left hc)

Asymptotic Equivalence Under Right Scalar Multiplication: $f = \Theta[l] (c \cdot g') \leftrightarrow f = \Theta[l] g'$ for $c \neq 0$

Informal description

Let $\mathbb{K}$ be a normed field, $F'$ be a normed space over $\mathbb{K}$, $f \colon \alpha \to E$ and $g' \colon \alpha \to F'$ be functions, $l$ be a filter on $\alpha$, and $c \in \mathbb{K}$ be a nonzero scalar. Then the asymptotic equivalence $f = \Theta[l] (x \mapsto c \cdot g'(x))$ holds if and only if $f = \Theta[l] g'$. In other words: $$ f = \Theta[l] (c \cdot g') \leftrightarrow f = \Theta[l] g'. $$

Asymptotics.isTheta_const_mul_left theorem

{c : 𝕜} {f : α → 𝕜} (hc : c ≠ 0) : (fun x ↦ c * f x) =Θ[l] g ↔ f =Θ[l] g

Full source

theorem isTheta_const_mul_left {c : 𝕜} {f : α → 𝕜} (hc : c ≠ 0) :
    (fun x ↦ c * f x) =Θ[l] g(fun x ↦ c * f x) =Θ[l] g ↔ f =Θ[l] g := by
  simpa only [← smul_eq_mul] using isTheta_const_smul_left hc

Asymptotic Equivalence Under Left Scalar Multiplication: $(c \cdot f) = \Theta[l] g \leftrightarrow f = \Theta[l] g$ for $c \neq 0$

Informal description

Let $\mathbb{K}$ be a normed field, $f : \alpha \to \mathbb{K}$ and $g : \alpha \to F$ be functions, and $l$ be a filter on $\alpha$. For any nonzero constant $c \in \mathbb{K}$, the function $x \mapsto c \cdot f(x)$ is asymptotically equivalent to $g$ up to a constant factor along $l$ if and only if $f$ is asymptotically equivalent to $g$ along $l$. In other words: $$(c \cdot f) = \Theta[l] g \leftrightarrow f = \Theta[l] g.$$

Asymptotics.isTheta_const_mul_right theorem

{c : 𝕜} {g : α → 𝕜} (hc : c ≠ 0) : (f =Θ[l] fun x ↦ c * g x) ↔ f =Θ[l] g

Full source

theorem isTheta_const_mul_right {c : 𝕜} {g : α → 𝕜} (hc : c ≠ 0) :
    (f =Θ[l] fun x ↦ c * g x) ↔ f =Θ[l] g := by
  simpa only [← smul_eq_mul] using isTheta_const_smul_right hc

Asymptotic Equivalence Under Right Scalar Multiplication: $f = \Theta[l] (c \cdot g) \leftrightarrow f = \Theta[l] g$ for $c \neq 0$

Informal description

Let $\mathbb{K}$ be a normed field, $f, g \colon \alpha \to \mathbb{K}$ be functions, $l$ be a filter on $\alpha$, and $c \in \mathbb{K}$ be a nonzero scalar. Then the asymptotic equivalence $f = \Theta[l] (x \mapsto c \cdot g(x))$ holds if and only if $f = \Theta[l] g$. In other words: $$ f = \Theta[l] (c \cdot g) \leftrightarrow f = \Theta[l] g. $$

Asymptotics.IsLittleO.right_isTheta_add theorem

{f₁ f₂ : α → E'} (h : f₁ =o[l] f₂) : f₂ =Θ[l] (f₁ + f₂)

Full source

theorem IsLittleO.right_isTheta_add {f₁ f₂ : α → E'} (h : f₁ =o[l] f₂) :
    f₂ =Θ[l] (f₁ + f₂) :=
  ⟨h.right_isBigO_add, h.add_isBigO (isBigO_refl _ _)⟩

Asymptotic equivalence of $f_2$ and $f_1 + f_2$ under little-o condition

Informal description

Let $f_1, f_2 \colon \alpha \to E'$ be functions mapping to a seminormed additive commutative group $E'$, and let $l$ be a filter on $\alpha$. If $f_1 = o[l] f_2$, then $f_2$ is asymptotically equivalent to $f_1 + f_2$ up to a constant factor, i.e., $f_2 = \Theta[l] (f_1 + f_2)$. This means there exist positive constants $C_1, C_2$ such that for all $x$ in some neighborhood determined by $l$, we have $C_1 \|f_1(x) + f_2(x)\| \leq \|f_2(x)\| \leq C_2 \|f_1(x) + f_2(x)\|$.

Asymptotics.IsLittleO.right_isTheta_add' theorem

{f₁ f₂ : α → E'} (h : f₁ =o[l] f₂) : f₂ =Θ[l] (f₂ + f₁)

Full source

theorem IsLittleO.right_isTheta_add' {f₁ f₂ : α → E'} (h : f₁ =o[l] f₂) :
    f₂ =Θ[l] (f₂ + f₁) :=
  add_comm f₁ f₂ ▸ h.right_isTheta_add

Asymptotic equivalence of $f_2$ and $f_2 + f_1$ under little-o condition

Informal description

Let $f_1, f_2 \colon \alpha \to E'$ be functions mapping to a seminormed additive commutative group $E'$, and let $l$ be a filter on $\alpha$. If $f_1 = o[l] f_2$, then $f_2$ is asymptotically equivalent to $f_2 + f_1$ up to a constant factor, i.e., $f_2 = \Theta[l] (f_2 + f_1)$. This means there exist positive constants $C_1, C_2$ such that for all $x$ in some neighborhood determined by $l$, we have $C_1 \|f_2(x) + f_1(x)\| \leq \|f_2(x)\| \leq C_2 \|f_2(x) + f_1(x)\|$.

Asymptotics.IsTheta.add_isLittleO theorem

{f₁ f₂ : α → E'} {g : α → F} (hΘ : f₁ =Θ[l] g) (ho : f₂ =o[l] g) : (f₁ + f₂) =Θ[l] g

Full source

lemma IsTheta.add_isLittleO {f₁ f₂ : α → E'} {g : α → F}
    (hΘ : f₁ =Θ[l] g) (ho : f₂ =o[l] g) : (f₁ + f₂) =Θ[l] g :=
  (ho.trans_isTheta hΘ.symm).right_isTheta_add'.symm.trans hΘ

Asymptotic Equivalence of Sum: $f_1 = \Theta(g) \land f_2 = o(g) \Rightarrow f_1 + f_2 = \Theta(g)$

Informal description

Let $f_1, f_2 \colon \alpha \to E'$ and $g \colon \alpha \to F$ be functions, where $E'$ is a seminormed additive commutative group and $F$ is a normed space. Let $l$ be a filter on $\alpha$. If $f_1$ is asymptotically equivalent to $g$ up to a constant factor (i.e., $f_1 = \Theta[l] g$) and $f_2$ is asymptotically dominated by $g$ (i.e., $f_2 = o[l] g$), then the sum $f_1 + f_2$ is asymptotically equivalent to $g$ up to a constant factor (i.e., $f_1 + f_2 = \Theta[l] g$). This means there exist positive constants $C_1, C_2$ such that for all $x$ in some neighborhood determined by $l$, we have: $$ C_1 \|g(x)\| \leq \|f_1(x) + f_2(x)\| \leq C_2 \|g(x)\|. $$

Asymptotics.IsLittleO.add_isTheta theorem

{f₁ f₂ : α → E'} {g : α → F} (ho : f₁ =o[l] g) (hΘ : f₂ =Θ[l] g) : (f₁ + f₂) =Θ[l] g

Full source

lemma IsLittleO.add_isTheta {f₁ f₂ : α → E'} {g : α → F}
    (ho : f₁ =o[l] g) (hΘ : f₂ =Θ[l] g) : (f₁ + f₂) =Θ[l] g :=
  add_comm f₁ f₂ ▸ hΘ.add_isLittleO ho

Asymptotic equivalence of sum: $f_1 = o(g) \land f_2 = \Theta(g) \Rightarrow f_1 + f_2 = \Theta(g)$

Informal description

Let $f_1, f_2 \colon \alpha \to E'$ and $g \colon \alpha \to F$ be functions, where $E'$ is a seminormed additive commutative group and $F$ is a normed space. Let $l$ be a filter on $\alpha$. If $f_1 = o[l] g$ (i.e., $f_1$ is asymptotically dominated by $g$) and $f_2 = \Theta[l] g$ (i.e., $f_2$ is asymptotically equivalent to $g$ up to a constant factor), then the sum $f_1 + f_2$ is asymptotically equivalent to $g$ up to a constant factor, i.e., $f_1 + f_2 = \Theta[l] g$. This means there exist positive constants $C_1, C_2$ such that for all $x$ in some neighborhood determined by $l$, we have: $$ C_1 \|g(x)\| \leq \|f_1(x) + f_2(x)\| \leq C_2 \|g(x)\|. $$

Asymptotics.IsTheta.fiberwise_right theorem

: f =Θ[l ×ˢ l'] g → ∀ᶠ x in l, (f ⟨x, ·⟩) =Θ[l'] (g ⟨x, ·⟩)

Full source

protected theorem IsTheta.fiberwise_right :
    f =Θ[l ×ˢ l'] g → ∀ᶠ x in l, (f ⟨x, ·⟩) =Θ[l'] (g ⟨x, ·⟩) := by
  simp only [IsTheta, eventually_and]
  exact fun ⟨h₁, h₂⟩ ↦ ⟨h₁.fiberwise_right, h₂.fiberwise_right⟩

Fiberwise Asymptotic Equivalence Along Product Filter (Right Component)

Informal description

Let $f$ and $g$ be functions such that $f = \Theta[l \times l'] g$ (i.e., $f$ is asymptotically equivalent to $g$ up to a constant factor with respect to the product filter $l \times l'$). Then for almost all $x$ in $l$, the function $f(x, \cdot)$ is asymptotically equivalent to $g(x, \cdot)$ with respect to the filter $l'$.

Asymptotics.IsTheta.fiberwise_left theorem

: f =Θ[l ×ˢ l'] g → ∀ᶠ y in l', (f ⟨·, y⟩) =Θ[l] (g ⟨·, y⟩)

Full source

protected theorem IsTheta.fiberwise_left :
    f =Θ[l ×ˢ l'] g → ∀ᶠ y in l', (f ⟨·, y⟩) =Θ[l] (g ⟨·, y⟩) := by
  simp only [IsTheta, eventually_and]
  exact fun ⟨h₁, h₂⟩ ↦ ⟨h₁.fiberwise_left, h₂.fiberwise_left⟩

Fiberwise Asymptotic Equivalence in First Variable

Informal description

Let $f$ and $g$ be functions such that $f = \Theta[l \times l'] g$ (i.e., $f$ is asymptotically equivalent to $g$ up to a constant factor with respect to the product filter $l \times l'$). Then for almost all $y$ in the filter $l'$, the function $x \mapsto f(x, y)$ is asymptotically equivalent to $x \mapsto g(x, y)$ with respect to the filter $l$.

Asymptotics.IsTheta.comp_fst theorem

: f =Θ[l] g → (f ∘ Prod.fst) =Θ[l ×ˢ l'] (g ∘ Prod.fst)

Full source

protected theorem IsTheta.comp_fst : f =Θ[l] g → (f ∘ Prod.fst) =Θ[l ×ˢ l'] (g ∘ Prod.fst) := by
  simp only [IsTheta, eventually_and]
  exact fun ⟨h₁, h₂⟩ ↦ ⟨h₁.comp_fst l', h₂.comp_fst l'⟩

Asymptotic Equivalence Preserved Under First Component Composition

Informal description

Let $f$ and $g$ be functions such that $f = \Theta[l] g$ (i.e., $f$ is asymptotically equivalent to $g$ up to a constant factor with respect to filter $l$). Then the composition $f \circ \pi_1$ is asymptotically equivalent to $g \circ \pi_1$ with respect to the product filter $l \times l'$, where $\pi_1$ denotes the projection onto the first component.

Asymptotics.IsTheta.comp_snd theorem

: f =Θ[l] g → (f ∘ Prod.snd) =Θ[l' ×ˢ l] (g ∘ Prod.snd)

Full source

protected theorem IsTheta.comp_snd : f =Θ[l] g → (f ∘ Prod.snd) =Θ[l' ×ˢ l] (g ∘ Prod.snd) := by
  simp only [IsTheta, eventually_and]
  exact fun ⟨h₁, h₂⟩ ↦ ⟨h₁.comp_snd l', h₂.comp_snd l'⟩

Asymptotic Equivalence Preserved Under Second Component Composition

Informal description

Given two functions $f$ and $g$ such that $f = \Theta[l] g$ (i.e., $f$ is asymptotically equivalent to $g$ up to a constant factor with respect to filter $l$), then the composition $f \circ \text{snd}$ is asymptotically equivalent to $g \circ \text{snd}$ with respect to the product filter $l' \times l$, where $\text{snd}$ denotes the projection onto the second component.

ContinuousOn.isTheta_principal theorem

 (hf : ContinuousOn f s) (hs : IsCompact s) (hc : ‖c‖ ≠ 0) (hC : ∀ i ∈ s, f i ≠ 0) : f =Θ[𝓟 s] fun _ => c

Full source

protected theorem isTheta_principal
    (hf : ContinuousOn f s) (hs : IsCompact s) (hc : ‖c‖‖c‖ ≠ 0) (hC : ∀ i ∈ s, f i ≠ 0) :
    f =Θ[𝓟 s] fun _ => c :=
  ⟨hf.isBigO_principal hs hc, hf.isBigO_rev_principal hs hC c⟩

Asymptotic Equivalence of Continuous Nonzero Function and Constant on Compact Set

Informal description

Let $X$ be a topological space and $E$ be a normed additive group. Let $f : X \to E$ be a function continuous on a subset $s \subseteq X$, and let $s$ be compact. Suppose $c \in E$ is a nonzero element (i.e., $\|c\| \neq 0$) and $f(x) \neq 0$ for all $x \in s$. Then $f$ is asymptotically equivalent to the constant function $\lambda \_. c$ on the principal filter generated by $s$, i.e., there exist positive constants $C_1, C_2$ such that for all $x \in s$, \[ C_1 \|c\| \leq \|f(x)\| \leq C_2 \|c\|. \]