Mathlib.Analysis.Asymptotics.Lemmas

Asymptotics.isBigOWith_principal theorem

{s : Set α} : IsBigOWith c (𝓟 s) f g ↔ ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖

Full source

@[simp]
theorem isBigOWith_principal {s : Set α} : IsBigOWithIsBigOWith c (𝓟 s) f g ↔ ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖ := by
  rw [IsBigOWith_def, eventually_principal]

Big-O With Constant $c$ on Principal Filter

Informal description

For any set $s$ of elements of type $\alpha$, the relation $\text{IsBigOWith}(c, \mathfrak{P}(s), f, g)$ holds if and only if for all $x \in s$, the norm of $f(x)$ is bounded by $c$ times the norm of $g(x)$, i.e., $\|f(x)\| \leq c \|g(x)\|$.

Asymptotics.isBigO_principal theorem

{s : Set α} : f =O[𝓟 s] g ↔ ∃ c, ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖

Full source

theorem isBigO_principal {s : Set α} : f =O[𝓟 s] gf =O[𝓟 s] g ↔ ∃ c, ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖ := by
  simp_rw [isBigO_iff, eventually_principal]

Big O Relation on Principal Filter

Informal description

For any set $s$ of elements of type $\alpha$, the relation $f = O(g)$ holds along the principal filter $\mathfrak{P}(s)$ if and only if there exists a constant $c \in \mathbb{R}$ such that for all $x \in s$, the norm of $f(x)$ is bounded by $c$ times the norm of $g(x)$, i.e., $\|f(x)\| \leq c \|g(x)\|$.

Asymptotics.isLittleO_principal theorem

{s : Set α} : f'' =o[𝓟 s] g' ↔ ∀ x ∈ s, f'' x = 0

Full source

@[simp]
theorem isLittleO_principal {s : Set α} : f'' =o[𝓟 s] g'f'' =o[𝓟 s] g' ↔ ∀ x ∈ s, f'' x = 0 := by
  refine ⟨fun h x hx ↦ norm_le_zero_iff.1 ?_, fun h ↦ ?_⟩
  · simp only [isLittleO_iff, isBigOWith_principal] at h
    have : Tendsto (fun c : ℝ => c * ‖g' x‖) (𝓝[>] 0) (𝓝 0) :=
      ((continuous_id.mul continuous_const).tendsto' _ _ (zero_mul _)).mono_left
        inf_le_left
    apply le_of_tendsto_of_tendsto tendsto_const_nhds this
    apply eventually_nhdsWithin_iff.2 (Eventually.of_forall (fun c hc ↦ ?_))
    exact eventually_principal.1 (h hc) x hx
  · apply (isLittleO_zero g' _).congr' ?_ EventuallyEq.rfl
    exact fun x hx ↦ (h x hx).symm

Characterization of Little-o on Principal Filter: $f'' = o(g')$ iff $f''$ vanishes on $s$

Informal description

For any set $s \subseteq \alpha$ and functions $f'' : \alpha \to E$, $g' : \alpha \to F$ where $E$ and $F$ are normed spaces, the relation $f'' = o(g')$ holds along the principal filter generated by $s$ if and only if $f''$ is identically zero on $s$, i.e., $f''(x) = 0$ for all $x \in s$.

Asymptotics.isBigOWith_top theorem

: IsBigOWith c ⊤ f g ↔ ∀ x, ‖f x‖ ≤ c * ‖g x‖

Full source

@[simp]
theorem isBigOWith_top : IsBigOWithIsBigOWith c ⊤ f g ↔ ∀ x, ‖f x‖ ≤ c * ‖g x‖ := by
  rw [IsBigOWith_def, eventually_top]

Global Big-O Bound with Constant $c$: $\|f(x)\| \leq c \|g(x)\|$ for all $x$

Informal description

For a real constant $c$ and functions $f, g : \alpha \to E$ where $E$ is a normed space, the relation $\text{IsBigOWith}(c, \top, f, g)$ holds if and only if for all $x$, the norm of $f(x)$ is bounded by $c$ times the norm of $g(x)$, i.e., $\|f(x)\| \leq c \|g(x)\|$.

Asymptotics.isBigO_top theorem

: f =O[⊤] g ↔ ∃ C, ∀ x, ‖f x‖ ≤ C * ‖g x‖

Full source

@[simp]
theorem isBigO_top : f =O[⊤] gf =O[⊤] g ↔ ∃ C, ∀ x, ‖f x‖ ≤ C * ‖g x‖ := by
  simp_rw [isBigO_iff, eventually_top]

Global Big-O Condition: $f = O(g) \leftrightarrow \exists C, \forall x, \|f(x)\| \leq C \|g(x)\|$

Informal description

Two functions $f$ and $g$ satisfy $f = O(g)$ globally (i.e., with respect to the trivial filter $\top$) if and only if there exists a constant $C \in \mathbb{R}$ such that for all $x$, the inequality $\|f(x)\| \leq C \|g(x)\|$ holds.

Asymptotics.isLittleO_top theorem

: f'' =o[⊤] g' ↔ ∀ x, f'' x = 0

Full source

@[simp]
theorem isLittleO_top : f'' =o[⊤] g'f'' =o[⊤] g' ↔ ∀ x, f'' x = 0 := by
  simp only [← principal_univ, isLittleO_principal, mem_univ, forall_true_left]

Global Little-o Condition: $f'' = o(g') \leftrightarrow f'' \equiv 0$

Informal description

For functions $f'' : \alpha \to E$ and $g' : \alpha \to F$ where $E$ and $F$ are normed spaces, the relation $f'' = o[⊤] g'$ holds (i.e., $f''$ is little-o of $g'$ globally) if and only if $f''$ is identically zero, meaning $f''(x) = 0$ for all $x \in \alpha$.

Asymptotics.isBigOWith_const_one theorem

(c : E) (l : Filter α) : IsBigOWith ‖c‖ l (fun _x : α => c) fun _x => (1 : F)

Full source

theorem isBigOWith_const_one (c : E) (l : Filter α) :
    IsBigOWith ‖c‖ l (fun _x : α => c) fun _x => (1 : F) := by simp [isBigOWith_iff]

Big-O Bound for Constant Function with Unit Norm: $\|c\| \cdot 1$

Informal description

For any element $c$ in a normed space $E$ and any filter $l$ on a type $\alpha$, the constant function $f(x) = c$ is bounded by $\|c\|$ times the constant function $g(x) = 1$ with respect to the filter $l$. In other words, $\text{IsBigOWith}(\|c\|, l, f, g)$ holds, where $f(x) = c$ and $g(x) = 1$ for all $x \in \alpha$.

Asymptotics.isBigO_const_one theorem

(c : E) (l : Filter α) : (fun _x : α => c) =O[l] fun _x => (1 : F)

Full source

theorem isBigO_const_one (c : E) (l : Filter α) : (fun _x : α => c) =O[l] fun _x => (1 : F) :=
  (isBigOWith_const_one F c l).isBigO

Constant Function is Big O of Unit Function: $c =O[l] 1$

Informal description

For any element $c$ in a normed space $E$ and any filter $l$ on a type $\alpha$, the constant function $f(x) = c$ is big O of the constant function $g(x) = 1$ with respect to the filter $l$, i.e., $f =O[l] g$.

Asymptotics.isLittleO_const_iff_isLittleO_one theorem

{c : F''} (hc : c ≠ 0) : (f =o[l] fun _x => c) ↔ f =o[l] fun _x => (1 : F)

Full source

theorem isLittleO_const_iff_isLittleO_one {c : F''} (hc : c ≠ 0) :
    (f =o[l] fun _x => c) ↔ f =o[l] fun _x => (1 : F) :=
  ⟨fun h => h.trans_isBigOWith (isBigOWith_const_one _ _ _) (norm_pos_iff.2 hc),
   fun h => h.trans_isBigO <| isBigO_const_const _ hc _⟩

Equivalence of Little-o Relations: $f = o(c) \leftrightarrow f = o(1)$ for $c \neq 0$

Informal description

For a function $f : \alpha \to E$ and a nonzero constant $c \in F''$, the relation $f = o[l] (c)$ holds if and only if $f = o[l] (1)$ with respect to the filter $l$ on $\alpha$.

Asymptotics.isLittleO_one_iff theorem

{f : α → E'''} : f =o[l] (fun _x => 1 : α → F) ↔ Tendsto f l (𝓝 0)

Full source

@[simp]
theorem isLittleO_one_iff {f : α → E'''} : f =o[l] (fun _x => 1 : α → F)f =o[l] (fun _x => 1 : α → F) ↔ Tendsto f l (𝓝 0) := by
  simp only [isLittleO_iff, norm_one, mul_one, Metric.nhds_basis_closedBall.tendsto_right_iff,
    Metric.mem_closedBall, dist_zero_right]

Characterization of Little-o with respect to the constant function 1: $f = o[l] (1) \leftrightarrow f \to 0$ along $l$

Informal description

For a function $f : \alpha \to E$ and a filter $l$ on $\alpha$, the relation $f = o[l] (1)$ holds if and only if $f$ tends to $0$ along the filter $l$.

Asymptotics.isBigO_one_iff theorem

: f =O[l] (fun _x => 1 : α → F) ↔ IsBoundedUnder (· ≤ ·) l fun x => ‖f x‖

Full source

@[simp]
theorem isBigO_one_iff : f =O[l] (fun _x => 1 : α → F)f =O[l] (fun _x => 1 : α → F) ↔
    IsBoundedUnder (· ≤ ·) l fun x => ‖f x‖ := by
  simp only [isBigO_iff, norm_one, mul_one, IsBoundedUnder, IsBounded, eventually_map]

Characterization of Big-O with respect to the constant function 1

Informal description

A function $f : \alpha \to E$ is asymptotically bounded by the constant function $1$ along a filter $l$ (i.e., $f = O[l] (1)$) if and only if the norm $\|f(x)\|$ is bounded under the order relation $\leq$ as $x$ tends to $l$.

Asymptotics.isLittleO_one_left_iff theorem

: (fun _x => 1 : α → F) =o[l] f ↔ Tendsto (fun x => ‖f x‖) l atTop

Full source

@[simp]
theorem isLittleO_one_left_iff : (fun _x => 1 : α → F) =o[l] f(fun _x => 1 : α → F) =o[l] f ↔ Tendsto (fun x => ‖f x‖) l atTop :=
  calc
    (fun _x => 1 : α → F) =o[l] f ↔ ∀ n : ℕ, ∀ᶠ x in l, ↑n * ‖(1 : F)‖ ≤ ‖f x‖ :=
      isLittleO_iff_nat_mul_le_aux <| Or.inl fun _x => by simp only [norm_one, zero_le_one]
    _ ↔ ∀ n : ℕ, True → ∀ᶠ x in l, ‖f x‖ ∈ Ici (n : ℝ)calc
    (fun _x => 1 : α → F) =o[l] f ↔ ∀ n : ℕ, ∀ᶠ x in l, ↑n * ‖(1 : F)‖ ≤ ‖f x‖ :=
      isLittleO_iff_nat_mul_le_aux <| Or.inl fun _x => by simp only [norm_one, zero_le_one]
    _ ↔ ∀ n : ℕ, True → ∀ᶠ x in l, ‖f x‖ ∈ Ici (n : ℝ) := by
      simp only [norm_one, mul_one, true_imp_iff, mem_Ici]
    _ ↔ Tendsto (fun x => ‖f x‖) l atTop :=
      atTop_hasCountableBasis_of_archimedean.1.tendsto_right_iff.symm

Characterization of $1 = o(f)$ via $\|f\| \to \infty$

Informal description

For a function $f : \alpha \to F$ and a filter $l$ on $\alpha$, the constant function $1$ is asymptotically dominated by $f$ (i.e., $1 = o[l] f$) if and only if the norm $\|f(x)\|$ tends to infinity along the filter $l$.

Filter.Tendsto.isBigO_one theorem

{c : E'} (h : Tendsto f' l (𝓝 c)) : f' =O[l] (fun _x => 1 : α → F)

Full source

theorem _root_.Filter.Tendsto.isBigO_one {c : E'} (h : Tendsto f' l (𝓝 c)) :
    f' =O[l] (fun _x => 1 : α → F) :=
  h.norm.isBoundedUnder_le.isBigO_one F

Functions Converging to a Limit are Big-O of One

Informal description

Let $f' : \alpha \to E'$ be a function and $l$ a filter on $\alpha$. If $f'$ tends to some limit $c \in E'$ along $l$, then $f'$ is asymptotically bounded by the constant function $1$ along $l$, i.e., $f' = O[l] (1)$.

Asymptotics.IsBigO.trans_tendsto_nhds theorem

(hfg : f =O[l] g') {y : F'} (hg : Tendsto g' l (𝓝 y)) : f =O[l] (fun _x => 1 : α → F)

Full source

theorem IsBigO.trans_tendsto_nhds (hfg : f =O[l] g') {y : F'} (hg : Tendsto g' l (𝓝 y)) :
    f =O[l] (fun _x => 1 : α → F) :=
  hfg.trans <| hg.isBigO_one F

Big-O Transitivity with Limit Tendency: $f = O(g')$ and $g' \to y$ implies $f = O(1)$

Informal description

Let $f : \alpha \to E$ and $g' : \alpha \to F'$ be functions to normed spaces, and let $l$ be a filter on $\alpha$. If $f$ is asymptotically bounded by $g'$ along $l$ (i.e., $f = O(g')$ at $l$) and $g'$ tends to a limit $y \in F'$ along $l$, then $f$ is asymptotically bounded by the constant function $1$ along $l$ (i.e., $f = O(1)$ at $l$).

Asymptotics.isBigO_one_nhds_ne_iff theorem

[TopologicalSpace α] {a : α} : f =O[𝓝[≠] a] (fun _ ↦ 1 : α → F) ↔ f =O[𝓝 a] (fun _ ↦ 1 : α → F)

Full source

/-- The condition `f = O[𝓝[≠] a] 1` is equivalent to `f = O[𝓝 a] 1`. -/
lemma isBigO_one_nhds_ne_iff [TopologicalSpace α] {a : α} :
    f =O[𝓝[≠] a] (fun _ ↦ 1 : α → F)f =O[𝓝[≠] a] (fun _ ↦ 1 : α → F) ↔ f =O[𝓝 a] (fun _ ↦ 1 : α → F) := by
  refine ⟨fun h ↦ ?_, fun h ↦ h.mono nhdsWithin_le_nhds⟩
  simp only [isBigO_one_iff, IsBoundedUnder, IsBounded, eventually_map] at h ⊢
  obtain ⟨c, hc⟩ := h
  use max c ‖f a‖
  filter_upwards [eventually_nhdsWithin_iff.mp hc] with b hb
  rcases eq_or_ne b a with rfl | hb'
  · apply le_max_right
  · exact (hb hb').trans (le_max_left ..)

Equivalence of Big-O Conditions at a Point and its Punctured Neighborhood

Informal description

Let $\alpha$ be a topological space and $a \in \alpha$. For a function $f : \alpha \to E$ (where $E$ is a normed space), the following are equivalent: 1. $f$ is big-O of the constant function $1$ along the punctured neighborhood filter $\mathfrak{N}[{\neq}a]a$. 2. $f$ is big-O of the constant function $1$ along the full neighborhood filter $\mathfrak{N}a$. In other words, $f = O(1)$ as $x \to a$ excluding $a$ if and only if $f = O(1)$ as $x \to a$ including $a$.

Asymptotics.isLittleO_const_iff theorem

{c : F''} (hc : c ≠ 0) : (f'' =o[l] fun _x => c) ↔ Tendsto f'' l (𝓝 0)

Full source

theorem isLittleO_const_iff {c : F''} (hc : c ≠ 0) :
    (f'' =o[l] fun _x => c) ↔ Tendsto f'' l (𝓝 0) :=
  (isLittleO_const_iff_isLittleO_one ℝ hc).trans (isLittleO_one_iff _)

Characterization of Little-o with respect to a nonzero constant: $f = o(c) \leftrightarrow f \to 0$ for $c \neq 0$

Informal description

For a function $f'' : \alpha \to E$ and a nonzero constant $c \in F''$, the relation $f'' = o[l] (c)$ holds if and only if $f''$ tends to $0$ along the filter $l$.

Asymptotics.isLittleO_id_const theorem

{c : F''} (hc : c ≠ 0) : (fun x : E'' => x) =o[𝓝 0] fun _x => c

Full source

theorem isLittleO_id_const {c : F''} (hc : c ≠ 0) : (fun x : E'' => x) =o[𝓝 0] fun _x => c :=
  (isLittleO_const_iff hc).mpr (continuous_id.tendsto 0)

Identity Function is Little-o of Nonzero Constant at Zero

Informal description

For any nonzero constant $c$ in a normed additive commutative group $F''$, the identity function $\text{id} : E'' \to E''$ satisfies $\text{id} = o_{\mathfrak{N}0} (x \mapsto c)$, where $\mathfrak{N}0$ is the neighborhood filter at $0$ in $E''$. In other words, the identity function is little-o of the constant function $x \mapsto c$ as $x$ approaches $0$.

Filter.IsBoundedUnder.isBigO_const theorem

(h : IsBoundedUnder (· ≤ ·) l (norm ∘ f)) {c : F''} (hc : c ≠ 0) : f =O[l] fun _x => c

Full source

theorem _root_.Filter.IsBoundedUnder.isBigO_const (h : IsBoundedUnder (· ≤ ·) l (normnorm ∘ f))
    {c : F''} (hc : c ≠ 0) : f =O[l] fun _x => c :=
  (h.isBigO_one ℝ).trans (isBigO_const_const _ hc _)

Bounded Norm Implies Big-O Relation with Nonzero Constant Function

Informal description

Let $f : \alpha \to E$ be a function to a normed space $E$, and let $l$ be a filter on $\alpha$. If the function $\|f\|$ is bounded above under the order relation $\leq$ along the filter $l$, then for any nonzero constant $c \in F''$, the function $f$ is big-O of the constant function $\lambda x \mapsto c$ along $l$, i.e., $f = O[l] (\lambda x \mapsto c)$.

Asymptotics.isBigO_const_of_tendsto theorem

{y : E''} (h : Tendsto f'' l (𝓝 y)) {c : F''} (hc : c ≠ 0) : f'' =O[l] fun _x => c

Full source

theorem isBigO_const_of_tendsto {y : E''} (h : Tendsto f'' l (𝓝 y)) {c : F''} (hc : c ≠ 0) :
    f'' =O[l] fun _x => c :=
  h.norm.isBoundedUnder_le.isBigO_const hc

Big-O Relation for Functions Tending to a Limit with Nonzero Constant Function

Informal description

Let $f''$ be a function from a type $\alpha$ to a normed space $E''$, and let $l$ be a filter on $\alpha$. If $f''$ tends to $y \in E''$ along the filter $l$, then for any nonzero constant $c \in F''$, the function $f''$ is big-O of the constant function $\lambda x \mapsto c$ along $l$, i.e., $f'' = O[l] (\lambda x \mapsto c)$.

Asymptotics.IsBigO.isBoundedUnder_le theorem

{c : F} (h : f =O[l] fun _x => c) : IsBoundedUnder (· ≤ ·) l (norm ∘ f)

Full source

theorem IsBigO.isBoundedUnder_le {c : F} (h : f =O[l] fun _x => c) :
    IsBoundedUnder (· ≤ ·) l (normnorm ∘ f) :=
  let ⟨c', hc'⟩ := h.bound
  ⟨c' * ‖c‖, eventually_map.2 hc'⟩

Boundedness of Norm under Big-O with Constant Function

Informal description

Let $f : \alpha \to E$ be a function and $c \in F$ be a nonzero constant. If $f$ is big-O of the constant function $\lambda x, c$ along a filter $l$ (i.e., $f =O[l] (\lambda x, c)$), then the function $\|f\|$ is bounded above under the order relation $\leq$ along the filter $l$.

Asymptotics.isBigO_const_of_ne theorem

{c : F''} (hc : c ≠ 0) : (f =O[l] fun _x => c) ↔ IsBoundedUnder (· ≤ ·) l (norm ∘ f)

Full source

theorem isBigO_const_of_ne {c : F''} (hc : c ≠ 0) :
    (f =O[l] fun _x => c) ↔ IsBoundedUnder (· ≤ ·) l (norm ∘ f) :=
  ⟨fun h => h.isBoundedUnder_le, fun h => h.isBigO_const hc⟩

Big-O Relation with Nonzero Constant Function is Equivalent to Bounded Norm

Informal description

For a function $f : \alpha \to E$ and a nonzero constant $c \in F''$, the relation $f = O[l] (\lambda x, c)$ holds if and only if the function $\|f\|$ is bounded above under the order relation $\leq$ along the filter $l$.

Asymptotics.isBigO_const_iff theorem

{c : F''} : (f'' =O[l] fun _x => c) ↔ (c = 0 → f'' =ᶠ[l] 0) ∧ IsBoundedUnder (· ≤ ·) l fun x => ‖f'' x‖

Full source

theorem isBigO_const_iff {c : F''} : (f'' =O[l] fun _x => c) ↔
    (c = 0 → f'' =ᶠ[l] 0) ∧ IsBoundedUnder (· ≤ ·) l fun x => ‖f'' x‖ := by
  refine ⟨fun h => ⟨fun hc => isBigO_zero_right_iff.1 (by rwa [← hc]), h.isBoundedUnder_le⟩, ?_⟩
  rintro ⟨hcf, hf⟩
  rcases eq_or_ne c 0 with (hc | hc)
  exacts [(hcf hc).trans_isBigO (isBigO_zero _ _), hf.isBigO_const hc]

Characterization of Big-O Relation with Constant Function: $f'' = O[l] c$

Informal description

For a function $f'' : \alpha \to E$ and a constant $c \in F''$, the relation $f'' = O[l] (\lambda x \mapsto c)$ holds if and only if both of the following conditions are satisfied: 1. If $c = 0$, then $f''$ is eventually zero along the filter $l$. 2. The function $\lambda x \mapsto \|f''(x)\|$ is bounded above under the order relation $\leq$ along the filter $l$.

Asymptotics.isBigO_iff_isBoundedUnder_le_div theorem

(h : ∀ᶠ x in l, g'' x ≠ 0) : f =O[l] g'' ↔ IsBoundedUnder (· ≤ ·) l fun x => ‖f x‖ / ‖g'' x‖

Full source

theorem isBigO_iff_isBoundedUnder_le_div (h : ∀ᶠ x in l, g'' x ≠ 0) :
    f =O[l] g''f =O[l] g'' ↔ IsBoundedUnder (· ≤ ·) l fun x => ‖f x‖ / ‖g'' x‖ := by
  simp only [isBigO_iff, IsBoundedUnder, IsBounded, eventually_map]
  exact
    exists_congr fun c =>
      eventually_congr <| h.mono fun x hx => (div_le_iff₀ <| norm_pos_iff.2 hx).symm

Big-O Characterization via Bounded Ratio of Norms

Informal description

Let $f$ and $g''$ be functions defined on a type $\alpha$ with values in normed spaces, and let $l$ be a filter on $\alpha$. Suppose that $g''(x) \neq 0$ for all $x$ in some neighborhood determined by $l$. Then $f = O(g'')$ with respect to $l$ if and only if the function $x \mapsto \frac{\|f(x)\|}{\|g''(x)\|}$ is bounded above under the order relation $\leq$ along the filter $l$.

Asymptotics.isBigO_const_left_iff_pos_le_norm theorem

{c : E''} (hc : c ≠ 0) : (fun _x => c) =O[l] f' ↔ ∃ b, 0 < b ∧ ∀ᶠ x in l, b ≤ ‖f' x‖

Full source

/-- `(fun x ↦ c) =O[l] f` if and only if `f` is bounded away from zero. -/
theorem isBigO_const_left_iff_pos_le_norm {c : E''} (hc : c ≠ 0) :
    (fun _x => c) =O[l] f'(fun _x => c) =O[l] f' ↔ ∃ b, 0 < b ∧ ∀ᶠ x in l, b ≤ ‖f' x‖ := by
  constructor
  · intro h
    rcases h.exists_pos with ⟨C, hC₀, hC⟩
    refine ⟨‖c‖ / C, div_pos (norm_pos_iff.2 hc) hC₀, ?_⟩
    exact hC.bound.mono fun x => (div_le_iff₀' hC₀).2
  · rintro ⟨b, hb₀, hb⟩
    refine IsBigO.of_bound (‖c‖ / b) (hb.mono fun x hx => ?_)
    rw [div_mul_eq_mul_div, mul_div_assoc]
    exact le_mul_of_one_le_right (norm_nonneg _) ((one_le_div hb₀).2 hx)

Big-O Condition for Constant Function: $(x \mapsto c) = O(f')$ if and only if $f'$ is bounded away from zero

Informal description

For any nonzero element $c$ in a normed space $E''$, the constant function $x \mapsto c$ is big O of a function $f'$ along a filter $l$ if and only if there exists a positive real number $b > 0$ such that $\|f'(x)\| \geq b$ for all $x$ in some neighborhood determined by $l$.

Asymptotics.IsBigO.trans_tendsto theorem

(hfg : f'' =O[l] g'') (hg : Tendsto g'' l (𝓝 0)) : Tendsto f'' l (𝓝 0)

Full source

theorem IsBigO.trans_tendsto (hfg : f'' =O[l] g'') (hg : Tendsto g'' l (𝓝 0)) :
    Tendsto f'' l (𝓝 0) :=
  (isLittleO_one_iff ℝ).1 <| hfg.trans_isLittleO <| (isLittleO_one_iff ℝ).2 hg

Big-O and Limit Zero: $f = O(g) \land g \to 0 \Rightarrow f \to 0$

Informal description

Let $f''$ and $g''$ be functions from a topological space $\alpha$ to normed spaces, and let $l$ be a filter on $\alpha$. If $f''$ is big O of $g''$ along $l$ (i.e., there exists a constant $C > 0$ such that $\|f''(x)\| \leq C \|g''(x)\|$ for all $x$ in some neighborhood in $l$) and $g''$ tends to $0$ along $l$, then $f''$ also tends to $0$ along $l$.

Asymptotics.isLittleO_id_one theorem

[One F''] [NeZero (1 : F'')] : (fun x : E'' => x) =o[𝓝 0] (1 : E'' → F'')

Full source

lemma isLittleO_id_one [One F''] [NeZero (1 : F'')] : (fun x : E'' => x) =o[𝓝 0] (1 : E'' → F'') :=
  isLittleO_id_const one_ne_zero

Identity Function is Little-o of Unit Constant at Zero

Informal description

Let $E''$ and $F''$ be normed additive commutative groups, where $F''$ has a multiplicative identity element $1$ satisfying $1 \neq 0$. Then the identity function $\text{id} : E'' \to E''$ satisfies $\text{id} = o_{\mathfrak{N}0} (x \mapsto 1)$, where $\mathfrak{N}0$ is the neighborhood filter at $0$ in $E''$. In other words, the identity function is little-o of the constant function $x \mapsto 1$ as $x$ approaches $0$.

Asymptotics.continuousAt_iff_isLittleO theorem

 {α : Type*} {E : Type*} [NormedRing E] [NormOneClass E] [TopologicalSpace α] {f : α → E} {x : α} :
  (ContinuousAt f x) ↔ (fun (y : α) ↦ f y - f x) =o[𝓝 x] (fun (_ : α) ↦ (1 : E))

Full source

theorem continuousAt_iff_isLittleO {α : Type*} {E : Type*} [NormedRing E] [NormOneClass E]
    [TopologicalSpace α] {f : α → E} {x : α} :
    (ContinuousAt f x) ↔ (fun (y : α) ↦ f y - f x) =o[𝓝 x] (fun (_ : α) ↦ (1 : E)) := by
  simp [ContinuousAt, ← tendsto_sub_nhds_zero_iff]

Characterization of Continuity via Little-o: $f$ continuous at $x$ $\iff$ $f(y)-f(x) = o(1)$ as $y \to x$

Informal description

Let $E$ be a normed ring with multiplicative identity of norm 1, and let $X$ be a topological space. A function $f \colon X \to E$ is continuous at a point $x \in X$ if and only if the function $y \mapsto f(y) - f(x)$ is $o(1)$ as $y \to x$ (i.e., $\|f(y) - f(x)\| = o(1)$ as $y \to x$).

Asymptotics.IsBigO.of_pow theorem

{f : α → 𝕜} {g : α → R} {n : ℕ} (hn : n ≠ 0) (h : (f ^ n) =O[l] (g ^ n)) : f =O[l] g

Full source

theorem IsBigO.of_pow {f : α → 𝕜} {g : α → R} {n : ℕ} (hn : n ≠ 0) (h : (f ^ n) =O[l] (g ^ n)) :
    f =O[l] g := by
  rcases h.exists_pos with ⟨C, _hC₀, hC⟩
  obtain ⟨c : ℝ, hc₀ : 0 ≤ c, hc : C ≤ c ^ n⟩ :=
    ((eventually_ge_atTop _).and <| (tendsto_pow_atTop hn).eventually_ge_atTop C).exists
  exact (hC.of_pow hn hc hc₀).isBigO

Big-O relation preserved under taking powers: $f^n =O(g^n) \implies f =O(g)$ for $n \neq 0$

Informal description

Let $f : \alpha \to \mathbb{K}$ and $g : \alpha \to R$ be functions, where $\mathbb{K}$ is a normed field and $R$ is a normed ring. If $n$ is a nonzero natural number and $f^n$ is big-O of $g^n$ along a filter $l$ (i.e., $f^n =O[l] g^n$), then $f$ is big-O of $g$ along the same filter (i.e., $f =O[l] g$).

Asymptotics.IsBigOWith.const_smul_self theorem

(c' : R) : IsBigOWith (‖c'‖) l (fun x => c' • f' x) f'

Full source

theorem IsBigOWith.const_smul_self (c' : R) :
    IsBigOWith (‖c'‖) l (fun x => c' • f' x) f' :=
  isBigOWith_of_le' _ fun _ => norm_smul_le _ _

Scalar Multiplication Preserves Big-O Bound: $\|c' \cdot f'\| \leq \|c'\| \cdot \|f'\|$

Informal description

For any scalar $c'$ in a normed ring $R$ and any function $f'$ mapping to a normed space, the function $x \mapsto c' \cdot f'(x)$ is big-O of $f'$ along the filter $l$ with constant $\|c'\|$. That is, $\|c' \cdot f'(x)\| \leq \|c'\| \cdot \|f'(x)\|$ holds for all $x$ in $l$ eventually.

Asymptotics.IsBigO.const_smul_self theorem

(c' : R) : (fun x => c' • f' x) =O[l] f'

Full source

theorem IsBigO.const_smul_self (c' : R) : (fun x => c' • f' x) =O[l] f' :=
  (IsBigOWith.const_smul_self _).isBigO

Scalar Multiplication Preserves Big-O Relation: $c' \cdot f' =O[l] f'$

Informal description

For any scalar $c'$ in a normed ring $R$ and any function $f' : \alpha \to E$ where $E$ is a normed space, the function $x \mapsto c' \cdot f'(x)$ is big-O of $f'$ along the filter $l$, i.e., $c' \cdot f' =O[l] f'$.

Asymptotics.IsBigOWith.const_smul_left theorem

(h : IsBigOWith c l f' g) (c' : R) : IsBigOWith (‖c'‖ * c) l (fun x => c' • f' x) g

Full source

theorem IsBigOWith.const_smul_left (h : IsBigOWith c l f' g) (c' : R) :
    IsBigOWith (‖c'‖ * c) l (fun x => c' • f' x) g :=
  .trans (.const_smul_self _) h (norm_nonneg _)

Scalar Multiplication Preserves Big-O Bound: $\|c' \cdot f'\| \leq \|c'\| \cdot c \cdot \|g\|$

Informal description

Let $f' : \alpha \to E$ and $g : \alpha \to F$ be functions to normed spaces, and let $l$ be a filter on $\alpha$. Suppose there exists a constant $c \geq 0$ such that $\|f'(x)\| \leq c \|g(x)\|$ for all $x$ in $l$ eventually. Then, for any scalar $c'$ in a normed ring $R$, the function $x \mapsto c' \cdot f'(x)$ satisfies $\|c' \cdot f'(x)\| \leq \|c'\| \cdot c \|g(x)\|$ for all $x$ in $l$ eventually.

Asymptotics.IsBigO.const_smul_left theorem

(h : f' =O[l] g) (c : R) : (c • f') =O[l] g

Full source

theorem IsBigO.const_smul_left (h : f' =O[l] g) (c : R) : (c • f') =O[l] g :=
  let ⟨_b, hb⟩ := h.isBigOWith
  (hb.const_smul_left _).isBigO

Scalar Multiplication Preserves Big-O Relation: $(c \cdot f') =O[l] g$

Informal description

Let $f' : \alpha \to E$ and $g : \alpha \to F$ be functions to normed spaces, and let $l$ be a filter on $\alpha$. If $f'$ is big-O of $g$ along $l$, denoted $f' =O[l] g$, then for any scalar $c$ in a normed ring $R$, the scalar multiple $c \cdot f'$ is also big-O of $g$ along $l$, i.e., $(c \cdot f') =O[l] g$.

Asymptotics.IsLittleO.const_smul_left theorem

(h : f' =o[l] g) (c : R) : (c • f') =o[l] g

Full source

theorem IsLittleO.const_smul_left (h : f' =o[l] g) (c : R) : (c • f') =o[l] g :=
  (IsBigO.const_smul_self _).trans_isLittleO h

Scalar Multiplication Preserves Little-o Relation: $(c \cdot f') = o[l] g$

Informal description

Let $f' : \alpha \to E$ and $g : \alpha \to F$ be functions to normed spaces, and let $l$ be a filter on $\alpha$. If $f'$ is little-o of $g$ along $l$ (i.e., $f' = o[l] g$), then for any scalar $c$ in a normed ring $R$, the scalar multiple $c \cdot f'$ is also little-o of $g$ along $l$ (i.e., $(c \cdot f') = o[l] g$).

Asymptotics.isBigO_const_smul_left theorem

{c : 𝕜} (hc : c ≠ 0) : (fun x => c • f' x) =O[l] g ↔ f' =O[l] g

Full source

theorem isBigO_const_smul_left {c : 𝕜} (hc : c ≠ 0) : (fun x => c • f' x) =O[l] g(fun x => c • f' x) =O[l] g ↔ f' =O[l] g := by
  have cne0 : ‖c‖‖c‖ ≠ 0 := norm_ne_zero_iff.mpr hc
  rw [← isBigO_norm_left]
  simp only [norm_smul]
  rw [isBigO_const_mul_left_iff cne0, isBigO_norm_left]

Big-O Equivalence Under Nonzero Scalar Multiplication: $(c \cdot f') = O(g) \leftrightarrow f' = O(g)$ for $c \neq 0$

Informal description

Let $\mathbb{K}$ be a normed field, $f' \colon \alpha \to E$ and $g \colon \alpha \to F$ be functions to normed spaces, $l$ be a filter on $\alpha$, and $c \in \mathbb{K}$ be a nonzero scalar. Then the scalar multiple function $x \mapsto c \cdot f'(x)$ is big-O of $g$ along $l$ if and only if $f'$ is big-O of $g$ along $l$. In other words: $$(c \cdot f') =O[l] g \leftrightarrow f' =O[l] g.$$

Asymptotics.isLittleO_const_smul_left theorem

{c : 𝕜} (hc : c ≠ 0) : (fun x => c • f' x) =o[l] g ↔ f' =o[l] g

Full source

theorem isLittleO_const_smul_left {c : 𝕜} (hc : c ≠ 0) :
    (fun x => c • f' x) =o[l] g(fun x => c • f' x) =o[l] g ↔ f' =o[l] g := by
  have cne0 : ‖c‖‖c‖ ≠ 0 := norm_ne_zero_iff.mpr hc
  rw [← isLittleO_norm_left]
  simp only [norm_smul]
  rw [isLittleO_const_mul_left_iff cne0, isLittleO_norm_left]

Equivalence of Little-o Relations under Nonzero Scalar Multiplication: $(c \cdot f') = o[l] g \leftrightarrow f' = o[l] g$ for $c \neq 0$

Informal description

Let $\mathbb{K}$ be a normed field, $f' \colon \alpha \to E$ and $g \colon \alpha \to F$ be functions to normed spaces, $l$ be a filter on $\alpha$, and $c \in \mathbb{K}$ be a nonzero scalar. Then the scalar multiple function $x \mapsto c \cdot f'(x)$ is little-o of $g$ along $l$ if and only if $f'$ is little-o of $g$ along $l$. In other words: \[ (c \cdot f') = o[l] g \leftrightarrow f' = o[l] g. \]

Asymptotics.isBigO_const_smul_right theorem

{c : 𝕜} (hc : c ≠ 0) : (f =O[l] fun x => c • f' x) ↔ f =O[l] f'

Full source

theorem isBigO_const_smul_right {c : 𝕜} (hc : c ≠ 0) :
    (f =O[l] fun x => c • f' x) ↔ f =O[l] f' := by
  have cne0 : ‖c‖‖c‖ ≠ 0 := norm_ne_zero_iff.mpr hc
  rw [← isBigO_norm_right]
  simp only [norm_smul]
  rw [isBigO_const_mul_right_iff cne0, isBigO_norm_right]

Equivalence of Big-O Relations Under Right Scalar Multiplication by Nonzero Constant: $f =O[l] (c \cdot f') \leftrightarrow f =O[l] f'$

Informal description

Let $\mathbb{K}$ be a normed field, $f \colon \alpha \to E$ and $f' \colon \alpha \to F$ be functions to normed spaces, $l$ be a filter on $\alpha$, and $c \in \mathbb{K}$ be a nonzero scalar. Then the following equivalence holds: \[ f =O[l] (x \mapsto c \cdot f'(x)) \quad \text{if and only if} \quad f =O[l] f'. \]

Asymptotics.isLittleO_const_smul_right theorem

{c : 𝕜} (hc : c ≠ 0) : (f =o[l] fun x => c • f' x) ↔ f =o[l] f'

Full source

theorem isLittleO_const_smul_right {c : 𝕜} (hc : c ≠ 0) :
    (f =o[l] fun x => c • f' x) ↔ f =o[l] f' := by
  have cne0 : ‖c‖‖c‖ ≠ 0 := norm_ne_zero_iff.mpr hc
  rw [← isLittleO_norm_right]
  simp only [norm_smul]
  rw [isLittleO_const_mul_right_iff cne0, isLittleO_norm_right]

Equivalence of Little-o Relations under Nonzero Scalar Multiplication: $f = o(c \cdot f') \leftrightarrow f = o(f')$ for $c \neq 0$

Informal description

Let $\mathbb{K}$ be a normed field, $f \colon \alpha \to E$ and $f' \colon \alpha \to F$ be functions to normed spaces, $l$ be a filter on $\alpha$, and $c \in \mathbb{K}$ be a nonzero scalar. Then the following are equivalent: 1. $f = o[l] (x \mapsto c \cdot f'(x))$ 2. $f = o[l] f'$ In other words, $f$ is little-o of the scalar multiple $c \cdot f'$ along $l$ if and only if $f$ is little-o of $f'$ along $l$.

Asymptotics.IsBigOWith.smul theorem

 (h₁ : IsBigOWith c l k₁ k₂) (h₂ : IsBigOWith c' l f' g') :
  IsBigOWith (c * c') l (fun x => k₁ x • f' x) fun x => k₂ x • g' x

Full source

theorem IsBigOWith.smul (h₁ : IsBigOWith c l k₁ k₂) (h₂ : IsBigOWith c' l f' g') :
    IsBigOWith (c * c') l (fun x => k₁ x • f' x) fun x => k₂ x • g' x := by
  simp only [IsBigOWith_def] at *
  filter_upwards [h₁, h₂] with _ hx₁ hx₂
  apply le_trans (norm_smul_le _ _)
  convert mul_le_mul hx₁ hx₂ (norm_nonneg _) (le_trans (norm_nonneg _) hx₁) using 1
  rw [norm_smul, mul_mul_mul_comm]

Product of Big-O Bounds: $\text{IsBigOWith}(c) \times \text{IsBigOWith}(c') \Rightarrow \text{IsBigOWith}(c \cdot c')$ for Scalar Multiplication

Informal description

Asymptotics.IsBigO.smul theorem

(h₁ : k₁ =O[l] k₂) (h₂ : f' =O[l] g') : (fun x => k₁ x • f' x) =O[l] fun x => k₂ x • g' x

Full source

theorem IsBigO.smul (h₁ : k₁ =O[l] k₂) (h₂ : f' =O[l] g') :
    (fun x => k₁ x • f' x) =O[l] fun x => k₂ x • g' x := by
  obtain ⟨c₁, h₁⟩ := h₁.isBigOWith
  obtain ⟨c₂, h₂⟩ := h₂.isBigOWith
  exact (h₁.smul h₂).isBigO

Big-O relation preserved under scalar multiplication: $k_1 =O(k_2)$ and $f' =O(g')$ implies $k_1 \cdot f' =O(k_2 \cdot g')$

Informal description

Let $k_1, k_2 : \alpha \to E$ and $f', g' : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If $k_1 =O[l] k_2$ and $f' =O[l] g'$, then the function $x \mapsto k_1(x) \cdot f'(x)$ is big O of $x \mapsto k_2(x) \cdot g'(x)$ along $l$.

Asymptotics.IsBigO.smul_isLittleO theorem

(h₁ : k₁ =O[l] k₂) (h₂ : f' =o[l] g') : (fun x => k₁ x • f' x) =o[l] fun x => k₂ x • g' x

Full source

theorem IsBigO.smul_isLittleO (h₁ : k₁ =O[l] k₂) (h₂ : f' =o[l] g') :
    (fun x => k₁ x • f' x) =o[l] fun x => k₂ x • g' x := by
  simp only [IsLittleO_def] at *
  intro c cpos
  rcases h₁.exists_pos with ⟨c', c'pos, hc'⟩
  exact (hc'.smul (h₂ (div_pos cpos c'pos))).congr_const (mul_div_cancel₀ _ (ne_of_gt c'pos))

Big-O and Little-o Interaction: $k_1 = O(k_2)$ and $f' = o(g')$ implies $k_1 \cdot f' = o(k_2 \cdot g')$

Informal description

Let $k_1, k_2 : \alpha \to E$ and $f', g' : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If $k_1$ is big O of $k_2$ along $l$ (i.e., $k_1 = O(k_2)$) and $f'$ is little o of $g'$ along $l$ (i.e., $f' = o(g')$), then the function $x \mapsto k_1(x) \cdot f'(x)$ is little o of $x \mapsto k_2(x) \cdot g'(x)$ along $l$ (i.e., $k_1 \cdot f' = o(k_2 \cdot g')$).

Asymptotics.IsLittleO.smul_isBigO theorem

(h₁ : k₁ =o[l] k₂) (h₂ : f' =O[l] g') : (fun x => k₁ x • f' x) =o[l] fun x => k₂ x • g' x

Full source

theorem IsLittleO.smul_isBigO (h₁ : k₁ =o[l] k₂) (h₂ : f' =O[l] g') :
    (fun x => k₁ x • f' x) =o[l] fun x => k₂ x • g' x := by
  simp only [IsLittleO_def] at *
  intro c cpos
  rcases h₂.exists_pos with ⟨c', c'pos, hc'⟩
  exact ((h₁ (div_pos cpos c'pos)).smul hc').congr_const (div_mul_cancel₀ _ (ne_of_gt c'pos))

Little-o of Scalar Product: $k_1 = o(k_2)$ and $f' = O(g')$ implies $k_1 \cdot f' = o(k_2 \cdot g')$

Informal description

Let $k_1, k_2 : \alpha \to E$ and $f', g' : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If $k_1 = o[l] k_2$ and $f' = O[l] g'$, then the function $x \mapsto k_1(x) \cdot f'(x)$ is $o[l]$ of the function $x \mapsto k_2(x) \cdot g'(x)$.

Asymptotics.IsLittleO.smul theorem

(h₁ : k₁ =o[l] k₂) (h₂ : f' =o[l] g') : (fun x => k₁ x • f' x) =o[l] fun x => k₂ x • g' x

Full source

theorem IsLittleO.smul (h₁ : k₁ =o[l] k₂) (h₂ : f' =o[l] g') :
    (fun x => k₁ x • f' x) =o[l] fun x => k₂ x • g' x :=
  h₁.smul_isBigO h₂.isBigO

Little-o of Scalar Product: $k_1 = o(k_2)$ and $f' = o(g')$ implies $k_1 \cdot f' = o(k_2 \cdot g')$

Informal description

Let $k_1, k_2 : \alpha \to E$ and $f', g' : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If $k_1 = o[l] k_2$ and $f' = o[l] g'$, then the function $x \mapsto k_1(x) \cdot f'(x)$ is $o[l]$ of the function $x \mapsto k_2(x) \cdot g'(x)$.

Asymptotics.IsBigO.listProd theorem

 {L : List ι} {f : ι → α → R} {g : ι → α → 𝕜} (hf : ∀ i ∈ L, f i =O[l] g i) :
  (fun x ↦ (L.map (f · x)).prod) =O[l] (fun x ↦ (L.map (g · x)).prod)

Full source

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

Big-O Preservation under List Product: $\prod_{i \in L} f_i(\cdot) =O[l] \prod_{i \in L} g_i(\cdot)$ when $f_i =O[l] g_i$ for all $i \in L$

Informal description

Let $L$ be a list of indices, and let $f_i \colon \alpha \to R$ and $g_i \colon \alpha \to \mathbb{K}$ be functions for each $i \in L$, where $R$ is a seminormed commutative ring and $\mathbb{K}$ is a normed field. If for every $i \in L$, the function $f_i$ is big-O of $g_i$ along a filter $l$ (i.e., $f_i =O[l] g_i$), then the product function $x \mapsto \prod_{i \in L} f_i(x)$ is big-O of the product function $x \mapsto \prod_{i \in L} g_i(x)$ along $l$ (i.e., $\prod_{i \in L} f_i(\cdot) =O[l] \prod_{i \in L} g_i(\cdot)$).

Asymptotics.IsBigO.multisetProd theorem

 {R 𝕜 : Type*} [SeminormedCommRing R] [NormedField 𝕜] {s : Multiset ι} {f : ι → α → R} {g : ι → α → 𝕜}
  (hf : ∀ i ∈ s, f i =O[l] g i) : (fun x ↦ (s.map (f · x)).prod) =O[l] (fun x ↦ (s.map (g · x)).prod)

Full source

theorem IsBigO.multisetProd {R 𝕜 : Type*} [SeminormedCommRing R] [NormedField 𝕜]
    {s : Multiset ι} {f : ι → α → R} {g : ι → α → 𝕜} (hf : ∀ i ∈ s, f i =O[l] g i) :
    (fun x ↦ (s.map (f · x)).prod) =O[l] (fun x ↦ (s.map (g · x)).prod) := by
  obtain ⟨l, rfl⟩ : ∃ l : List ι, ↑l = s := Quotient.mk_surjective s
  exact mod_cast IsBigO.listProd hf

Big-O Preservation under Multiset Product: $\prod_{i \in s} f_i(\cdot) =O[l] \prod_{i \in s} g_i(\cdot)$ when $f_i =O[l] g_i$ for all $i \in s$

Informal description

Let $R$ be a seminormed commutative ring and $\mathbb{K}$ a normed field. Given a multiset $s$ of indices and functions $f_i \colon \alpha \to R$, $g_i \colon \alpha \to \mathbb{K}$ for each $i \in s$, if for every $i \in s$ the function $f_i$ is big-O of $g_i$ along a filter $l$ (i.e., $f_i =O[l] g_i$), then the product function $x \mapsto \prod_{i \in s} f_i(x)$ is big-O of the product function $x \mapsto \prod_{i \in s} g_i(x)$ along $l$ (i.e., $\prod_{i \in s} f_i(\cdot) =O[l] \prod_{i \in s} g_i(\cdot)$).

Asymptotics.IsBigO.finsetProd theorem

 {R 𝕜 : Type*} [SeminormedCommRing R] [NormedField 𝕜] {s : Finset ι} {f : ι → α → R} {g : ι → α → 𝕜}
  (hf : ∀ i ∈ s, f i =O[l] g i) : (∏ i ∈ s, f i ·) =O[l] (∏ i ∈ s, g i ·)

Full source

theorem IsBigO.finsetProd {R 𝕜 : Type*} [SeminormedCommRing R] [NormedField 𝕜]
    {s : Finset ι} {f : ι → α → R} {g : ι → α → 𝕜}
    (hf : ∀ i ∈ s, f i =O[l] g i) : (∏ i ∈ s, f i ·) =O[l] (∏ i ∈ s, g i ·) :=
  .multisetProd hf

Big-O Preservation under Finite Product: $\prod_{i \in s} f_i(\cdot) =O[l] \prod_{i \in s} g_i(\cdot)$ when $f_i =O[l] g_i$ for all $i \in s$

Informal description

Let $R$ be a seminormed commutative ring and $\mathbb{K}$ a normed field. Given a finite set $s$ of indices and functions $f_i \colon \alpha \to R$, $g_i \colon \alpha \to \mathbb{K}$ for each $i \in s$, if for every $i \in s$ the function $f_i$ is big-O of $g_i$ along a filter $l$ (i.e., $f_i =O[l] g_i$), then the product function $x \mapsto \prod_{i \in s} f_i(x)$ is big-O of the product function $x \mapsto \prod_{i \in s} g_i(x)$ along $l$ (i.e., $\prod_{i \in s} f_i(\cdot) =O[l] \prod_{i \in s} g_i(\cdot)$).

Asymptotics.IsLittleO.listProd theorem

 {L : List ι} {f : ι → α → R} {g : ι → α → 𝕜} (h₁ : ∀ i ∈ L, f i =O[l] g i) (h₂ : ∃ i ∈ L, f i =o[l] g i) :
  (fun x ↦ (L.map (f · x)).prod) =o[l] (fun x ↦ (L.map (g · x)).prod)

Full source

theorem IsLittleO.listProd {L : List ι} {f : ι → α → R} {g : ι → α → 𝕜}
    (h₁ : ∀ i ∈ L, f i =O[l] g i) (h₂ : ∃ i ∈ L, f i =o[l] g i) :
    (fun x ↦ (L.map (f · x)).prod) =o[l] (fun x ↦ (L.map (g · x)).prod) := by
  induction L with
  | nil => simp at h₂
  | cons i L ihL =>
    simp only [List.map_cons, List.prod_cons, List.forall_mem_cons, List.exists_mem_cons_iff]
      at h₁ h₂ ⊢
    cases h₂ with
    | inl hi => exact hi.mul_isBigO <| .listProd h₁.2
    | inr hL => exact h₁.1.mul_isLittleO <| ihL h₁.2 hL

Product of Big-O and Little-o Functions in List Form: $\prod_{i \in L} f_i(\cdot) =o[l] \prod_{i \in L} g_i(\cdot)$ when $f_i =O[l] g_i$ for all $i \in L$ and $f_i =o[l] g_i$ for some $i \in L$

Informal description

Let $L$ be a list of indices, and let $f_i \colon \alpha \to R$ and $g_i \colon \alpha \to \mathbb{K}$ be functions for each $i \in L$, where $R$ is a seminormed commutative ring and $\mathbb{K}$ is a normed field. If for every $i \in L$, the function $f_i$ is big-O of $g_i$ along a filter $l$ (i.e., $f_i =O[l] g_i$), and there exists at least one $i \in L$ such that $f_i$ is little-o of $g_i$ along $l$ (i.e., $f_i =o[l] g_i$), then the product function $x \mapsto \prod_{i \in L} f_i(x)$ is little-o of the product function $x \mapsto \prod_{i \in L} g_i(x)$ along $l$ (i.e., $\prod_{i \in L} f_i(\cdot) =o[l] \prod_{i \in L} g_i(\cdot)$).

Asymptotics.IsLittleO.multisetProd theorem

 {R 𝕜 : Type*} [SeminormedCommRing R] [NormedField 𝕜] {s : Multiset ι} {f : ι → α → R} {g : ι → α → 𝕜}
  (h₁ : ∀ i ∈ s, f i =O[l] g i) (h₂ : ∃ i ∈ s, f i =o[l] g i) :
  (fun x ↦ (s.map (f · x)).prod) =o[l] (fun x ↦ (s.map (g · x)).prod)

Full source

theorem IsLittleO.multisetProd {R 𝕜 : Type*} [SeminormedCommRing R] [NormedField 𝕜]
    {s : Multiset ι} {f : ι → α → R} {g : ι → α → 𝕜} (h₁ : ∀ i ∈ s, f i =O[l] g i)
    (h₂ : ∃ i ∈ s, f i =o[l] g i) :
    (fun x ↦ (s.map (f · x)).prod) =o[l] (fun x ↦ (s.map (g · x)).prod) := by
  obtain ⟨l, rfl⟩ : ∃ l : List ι, ↑l = s := Quotient.mk_surjective s
  exact mod_cast IsLittleO.listProd h₁ h₂

Product of Big-O and Little-o Functions in Multiset Form: $\prod_{i \in s} f_i(\cdot) =o[l] \prod_{i \in s} g_i(\cdot)$ when $f_i =O[l] g_i$ for all $i \in s$ and $f_i =o[l] g_i$ for some $i \in s$

Informal description

Let $R$ be a seminormed commutative ring and $\mathbb{K}$ a normed field. Given a multiset $s$ of indices and functions $f_i \colon \alpha \to R$, $g_i \colon \alpha \to \mathbb{K}$ for each $i \in s$, if for every $i \in s$ the function $f_i$ is big-O of $g_i$ along a filter $l$ (i.e., $f_i =O[l] g_i$), and there exists at least one $i \in s$ such that $f_i$ is little-o of $g_i$ along $l$ (i.e., $f_i =o[l] g_i$), then the product function $x \mapsto \prod_{i \in s} f_i(x)$ is little-o of the product function $x \mapsto \prod_{i \in s} g_i(x)$ along $l$ (i.e., $\prod_{i \in s} f_i(\cdot) =o[l] \prod_{i \in s} g_i(\cdot)$).

Asymptotics.IsLittleO.finsetProd theorem

 {R 𝕜 : Type*} [SeminormedCommRing R] [NormedField 𝕜] {s : Finset ι} {f : ι → α → R} {g : ι → α → 𝕜}
  (h₁ : ∀ i ∈ s, f i =O[l] g i) (h₂ : ∃ i ∈ s, f i =o[l] g i) : (∏ i ∈ s, f i ·) =o[l] (∏ i ∈ s, g i ·)

Full source

theorem IsLittleO.finsetProd {R 𝕜 : Type*} [SeminormedCommRing R] [NormedField 𝕜]
    {s : Finset ι} {f : ι → α → R} {g : ι → α → 𝕜} (h₁ : ∀ i ∈ s, f i =O[l] g i)
    (h₂ : ∃ i ∈ s, f i =o[l] g i) : (∏ i ∈ s, f i ·) =o[l] (∏ i ∈ s, g i ·) :=
  .multisetProd h₁ h₂

Product of Big-O and Little-o Functions in Finite Set Form: $\prod_{i \in s} f_i(\cdot) = o[l] \prod_{i \in s} g_i(\cdot)$ when $f_i = O[l] g_i$ for all $i \in s$ and $f_i = o[l] g_i$ for some $i \in s$

Informal description

Let $R$ be a seminormed commutative ring and $\mathbb{K}$ a normed field. Given a finite set $s$ of indices and functions $f_i \colon \alpha \to R$, $g_i \colon \alpha \to \mathbb{K}$ for each $i \in s$, if for every $i \in s$ the function $f_i$ is big-O of $g_i$ along a filter $l$ (i.e., $f_i = O[l] g_i$), and there exists at least one $i \in s$ such that $f_i$ is little-o of $g_i$ along $l$ (i.e., $f_i = o[l] g_i$), then the product function $\prod_{i \in s} f_i(\cdot)$ is little-o of the product function $\prod_{i \in s} g_i(\cdot)$ along $l$ (i.e., $\prod_{i \in s} f_i(\cdot) = o[l] \prod_{i \in s} g_i(\cdot)$).

Asymptotics.IsLittleO.tendsto_div_nhds_zero theorem

{f g : α → 𝕜} (h : f =o[l] g) : Tendsto (fun x => f x / g x) l (𝓝 0)

Full source

theorem IsLittleO.tendsto_div_nhds_zero {f g : α → 𝕜} (h : f =o[l] g) :
    Tendsto (fun x => f x / g x) l (𝓝 0) :=
  (isLittleO_one_iff 𝕜).mp <| by
    calc
      (fun x => f x / g x) =o[l] fun x => g x / g x := by
        simpa only [div_eq_mul_inv] using h.mul_isBigO (isBigO_refl _ _)
      _ =O[l] fun _x => (1 : 𝕜) := isBigO_of_le _ fun x => by simp [div_self_le_one]

Little-o Implies Tendency of Quotient to Zero

Informal description

For functions $f, g \colon \alpha \to \mathbb{K}$ (where $\mathbb{K}$ is a normed field) and a filter $l$ on $\alpha$, if $f = o[l] g$, then the function $x \mapsto f(x)/g(x)$ tends to $0$ along the filter $l$.

Asymptotics.IsLittleO.tendsto_inv_smul_nhds_zero theorem

 [Module 𝕜 E'] [IsBoundedSMul 𝕜 E'] {f : α → E'} {g : α → 𝕜} {l : Filter α} (h : f =o[l] g) :
  Tendsto (fun x => (g x)⁻¹ • f x) l (𝓝 0)

Full source

theorem IsLittleO.tendsto_inv_smul_nhds_zero [Module 𝕜 E'] [IsBoundedSMul 𝕜 E']
    {f : α → E'} {g : α → 𝕜}
    {l : Filter α} (h : f =o[l] g) : Tendsto (fun x => (g x)⁻¹ • f x) l (𝓝 0) := by
  simpa only [div_eq_inv_mul, ← norm_inv, ← norm_smul, ← tendsto_zero_iff_norm_tendsto_zero] using
    h.norm_norm.tendsto_div_nhds_zero

Little-o Implies Tendency of Inverse Scalar Multiplication to Zero

Informal description

Let $\mathbb{K}$ be a normed field and $E'$ be a module over $\mathbb{K}$ with a bounded scalar multiplication. For functions $f \colon \alpha \to E'$ and $g \colon \alpha \to \mathbb{K}$, and a filter $l$ on $\alpha$, if $f = o[l] g$, then the function $x \mapsto (g(x))^{-1} \cdot f(x)$ tends to $0$ along the filter $l$.

Asymptotics.isLittleO_iff_tendsto' theorem

{f g : α → 𝕜} (hgf : ∀ᶠ x in l, g x = 0 → f x = 0) : f =o[l] g ↔ Tendsto (fun x => f x / g x) l (𝓝 0)

Full source

theorem isLittleO_iff_tendsto' {f g : α → 𝕜} (hgf : ∀ᶠ x in l, g x = 0 → f x = 0) :
    f =o[l] gf =o[l] g ↔ Tendsto (fun x => f x / g x) l (𝓝 0) :=
  ⟨IsLittleO.tendsto_div_nhds_zero, fun h =>
    (((isLittleO_one_iff _).mpr h).mul_isBigO (isBigO_refl g l)).congr'
      (hgf.mono fun _x => div_mul_cancel_of_imp) (Eventually.of_forall fun _x => one_mul _)⟩

Characterization of Little-o via Tendency of Quotient to Zero with Eventual Zero Condition

Informal description

Let $f, g \colon \alpha \to \mathbb{K}$ be functions with values in a normed field $\mathbb{K}$, and let $l$ be a filter on $\alpha$. Suppose that for all $x$ in a neighborhood of $l$, if $g(x) = 0$ then $f(x) = 0$. Then $f = o[l] g$ if and only if the function $x \mapsto f(x)/g(x)$ tends to $0$ along the filter $l$. Here, $f = o[l] g$ means that for every $\epsilon > 0$, there exists a neighborhood in $l$ such that for all $x$ in this neighborhood, $\|f(x)\| \leq \epsilon \|g(x)\|$.

Asymptotics.isLittleO_iff_tendsto theorem

{f g : α → 𝕜} (hgf : ∀ x, g x = 0 → f x = 0) : f =o[l] g ↔ Tendsto (fun x => f x / g x) l (𝓝 0)

Full source

theorem isLittleO_iff_tendsto {f g : α → 𝕜} (hgf : ∀ x, g x = 0 → f x = 0) :
    f =o[l] gf =o[l] g ↔ Tendsto (fun x => f x / g x) l (𝓝 0) :=
  isLittleO_iff_tendsto' (Eventually.of_forall hgf)

Characterization of Little-o via Tendency of Quotient to Zero with Pointwise Zero Condition

Informal description

Let $f, g \colon \alpha \to \mathbb{K}$ be functions with values in a normed field $\mathbb{K}$, and let $l$ be a filter on $\alpha$. Suppose that for all $x \in \alpha$, if $g(x) = 0$ then $f(x) = 0$. Then $f = o[l] g$ if and only if the function $x \mapsto f(x)/g(x)$ tends to $0$ along the filter $l$. Here, $f = o[l] g$ means that for every $\epsilon > 0$, there exists a neighborhood in $l$ such that for all $x$ in this neighborhood, $\|f(x)\| \leq \epsilon \|g(x)\|$.

Asymptotics.isLittleO_const_left_of_ne theorem

{c : E''} (hc : c ≠ 0) : (fun _x => c) =o[l] g ↔ Tendsto (fun x => ‖g x‖) l atTop

Full source

theorem isLittleO_const_left_of_ne {c : E''} (hc : c ≠ 0) :
    (fun _x => c) =o[l] g(fun _x => c) =o[l] g ↔ Tendsto (fun x => ‖g x‖) l atTop := by
  simp only [← isLittleO_one_left_iff ℝ]
  exact ⟨(isBigO_const_const (1 : ℝ) hc l).trans_isLittleO,
    (isBigO_const_one ℝ c l).trans_isLittleO⟩

Characterization of $c = o(g)$ via $\|g\| \to \infty$ for nonzero $c$

Informal description

For a nonzero constant $c \in E''$ and a function $g : \alpha \to F''$, the constant function $f(x) = c$ is asymptotically dominated by $g$ (i.e., $f = o[l] g$) if and only if the norm $\|g(x)\|$ tends to infinity along the filter $l$.

Asymptotics.isLittleO_const_left theorem

{c : E''} : (fun _x => c) =o[l] g'' ↔ c = 0 ∨ Tendsto (norm ∘ g'') l atTop

Full source

@[simp]
theorem isLittleO_const_left {c : E''} :
    (fun _x => c) =o[l] g''(fun _x => c) =o[l] g'' ↔ c = 0 ∨ Tendsto (norm ∘ g'') l atTop := by
  rcases eq_or_ne c 0 with (rfl | hc)
  · simp only [isLittleO_zero, eq_self_iff_true, true_or]
  · simp only [hc, false_or, isLittleO_const_left_of_ne hc]; rfl

Characterization of $ c = o[l] g'' $ via $ c = 0 $ or $ \|g''\| \to \infty $

Informal description

For a constant function $ f(x) = c $ (where $ c \in E'' $) and a function $ g'' : \alpha \to F'' $, the relation $ f = o[l] g'' $ holds if and only if either $ c = 0 $ or the norm $ \|g''(x)\| $ tends to infinity along the filter $ l $.

Asymptotics.isLittleO_const_const_iff theorem

[NeBot l] {d : E''} {c : F''} : ((fun _x => d) =o[l] fun _x => c) ↔ d = 0

Full source

@[simp 1001] -- Porting note: increase priority so that this triggers before `isLittleO_const_left`
theorem isLittleO_const_const_iff [NeBot l] {d : E''} {c : F''} :
    ((fun _x => d) =o[l] fun _x => c) ↔ d = 0 := by
  have : ¬Tendsto (Function.const α ‖c‖) l atTop :=
    not_tendsto_atTop_of_tendsto_nhds tendsto_const_nhds
  simp only [isLittleO_const_left, or_iff_left_iff_imp]
  exact fun h => (this h).elim

Characterization of Little-o for Constant Functions: $d = o[l] c \leftrightarrow d = 0$

Informal description

Let $l$ be a non-trivial filter on a type $\alpha$, and let $d \in E''$ and $c \in F''$ be constants. The asymptotic relation $d = o[l] c$ holds if and only if $d = 0$.

Asymptotics.isLittleO_pure theorem

{x} : f'' =o[pure x] g'' ↔ f'' x = 0

Full source

@[simp]
theorem isLittleO_pure {x} : f'' =o[pure x] g''f'' =o[pure x] g'' ↔ f'' x = 0 :=
  calc
    f'' =o[pure x] g'' ↔ (fun _y : α => f'' x) =o[pure x] fun _ => g'' x := isLittleO_congr rfl rfl
    _ ↔ f'' x = 0 := isLittleO_const_const_iff

Little-o Relation at a Point: $f'' = o[\text{pure }x] g'' \leftrightarrow f''(x) = 0$

Informal description

For functions $f'' : \alpha \to E''$ and $g'' : \alpha \to F''$ and a point $x \in \alpha$, the relation $f'' = o[\text{pure }x] g''$ holds if and only if $f''(x) = 0$. Here, $\text{pure }x$ denotes the filter of neighborhoods of $x$.

Asymptotics.isLittleO_const_id_cobounded theorem

(c : F'') : (fun _ => c) =o[Bornology.cobounded E''] id

Full source

theorem isLittleO_const_id_cobounded (c : F'') :
    (fun _ => c) =o[Bornology.cobounded E''] id :=
  isLittleO_const_left.2 <| .inr tendsto_norm_cobounded_atTop

Constant Function is Little-o of Identity with Respect to Cobounded Filter

Informal description

For any constant function $ f(x) = c $ (where $ c \in F'' $) and the identity function $ \text{id} : E'' \to E'' $, the relation $ f = o[\text{cobounded } E''] \text{id} $ holds. Here, $\text{cobounded } E''$ denotes the filter of cobounded sets in the bornology of $ E'' $.

Asymptotics.isLittleO_const_id_atTop theorem

(c : E'') : (fun _x : ℝ => c) =o[atTop] id

Full source

theorem isLittleO_const_id_atTop (c : E'') : (fun _x : ℝ => c) =o[atTop] id :=
  isLittleO_const_left.2 <| Or.inr tendsto_abs_atTop_atTop

Constant function is little-o of identity at infinity ($c = o(x)$ as $x \to \infty$)

Informal description

For any constant function $f(x) = c$ (where $c \in E''$) and the identity function $\mathrm{id}(x) = x$ on the real numbers, the relation $f = o(\mathrm{id})$ holds as $x \to \infty$.

Asymptotics.isLittleO_const_id_atBot theorem

(c : E'') : (fun _x : ℝ => c) =o[atBot] id

Full source

theorem isLittleO_const_id_atBot (c : E'') : (fun _x : ℝ => c) =o[atBot] id :=
  isLittleO_const_left.2 <| Or.inr tendsto_abs_atBot_atTop

Constant function is little-o of identity at negative infinity ($f(x) = c = o(x)$ as $x \to -\infty$)

Informal description

For any constant function $f(x) = c$ (where $c \in E''$) and the identity function $\mathrm{id}(x) = x$ on the real numbers, the relation $f = o(\mathrm{id})$ holds as $x \to -\infty$. This means that for any positive real number $\varepsilon > 0$, there exists a real number $M$ such that for all $x < M$, we have $\|c\| \leq \varepsilon \|x\|$.

Asymptotics.isBigOWith_of_eq_mul theorem

{u v : α → R} (φ : α → R) (hφ : ∀ᶠ x in l, ‖φ x‖ ≤ c) (h : u =ᶠ[l] φ * v) : IsBigOWith c l u v

Full source

/-- If `‖φ‖` is eventually bounded by `c`, and `u =ᶠ[l] φ * v`, then we have `IsBigOWith c u v l`.
    This does not require any assumptions on `c`, which is why we keep this version along with
    `IsBigOWith_iff_exists_eq_mul`. -/
theorem isBigOWith_of_eq_mul {u v : α → R} (φ : α → R) (hφ : ∀ᶠ x in l, ‖φ x‖ ≤ c)
    (h : u =ᶠ[l] φ * v) :
    IsBigOWith c l u v := by
  simp only [IsBigOWith_def]
  refine h.symm.rw (fun x a => ‖a‖ ≤ c * ‖v x‖) (hφ.mono fun x hx => ?_)
  simp only [Pi.mul_apply]
  refine (norm_mul_le _ _).trans ?_
  gcongr

Asymptotic Bound via Pointwise Multiplication: $\|\varphi\| \leq c$ and $u = \varphi \cdot v$ implies $u = O_c(v)$

Informal description

Let $R$ be a seminormed ring, $\alpha$ a type, and $l$ a filter on $\alpha$. Given functions $u, v : \alpha \to R$ and $\varphi : \alpha \to R$, if $\|\varphi(x)\|$ is eventually bounded by $c$ in the filter $l$ (i.e., $\forallᶠ x \text{ in } l, \|\varphi(x)\| \leq c$) and $u$ is eventually equal to $\varphi \cdot v$ in $l$ (i.e., $u =ᶠ[l] \varphi \cdot v$), then $u$ is asymptotically bounded by $v$ with constant $c$ in the filter $l$ (i.e., $\text{IsBigOWith}(c, l, u, v)$).

Asymptotics.isBigOWith_iff_exists_eq_mul theorem

(hc : 0 ≤ c) : IsBigOWith c l u v ↔ ∃ φ : α → 𝕜, (∀ᶠ x in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v

Full source

theorem isBigOWith_iff_exists_eq_mul (hc : 0 ≤ c) :
    IsBigOWithIsBigOWith c l u v ↔ ∃ φ : α → 𝕜, (∀ᶠ x in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v := by
  constructor
  · intro h
    use fun x => u x / v x
    refine ⟨Eventually.mono h.bound fun y hy => ?_, h.eventually_mul_div_cancel.symm⟩
    simpa using div_le_of_le_mul₀ (norm_nonneg _) hc hy
  · rintro ⟨φ, hφ, h⟩
    exact isBigOWith_of_eq_mul φ hφ h

Characterization of Big-O Bound via Pointwise Multiplication: $\text{IsBigOWith}(c, l, u, v) \leftrightarrow \exists \varphi, (\|\varphi\| \leq c) \land (u = \varphi \cdot v)$

Informal description

For any nonnegative real number $c \geq 0$, the relation $\text{IsBigOWith}(c, l, u, v)$ holds if and only if there exists a function $\varphi : \alpha \to \mathbb{K}$ such that $\|\varphi(x)\|$ is eventually bounded by $c$ along the filter $l$ and $u$ is eventually equal to $\varphi \cdot v$ along $l$. In other words, $u$ is asymptotically bounded by $v$ with constant $c$ if and only if $u$ can be expressed as $\varphi \cdot v$ with $\|\varphi\|$ eventually bounded by $c$.

Asymptotics.IsBigOWith.exists_eq_mul theorem

(h : IsBigOWith c l u v) (hc : 0 ≤ c) : ∃ φ : α → 𝕜, (∀ᶠ x in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v

Full source

theorem IsBigOWith.exists_eq_mul (h : IsBigOWith c l u v) (hc : 0 ≤ c) :
    ∃ φ : α → 𝕜, (∀ᶠ x in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v :=
  (isBigOWith_iff_exists_eq_mul hc).mp h

Existence of Multiplicative Representation for Big-O Bound

Informal description

Let $c \geq 0$ be a nonnegative real number, and suppose that $u$ is asymptotically bounded by $v$ with constant $c$ along the filter $l$ (i.e., $\text{IsBigOWith}(c, l, u, v)$ holds). Then there exists a function $\varphi : \alpha \to \mathbb{K}$ such that $\|\varphi(x)\|$ is eventually bounded by $c$ along $l$ and $u$ is eventually equal to $\varphi \cdot v$ along $l$.

Asymptotics.isBigO_iff_exists_eq_mul theorem

: u =O[l] v ↔ ∃ φ : α → 𝕜, l.IsBoundedUnder (· ≤ ·) (norm ∘ φ) ∧ u =ᶠ[l] φ * v

Full source

theorem isBigO_iff_exists_eq_mul :
    u =O[l] vu =O[l] v ↔ ∃ φ : α → 𝕜, l.IsBoundedUnder (· ≤ ·) (norm ∘ φ) ∧ u =ᶠ[l] φ * v := by
  constructor
  · rintro h
    rcases h.exists_nonneg with ⟨c, hnnc, hc⟩
    rcases hc.exists_eq_mul hnnc with ⟨φ, hφ, huvφ⟩
    exact ⟨φ, ⟨c, hφ⟩, huvφ⟩
  · rintro ⟨φ, ⟨c, hφ⟩, huvφ⟩
    exact isBigO_iff_isBigOWith.2 ⟨c, isBigOWith_of_eq_mul φ hφ huvφ⟩

Characterization of Big-O via Bounded Multiplicative Representation

Informal description

Let $u, v : \alpha \to \mathbb{K}$ be functions and $l$ a filter on $\alpha$. Then $u = O[l] v$ if and only if there exists a function $\varphi : \alpha \to \mathbb{K}$ such that: 1. The norm $\|\varphi(x)\|$ is bounded under $l$ (i.e., $\exists C > 0, \forall^l x, \|\varphi(x)\| \leq C$), and 2. $u$ is eventually equal to $\varphi \cdot v$ along $l$ (i.e., $\forall^l x, u(x) = \varphi(x) \cdot v(x)$).

Asymptotics.isLittleO_iff_exists_eq_mul theorem

: u =o[l] v ↔ ∃ φ : α → 𝕜, Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v

Full source

theorem isLittleO_iff_exists_eq_mul :
    u =o[l] vu =o[l] v ↔ ∃ φ : α → 𝕜, Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v := by
  constructor
  · exact fun h => ⟨fun x => u x / v x, h.tendsto_div_nhds_zero, h.eventually_mul_div_cancel.symm⟩
  · simp only [IsLittleO_def]
    rintro ⟨φ, hφ, huvφ⟩ c hpos
    rw [NormedAddCommGroup.tendsto_nhds_zero] at hφ
    exact isBigOWith_of_eq_mul _ ((hφ c hpos).mono fun x => le_of_lt) huvφ

Characterization of Little-o via Vanishing Multiplicative Representation

Informal description

Let $\mathbb{K}$ be a normed field, $\alpha$ a type, and $l$ a filter on $\alpha$. For functions $u, v \colon \alpha \to \mathbb{K}$, the relation $u = o[l] v$ holds if and only if there exists a function $\varphi \colon \alpha \to \mathbb{K}$ such that: 1. $\varphi$ tends to $0$ along $l$ (i.e., $\lim_{x \to l} \varphi(x) = 0$), and 2. $u$ is eventually equal to $\varphi \cdot v$ along $l$ (i.e., $u(x) = \varphi(x) \cdot v(x)$ for all $x$ in some neighborhood in $l$).

Asymptotics.div_isBoundedUnder_of_isBigO theorem

 {α : Type*} {l : Filter α} {f g : α → 𝕜} (h : f =O[l] g) : IsBoundedUnder (· ≤ ·) l fun x => ‖f x / g x‖

Full source

theorem div_isBoundedUnder_of_isBigO {α : Type*} {l : Filter α} {f g : α → 𝕜} (h : f =O[l] g) :
    IsBoundedUnder (· ≤ ·) l fun x => ‖f x / g x‖ := by
  obtain ⟨c, h₀, hc⟩ := h.exists_nonneg
  refine ⟨c, eventually_map.2 (hc.bound.mono fun x hx => ?_)⟩
  rw [norm_div]
  exact div_le_of_le_mul₀ (norm_nonneg _) h₀ hx

Boundedness of $\|f/g\|$ under Big-O condition

Informal description

For any functions $f, g \colon \alpha \to \mathbb{K}$ (where $\mathbb{K}$ is a normed field) and any filter $l$ on $\alpha$, if $f$ is big O of $g$ along $l$ (i.e., $f = O(g)$ as $x \to l$), then the function $\|f(x)/g(x)\|$ is bounded above along $l$.

Asymptotics.isBigO_iff_div_isBoundedUnder theorem

 {α : Type*} {l : Filter α} {f g : α → 𝕜} (hgf : ∀ᶠ x in l, g x = 0 → f x = 0) :
  f =O[l] g ↔ IsBoundedUnder (· ≤ ·) l fun x => ‖f x / g x‖

Full source

theorem isBigO_iff_div_isBoundedUnder {α : Type*} {l : Filter α} {f g : α → 𝕜}
    (hgf : ∀ᶠ x in l, g x = 0 → f x = 0) :
    f =O[l] gf =O[l] g ↔ IsBoundedUnder (· ≤ ·) l fun x => ‖f x / g x‖ := by
  refine ⟨div_isBoundedUnder_of_isBigO, fun h => ?_⟩
  obtain ⟨c, hc⟩ := h
  simp only [eventually_map, norm_div] at hc
  refine IsBigO.of_bound c (hc.mp <| hgf.mono fun x hx₁ hx₂ => ?_)
  by_cases hgx : g x = 0
  · simp [hx₁ hgx, hgx]
  · exact (div_le_iff₀ (norm_pos_iff.2 hgx)).mp hx₂

Big-O condition via boundedness of $\|f/g\|$ under filter convergence

Informal description

Let $f, g \colon \alpha \to \mathbb{K}$ be functions valued in a normed field $\mathbb{K}$, and let $l$ be a filter on $\alpha$. Suppose that for all $x$ in a neighborhood determined by $l$, $g(x) = 0$ implies $f(x) = 0$. Then $f$ is big O of $g$ along $l$ (i.e., $f = O(g)$ as $x \to l$) if and only if the function $\|f(x)/g(x)\|$ is bounded above along $l$.

Asymptotics.isBigO_of_div_tendsto_nhds theorem

 {α : Type*} {l : Filter α} {f g : α → 𝕜} (hgf : ∀ᶠ x in l, g x = 0 → f x = 0) (c : 𝕜)
  (H : Filter.Tendsto (f / g) l (𝓝 c)) : f =O[l] g

Full source

theorem isBigO_of_div_tendsto_nhds {α : Type*} {l : Filter α} {f g : α → 𝕜}
    (hgf : ∀ᶠ x in l, g x = 0 → f x = 0) (c : 𝕜) (H : Filter.Tendsto (f / g) l (𝓝 c)) :
    f =O[l] g :=
  (isBigO_iff_div_isBoundedUnder hgf).2 <| H.norm.isBoundedUnder_le

Big-O condition via ratio convergence to a limit

Informal description

Let $\alpha$ be a type, $l$ a filter on $\alpha$, and $f, g \colon \alpha \to \mathbb{K}$ functions valued in a normed field $\mathbb{K}$. Suppose that for all $x$ in a neighborhood determined by $l$, $g(x) = 0$ implies $f(x) = 0$. If the ratio $f/g$ tends to a limit $c \in \mathbb{K}$ along $l$, then $f$ is big O of $g$ along $l$, i.e., $f = O(g)$ as $x \to l$.

Asymptotics.IsLittleO.tendsto_zero_of_tendsto theorem

 {α E 𝕜 : Type*} [NormedAddCommGroup E] [NormedField 𝕜] {u : α → E} {v : α → 𝕜} {l : Filter α} {y : 𝕜} (huv : u =o[l] v)
  (hv : Tendsto v l (𝓝 y)) : Tendsto u l (𝓝 0)

Full source

theorem IsLittleO.tendsto_zero_of_tendsto {α E 𝕜 : Type*} [NormedAddCommGroup E] [NormedField 𝕜]
    {u : α → E} {v : α → 𝕜} {l : Filter α} {y : 𝕜} (huv : u =o[l] v) (hv : Tendsto v l (𝓝 y)) :
    Tendsto u l (𝓝 0) := by
  suffices h : u =o[l] fun _x => (1 : 𝕜) by
    rwa [isLittleO_one_iff] at h
  exact huv.trans_isBigO (hv.isBigO_one 𝕜)

Little-o Implies Tendency to Zero under Convergence of Dominant Function

Informal description

Let $E$ be a normed additive commutative group, $\mathbb{k}$ a normed field, and $l$ a filter on a type $\alpha$. For functions $u : \alpha \to E$ and $v : \alpha \to \mathbb{k}$, if $u$ is little-o of $v$ with respect to $l$ (i.e., $u = o[l] v$) and $v$ tends to $y \in \mathbb{k}$ along $l$, then $u$ tends to $0$ along $l$.

Asymptotics.isLittleO_pow_pow theorem

{m n : ℕ} (h : m < n) : (fun x : 𝕜 => x ^ n) =o[𝓝 0] fun x => x ^ m

Full source

theorem isLittleO_pow_pow {m n : ℕ} (h : m < n) : (fun x : 𝕜 => x ^ n) =o[𝓝 0] fun x => x ^ m := by
  rcases lt_iff_exists_add.1 h with ⟨p, hp0 : 0 < p, rfl⟩
  suffices (fun x : 𝕜 => x ^ m * x ^ p) =o[𝓝 0] fun x => x ^ m * 1 ^ p by
    simpa only [pow_add, one_pow, mul_one]
  exact IsBigO.mul_isLittleO (isBigO_refl _ _)
    (IsLittleO.pow ((isLittleO_one_iff _).2 tendsto_id) hp0)

Little-o relation for powers: $x^n = o(x^m)$ as $x \to 0$ when $m < n$

Informal description

For any natural numbers $m$ and $n$ such that $m < n$, the function $x \mapsto x^n$ is little-o of the function $x \mapsto x^m$ as $x$ tends to $0$ in a normed field $\mathbb{k}$. That is, $x^n = o(x^m)$ as $x \to 0$.

Asymptotics.isLittleO_norm_pow_norm_pow theorem

{m n : ℕ} (h : m < n) : (fun x : E' => ‖x‖ ^ n) =o[𝓝 0] fun x => ‖x‖ ^ m

Full source

theorem isLittleO_norm_pow_norm_pow {m n : ℕ} (h : m < n) :
    (fun x : E' => ‖x‖ ^ n) =o[𝓝 0] fun x => ‖x‖ ^ m :=
  (isLittleO_pow_pow h).comp_tendsto tendsto_norm_zero

Little-o relation for norms of powers: $\|x\|^n = o(\|x\|^m)$ as $x \to 0$ when $m < n$

Informal description

For any natural numbers $m$ and $n$ with $m < n$, the function $x \mapsto \|x\|^n$ is little-o of the function $x \mapsto \|x\|^m$ as $x$ tends to $0$ in a seminormed additive commutative group $E'$. That is, $\|x\|^n = o(\|x\|^m)$ as $x \to 0$.

Asymptotics.isLittleO_pow_id theorem

{n : ℕ} (h : 1 < n) : (fun x : 𝕜 => x ^ n) =o[𝓝 0] fun x => x

Full source

theorem isLittleO_pow_id {n : ℕ} (h : 1 < n) : (fun x : 𝕜 => x ^ n) =o[𝓝 0] fun x => x := by
  convert isLittleO_pow_pow h (𝕜 := 𝕜)
  simp only [pow_one]

Little-o relation for powers: $x^n = o(x)$ as $x \to 0$ when $n > 1$

Informal description

For any natural number $n > 1$, the function $x \mapsto x^n$ is little-o of the identity function $x \mapsto x$ as $x$ tends to $0$ in a normed division ring $\mathbb{k}$. That is, $x^n = o(x)$ as $x \to 0$.

Asymptotics.isLittleO_norm_pow_id theorem

{n : ℕ} (h : 1 < n) : (fun x : E' => ‖x‖ ^ n) =o[𝓝 0] fun x => x

Full source

theorem isLittleO_norm_pow_id {n : ℕ} (h : 1 < n) :
    (fun x : E' => ‖x‖ ^ n) =o[𝓝 0] fun x => x := by
  have := @isLittleO_norm_pow_norm_pow E' _ _ _ h
  simp only [pow_one] at this
  exact isLittleO_norm_right.mp this

Little-o relation for norms of powers: $\|x\|^n = o(x)$ as $x \to 0$ when $n > 1$

Informal description

For any natural number $n > 1$, the function $x \mapsto \|x\|^n$ is little-o of the identity function $x \mapsto x$ as $x$ tends to $0$ in a seminormed additive commutative group $E'$. That is, $\|x\|^n = o(x)$ as $x \to 0$.

Asymptotics.isLittleO_pow_sub_pow_sub theorem

(x₀ : E') {n m : ℕ} (h : n < m) : (fun x => ‖x - x₀‖ ^ m) =o[𝓝 x₀] fun x => ‖x - x₀‖ ^ n

Full source

theorem isLittleO_pow_sub_pow_sub (x₀ : E') {n m : ℕ} (h : n < m) :
    (fun x => ‖x - x₀‖ ^ m) =o[𝓝 x₀] fun x => ‖x - x₀‖ ^ n :=
  haveI : Tendsto (fun x => ‖x - x₀‖) (𝓝 x₀) (𝓝 0) := by
    apply tendsto_norm_zero.comp
    rw [← sub_self x₀]
    exact tendsto_id.sub tendsto_const_nhds
  (isLittleO_pow_pow h).comp_tendsto this

Little-o relation for powers of distance: $\|x - x_0\|^m = o(\|x - x_0\|^n)$ as $x \to x_0$ when $n < m$

Informal description

Let $E'$ be a seminormed additive commutative group, $x_0 \in E'$, and $n, m \in \mathbb{N}$ with $n < m$. Then the function $x \mapsto \|x - x_0\|^m$ is little-o of the function $x \mapsto \|x - x_0\|^n$ as $x$ tends to $x_0$ in the neighborhood filter of $x_0$. That is, $\|x - x_0\|^m = o(\|x - x_0\|^n)$ as $x \to x_0$.

Asymptotics.isLittleO_pow_sub_sub theorem

(x₀ : E') {m : ℕ} (h : 1 < m) : (fun x => ‖x - x₀‖ ^ m) =o[𝓝 x₀] fun x => x - x₀

Full source

theorem isLittleO_pow_sub_sub (x₀ : E') {m : ℕ} (h : 1 < m) :
    (fun x => ‖x - x₀‖ ^ m) =o[𝓝 x₀] fun x => x - x₀ := by
  simpa only [isLittleO_norm_right, pow_one] using isLittleO_pow_sub_pow_sub x₀ h

Little-o relation for higher powers of distance: $\|x - x_0\|^m = o(x - x_0)$ as $x \to x_0$ when $m > 1$

Informal description

Let $E'$ be a seminormed additive commutative group, $x_0 \in E'$, and $m \in \mathbb{N}$ with $1 < m$. Then the function $x \mapsto \|x - x_0\|^m$ is little-o of the function $x \mapsto x - x_0$ as $x$ tends to $x_0$ in the neighborhood filter of $x_0$. That is, $\|x - x_0\|^m = o(x - x_0)$ as $x \to x_0$.

Asymptotics.IsBigOWith.right_le_sub_of_lt_one theorem

 {f₁ f₂ : α → E'} (h : IsBigOWith c l f₁ f₂) (hc : c < 1) : IsBigOWith (1 / (1 - c)) l f₂ fun x => f₂ x - f₁ x

Full source

theorem IsBigOWith.right_le_sub_of_lt_one {f₁ f₂ : α → E'} (h : IsBigOWith c l f₁ f₂) (hc : c < 1) :
    IsBigOWith (1 / (1 - c)) l f₂ fun x => f₂ x - f₁ x :=
  IsBigOWith.of_bound <|
    mem_of_superset h.bound fun x hx => by
      simp only [mem_setOf_eq] at hx ⊢
      rw [mul_comm, one_div, ← div_eq_mul_inv, le_div_iff₀, mul_sub, mul_one, mul_comm]
      · exact le_trans (sub_le_sub_left hx _) (norm_sub_norm_le _ _)
      · exact sub_pos.2 hc

Big-O bound for $f₂$ in terms of $f₂ - f₁$ when $f₁ = O_c(f₂)$ with $c < 1$

Informal description

Let $f₁, f₂ : α → E'$ be functions and $l$ be a filter on $α$. If there exists a constant $c < 1$ such that $\|f₁(x)\| ≤ c \|f₂(x)\|$ for all $x$ in $l$ eventually, then $\|f₂(x)\| ≤ \frac{1}{1-c} \|f₂(x) - f₁(x)\|$ holds for all $x$ in $l$ eventually.

Asymptotics.IsBigOWith.right_le_add_of_lt_one theorem

 {f₁ f₂ : α → E'} (h : IsBigOWith c l f₁ f₂) (hc : c < 1) : IsBigOWith (1 / (1 - c)) l f₂ fun x => f₁ x + f₂ x

Full source

theorem IsBigOWith.right_le_add_of_lt_one {f₁ f₂ : α → E'} (h : IsBigOWith c l f₁ f₂) (hc : c < 1) :
    IsBigOWith (1 / (1 - c)) l f₂ fun x => f₁ x + f₂ x :=
  (h.neg_right.right_le_sub_of_lt_one hc).neg_right.of_neg_left.congr rfl (fun _ ↦ rfl) fun x ↦ by
    rw [neg_sub, sub_neg_eq_add]

Big-O bound for $f₂$ in terms of $f₁ + f₂$ when $f₁ = O_c(f₂)$ with $c < 1$

Informal description

Let $f₁, f₂ : α → E'$ be functions and $l$ be a filter on $α$. If there exists a constant $c < 1$ such that $\|f₁(x)\| ≤ c \|f₂(x)\|$ for all $x$ in $l$ eventually, then $\|f₂(x)\| ≤ \frac{1}{1-c} \|f₁(x) + f₂(x)\|$ holds for all $x$ in $l$ eventually.

Asymptotics.IsLittleO.right_isBigO_sub theorem

{f₁ f₂ : α → E'} (h : f₁ =o[l] f₂) : f₂ =O[l] fun x => f₂ x - f₁ x

Full source

theorem IsLittleO.right_isBigO_sub {f₁ f₂ : α → E'} (h : f₁ =o[l] f₂) :
    f₂ =O[l] fun x => f₂ x - f₁ x :=
  ((h.def' one_half_pos).right_le_sub_of_lt_one one_half_lt_one).isBigO

Big-O relation between $f₂$ and $f₂ - f₁$ under little-o condition

Informal description

Let $f₁, f₂ : \alpha \to E'$ be functions between seminormed additive commutative groups, and let $l$ be a filter on $\alpha$. If $f₁$ is little-o of $f₂$ along $l$, then $f₂$ is big-O of the function $x \mapsto f₂(x) - f₁(x)$ along $l$.

Asymptotics.IsLittleO.right_isBigO_add theorem

{f₁ f₂ : α → E'} (h : f₁ =o[l] f₂) : f₂ =O[l] fun x => f₁ x + f₂ x

Full source

theorem IsLittleO.right_isBigO_add {f₁ f₂ : α → E'} (h : f₁ =o[l] f₂) :
    f₂ =O[l] fun x => f₁ x + f₂ x :=
  ((h.def' one_half_pos).right_le_add_of_lt_one one_half_lt_one).isBigO

Big-O relation between $f₂$ and $f₁ + f₂$ under little-o condition

Informal description

Let $f₁, f₂ : \alpha \to E'$ be functions between seminormed additive commutative groups, and let $l$ be a filter on $\alpha$. If $f₁ = o[l] f₂$, then $f₂ = O[l] (f₁ + f₂)$.

Asymptotics.IsLittleO.right_isBigO_add' theorem

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

Full source

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

Big-O relation between $f_2$ and $f_2 + f_1$ under little-o condition

Informal description

Let $f_1, f_2 : \alpha \to E'$ be functions from a type $\alpha$ to a seminormed additive commutative group $E'$, and let $l$ be a filter on $\alpha$. If $f_1$ is little-o of $f_2$ along $l$ (i.e., $f_1 = o[l] f_2$), then $f_2$ is big-O of $f_2 + f_1$ along $l$ (i.e., $f_2 = O[l] (f_2 + f_1)$).

Asymptotics.bound_of_isBigO_cofinite theorem

(h : f =O[cofinite] g'') : ∃ C > 0, ∀ ⦃x⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖

Full source

/-- If `f x = O(g x)` along `cofinite`, then there exists a positive constant `C` such that
`‖f x‖ ≤ C * ‖g x‖` whenever `g x ≠ 0`. -/
theorem bound_of_isBigO_cofinite (h : f =O[cofinite] g'') :
    ∃ C > 0, ∀ ⦃x⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖ := by
  rcases h.exists_pos with ⟨C, C₀, hC⟩
  rw [IsBigOWith_def, eventually_cofinite] at hC
  rcases (hC.toFinset.image fun x => ‖f x‖ / ‖g'' x‖).exists_le with ⟨C', hC'⟩
  have : ∀ x, C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ / ‖g'' x‖ ≤ C' := by simpa using hC'
  refine ⟨max C C', lt_max_iff.2 (Or.inl C₀), fun x h₀ => ?_⟩
  rw [max_mul_of_nonneg _ _ (norm_nonneg _), le_max_iff, or_iff_not_imp_left, not_le]
  exact fun hx => (div_le_iff₀ (norm_pos_iff.2 h₀)).1 (this _ hx)

Existence of Constant for Big-O Relation Along Cofinite Filter

Informal description

If $f = O(g)$ along the cofinite filter, then there exists a positive constant $C > 0$ such that for all $x$ with $g(x) \neq 0$, the inequality $\|f(x)\| \leq C \|g(x)\|$ holds.

Asymptotics.isBigO_cofinite_iff theorem

(h : ∀ x, g'' x = 0 → f'' x = 0) : f'' =O[cofinite] g'' ↔ ∃ C, ∀ x, ‖f'' x‖ ≤ C * ‖g'' x‖

Full source

theorem isBigO_cofinite_iff (h : ∀ x, g'' x = 0 → f'' x = 0) :
    f'' =O[cofinite] g''f'' =O[cofinite] g'' ↔ ∃ C, ∀ x, ‖f'' x‖ ≤ C * ‖g'' x‖ := by
  classical
  exact ⟨fun h' =>
    let ⟨C, _C₀, hC⟩ := bound_of_isBigO_cofinite h'
    ⟨C, fun x => if hx : g'' x = 0 then by simp [h _ hx, hx] else hC hx⟩,
    fun h => (isBigO_top.2 h).mono le_top⟩

Big-O Criterion Along Cofinite Filter: $f = O(g) \leftrightarrow \exists C, \forall x, \|f(x)\| \leq C \|g(x)\|$

Informal description

For functions $f''$ and $g''$ from a type $\alpha$ to normed spaces, if $g''(x) = 0$ implies $f''(x) = 0$ for all $x$, then $f''$ is big-O of $g''$ along the cofinite filter if and only if there exists a constant $C$ such that for all $x$, $\|f''(x)\| \leq C \|g''(x)\|$.

Asymptotics.bound_of_isBigO_nat_atTop theorem

 {f : ℕ → E} {g'' : ℕ → E''} (h : f =O[atTop] g'') : ∃ C > 0, ∀ ⦃x⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖

Full source

theorem bound_of_isBigO_nat_atTop {f : ℕ → E} {g'' : ℕ → E''} (h : f =O[atTop] g'') :
    ∃ C > 0, ∀ ⦃x⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖ :=
  bound_of_isBigO_cofinite <| by rwa [Nat.cofinite_eq_atTop]

Existence of Constant for Big-O Relation Along Natural Number Sequence at Infinity

Informal description

For sequences $f : \mathbb{N} \to E$ and $g : \mathbb{N} \to E''$ of elements in normed additive commutative groups, if $f = O(g)$ as $n \to \infty$ (i.e., along the `atTop` filter on $\mathbb{N}$), then there exists a positive constant $C > 0$ such that for all $x \in \mathbb{N}$ with $g(x) \neq 0$, the inequality $\|f(x)\| \leq C \|g(x)\|$ holds.

Asymptotics.isBigO_nat_atTop_iff theorem

 {f : ℕ → E''} {g : ℕ → F''} (h : ∀ x, g x = 0 → f x = 0) : f =O[atTop] g ↔ ∃ C, ∀ x, ‖f x‖ ≤ C * ‖g x‖

Full source

theorem isBigO_nat_atTop_iff {f : ℕ → E''} {g : ℕ → F''} (h : ∀ x, g x = 0 → f x = 0) :
    f =O[atTop] gf =O[atTop] g ↔ ∃ C, ∀ x, ‖f x‖ ≤ C * ‖g x‖ := by
  rw [← Nat.cofinite_eq_atTop, isBigO_cofinite_iff h]

Big-O Criterion for Sequences at Infinity: $f = O(g) \leftrightarrow \exists C, \forall x, \|f(x)\| \leq C \|g(x)\|$

Informal description

For sequences $f \colon \mathbb{N} \to E''$ and $g \colon \mathbb{N} \to F''$ in normed spaces, if $g(x) = 0$ implies $f(x) = 0$ for all $x \in \mathbb{N}$, then $f$ is big-O of $g$ as $n \to \infty$ (i.e., along the `atTop` filter on $\mathbb{N}$) if and only if there exists a constant $C > 0$ such that $\|f(x)\| \leq C \|g(x)\|$ for all $x \in \mathbb{N}$.

Asymptotics.isBigO_one_nat_atTop_iff theorem

{f : ℕ → E''} : f =O[atTop] (fun _n => 1 : ℕ → ℝ) ↔ ∃ C, ∀ n, ‖f n‖ ≤ C

Full source

theorem isBigO_one_nat_atTop_iff {f : ℕ → E''} :
    f =O[atTop] (fun _n => 1 : ℕ → ℝ)f =O[atTop] (fun _n => 1 : ℕ → ℝ) ↔ ∃ C, ∀ n, ‖f n‖ ≤ C :=
  Iff.trans (isBigO_nat_atTop_iff fun _ h => (one_ne_zero h).elim) <| by
    simp only [norm_one, mul_one]

Big-O Criterion for Bounded Sequences: $f = O(1) \leftrightarrow \exists C, \forall n, \|f(n)\| \leq C$

Informal description

For a sequence $f \colon \mathbb{N} \to E''$ in a normed space, $f$ is big-O of the constant sequence $1$ as $n \to \infty$ (i.e., $f = O(1)$ along the `atTop` filter on $\mathbb{N}$) if and only if there exists a constant $C > 0$ such that $\|f(n)\| \leq C$ for all $n \in \mathbb{N}$.

Asymptotics.IsBigO.nat_of_atTop theorem

 {f : ℕ → E''} {g : ℕ → F''} (hfg : f =O[atTop] g) {l : Filter ℕ} (h : ∀ᶠ n in l, g n = 0 → f n = 0) : f =O[l] g

Full source

theorem IsBigO.nat_of_atTop {f : ℕ → E''} {g : ℕ → F''} (hfg : f =O[atTop] g)
    {l : Filter ℕ} (h : ∀ᶠ n in l, g n = 0 → f n = 0) : f =O[l] g := by
  obtain ⟨C, hC_pos, hC⟩ := bound_of_isBigO_nat_atTop hfg
  refine isBigO_iff.mpr ⟨C, ?_⟩
  filter_upwards [h] with x h
  by_cases hf : f x = 0
  · simp [hf, hC_pos]
  exact hC fun a ↦ hf (h a)

Big-O Relation Preserved Under Filter Restriction for Sequences

Informal description

Let $f : \mathbb{N} \to E''$ and $g : \mathbb{N} \to F''$ be sequences in normed additive commutative groups. If $f = O(g)$ as $n \to \infty$ (i.e., along the `atTop` filter on $\mathbb{N}$), and if for all sufficiently large $n$ in the filter $l$ on $\mathbb{N}$ we have that $g(n) = 0$ implies $f(n) = 0$, then $f = O(g)$ along the filter $l$.

Asymptotics.isBigOWith_pi theorem

 {ι : Type*} [Fintype ι] {E' : ι → Type*} [∀ i, NormedAddCommGroup (E' i)] {f : α → ∀ i, E' i} {C : ℝ} (hC : 0 ≤ C) :
  IsBigOWith C l f g' ↔ ∀ i, IsBigOWith C l (fun x => f x i) g'

Full source

theorem isBigOWith_pi {ι : Type*} [Fintype ι] {E' : ι → Type*} [∀ i, NormedAddCommGroup (E' i)]
    {f : α → ∀ i, E' i} {C : ℝ} (hC : 0 ≤ C) :
    IsBigOWithIsBigOWith C l f g' ↔ ∀ i, IsBigOWith C l (fun x => f x i) g' := by
  have : ∀ x, 0 ≤ C * ‖g' x‖ := fun x => mul_nonneg hC (norm_nonneg _)
  simp only [isBigOWith_iff, pi_norm_le_iff_of_nonneg (this _), eventually_all]

Componentwise Big-O Bound for Product Spaces

Informal description

Let $\iota$ be a finite type, and for each $i \in \iota$, let $E'_i$ be a normed additive commutative group. Given functions $f : \alpha \to \prod_{i \in \iota} E'_i$ and $g' : \alpha \to F$ (where $F$ is another normed space), and a nonnegative real constant $C \geq 0$, the following are equivalent: 1. The function $f$ satisfies $\|f(x)\| \leq C \|g'(x)\|$ for all $x$ in $l$ eventually. 2. For each $i \in \iota$, the component function $x \mapsto f(x)_i$ satisfies $\|f(x)_i\| \leq C \|g'(x)\|$ for all $x$ in $l$ eventually.

Asymptotics.isBigO_pi theorem

 {ι : Type*} [Fintype ι] {E' : ι → Type*} [∀ i, NormedAddCommGroup (E' i)] {f : α → ∀ i, E' i} :
  f =O[l] g' ↔ ∀ i, (fun x => f x i) =O[l] g'

Full source

@[simp]
theorem isBigO_pi {ι : Type*} [Fintype ι] {E' : ι → Type*} [∀ i, NormedAddCommGroup (E' i)]
    {f : α → ∀ i, E' i} : f =O[l] g'f =O[l] g' ↔ ∀ i, (fun x => f x i) =O[l] g' := by
  simp only [isBigO_iff_eventually_isBigOWith, ← eventually_all]
  exact eventually_congr (eventually_atTop.2 ⟨0, fun c => isBigOWith_pi⟩)

Componentwise Big-O Relation for Product Spaces

Informal description

Let $\iota$ be a finite index set, and for each $i \in \iota$, let $E'_i$ be a normed additive commutative group. Given functions $f : \alpha \to \prod_{i \in \iota} E'_i$ and $g' : \alpha \to F$ (where $F$ is another normed space), the following are equivalent: 1. The function $f$ is big-O of $g'$ with respect to the filter $l$, i.e., $f = O[l] g'$. 2. For each $i \in \iota$, the component function $x \mapsto f(x)_i$ is big-O of $g'$ with respect to $l$, i.e., $(\lambda x, f(x)_i) = O[l] g'$.

Asymptotics.isLittleO_pi theorem

 {ι : Type*} [Fintype ι] {E' : ι → Type*} [∀ i, NormedAddCommGroup (E' i)] {f : α → ∀ i, E' i} :
  f =o[l] g' ↔ ∀ i, (fun x => f x i) =o[l] g'

Full source

@[simp]
theorem isLittleO_pi {ι : Type*} [Fintype ι] {E' : ι → Type*} [∀ i, NormedAddCommGroup (E' i)]
    {f : α → ∀ i, E' i} : f =o[l] g'f =o[l] g' ↔ ∀ i, (fun x => f x i) =o[l] g' := by
  simp +contextual only [IsLittleO_def, isBigOWith_pi, le_of_lt]
  exact ⟨fun h i c hc => h hc i, fun h c hc i => h i hc⟩

Little-o relation for product spaces componentwise

Informal description

Let $\iota$ be a finite type, and for each $i \in \iota$, let $E'_i$ be a normed additive commutative group. Given functions $f : \alpha \to \prod_{i \in \iota} E'_i$ and $g' : \alpha \to F$ (where $F$ is another normed space), the following are equivalent: 1. The function $f$ is little-o of $g'$ with respect to the filter $l$, i.e., $f = o[l] g'$. 2. For each $i \in \iota$, the component function $x \mapsto f(x)_i$ is little-o of $g'$ with respect to $l$, i.e., $(\lambda x, f(x)_i) = o[l] g'$.

Asymptotics.IsBigO.natCast_atTop theorem

 {R : Type*} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] {f : R → E} {g : R → F}
  (h : f =O[atTop] g) : (fun (n : ℕ) => f n) =O[atTop] (fun n => g n)

Full source

theorem IsBigO.natCast_atTop {R : Type*} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R]
    [Archimedean R]
    {f : R → E} {g : R → F} (h : f =O[atTop] g) :
    (fun (n : ℕ) => f n) =O[atTop] (fun n => g n) :=
  IsBigO.comp_tendsto h tendsto_natCast_atTop_atTop

Restriction of Big-O Relation to Natural Numbers Preserves Asymptotic Behavior at Infinity

Informal description

Let $R$ be a strict ordered Archimedean semiring, and let $f : R \to E$ and $g : R \to F$ be functions between normed spaces. If $f$ is big-O of $g$ as $x \to \infty$ (i.e., $f = O(g)$ along the filter `atTop`), then the restriction of $f$ to natural numbers is big-O of the restriction of $g$ to natural numbers as $n \to \infty$ (i.e., $(\lambda n, f(n)) = O(\lambda n, g(n))$ along the filter `atTop` on $\mathbb{N}$).

Asymptotics.IsLittleO.natCast_atTop theorem

 {R : Type*} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] {f : R → E} {g : R → F}
  (h : f =o[atTop] g) : (fun (n : ℕ) => f n) =o[atTop] (fun n => g n)

Full source

theorem IsLittleO.natCast_atTop {R : Type*} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R]
    [Archimedean R]
    {f : R → E} {g : R → F} (h : f =o[atTop] g) :
    (fun (n : ℕ) => f n) =o[atTop] (fun n => g n) :=
  IsLittleO.comp_tendsto h tendsto_natCast_atTop_atTop

Restriction of Little-o Relation from Archimedean Semiring to Natural Numbers

Informal description

Let $R$ be an Archimedean strictly ordered semiring, and let $E$, $F$ be normed spaces. If $f : R \to E$ and $g : R \to F$ satisfy $f = o(g)$ as $x \to \infty$ in $R$, then the restricted functions $\tilde{f} : \mathbb{N} \to E$ and $\tilde{g} : \mathbb{N} \to F$ defined by $\tilde{f}(n) = f(n)$ and $\tilde{g}(n) = g(n)$ satisfy $\tilde{f} = o(\tilde{g})$ as $n \to \infty$ in $\mathbb{N}$.

Asymptotics.isBigO_atTop_iff_eventually_exists theorem

 {α : Type*} [SemilatticeSup α] [Nonempty α] {f : α → E} {g : α → F} :
  f =O[atTop] g ↔ ∀ᶠ n₀ in atTop, ∃ c, ∀ n ≥ n₀, ‖f n‖ ≤ c * ‖g n‖

Full source

theorem isBigO_atTop_iff_eventually_exists {α : Type*} [SemilatticeSup α] [Nonempty α]
    {f : α → E} {g : α → F} : f =O[atTop] gf =O[atTop] g ↔ ∀ᶠ n₀ in atTop, ∃ c, ∀ n ≥ n₀, ‖f n‖ ≤ c * ‖g n‖ := by
  rw [isBigO_iff, exists_eventually_atTop]

Characterization of Big-O at Infinity via Eventual Norm Bounds

Informal description

Let $\alpha$ be a nonempty join-semilattice, and let $f : \alpha \to E$ and $g : \alpha \to F$ be functions. Then $f = O(g)$ as $n \to \infty$ if and only if there exists a threshold $n_0 \in \alpha$ such that for all $n \geq n_0$, there exists a constant $c \in \mathbb{R}$ satisfying $\|f(n)\| \leq c \|g(n)\|$.

Asymptotics.isBigO_atTop_iff_eventually_exists_pos theorem

 {α : Type*} [SemilatticeSup α] [Nonempty α] {f : α → G} {g : α → G'} :
  f =O[atTop] g ↔ ∀ᶠ n₀ in atTop, ∃ c > 0, ∀ n ≥ n₀, c * ‖f n‖ ≤ ‖g n‖

Full source

theorem isBigO_atTop_iff_eventually_exists_pos {α : Type*}
    [SemilatticeSup α] [Nonempty α] {f : α → G} {g : α → G'} :
    f =O[atTop] gf =O[atTop] g ↔ ∀ᶠ n₀ in atTop, ∃ c > 0, ∀ n ≥ n₀, c * ‖f n‖ ≤ ‖g n‖ := by
  simp_rw [isBigO_iff'', ← exists_prop, Subtype.exists', exists_eventually_atTop]

Characterization of Big-O at Infinity via Eventual Positive Norm Bounds

Informal description

Let $\alpha$ be a nonempty join-semilattice, and let $f, g : \alpha \to G$ be functions into seminormed additive commutative groups $G$ and $G'$. Then $f = O(g)$ as $n \to \infty$ if and only if there exists a threshold $n_0 \in \alpha$ such that for all $n \geq n_0$, there exists a positive constant $c > 0$ satisfying $c \|f(n)\| \leq \|g(n)\|$.

Asymptotics.isBigO_mul_iff_isBigO_div theorem

{f g h : α → 𝕜} (hf : ∀ᶠ x in l, f x ≠ 0) : (fun x ↦ f x * g x) =O[l] h ↔ g =O[l] (fun x ↦ h x / f x)

Full source

lemma isBigO_mul_iff_isBigO_div {f g h : α → 𝕜} (hf : ∀ᶠ x in l, f x ≠ 0) :
    (fun x ↦ f x * g x) =O[l] h(fun x ↦ f x * g x) =O[l] h ↔ g =O[l] (fun x ↦ h x / f x) := by
  rw [isBigO_iff', isBigO_iff']
  refine ⟨fun ⟨c, hc, H⟩ ↦ ⟨c, hc, ?_⟩, fun ⟨c, hc, H⟩ ↦ ⟨c, hc, ?_⟩⟩ <;>
  · refine H.congr <| Eventually.mp hf <| Eventually.of_forall fun x hx ↦ ?_
    rw [norm_mul, norm_div, ← mul_div_assoc, le_div_iff₀' (norm_pos_iff.mpr hx)]

Big-O equivalence for products and quotients: $f \cdot g = O(h) \leftrightarrow g = O(h/f)$

Informal description

Let $\alpha$ be a type, $\mathbb{k}$ a normed field, and $l$ a filter on $\alpha$. For functions $f, g, h : \alpha \to \mathbb{k}$ such that $f(x) \neq 0$ for all $x$ in some neighborhood determined by $l$, the product function $x \mapsto f(x) \cdot g(x)$ is big-O of $h$ along $l$ if and only if $g$ is big-O of the quotient function $x \mapsto h(x)/f(x)$ along $l$.

summable_of_isBigO theorem

 {ι E} [SeminormedAddCommGroup E] [CompleteSpace E] {f : ι → E} {g : ι → ℝ} (hg : Summable g) (h : f =O[cofinite] g) :
  Summable f

Full source

theorem summable_of_isBigO {ι E} [SeminormedAddCommGroup E] [CompleteSpace E]
    {f : ι → E} {g : ι → ℝ} (hg : Summable g) (h : f =O[cofinite] g) : Summable f :=
  let ⟨C, hC⟩ := h.isBigOWith
  .of_norm_bounded_eventually (fun x => C * ‖g x‖) (hg.abs.mul_left _) hC.bound

Summability from Big-O Condition Along Cofinite Filter

Informal description

Let $E$ be a complete seminormed additive commutative group, and let $f \colon \iota \to E$ and $g \colon \iota \to \mathbb{R}$ be functions. If the series $\sum_{i \in \iota} g(i)$ is summable and $f$ is big-O of $g$ along the cofinite filter (i.e., there exists a constant $C > 0$ and a finite subset $S \subseteq \iota$ such that $\|f(i)\| \leq C \|g(i)\|$ for all $i \notin S$), then the series $\sum_{i \in \iota} f(i)$ is summable.

summable_of_isBigO_nat theorem

 {E} [SeminormedAddCommGroup E] [CompleteSpace E] {f : ℕ → E} {g : ℕ → ℝ} (hg : Summable g) (h : f =O[atTop] g) :
  Summable f

Full source

theorem summable_of_isBigO_nat {E} [SeminormedAddCommGroup E] [CompleteSpace E]
    {f : ℕ → E} {g : ℕ → ℝ} (hg : Summable g) (h : f =O[atTop] g) : Summable f :=
  summable_of_isBigO hg <| Nat.cofinite_eq_atTop.symm ▸ h

Summability of Sequence from Big-O Condition at Infinity

Informal description

Let $E$ be a complete seminormed additive commutative group, and let $f \colon \mathbb{N} \to E$ and $g \colon \mathbb{N} \to \mathbb{R}$ be sequences. If the series $\sum_{n=0}^\infty g(n)$ is summable and $f$ is big-O of $g$ at infinity (i.e., there exist constants $C > 0$ and $N \in \mathbb{N}$ such that $\|f(n)\| \leq C \|g(n)\|$ for all $n \geq N$), then the series $\sum_{n=0}^\infty f(n)$ is summable.

Asymptotics.IsBigO.comp_summable_norm theorem

 {ι E F : Type*} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] {f : E → F} {g : ι → E} (hf : f =O[𝓝 0] id)
  (hg : Summable (‖g ·‖)) : Summable (‖f <| g ·‖)

Full source

lemma Asymptotics.IsBigO.comp_summable_norm {ι E F : Type*}
    [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] {f : E → F} {g : ι → E}
    (hf : f =O[𝓝 0] id) (hg : Summable (‖g ·‖)) : Summable (‖f <| g ·‖) :=
  summable_of_isBigO hg <| hf.norm_norm.comp_tendsto <|
    tendsto_zero_iff_norm_tendsto_zero.2 hg.tendsto_cofinite_zero

Summability of Norm Composition under Big-O Condition Near Zero

Informal description

Let $E$ and $F$ be seminormed additive commutative groups, and let $f \colon E \to F$ be a function that is big-O of the identity function near $0$ (i.e., there exists a neighborhood of $0$ and a constant $C > 0$ such that $\|f(x)\| \leq C\|x\|$ for all $x$ in this neighborhood). If $g \colon \iota \to E$ is a function such that the series $\sum_{i \in \iota} \|g(i)\|$ is summable, then the series $\sum_{i \in \iota} \|f(g(i))\|$ is also summable.

PartialHomeomorph.isBigOWith_congr theorem

 (e : PartialHomeomorph α β) {b : β} (hb : b ∈ e.target) {f : β → E} {g : β → F} {C : ℝ} :
  IsBigOWith C (𝓝 b) f g ↔ IsBigOWith C (𝓝 (e.symm b)) (f ∘ e) (g ∘ e)

Full source

/-- Transfer `IsBigOWith` over a `PartialHomeomorph`. -/
theorem isBigOWith_congr (e : PartialHomeomorph α β) {b : β} (hb : b ∈ e.target) {f : β → E}
    {g : β → F} {C : ℝ} : IsBigOWithIsBigOWith C (𝓝 b) f g ↔ IsBigOWith C (𝓝 (e.symm b)) (f ∘ e) (g ∘ e) :=
  ⟨fun h =>
    h.comp_tendsto <| by
      have := e.continuousAt (e.map_target hb)
      rwa [ContinuousAt, e.rightInvOn hb] at this,
    fun h =>
    (h.comp_tendsto (e.continuousAt_symm hb)).congr' rfl
      ((e.eventually_right_inverse hb).mono fun _ hx => congr_arg f hx)
      ((e.eventually_right_inverse hb).mono fun _ hx => congr_arg g hx)⟩

Equivalence of Big-O Conditions Under Partial Homeomorphism

Informal description

Let $e$ be a partial homeomorphism between topological spaces $\alpha$ and $\beta$, and let $b \in \beta$ be a point in the target of $e$. For functions $f: \beta \to E$ and $g: \beta \to F$ (where $E$ and $F$ are normed spaces) and a real constant $C$, the following are equivalent: 1. $f$ is big-O of $g$ with constant $C$ near $b$ (i.e., $\|f(x)\| \leq C\|g(x)\|$ for all $x$ in some neighborhood of $b$). 2. The composition $f \circ e$ is big-O of $g \circ e$ with constant $C$ near $e^{-1}(b)$.

PartialHomeomorph.isBigO_congr theorem

 (e : PartialHomeomorph α β) {b : β} (hb : b ∈ e.target) {f : β → E} {g : β → F} :
  f =O[𝓝 b] g ↔ (f ∘ e) =O[𝓝 (e.symm b)] (g ∘ e)

Full source

/-- Transfer `IsBigO` over a `PartialHomeomorph`. -/
theorem isBigO_congr (e : PartialHomeomorph α β) {b : β} (hb : b ∈ e.target) {f : β → E}
    {g : β → F} : f =O[𝓝 b] gf =O[𝓝 b] g ↔ (f ∘ e) =O[𝓝 (e.symm b)] (g ∘ e) := by
  simp only [IsBigO_def]
  exact exists_congr fun C => e.isBigOWith_congr hb

Equivalence of Big-O Conditions Under Partial Homeomorphism

Informal description

Let $e$ be a partial homeomorphism between topological spaces $\alpha$ and $\beta$, and let $b \in \beta$ be a point in the target of $e$. For functions $f: \beta \to E$ and $g: \beta \to F$ (where $E$ and $F$ are normed spaces), the following are equivalent: 1. $f$ is big-O of $g$ near $b$ (i.e., there exists $C>0$ such that $\|f(x)\| \leq C\|g(x)\|$ for all $x$ in some neighborhood of $b$). 2. The composition $f \circ e$ is big-O of $g \circ e$ near $e^{-1}(b)$.

PartialHomeomorph.isLittleO_congr theorem

 (e : PartialHomeomorph α β) {b : β} (hb : b ∈ e.target) {f : β → E} {g : β → F} :
  f =o[𝓝 b] g ↔ (f ∘ e) =o[𝓝 (e.symm b)] (g ∘ e)

Full source

/-- Transfer `IsLittleO` over a `PartialHomeomorph`. -/
theorem isLittleO_congr (e : PartialHomeomorph α β) {b : β} (hb : b ∈ e.target) {f : β → E}
    {g : β → F} : f =o[𝓝 b] gf =o[𝓝 b] g ↔ (f ∘ e) =o[𝓝 (e.symm b)] (g ∘ e) := by
  simp only [IsLittleO_def]
  exact forall₂_congr fun c _hc => e.isBigOWith_congr hb

Equivalence of Little-o Conditions Under Partial Homeomorphism

Informal description

Let $e$ be a partial homeomorphism between topological spaces $\alpha$ and $\beta$, and let $b \in \beta$ be a point in the target of $e$. For functions $f: \beta \to E$ and $g: \beta \to F$ (where $E$ and $F$ are normed spaces), the following are equivalent: 1. $f$ is little-o of $g$ near $b$ (i.e., $f = o(g)$ as $x \to b$). 2. The composition $f \circ e$ is little-o of $g \circ e$ near $e^{-1}(b)$.

Homeomorph.isBigOWith_congr theorem

 (e : α ≃ₜ β) {b : β} {f : β → E} {g : β → F} {C : ℝ} :
  IsBigOWith C (𝓝 b) f g ↔ IsBigOWith C (𝓝 (e.symm b)) (f ∘ e) (g ∘ e)

Full source

/-- Transfer `IsBigOWith` over a `Homeomorph`. -/
theorem isBigOWith_congr (e : α ≃ₜ β) {b : β} {f : β → E} {g : β → F} {C : ℝ} :
    IsBigOWithIsBigOWith C (𝓝 b) f g ↔ IsBigOWith C (𝓝 (e.symm b)) (f ∘ e) (g ∘ e) :=
  e.toPartialHomeomorph.isBigOWith_congr trivial

Big-O Condition Preservation Under Homeomorphism

Informal description

Let $e \colon \alpha \simeq \beta$ be a homeomorphism between topological spaces $\alpha$ and $\beta$, and let $b \in \beta$. For functions $f \colon \beta \to E$ and $g \colon \beta \to F$ (where $E$ and $F$ are normed spaces) and a real constant $C > 0$, the following are equivalent: 1. $f$ is eventually bounded by $C \cdot g$ near $b$ (i.e., $\|f(x)\| \leq C \|g(x)\|$ for all $x$ in some neighborhood of $b$). 2. The composition $f \circ e$ is eventually bounded by $C \cdot (g \circ e)$ near $e^{-1}(b)$.

Homeomorph.isBigO_congr theorem

(e : α ≃ₜ β) {b : β} {f : β → E} {g : β → F} : f =O[𝓝 b] g ↔ (f ∘ e) =O[𝓝 (e.symm b)] (g ∘ e)

Full source

/-- Transfer `IsBigO` over a `Homeomorph`. -/
theorem isBigO_congr (e : α ≃ₜ β) {b : β} {f : β → E} {g : β → F} :
    f =O[𝓝 b] gf =O[𝓝 b] g ↔ (f ∘ e) =O[𝓝 (e.symm b)] (g ∘ e) := by
  simp only [IsBigO_def]
  exact exists_congr fun C => e.isBigOWith_congr

Big-O Condition Preservation Under Homeomorphism

Informal description

Let $e \colon \alpha \simeq \beta$ be a homeomorphism between topological spaces $\alpha$ and $\beta$, and let $b \in \beta$. For functions $f \colon \beta \to E$ and $g \colon \beta \to F$ (where $E$ and $F$ are normed spaces), the following are equivalent: 1. $f$ is big-O of $g$ near $b$ (i.e., there exists $C > 0$ such that $\|f(x)\| \leq C \|g(x)\|$ for all $x$ in some neighborhood of $b$). 2. The composition $f \circ e$ is big-O of $g \circ e$ near $e^{-1}(b)$.

Homeomorph.isLittleO_congr theorem

(e : α ≃ₜ β) {b : β} {f : β → E} {g : β → F} : f =o[𝓝 b] g ↔ (f ∘ e) =o[𝓝 (e.symm b)] (g ∘ e)

Full source

/-- Transfer `IsLittleO` over a `Homeomorph`. -/
theorem isLittleO_congr (e : α ≃ₜ β) {b : β} {f : β → E} {g : β → F} :
    f =o[𝓝 b] gf =o[𝓝 b] g ↔ (f ∘ e) =o[𝓝 (e.symm b)] (g ∘ e) := by
  simp only [IsLittleO_def]
  exact forall₂_congr fun c _hc => e.isBigOWith_congr

Little-o Condition Preservation Under Homeomorphism

Informal description

Let $e \colon \alpha \simeq \beta$ be a homeomorphism between topological spaces $\alpha$ and $\beta$, and let $b \in \beta$. For functions $f \colon \beta \to E$ and $g \colon \beta \to F$ (where $E$ and $F$ are normed spaces), the following are equivalent: 1. $f$ is little-o of $g$ near $b$ (i.e., $\|f(x)\| / \|g(x)\| \to 0$ as $x \to b$). 2. The composition $f \circ e$ is little-o of $g \circ e$ near $e^{-1}(b)$.

ContinuousOn.isBigOWith_principal theorem

 (hf : ContinuousOn f s) (hs : IsCompact s) (hc : ‖c‖ ≠ 0) :
  IsBigOWith (sSup (Norm.norm '' (f '' s)) / ‖c‖) (𝓟 s) f fun _ => c

Full source

protected theorem isBigOWith_principal
    (hf : ContinuousOn f s) (hs : IsCompact s) (hc : ‖c‖‖c‖ ≠ 0) :
    IsBigOWith (sSup (Norm.normNorm.norm '' (f '' s)) / ‖c‖) (𝓟 s) f fun _ => c := by
  rw [isBigOWith_principal, div_mul_cancel₀ _ hc]
  exact fun x hx ↦ hs.image_of_continuousOn hf |>.image continuous_norm
   |>.isLUB_sSup (Set.image_nonempty.mpr <| Set.image_nonempty.mpr ⟨x, hx⟩)
   |>.left <| Set.mem_image_of_mem _ <| Set.mem_image_of_mem _ hx

Big-O Bound for Continuous Functions on Compact Sets with Constant Function

Informal description

Let $f : X \to E$ be a function continuous on a compact subset $s \subseteq X$, and let $c \in F$ be a nonzero element (i.e., $\|c\| \neq 0$). Then, the function $f$ is big-O with constant $\sup \{\|f(x)\| \mid x \in s\} / \|c\|$ of the constant function $\lambda \_. c$ on the principal filter generated by $s$. In other words, for all $x \in s$, we have $\|f(x)\| \leq \left(\sup_{y \in s} \|f(y)\|\right) \cdot \|c\|^{-1} \cdot \|c\|$.

ContinuousOn.isBigO_principal theorem

(hf : ContinuousOn f s) (hs : IsCompact s) (hc : ‖c‖ ≠ 0) : f =O[𝓟 s] fun _ => c

Full source

protected theorem isBigO_principal (hf : ContinuousOn f s) (hs : IsCompact s)
    (hc : ‖c‖‖c‖ ≠ 0) : f =O[𝓟 s] fun _ => c :=
  (hf.isBigOWith_principal hs hc).isBigO

Big-O Bound for Continuous Functions on Compact Sets Relative to Constant Function

Informal description

Let $f : X \to E$ be a function continuous on a compact subset $s \subseteq X$, and let $c \in F$ be a nonzero element (i.e., $\|c\| \neq 0$). Then, the function $f$ is big-O of the constant function $\lambda \_. c$ on the principal filter generated by $s$, i.e., there exists a constant $C > 0$ such that for all $x \in s$, $\|f(x)\| \leq C \|c\|$.

ContinuousOn.isBigOWith_rev_principal theorem

 (hf : ContinuousOn f s) (hs : IsCompact s) (hC : ∀ i ∈ s, f i ≠ 0) (c : F) :
  IsBigOWith (‖c‖ / sInf (Norm.norm '' (f '' s))) (𝓟 s) (fun _ => c) f

Full source

protected theorem isBigOWith_rev_principal
    (hf : ContinuousOn f s) (hs : IsCompact s) (hC : ∀ i ∈ s, f i ≠ 0) (c : F) :
    IsBigOWith (‖c‖ / sInf (Norm.normNorm.norm '' (f '' s))) (𝓟 s) (fun _ => c) f := by
  refine isBigOWith_principal.mpr fun x hx ↦ ?_
  rw [mul_comm_div]
  replace hs := hs.image_of_continuousOn hf |>.image continuous_norm
  have h_sInf := hs.isGLB_sInf <| Set.image_nonempty.mpr <| Set.image_nonempty.mpr ⟨x, hx⟩
  refine le_mul_of_one_le_right (norm_nonneg c) <| (one_le_div ?_).mpr <|
    h_sInf.1 <| Set.mem_image_of_mem _ <| Set.mem_image_of_mem _ hx
  obtain ⟨_, ⟨x, hx, hCx⟩, hnormCx⟩ := hs.sInf_mem h_sInf.nonempty
  rw [← hnormCx, ← hCx]
  exact (norm_ne_zero_iff.mpr (hC x hx)).symm.lt_of_le (norm_nonneg _)

Asymptotic Bound for Constant Function Relative to Nonzero Continuous Function on Compact Set

Informal description

Let $f : X \to E$ be a function continuous on a compact subset $s \subseteq X$, and suppose $f(x) \neq 0$ for all $x \in s$. Then, for any constant $c \in F$, the function $\lambda \_. c$ is asymptotically bounded by $f$ on $s$ with constant $\|c\| / \inf \{\|f(x)\| \mid x \in s\}$. That is, there exists a constant $C = \|c\| / \inf \{\|f(x)\| \mid x \in s\}$ such that for all $x \in s$, $\|c\| \leq C \|f(x)\|$.

ContinuousOn.isBigO_rev_principal theorem

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

Full source

protected theorem isBigO_rev_principal (hf : ContinuousOn f s)
    (hs : IsCompact s) (hC : ∀ i ∈ s, f i ≠ 0) (c : F) : (fun _ => c) =O[𝓟 s] f :=
  (hf.isBigOWith_rev_principal hs hC c).isBigO

Asymptotic Bound for Constant Function Relative to Nonzero Continuous Function on Compact Set

Informal description

Let $X$ and $E$ be topological and normed additive groups respectively, and let $f : X \to E$ be a function that is continuous on a compact subset $s \subseteq X$. If $f(x) \neq 0$ for all $x \in s$, then for any constant $c \in F$, the constant function $\lambda x. c$ is asymptotically bounded by $f$ on $s$, i.e., $(\lambda x. c) = O(f)$ uniformly on $s$.

NormedField.tendsto_zero_smul_of_tendsto_zero_of_bounded theorem

 {ι 𝕜 𝔸 : Type*} [NormedDivisionRing 𝕜] [NormedAddCommGroup 𝔸] [Module 𝕜 𝔸] [IsBoundedSMul 𝕜 𝔸] {l : Filter ι}
  {ε : ι → 𝕜} {f : ι → 𝔸} (hε : Tendsto ε l (𝓝 0)) (hf : IsBoundedUnder (· ≤ ·) l (norm ∘ f)) : Tendsto (ε • f) l (𝓝 0)

Full source

/-- The (scalar) product of a sequence that tends to zero with a bounded one also tends to zero. -/
lemma NormedField.tendsto_zero_smul_of_tendsto_zero_of_bounded {ι 𝕜 𝔸 : Type*}
    [NormedDivisionRing 𝕜] [NormedAddCommGroup 𝔸] [Module 𝕜 𝔸] [IsBoundedSMul 𝕜 𝔸] {l : Filter ι}
    {ε : ι → 𝕜} {f : ι → 𝔸} (hε : Tendsto ε l (𝓝 0)) (hf : IsBoundedUnder (· ≤ ·) l (normnorm ∘ f)) :
    Tendsto (ε • f) l (𝓝 0) := by
  rw [← isLittleO_one_iff 𝕜] at hε ⊢
  simpa using IsLittleO.smul_isBigO hε (hf.isBigO_const (one_ne_zero : (1 : 𝕜) ≠ 0))

Scalar product of a zero-tending sequence with a bounded sequence tends to zero

Informal description

Let $\mathbb{K}$ be a normed division ring, $\mathbb{A}$ a normed additive commutative group with a $\mathbb{K}$-module structure, and $\mathbb{K} \times \mathbb{A} \to \mathbb{A}$ a bounded scalar multiplication. Let $l$ be a filter on a type $\iota$, and let $\varepsilon : \iota \to \mathbb{K}$ and $f : \iota \to \mathbb{A}$ be functions such that: 1. $\varepsilon$ tends to $0$ along $l$, and 2. The function $\|f\|$ is bounded above under the order relation $\leq$ along $l$. Then the scalar product $\varepsilon \cdot f$ tends to $0$ along $l$.