Mathlib.Analysis.Asymptotics.Defs

Asymptotics.IsBigOWith definition

Full source

/-- This version of the Landau notation `IsBigOWith C l f g` where `f` and `g` are two functions on
a type `α` and `l` is a filter on `α`, means that eventually for `l`, `‖f‖` is bounded by `C * ‖g‖`.
In other words, `‖f‖ / ‖g‖` is eventually bounded by `C`, modulo division by zero issues that are
avoided by this definition. Probably you want to use `IsBigO` instead of this relation. -/
irreducible_def IsBigOWith (c : ℝ) (l : Filter α) (f : α → E) (g : α → F) : Prop :=
  ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖

Big-O bound with constant $C$

Informal description

Given a real constant $C$, a filter $l$ on a type $\alpha$, and two functions $f: \alpha \to E$ and $g: \alpha \to F$ where $E$ and $F$ are normed spaces, the relation $\text{IsBigOWith}(C, l, f, g)$ holds if, for all $x$ in $l$ eventually, the norm of $f(x)$ is bounded by $C$ times the norm of $g(x)$. In other words, the ratio $\|f(x)\| / \|g(x)\|$ is eventually bounded by $C$, avoiding division by zero issues by using this multiplicative formulation.

Asymptotics.IsBigOWith_def theorem

: eta_helper Eq✝ @IsBigOWith.{} @(delta% @definition✝)

Full source

/-- This version of the Landau notation `IsBigOWith C l f g` where `f` and `g` are two functions on
a type `α` and `l` is a filter on `α`, means that eventually for `l`, `‖f‖` is bounded by `C * ‖g‖`.
In other words, `‖f‖ / ‖g‖` is eventually bounded by `C`, modulo division by zero issues that are
avoided by this definition. Probably you want to use `IsBigO` instead of this relation. -/
irreducible_def IsBigOWith (c : ℝ) (l : Filter α) (f : α → E) (g : α → F) : Prop :=
  ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖

Characterization of Big-O With Constant $c$

Informal description

The relation $\text{IsBigOWith}(c, l, f, g)$ holds if and only if for all $x$ in the filter $l$ eventually, the norm of $f(x)$ is bounded by $c$ times the norm of $g(x)$, i.e., $\|f(x)\| ≤ c \cdot \|g(x)\|$.

Asymptotics.isBigOWith_iff theorem

: IsBigOWith c l f g ↔ ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖

Full source

/-- Definition of `IsBigOWith`. We record it in a lemma as `IsBigOWith` is irreducible. -/
theorem isBigOWith_iff : IsBigOWithIsBigOWith c l f g ↔ ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖ := by rw [IsBigOWith_def]

Characterization of Big-O With Constant $c$: $\|f(x)\| \leq c \cdot \|g(x)\|$ Eventually

Informal description

For a real constant $c$, a filter $l$ on a type $\alpha$, and functions $f: \alpha \to E$, $g: \alpha \to F$ where $E$ and $F$ are normed spaces, the relation $\text{IsBigOWith}(c, l, f, g)$ holds if and only if for all $x$ in $l$ eventually, the norm of $f(x)$ is bounded by $c$ times the norm of $g(x)$, i.e., $\|f(x)\| \leq c \cdot \|g(x)\|$.

Asymptotics.IsBigO definition

Full source

/-- The Landau notation `f =O[l] g` where `f` and `g` are two functions on a type `α` and `l` is
a filter on `α`, means that eventually for `l`, `‖f‖` is bounded by a constant multiple of `‖g‖`.
In other words, `‖f‖ / ‖g‖` is eventually bounded, modulo division by zero issues that are avoided
by this definition. -/
irreducible_def IsBigO (l : Filter α) (f : α → E) (g : α → F) : Prop :=
  ∃ c : ℝ, IsBigOWith c l f g

Big O notation for function comparison along a filter

Informal description

The relation $f =O[l] g$ between two functions $f : \alpha \to E$ and $g : \alpha \to F$ along a filter $l$ on $\alpha$ means that there exists a constant $C \in \mathbb{R}$ such that $\|f(x)\| \leq C\|g(x)\|$ holds for all $x$ in some neighborhood determined by $l$. Here, $\|\cdot\|$ denotes the norm on the respective spaces $E$ and $F$.

Asymptotics.IsBigO_def theorem

: eta_helper Eq✝ @IsBigO.{} @(delta% @definition✝)

Full source

/-- The Landau notation `f =O[l] g` where `f` and `g` are two functions on a type `α` and `l` is
a filter on `α`, means that eventually for `l`, `‖f‖` is bounded by a constant multiple of `‖g‖`.
In other words, `‖f‖ / ‖g‖` is eventually bounded, modulo division by zero issues that are avoided
by this definition. -/
irreducible_def IsBigO (l : Filter α) (f : α → E) (g : α → F) : Prop :=
  ∃ c : ℝ, IsBigOWith c l f g

Definition of Big-O Relation via Norm Bounds

Informal description

The relation $f =O[l] g$ between two functions $f : \alpha \to E$ and $g : \alpha \to F$ along a filter $l$ on $\alpha$ holds if and only if there exists a constant $C \in \mathbb{R}_{\geq 0}$ such that $\|f(x)\| \leq C\|g(x)\|$ for all $x$ in some neighborhood determined by $l$, where $\|\cdot\|$ denotes the norm on the respective spaces $E$ and $F$.

Asymptotics.term_=O[_]_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
notation:100 f " =O[" l "] " g:100 => IsBigO l f g

Big O notation for function comparison along a filter

Informal description

The notation $f =O[l] g$ denotes that the function $f$ is big O of the function $g$ along the filter $l$, meaning there exists some constant $C$ such that $\|f(x)\| \leq C\|g(x)\|$ for all $x$ in some neighborhood determined by $l$.

Asymptotics.isBigO_iff_isBigOWith theorem

: f =O[l] g ↔ ∃ c : ℝ, IsBigOWith c l f g

Full source

/-- Definition of `IsBigO` in terms of `IsBigOWith`. We record it in a lemma as `IsBigO` is
irreducible. -/
theorem isBigO_iff_isBigOWith : f =O[l] gf =O[l] g ↔ ∃ c : ℝ, IsBigOWith c l f g := by rw [IsBigO_def]

Big-O Relation via Existence of Constant Bound

Informal description

For two functions $f : \alpha \to E$ and $g : \alpha \to F$ and a filter $l$ on $\alpha$, the relation $f =O[l] g$ holds if and only if there exists a real constant $c$ such that $\text{IsBigOWith}(c, l, f, g)$ is satisfied, meaning $\|f(x)\| \leq c \|g(x)\|$ for all $x$ in some neighborhood determined by $l$.

Asymptotics.isBigO_iff theorem

: f =O[l] g ↔ ∃ c : ℝ, ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖

Full source

/-- Definition of `IsBigO` in terms of filters. -/
theorem isBigO_iff : f =O[l] gf =O[l] g ↔ ∃ c : ℝ, ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖ := by
  simp only [IsBigO_def, IsBigOWith_def]

Characterization of Big-O Relation via Norm Bounds

Informal description

For two functions $f : \alpha \to E$ and $g : \alpha \to F$ and a filter $l$ on $\alpha$, the relation $f =O[l] g$ holds if and only if there exists a real constant $c$ such that for all $x$ in some neighborhood determined by $l$, the inequality $\|f(x)\| \leq c \|g(x)\|$ is satisfied.

Asymptotics.isBigO_iff' theorem

{g : α → E'''} : f =O[l] g ↔ ∃ c > 0, ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖

Full source

/-- Definition of `IsBigO` in terms of filters, with a positive constant. -/
theorem isBigO_iff' {g : α → E'''} :
    f =O[l] gf =O[l] g ↔ ∃ c > 0, ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖ := by
  refine ⟨fun h => ?mp, fun h => ?mpr⟩
  case mp =>
    rw [isBigO_iff] at h
    obtain ⟨c, hc⟩ := h
    refine ⟨max c 1, zero_lt_one.trans_le (le_max_right _ _), ?_⟩
    filter_upwards [hc] with x hx
    apply hx.trans
    gcongr
    exact le_max_left _ _
  case mpr =>
    rw [isBigO_iff]
    obtain ⟨c, ⟨_, hc⟩⟩ := h
    exact ⟨c, hc⟩

Characterization of Big-O Relation via Positive Constant Bound

Informal description

For functions $f : \alpha \to E$ and $g : \alpha \to E'''$ and a filter $l$ on $\alpha$, the relation $f =O[l] g$ holds if and only if there exists a positive real constant $c > 0$ such that for all $x$ in some neighborhood determined by $l$, the inequality $\|f(x)\| \leq c \|g(x)\|$ is satisfied.

Asymptotics.isBigO_iff'' theorem

{g : α → E'''} : f =O[l] g ↔ ∃ c > 0, ∀ᶠ x in l, c * ‖f x‖ ≤ ‖g x‖

Full source

/-- Definition of `IsBigO` in terms of filters, with the constant in the lower bound. -/
theorem isBigO_iff'' {g : α → E'''} :
    f =O[l] gf =O[l] g ↔ ∃ c > 0, ∀ᶠ x in l, c * ‖f x‖ ≤ ‖g x‖ := by
  refine ⟨fun h => ?mp, fun h => ?mpr⟩
  case mp =>
    rw [isBigO_iff'] at h
    obtain ⟨c, ⟨hc_pos, hc⟩⟩ := h
    refine ⟨c⁻¹, ⟨by positivity, ?_⟩⟩
    filter_upwards [hc] with x hx
    rwa [inv_mul_le_iff₀ (by positivity)]
  case mpr =>
    rw [isBigO_iff']
    obtain ⟨c, ⟨hc_pos, hc⟩⟩ := h
    refine ⟨c⁻¹, ⟨by positivity, ?_⟩⟩
    filter_upwards [hc] with x hx
    rwa [← inv_inv c, inv_mul_le_iff₀ (by positivity)] at hx

Characterization of Big-O Relation via Reverse Norm Bound with Positive Constant

Informal description

For functions $f : \alpha \to E$ and $g : \alpha \to E'''$ and a filter $l$ on $\alpha$, the relation $f =O[l] g$ holds if and only if there exists a positive real constant $c > 0$ such that for all $x$ in some neighborhood determined by $l$, the inequality $c \|f(x)\| \leq \|g(x)\|$ is satisfied.

Asymptotics.IsBigO.of_bound theorem

(c : ℝ) (h : ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖) : f =O[l] g

Full source

theorem IsBigO.of_bound (c : ℝ) (h : ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖) : f =O[l] g :=
  isBigO_iff.2 ⟨c, h⟩

Big-O condition from norm bound

Informal description

Let $f : \alpha \to E$ and $g : \alpha \to F$ be functions, and let $l$ be a filter on $\alpha$. If there exists a real constant $c$ such that $\|f(x)\| \leq c \|g(x)\|$ holds for all $x$ in some neighborhood determined by $l$, then $f$ is big O of $g$ along $l$, denoted $f =O[l] g$.

Asymptotics.IsBigO.of_bound' theorem

(h : ∀ᶠ x in l, ‖f x‖ ≤ ‖g x‖) : f =O[l] g

Full source

theorem IsBigO.of_bound' (h : ∀ᶠ x in l, ‖f x‖ ≤ ‖g x‖) : f =O[l] g :=
  .of_bound 1 <| by simpa only [one_mul] using h

Big-O condition from unit norm bound

Informal description

Let $f : \alpha \to E$ and $g : \alpha \to F$ be functions, and let $l$ be a filter on $\alpha$. If $\|f(x)\| \leq \|g(x)\|$ holds for all $x$ in some neighborhood determined by $l$, then $f$ is big O of $g$ along $l$, denoted $f =O[l] g$.

Asymptotics.IsBigO.bound theorem

: f =O[l] g → ∃ c : ℝ, ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖

Full source

theorem IsBigO.bound : f =O[l] g → ∃ c : ℝ, ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖ :=
  isBigO_iff.1

Existence of Constant for Big-O Relation

Informal description

If $f =O[l] g$ holds for functions $f : \alpha \to E$ and $g : \alpha \to F$ along a filter $l$ on $\alpha$, then there exists a real constant $c$ such that $\|f(x)\| \leq c \|g(x)\|$ for all $x$ in some neighborhood determined by $l$.

Asymptotics.IsBigO.of_norm_eventuallyLE theorem

{g : α → ℝ} (h : (‖f ·‖) ≤ᶠ[l] g) : f =O[l] g

Full source

/-- See also `Filter.Eventually.isBigO`, which is the same lemma
stated using `Filter.Eventually` instead of `Filter.EventuallyLE`. -/
theorem IsBigO.of_norm_eventuallyLE {g : α → ℝ} (h : (‖f ·‖) ≤ᶠ[l] g) : f =O[l] g :=
  .of_bound' <| h.mono fun _ h ↦ h.trans <| le_abs_self _

Big-O condition from eventual norm bound

Informal description

Let $f : \alpha \to E$ be a function and $g : \alpha \to \mathbb{R}$ be a real-valued function, where $E$ is a normed space. If the norm of $f$ is eventually bounded by $g$ along the filter $l$ (i.e., $\|f(x)\| \leq g(x)$ for all $x$ in some neighborhood determined by $l$), then $f$ is big O of $g$ along $l$, denoted $f =O[l] g$.

Asymptotics.IsBigO.of_norm_le theorem

{g : α → ℝ} (h : ∀ x, ‖f x‖ ≤ g x) : f =O[l] g

Full source

theorem IsBigO.of_norm_le {g : α → ℝ} (h : ∀ x, ‖f x‖ ≤ g x) : f =O[l] g :=
  .of_norm_eventuallyLE <| .of_forall h

Big-O condition from pointwise norm bound

Informal description

Let $f : \alpha \to E$ be a function to a normed space $E$ and $g : \alpha \to \mathbb{R}$ be a real-valued function. If for every $x \in \alpha$ the norm $\|f(x)\|$ is bounded by $g(x)$, then $f$ is big O of $g$ along any filter $l$ on $\alpha$, denoted $f =O[l] g$.

Asymptotics.IsLittleO definition

Full source

/-- The Landau notation `f =o[l] g` where `f` and `g` are two functions on a type `α` and `l` is
a filter on `α`, means that eventually for `l`, `‖f‖` is bounded by an arbitrarily small constant
multiple of `‖g‖`. In other words, `‖f‖ / ‖g‖` tends to `0` along `l`, modulo division by zero
issues that are avoided by this definition. -/
irreducible_def IsLittleO (l : Filter α) (f : α → E) (g : α → F) : Prop :=
  ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g

Little-o asymptotic relation

Informal description

The relation $ f = o[l] g $ between two functions $ f : \alpha \to E $ and $ g : \alpha \to F $ with respect to a filter $ l $ on $ \alpha $ means that for every positive real number $ c $, there exists a neighborhood in $ l $ such that for all $ x $ in this neighborhood, the norm of $ f(x) $ is bounded by $ c $ times the norm of $ g(x) $, i.e., $ \|f(x)\| \leq c \|g(x)\| $. This captures the idea that $ f $ grows asymptotically slower than $ g $ as the argument approaches the limit defined by $ l $.

Asymptotics.IsLittleO_def theorem

: eta_helper Eq✝ @IsLittleO.{} @(delta% @definition✝)

Full source

/-- The Landau notation `f =o[l] g` where `f` and `g` are two functions on a type `α` and `l` is
a filter on `α`, means that eventually for `l`, `‖f‖` is bounded by an arbitrarily small constant
multiple of `‖g‖`. In other words, `‖f‖ / ‖g‖` tends to `0` along `l`, modulo division by zero
issues that are avoided by this definition. -/
irreducible_def IsLittleO (l : Filter α) (f : α → E) (g : α → F) : Prop :=
  ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g

Definition of Little-o Asymptotic Relation

Informal description

The relation $f = o[l] g$ between two functions $f : \alpha \to E$ and $g : \alpha \to F$ with respect to a filter $l$ on $\alpha$ holds if and only if for every positive real number $c$, there exists a neighborhood in $l$ such that for all $x$ in this neighborhood, $\|f(x)\| \leq c \|g(x)\|$.

Asymptotics.term_=o[_]_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
notation:100 f " =o[" l "] " g:100 => IsLittleO l f g

Little-o notation for asymptotic comparison

Informal description

The notation `f =o[l] g` denotes that the function `f` is little-o of `g` along the filter `l`, meaning that `f` grows asymptotically slower than `g` as the argument approaches the limit defined by `l`. More precisely, `f =o[l] g` means that for any positive real number `c`, there exists a neighborhood in the filter `l` such that for all `x` in this neighborhood, the norm of `f x` is bounded by `c` times the norm of `g x`, i.e., `‖f x‖ ≤ c * ‖g x‖`. This notation is used to express the asymptotic behavior of functions, particularly in the context of limits and calculus.

Asymptotics.isLittleO_iff_forall_isBigOWith theorem

: f =o[l] g ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g

Full source

/-- Definition of `IsLittleO` in terms of `IsBigOWith`. -/
theorem isLittleO_iff_forall_isBigOWith : f =o[l] gf =o[l] g ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g := by
  rw [IsLittleO_def]

Characterization of Little-o via Big-O With Arbitrary Constant

Informal description

For functions $f : \alpha \to E$ and $g : \alpha \to F$ (where $E$ and $F$ are normed spaces) and a filter $l$ on $\alpha$, the relation $f = o[l] g$ holds if and only if for every positive real number $c > 0$, the function $f$ is eventually bounded by $c \cdot g$ along $l$ (i.e., $\text{IsBigOWith}(c, l, f, g)$ holds).

Asymptotics.isLittleO_iff theorem

: f =o[l] g ↔ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖

Full source

/-- Definition of `IsLittleO` in terms of filters. -/
theorem isLittleO_iff : f =o[l] gf =o[l] g ↔ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖ := by
  simp only [IsLittleO_def, IsBigOWith_def]

Characterization of Little-o Relation via Norm Bounds

Informal description

For functions $f : \alpha \to E$ and $g : \alpha \to F$ (where $E$ and $F$ are normed spaces) and a filter $l$ on $\alpha$, the relation $f = o[l] g$ holds if and only if for every positive real number $c > 0$, there exists a neighborhood in $l$ such that for all $x$ in this neighborhood, $\|f(x)\| \leq c \cdot \|g(x)\|$.

Asymptotics.IsLittleO.def theorem

(h : f =o[l] g) (hc : 0 < c) : ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖

Full source

theorem IsLittleO.def (h : f =o[l] g) (hc : 0 < c) : ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖ :=
  isLittleO_iff.1 h hc

Norm Bound Characterization of Little-o Relation

Informal description

Let $f : \alpha \to E$ and $g : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If $f = o[l] g$ and $c > 0$ is a positive real number, then there exists a neighborhood in $l$ such that for all $x$ in this neighborhood, $\|f(x)\| \leq c \cdot \|g(x)\|$.

Asymptotics.IsLittleO.def' theorem

(h : f =o[l] g) (hc : 0 < c) : IsBigOWith c l f g

Full source

theorem IsLittleO.def' (h : f =o[l] g) (hc : 0 < c) : IsBigOWith c l f g :=
  isBigOWith_iff.2 <| isLittleO_iff.1 h hc

Little-o Implies Big-O With Any Positive Constant

Informal description

Let $f : \alpha \to E$ and $g : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If $f = o[l] g$ and $c > 0$ is a positive real number, then there exists a constant $C$ such that $\|f(x)\| \leq C \cdot \|g(x)\|$ for all $x$ in some neighborhood in $l$.

Asymptotics.IsLittleO.eventuallyLE theorem

(h : f =o[l] g) : ∀ᶠ x in l, ‖f x‖ ≤ ‖g x‖

Full source

theorem IsLittleO.eventuallyLE (h : f =o[l] g) : ∀ᶠ x in l, ‖f x‖ ≤ ‖g x‖ := by
  simpa using h.def zero_lt_one

Norm Bound in Little-o Relation: $\|f(x)\| \leq \|g(x)\|$ Eventually

Informal description

Let $f : \alpha \to E$ and $g : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If $f = o[l] g$, then for all $x$ in some neighborhood in $l$, the norm of $f(x)$ is bounded by the norm of $g(x)$, i.e., $\|f(x)\| \leq \|g(x)\|$.

Asymptotics.IsBigOWith.isBigO theorem

(h : IsBigOWith c l f g) : f =O[l] g

Full source

theorem IsBigOWith.isBigO (h : IsBigOWith c l f g) : f =O[l] g := by rw [IsBigO_def]; exact ⟨c, h⟩

Big-O Bound Implies Big-O Relation

Informal description

If there exists a constant $C \geq 0$ such that $\|f(x)\| \leq C \|g(x)\|$ holds for all $x$ in some neighborhood determined by the filter $l$, then $f$ is big O of $g$ along $l$, denoted $f =O[l] g$.

Asymptotics.IsLittleO.isBigOWith theorem

(hgf : f =o[l] g) : IsBigOWith 1 l f g

Full source

theorem IsLittleO.isBigOWith (hgf : f =o[l] g) : IsBigOWith 1 l f g :=
  hgf.def' zero_lt_one

Little-o Implies Big-O with Constant One

Informal description

Let $f : \alpha \to E$ and $g : \alpha \to F$ be functions between 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 there exists a neighborhood in $l$ such that for all $x$ in this neighborhood, $\|f(x)\| \leq \|g(x)\|$.

Asymptotics.IsLittleO.isBigO theorem

(hgf : f =o[l] g) : f =O[l] g

Full source

theorem IsLittleO.isBigO (hgf : f =o[l] g) : f =O[l] g :=
  hgf.isBigOWith.isBigO

Little-o implies Big-O along a filter

Informal description

If a function $f$ is little-o of a function $g$ along a filter $l$, then $f$ is also big-O of $g$ along $l$. In other words, if $f = o[l] g$, then $f = O[l] g$.

Asymptotics.IsBigO.isBigOWith theorem

: f =O[l] g → ∃ c : ℝ, IsBigOWith c l f g

Full source

theorem IsBigO.isBigOWith : f =O[l] g → ∃ c : ℝ, IsBigOWith c l f g :=
  isBigO_iff_isBigOWith.1

Existence of Constant in Big-O Relation

Informal description

If a function $f$ is big O of a function $g$ along a filter $l$, denoted $f =O[l] g$, then there exists a real constant $c$ such that $\|f(x)\| \leq c \|g(x)\|$ holds for all $x$ in some neighborhood determined by $l$.

Asymptotics.IsBigOWith.weaken theorem

(h : IsBigOWith c l f g') (hc : c ≤ c') : IsBigOWith c' l f g'

Full source

theorem IsBigOWith.weaken (h : IsBigOWith c l f g') (hc : c ≤ c') : IsBigOWith c' l f g' :=
  IsBigOWith.of_bound <|
    mem_of_superset h.bound fun x hx =>
      calc
        ‖f x‖ ≤ c * ‖g' x‖ := hx
        _ ≤ _ := by gcongr

Weakening of Big-O Constant: $c \leq c' \implies \text{IsBigOWith}(c, l, f, g) \to \text{IsBigOWith}(c', l, f, g)$

Informal description

Let $f$ and $g'$ be functions from a type $\alpha$ to normed spaces $E$ and $F$ respectively, and let $l$ be a filter on $\alpha$. If there exists a real constant $c$ such that $\|f(x)\| \leq c \|g'(x)\|$ holds for all $x$ in some neighborhood determined by $l$ (i.e., $\text{IsBigOWith}(c, l, f, g')$ holds), and if $c \leq c'$ for some other constant $c'$, then $\text{IsBigOWith}(c', l, f, g')$ also holds.

Asymptotics.IsBigOWith.exists_pos theorem

(h : IsBigOWith c l f g') : ∃ c' > 0, IsBigOWith c' l f g'

Full source

theorem IsBigOWith.exists_pos (h : IsBigOWith c l f g') :
    ∃ c' > 0, IsBigOWith c' l f g' :=
  ⟨max c 1, lt_of_lt_of_le zero_lt_one (le_max_right c 1), h.weaken <| le_max_left c 1⟩

Existence of Positive Constant in Big-O Bound

Informal description

Given a function $f$ and a function $g'$ defined on a type $\alpha$ with values in normed spaces, and a filter $l$ on $\alpha$, if there exists a real constant $c$ such that $\|f(x)\| \leq c \|g'(x)\|$ holds for all $x$ in some neighborhood determined by $l$ (i.e., $\text{IsBigOWith}(c, l, f, g')$ holds), then there exists a positive constant $c' > 0$ such that $\text{IsBigOWith}(c', l, f, g')$ also holds.

Asymptotics.IsBigO.exists_pos theorem

(h : f =O[l] g') : ∃ c > 0, IsBigOWith c l f g'

Full source

theorem IsBigO.exists_pos (h : f =O[l] g') : ∃ c > 0, IsBigOWith c l f g' :=
  let ⟨_c, hc⟩ := h.isBigOWith
  hc.exists_pos

Existence of Positive Constant in Big-O Relation

Informal description

If a function $f$ is big O of a function $g'$ along a filter $l$, denoted $f =O[l] g'$, then there exists a positive real constant $c > 0$ such that $\|f(x)\| \leq c \|g'(x)\|$ holds for all $x$ in some neighborhood determined by $l$.

Asymptotics.IsBigOWith.exists_nonneg theorem

(h : IsBigOWith c l f g') : ∃ c' ≥ 0, IsBigOWith c' l f g'

Full source

theorem IsBigOWith.exists_nonneg (h : IsBigOWith c l f g') :
    ∃ c' ≥ 0, IsBigOWith c' l f g' :=
  let ⟨c, cpos, hc⟩ := h.exists_pos
  ⟨c, le_of_lt cpos, hc⟩

Existence of Nonnegative Constant in Big-O Bound

Informal description

Given a function $f$ and a function $g'$ defined on a type $\alpha$ with values in normed spaces, and a filter $l$ on $\alpha$, if there exists a real constant $c$ such that $\|f(x)\| \leq c \|g'(x)\|$ holds for all $x$ in some neighborhood determined by $l$ (i.e., $\text{IsBigOWith}(c, l, f, g')$ holds), then there exists a nonnegative constant $c' \geq 0$ such that $\text{IsBigOWith}(c', l, f, g')$ also holds.

Asymptotics.IsBigO.exists_nonneg theorem

(h : f =O[l] g') : ∃ c ≥ 0, IsBigOWith c l f g'

Full source

theorem IsBigO.exists_nonneg (h : f =O[l] g') : ∃ c ≥ 0, IsBigOWith c l f g' :=
  let ⟨_c, hc⟩ := h.isBigOWith
  hc.exists_nonneg

Existence of Nonnegative Constant in Big-O Relation

Informal description

If a function $f$ is big O of a function $g'$ along a filter $l$, then there exists a nonnegative constant $c \geq 0$ such that $\|f(x)\| \leq c \|g'(x)\|$ holds for all $x$ in some neighborhood determined by $l$.

Asymptotics.isBigO_iff_eventually_isBigOWith theorem

: f =O[l] g' ↔ ∀ᶠ c in atTop, IsBigOWith c l f g'

Full source

/-- `f = O(g)` if and only if `IsBigOWith c f g` for all sufficiently large `c`. -/
theorem isBigO_iff_eventually_isBigOWith : f =O[l] g'f =O[l] g' ↔ ∀ᶠ c in atTop, IsBigOWith c l f g' :=
  isBigO_iff_isBigOWith.trans
    ⟨fun ⟨c, hc⟩ => mem_atTop_sets.2 ⟨c, fun _c' hc' => hc.weaken hc'⟩, fun h => h.exists⟩

Big-O Characterization via Eventual Bounds: $f =O[l] g' \leftrightarrow \forall c \gg 1, \text{IsBigOWith}(c, l, f, g')$

Informal description

For two functions $f$ and $g'$ defined on a type $\alpha$ with values in normed spaces, and a filter $l$ on $\alpha$, the relation $f =O[l] g'$ holds if and only if for all sufficiently large real constants $c$, the inequality $\|f(x)\| \leq c \|g'(x)\|$ holds for all $x$ in some neighborhood determined by $l$.

Asymptotics.isBigO_iff_eventually theorem

: f =O[l] g' ↔ ∀ᶠ c in atTop, ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g' x‖

Full source

/-- `f = O(g)` if and only if `∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖` for all sufficiently large `c`. -/
theorem isBigO_iff_eventually : f =O[l] g'f =O[l] g' ↔ ∀ᶠ c in atTop, ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g' x‖ :=
  isBigO_iff_eventually_isBigOWith.trans <| by simp only [IsBigOWith_def]

Big-O Characterization via Eventual Bounds: $f =O[l] g' \leftrightarrow \forall c \gg 1, \forall x \in l \text{ eventually}, \|f(x)\| \leq c \|g'(x)\|$

Informal description

For two functions $f$ and $g'$ defined on a type $\alpha$ with values in normed spaces, and a filter $l$ on $\alpha$, the relation $f =O[l] g'$ holds if and only if for all sufficiently large real constants $c$, the inequality $\|f(x)\| \leq c \|g'(x)\|$ holds for all $x$ in some neighborhood determined by $l$.

Asymptotics.IsBigO.exists_mem_basis theorem

 {ι} {p : ι → Prop} {s : ι → Set α} (h : f =O[l] g') (hb : l.HasBasis p s) :
  ∃ c > 0, ∃ i : ι, p i ∧ ∀ x ∈ s i, ‖f x‖ ≤ c * ‖g' x‖

Full source

theorem IsBigO.exists_mem_basis {ι} {p : ι → Prop} {s : ι → Set α} (h : f =O[l] g')
    (hb : l.HasBasis p s) :
    ∃ c > 0, ∃ i : ι, p i ∧ ∀ x ∈ s i, ‖f x‖ ≤ c * ‖g' x‖ :=
  flip Exists.imp h.exists_pos fun c h => by
    simpa only [isBigOWith_iff, hb.eventually_iff, exists_prop] using h

Existence of Local Big-O Bound via Filter Basis

Informal description

Let $f$ and $g'$ be functions from a type $\alpha$ to normed spaces, and let $l$ be a filter on $\alpha$ with a basis consisting of sets $s_i$ indexed by a predicate $p$. If $f$ is big O of $g'$ along $l$ (i.e., $f =O[l] g'$), then there exists a positive constant $c > 0$, an index $i$ such that $p(i)$ holds, and for all $x \in s_i$, the inequality $\|f(x)\| \leq c \|g'(x)\|$ is satisfied.

Asymptotics.isBigOWith_inv theorem

(hc : 0 < c) : IsBigOWith c⁻¹ l f g ↔ ∀ᶠ x in l, c * ‖f x‖ ≤ ‖g x‖

Full source

theorem isBigOWith_inv (hc : 0 < c) : IsBigOWithIsBigOWith c⁻¹ l f g ↔ ∀ᶠ x in l, c * ‖f x‖ ≤ ‖g x‖ := by
  simp only [IsBigOWith_def, ← div_eq_inv_mul, le_div_iff₀' hc]

Big-O With Inverse Constant: $\text{IsBigOWith}(c^{-1}, l, f, g) \leftrightarrow \forall x \in l \text{ eventually}, c \cdot \|f(x)\| \leq \|g(x)\|$

Informal description

For any positive real number $c > 0$, the relation $\text{IsBigOWith}(c^{-1}, l, f, g)$ holds if and only if, for all $x$ in the filter $l$ eventually, $c \cdot \|f(x)\| \leq \|g(x)\|$.

Asymptotics.isLittleO_iff_nat_mul_le_aux theorem

 (h₀ : (∀ x, 0 ≤ ‖f x‖) ∨ ∀ x, 0 ≤ ‖g x‖) : f =o[l] g ↔ ∀ n : ℕ, ∀ᶠ x in l, ↑n * ‖f x‖ ≤ ‖g x‖

Full source

theorem isLittleO_iff_nat_mul_le_aux (h₀ : (∀ x, 0 ≤ ‖f x‖) ∨ ∀ x, 0 ≤ ‖g x‖) :
    f =o[l] gf =o[l] g ↔ ∀ n : ℕ, ∀ᶠ x in l, ↑n * ‖f x‖ ≤ ‖g x‖ := by
  constructor
  · rintro H (_ | n)
    · refine (H.def one_pos).mono fun x h₀' => ?_
      rw [Nat.cast_zero, zero_mul]
      refine h₀.elim (fun hf => (hf x).trans ?_) fun hg => hg x
      rwa [one_mul] at h₀'
    · have : (0 : ℝ) < n.succ := Nat.cast_pos.2 n.succ_pos
      exact (isBigOWith_inv this).1 (H.def' <| inv_pos.2 this)
  · refine fun H => isLittleO_iff.2 fun ε ε0 => ?_
    rcases exists_nat_gt ε⁻¹ with ⟨n, hn⟩
    have hn₀ : (0 : ℝ) < n := (inv_pos.2 ε0).trans hn
    refine ((isBigOWith_inv hn₀).2 (H n)).bound.mono fun x hfg => ?_
    refine hfg.trans (mul_le_mul_of_nonneg_right (inv_le_of_inv_le₀ ε0 hn.le) ?_)
    refine h₀.elim (fun hf => nonneg_of_mul_nonneg_right ((hf x).trans hfg) ?_) fun h => h x
    exact inv_pos.2 hn₀

Characterization of Little-o via Natural Number Multiples

Informal description

Let $f : \alpha \to E$ and $g : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. Suppose that either $\|f(x)\| \geq 0$ for all $x$ or $\|g(x)\| \geq 0$ for all $x$. Then $f = o[l] g$ if and only if for every natural number $n$, there exists a neighborhood in $l$ such that for all $x$ in this neighborhood, $n \cdot \|f(x)\| \leq \|g(x)\|$.

Asymptotics.isLittleO_iff_nat_mul_le theorem

: f =o[l] g' ↔ ∀ n : ℕ, ∀ᶠ x in l, ↑n * ‖f x‖ ≤ ‖g' x‖

Full source

theorem isLittleO_iff_nat_mul_le : f =o[l] g'f =o[l] g' ↔ ∀ n : ℕ, ∀ᶠ x in l, ↑n * ‖f x‖ ≤ ‖g' x‖ :=
  isLittleO_iff_nat_mul_le_aux (Or.inr fun _x => norm_nonneg _)

Characterization of Little-o via Natural Number Multiples: $f = o(l) g' \leftrightarrow \forall n \in \mathbb{N}, \forall x \in l \text{ eventually}, n \cdot \|f(x)\| \leq \|g'(x)\|$

Informal description

Let $f : \alpha \to E$ and $g' : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. Then $f = o[l] g'$ if and only if for every natural number $n$, there exists a neighborhood in $l$ such that for all $x$ in this neighborhood, $n \cdot \|f(x)\| \leq \|g'(x)\|$.

Asymptotics.isLittleO_iff_nat_mul_le' theorem

: f' =o[l] g ↔ ∀ n : ℕ, ∀ᶠ x in l, ↑n * ‖f' x‖ ≤ ‖g x‖

Full source

theorem isLittleO_iff_nat_mul_le' : f' =o[l] gf' =o[l] g ↔ ∀ n : ℕ, ∀ᶠ x in l, ↑n * ‖f' x‖ ≤ ‖g x‖ :=
  isLittleO_iff_nat_mul_le_aux (Or.inl fun _x => norm_nonneg _)

Characterization of Little-o via Natural Number Multiples (Primed Version)

Informal description

Let $f' : \alpha \to E'$ and $g : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. Then $f'$ is little-o of $g$ with respect to $l$ if and only if for every natural number $n$, there exists a neighborhood in $l$ such that for all $x$ in this neighborhood, $n \cdot \|f'(x)\| \leq \|g(x)\|$.

Asymptotics.isLittleO_of_subsingleton theorem

[Subsingleton E'] : f' =o[l] g'

Full source

@[nontriviality]
theorem isLittleO_of_subsingleton [Subsingleton E'] : f' =o[l] g' :=
  IsLittleO.of_bound fun c hc => by simp [Subsingleton.elim (f' _) 0, mul_nonneg hc.le]

Little-o relation for subsingleton-valued functions

Informal description

If the codomain $E'$ of $f'$ is a subsingleton (i.e., has at most one element), then $f'$ is little-o of $g'$ with respect to the filter $l$.

Asymptotics.isBigO_of_subsingleton theorem

[Subsingleton E'] : f' =O[l] g'

Full source

@[nontriviality]
theorem isBigO_of_subsingleton [Subsingleton E'] : f' =O[l] g' :=
  isLittleO_of_subsingleton.isBigO

Big-O relation for subsingleton-valued functions

Informal description

If the codomain $E'$ of the function $f'$ is a subsingleton (i.e., has at most one element), then $f'$ is big-O of $g'$ along the filter $l$.

Asymptotics.isBigOWith_congr theorem

 (hc : c₁ = c₂) (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) : IsBigOWith c₁ l f₁ g₁ ↔ IsBigOWith c₂ l f₂ g₂

Full source

theorem isBigOWith_congr (hc : c₁ = c₂) (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) :
    IsBigOWithIsBigOWith c₁ l f₁ g₁ ↔ IsBigOWith c₂ l f₂ g₂ := by
  simp only [IsBigOWith_def]
  subst c₂
  apply Filter.eventually_congr
  filter_upwards [hf, hg] with _ e₁ e₂
  rw [e₁, e₂]

Congruence of Big-O With Relation Under Eventual Equality

Informal description

For real constants $c_1$ and $c_2$ such that $c_1 = c_2$, and functions $f_1, f_2, g_1, g_2$ such that $f_1$ and $f_2$ are eventually equal along the filter $l$, and $g_1$ and $g_2$ are eventually equal along $l$, the relation $\text{IsBigOWith}(c_1, l, f_1, g_1)$ holds if and only if $\text{IsBigOWith}(c_2, l, f_2, g_2)$ holds.

Asymptotics.IsBigOWith.congr' theorem

 (h : IsBigOWith c₁ l f₁ g₁) (hc : c₁ = c₂) (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) : IsBigOWith c₂ l f₂ g₂

Full source

theorem IsBigOWith.congr' (h : IsBigOWith c₁ l f₁ g₁) (hc : c₁ = c₂) (hf : f₁ =ᶠ[l] f₂)
    (hg : g₁ =ᶠ[l] g₂) : IsBigOWith c₂ l f₂ g₂ :=
  (isBigOWith_congr hc hf hg).mp h

Big-O With Relation Preserved Under Eventual Equality

Informal description

Let $c_1, c_2$ be real constants with $c_1 = c_2$, and let $f_1, f_2 : \alpha \to E$ and $g_1, g_2 : \alpha \to F$ be functions such that $f_1$ and $f_2$ are eventually equal along the filter $l$, and $g_1$ and $g_2$ are eventually equal along $l$. If $\text{IsBigOWith}(c_1, l, f_1, g_1)$ holds, then $\text{IsBigOWith}(c_2, l, f_2, g_2)$ also holds.

Asymptotics.IsBigOWith.congr theorem

 (h : IsBigOWith c₁ l f₁ g₁) (hc : c₁ = c₂) (hf : ∀ x, f₁ x = f₂ x) (hg : ∀ x, g₁ x = g₂ x) : IsBigOWith c₂ l f₂ g₂

Full source

theorem IsBigOWith.congr (h : IsBigOWith c₁ l f₁ g₁) (hc : c₁ = c₂) (hf : ∀ x, f₁ x = f₂ x)
    (hg : ∀ x, g₁ x = g₂ x) : IsBigOWith c₂ l f₂ g₂ :=
  h.congr' hc (univ_mem' hf) (univ_mem' hg)

Big-O With Relation Preserved Under Pointwise Equality

Informal description

Let $c_1, c_2$ be real constants with $c_1 = c_2$, and let $f_1, f_2 : \alpha \to E$ and $g_1, g_2 : \alpha \to F$ be functions such that $f_1(x) = f_2(x)$ and $g_1(x) = g_2(x)$ for all $x \in \alpha$. If $\text{IsBigOWith}(c_1, l, f_1, g_1)$ holds, then $\text{IsBigOWith}(c_2, l, f_2, g_2)$ also holds.

Asymptotics.IsBigOWith.congr_left theorem

(h : IsBigOWith c l f₁ g) (hf : ∀ x, f₁ x = f₂ x) : IsBigOWith c l f₂ g

Full source

theorem IsBigOWith.congr_left (h : IsBigOWith c l f₁ g) (hf : ∀ x, f₁ x = f₂ x) :
    IsBigOWith c l f₂ g :=
  h.congr rfl hf fun _ => rfl

Big-O With Relation Preserved Under Left Pointwise Equality

Informal description

Let $c$ be a real constant, $l$ a filter on a type $\alpha$, and $g : \alpha \to F$ a function where $F$ is a normed space. For two functions $f_1, f_2 : \alpha \to E$ where $E$ is a normed space, if $\text{IsBigOWith}(c, l, f_1, g)$ holds and $f_1(x) = f_2(x)$ for all $x \in \alpha$, then $\text{IsBigOWith}(c, l, f_2, g)$ also holds.

Asymptotics.IsBigOWith.congr_right theorem

(h : IsBigOWith c l f g₁) (hg : ∀ x, g₁ x = g₂ x) : IsBigOWith c l f g₂

Full source

theorem IsBigOWith.congr_right (h : IsBigOWith c l f g₁) (hg : ∀ x, g₁ x = g₂ x) :
    IsBigOWith c l f g₂ :=
  h.congr rfl (fun _ => rfl) hg

Big-O With Relation Preserved Under Right Function Equality

Informal description

Let $f : \alpha \to E$ and $g_1, g_2 : \alpha \to F$ be functions, where $E$ and $F$ are normed spaces, and let $l$ be a filter on $\alpha$. If $\text{IsBigOWith}(c, l, f, g_1)$ holds and $g_1(x) = g_2(x)$ for all $x \in \alpha$, then $\text{IsBigOWith}(c, l, f, g_2)$ also holds.

Asymptotics.IsBigOWith.congr_const theorem

(h : IsBigOWith c₁ l f g) (hc : c₁ = c₂) : IsBigOWith c₂ l f g

Full source

theorem IsBigOWith.congr_const (h : IsBigOWith c₁ l f g) (hc : c₁ = c₂) : IsBigOWith c₂ l f g :=
  h.congr hc (fun _ => rfl) fun _ => rfl

Big-O With Relation Preserved Under Constant Change

Informal description

Let $f$ and $g$ be functions and $l$ a filter. If $\text{IsBigOWith}(c_1, l, f, g)$ holds and $c_1 = c_2$, then $\text{IsBigOWith}(c_2, l, f, g)$ also holds.

Asymptotics.isBigO_congr theorem

(hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) : f₁ =O[l] g₁ ↔ f₂ =O[l] g₂

Full source

theorem isBigO_congr (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) : f₁ =O[l] g₁f₁ =O[l] g₁ ↔ f₂ =O[l] g₂ := by
  simp only [IsBigO_def]
  exact exists_congr fun c => isBigOWith_congr rfl hf hg

Big-O Congruence under Eventual Equality

Informal description

For functions $f_1, f_2, g_1, g_2$ and a filter $l$, if $f_1$ and $f_2$ are eventually equal along $l$, and $g_1$ and $g_2$ are eventually equal along $l$, then $f_1$ is big-O of $g_1$ along $l$ if and only if $f_2$ is big-O of $g_2$ along $l$.

Asymptotics.IsBigO.congr' theorem

(h : f₁ =O[l] g₁) (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) : f₂ =O[l] g₂

Full source

theorem IsBigO.congr' (h : f₁ =O[l] g₁) (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) : f₂ =O[l] g₂ :=
  (isBigO_congr hf hg).mp h

Big-O Preservation under Eventual Equality

Informal description

Let $f_1, f_2, g_1, g_2$ be functions and $l$ a filter. If $f_1$ is big-O of $g_1$ along $l$ (i.e., $f_1 =O[l] g_1$), and $f_1$ is eventually equal to $f_2$ along $l$, and $g_1$ is eventually equal to $g_2$ along $l$, then $f_2$ is big-O of $g_2$ along $l$ (i.e., $f_2 =O[l] g_2$).

Asymptotics.IsBigO.congr theorem

(h : f₁ =O[l] g₁) (hf : ∀ x, f₁ x = f₂ x) (hg : ∀ x, g₁ x = g₂ x) : f₂ =O[l] g₂

Full source

theorem IsBigO.congr (h : f₁ =O[l] g₁) (hf : ∀ x, f₁ x = f₂ x) (hg : ∀ x, g₁ x = g₂ x) :
    f₂ =O[l] g₂ :=
  h.congr' (univ_mem' hf) (univ_mem' hg)

Big-O Preservation under Pointwise Equality

Informal description

Let $f_1, f_2, g_1, g_2$ be functions and $l$ a filter. If $f_1$ is big-O of $g_1$ along $l$ (i.e., $f_1 =O[l] g_1$), and for all $x$, $f_1(x) = f_2(x)$ and $g_1(x) = g_2(x)$, then $f_2$ is big-O of $g_2$ along $l$ (i.e., $f_2 =O[l] g_2$).

Asymptotics.IsBigO.congr_left theorem

(h : f₁ =O[l] g) (hf : ∀ x, f₁ x = f₂ x) : f₂ =O[l] g

Full source

theorem IsBigO.congr_left (h : f₁ =O[l] g) (hf : ∀ x, f₁ x = f₂ x) : f₂ =O[l] g :=
  h.congr hf fun _ => rfl

Big-O Preservation under Left Pointwise Equality

Informal description

Let $f_1, f_2, g$ be functions and $l$ a filter. If $f_1$ is big-O of $g$ along $l$ (i.e., $f_1 =O[l] g$), and for all $x$, $f_1(x) = f_2(x)$, then $f_2$ is big-O of $g$ along $l$ (i.e., $f_2 =O[l] g$).

Asymptotics.IsBigO.congr_right theorem

(h : f =O[l] g₁) (hg : ∀ x, g₁ x = g₂ x) : f =O[l] g₂

Full source

theorem IsBigO.congr_right (h : f =O[l] g₁) (hg : ∀ x, g₁ x = g₂ x) : f =O[l] g₂ :=
  h.congr (fun _ => rfl) hg

Big-O Preservation under Right Function Equality

Informal description

Let $f$, $g_1$, and $g_2$ be functions and $l$ a filter. If $f$ is big-O of $g_1$ along $l$ (i.e., $f =O[l] g_1$), and for all $x$, $g_1(x) = g_2(x)$, then $f$ is big-O of $g_2$ along $l$ (i.e., $f =O[l] g_2$).

Asymptotics.isLittleO_congr theorem

(hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) : f₁ =o[l] g₁ ↔ f₂ =o[l] g₂

Full source

theorem isLittleO_congr (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) : f₁ =o[l] g₁f₁ =o[l] g₁ ↔ f₂ =o[l] g₂ := by
  simp only [IsLittleO_def]
  exact forall₂_congr fun c _hc => isBigOWith_congr (Eq.refl c) hf hg

Little-o Congruence Under Eventual Equality

Informal description

For functions $f_1, f_2 : \alpha \to E$ and $g_1, g_2 : \alpha \to F$ where $E$ and $F$ are normed spaces, and a filter $l$ on $\alpha$, if $f_1$ and $f_2$ are eventually equal along $l$ and $g_1$ and $g_2$ are eventually equal along $l$, then $f_1 = o[l] g_1$ if and only if $f_2 = o[l] g_2$. Here, $f = o[l] g$ means that for every $c > 0$, there exists a neighborhood in $l$ such that for all $x$ in this neighborhood, $\|f(x)\| \leq c \|g(x)\|$.

Asymptotics.IsLittleO.congr' theorem

(h : f₁ =o[l] g₁) (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) : f₂ =o[l] g₂

Full source

theorem IsLittleO.congr' (h : f₁ =o[l] g₁) (hf : f₁ =ᶠ[l] f₂) (hg : g₁ =ᶠ[l] g₂) : f₂ =o[l] g₂ :=
  (isLittleO_congr hf hg).mp h

Little-o Congruence Under Eventual Equality (Variant)

Informal description

Let $f_1, f_2 : \alpha \to E$ and $g_1, g_2 : \alpha \to F$ be functions where $E$ and $F$ are normed spaces, and let $l$ be a filter on $\alpha$. If $f_1 = o[l] g_1$, and $f_1$ is eventually equal to $f_2$ along $l$, and $g_1$ is eventually equal to $g_2$ along $l$, then $f_2 = o[l] g_2$. Here, $f = o[l] g$ means that for every $c > 0$, there exists a neighborhood in $l$ such that for all $x$ in this neighborhood, $\|f(x)\| \leq c \|g(x)\|$.

Asymptotics.IsLittleO.congr theorem

(h : f₁ =o[l] g₁) (hf : ∀ x, f₁ x = f₂ x) (hg : ∀ x, g₁ x = g₂ x) : f₂ =o[l] g₂

Full source

theorem IsLittleO.congr (h : f₁ =o[l] g₁) (hf : ∀ x, f₁ x = f₂ x) (hg : ∀ x, g₁ x = g₂ x) :
    f₂ =o[l] g₂ :=
  h.congr' (univ_mem' hf) (univ_mem' hg)

Little-o Congruence Under Pointwise Equality

Informal description

Let $f_1, f_2 : \alpha \to E$ and $g_1, g_2 : \alpha \to F$ be functions where $E$ and $F$ are normed spaces, and let $l$ be a filter on $\alpha$. If $f_1 = o[l] g_1$, and $f_1(x) = f_2(x)$ for all $x$, and $g_1(x) = g_2(x)$ for all $x$, then $f_2 = o[l] g_2$. Here, $f = o[l] g$ means that for every $c > 0$, there exists a neighborhood in $l$ such that for all $x$ in this neighborhood, $\|f(x)\| \leq c \|g(x)\|$.

Asymptotics.IsLittleO.congr_left theorem

(h : f₁ =o[l] g) (hf : ∀ x, f₁ x = f₂ x) : f₂ =o[l] g

Full source

theorem IsLittleO.congr_left (h : f₁ =o[l] g) (hf : ∀ x, f₁ x = f₂ x) : f₂ =o[l] g :=
  h.congr hf fun _ => rfl

Little-o Congruence Under Pointwise Equality (Left Variant)

Informal description

Let $f_1, f_2 : \alpha \to E$ and $g : \alpha \to F$ be functions, where $E$ and $F$ are normed spaces, and let $l$ be a filter on $\alpha$. If $f_1 = o[l] g$ and $f_1(x) = f_2(x)$ for all $x$, then $f_2 = o[l] g$. Here, $f = o[l] g$ means that for every $c > 0$, there exists a neighborhood in $l$ such that for all $x$ in this neighborhood, $\|f(x)\| \leq c \|g(x)\|$.

Asymptotics.IsLittleO.congr_right theorem

(h : f =o[l] g₁) (hg : ∀ x, g₁ x = g₂ x) : f =o[l] g₂

Full source

theorem IsLittleO.congr_right (h : f =o[l] g₁) (hg : ∀ x, g₁ x = g₂ x) : f =o[l] g₂ :=
  h.congr (fun _ => rfl) hg

Little-o Congruence Under Right Pointwise Equality

Informal description

Let $f : \alpha \to E$ and $g_1, g_2 : \alpha \to F$ be functions where $E$ and $F$ are normed spaces, and let $l$ be a filter on $\alpha$. If $f = o[l] g_1$ and $g_1(x) = g_2(x)$ for all $x$, then $f = o[l] g_2$. Here, $f = o[l] g$ means that for every $c > 0$, there exists a neighborhood in $l$ such that for all $x$ in this neighborhood, $\|f(x)\| \leq c \|g(x)\|$.

Filter.EventuallyEq.trans_isBigO theorem

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

Full source

@[trans]
theorem _root_.Filter.EventuallyEq.trans_isBigO {f₁ f₂ : α → E} {g : α → F} (hf : f₁ =ᶠ[l] f₂)
    (h : f₂ =O[l] g) : f₁ =O[l] g :=
  h.congr' hf.symm EventuallyEq.rfl

Big-O Preservation under Eventual Equality of Functions

Informal description

Let $f_1, f_2 : \alpha \to E$ and $g : \alpha \to F$ be functions, and let $l$ be a filter on $\alpha$. If $f_1$ is eventually equal to $f_2$ along $l$ (i.e., $f_1 =ᶠ[l] f_2$) and $f_2$ is big-O of $g$ along $l$ (i.e., $f_2 =O[l] g$), then $f_1$ is big-O of $g$ along $l$ (i.e., $f_1 =O[l] g$).

Asymptotics.transEventuallyEqIsBigO instance

: @Trans (α → E) (α → E) (α → F) (· =ᶠ[l] ·) (· =O[l] ·) (· =O[l] ·)

Full source

instance transEventuallyEqIsBigO :
    @Trans (α → E) (α → E) (α → F) (· =ᶠ[l] ·) (· =O[l] ·) (· =O[l] ·) where
  trans := Filter.EventuallyEq.trans_isBigO

Transitivity of Big-O with Eventual Equality

Informal description

The relation $\cdot =O[l] \cdot$ is transitive with respect to eventual equality along the filter $l$. That is, for functions $f_1, f_2 : \alpha \to E$ and $g : \alpha \to F$, if $f_1$ is eventually equal to $f_2$ along $l$ and $f_2$ is big-O of $g$ along $l$, then $f_1$ is big-O of $g$ along $l$.

Filter.EventuallyEq.trans_isLittleO theorem

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

Full source

@[trans]
theorem _root_.Filter.EventuallyEq.trans_isLittleO {f₁ f₂ : α → E} {g : α → F} (hf : f₁ =ᶠ[l] f₂)
    (h : f₂ =o[l] g) : f₁ =o[l] g :=
  h.congr' hf.symm EventuallyEq.rfl

Transitivity of Little-o under Eventual Equality

Informal description

Let $f_1, f_2 : \alpha \to E$ and $g : \alpha \to F$ be functions where $E$ and $F$ are normed spaces, and let $l$ be a filter on $\alpha$. If $f_1$ is eventually equal to $f_2$ along $l$ and $f_2 = o[l] g$, then $f_1 = o[l] g$. Here, $f = o[l] g$ means that for every $c > 0$, there exists a neighborhood in $l$ such that for all $x$ in this neighborhood, $\|f(x)\| \leq c \|g(x)\|$.

Asymptotics.transEventuallyEqIsLittleO instance

: @Trans (α → E) (α → E) (α → F) (· =ᶠ[l] ·) (· =o[l] ·) (· =o[l] ·)

Full source

instance transEventuallyEqIsLittleO :
    @Trans (α → E) (α → E) (α → F) (· =ᶠ[l] ·) (· =o[l] ·) (· =o[l] ·) where
  trans := Filter.EventuallyEq.trans_isLittleO

Transitivity of Little-o under Eventual Equality

Informal description

The relation $\cdot =o[l] \cdot$ on functions is transitive with respect to eventual equality. That is, for functions $f_1, f_2 : \alpha \to E$ and $g : \alpha \to F$, if $f_1$ is eventually equal to $f_2$ along the filter $l$ and $f_2$ is little-o of $g$ along $l$, then $f_1$ is little-o of $g$ along $l$.

Asymptotics.IsBigO.trans_eventuallyEq theorem

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

Full source

@[trans]
theorem IsBigO.trans_eventuallyEq {f : α → E} {g₁ g₂ : α → F} (h : f =O[l] g₁) (hg : g₁ =ᶠ[l] g₂) :
    f =O[l] g₂ :=
  h.congr' EventuallyEq.rfl hg

Big-O Preservation under Eventual Equality of Dominant Functions

Informal description

Let $f : \alpha \to E$ and $g_1, g_2 : \alpha \to F$ be functions, and let $l$ be a filter on $\alpha$. If $f$ is big-O of $g_1$ along $l$ (i.e., $f =O[l] g_1$) and $g_1$ is eventually equal to $g_2$ along $l$, then $f$ is big-O of $g_2$ along $l$ (i.e., $f =O[l] g_2$).

Asymptotics.transIsBigOEventuallyEq instance

: @Trans (α → E) (α → F) (α → F) (· =O[l] ·) (· =ᶠ[l] ·) (· =O[l] ·)

Full source

instance transIsBigOEventuallyEq :
    @Trans (α → E) (α → F) (α → F) (· =O[l] ·) (· =ᶠ[l] ·) (· =O[l] ·) where
  trans := IsBigO.trans_eventuallyEq

Transitivity of Big-O with Eventual Equality

Informal description

The relation $\cdot =O[l] \cdot$ between functions is transitive with respect to eventual equality along the filter $l$. That is, if $f : \alpha \to E$ is big-O of $g_1 : \alpha \to F$ along $l$, and $g_1$ is eventually equal to $g_2 : \alpha \to F$ along $l$, then $f$ is also big-O of $g_2$ along $l$.

Asymptotics.IsLittleO.trans_eventuallyEq theorem

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

Full source

@[trans]
theorem IsLittleO.trans_eventuallyEq {f : α → E} {g₁ g₂ : α → F} (h : f =o[l] g₁)
    (hg : g₁ =ᶠ[l] g₂) : f =o[l] g₂ :=
  h.congr' EventuallyEq.rfl hg

Little-o Preservation under Eventual Equality of Dominant Functions

Informal description

Let $f : \alpha \to E$ and $g_1, g_2 : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If $f = o[l] g_1$ and $g_1$ is eventually equal to $g_2$ along $l$, then $f = o[l] g_2$. Here, $f = o[l] g$ means that for every $c > 0$, there exists a neighborhood in $l$ such that for all $x$ in this neighborhood, $\|f(x)\| \leq c \|g(x)\|$.

Asymptotics.transIsLittleOEventuallyEq instance

: @Trans (α → E) (α → F) (α → F) (· =o[l] ·) (· =ᶠ[l] ·) (· =o[l] ·)

Full source

instance transIsLittleOEventuallyEq :
    @Trans (α → E) (α → F) (α → F) (· =o[l] ·) (· =ᶠ[l] ·) (· =o[l] ·) where
  trans := IsLittleO.trans_eventuallyEq

Transitivity of Little-o with Eventual Equality

Informal description

The relation $\cdot = o[l] \cdot$ between functions $\alpha \to E$ and $\alpha \to F$ is transitive with respect to eventual equality. That is, if $f = o[l] g_1$ and $g_1$ is eventually equal to $g_2$ along the filter $l$, then $f = o[l] g_2$.

Asymptotics.IsBigOWith.comp_tendsto theorem

 (hcfg : IsBigOWith c l f g) {k : β → α} {l' : Filter β} (hk : Tendsto k l' l) : IsBigOWith c l' (f ∘ k) (g ∘ k)

Full source

theorem IsBigOWith.comp_tendsto (hcfg : IsBigOWith c l f g) {k : β → α} {l' : Filter β}
    (hk : Tendsto k l' l) : IsBigOWith c l' (f ∘ k) (g ∘ k) :=
  IsBigOWith.of_bound <| hk hcfg.bound

Composition Preserves Big-O Bound Under Tendsto

Informal description

Let $f: \alpha \to E$ and $g: \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If $f$ is big-O of $g$ along $l$ with constant $c$ (i.e., $\text{IsBigOWith}(c, l, f, g)$ holds), and $k: \beta \to \alpha$ is a function such that $k$ tends to $l$ along a filter $l'$ on $\beta$, then the composition $f \circ k$ is big-O of $g \circ k$ along $l'$ with the same constant $c$.

Asymptotics.IsBigO.comp_tendsto theorem

(hfg : f =O[l] g) {k : β → α} {l' : Filter β} (hk : Tendsto k l' l) : (f ∘ k) =O[l'] (g ∘ k)

Full source

theorem IsBigO.comp_tendsto (hfg : f =O[l] g) {k : β → α} {l' : Filter β} (hk : Tendsto k l' l) :
    (f ∘ k) =O[l'] (g ∘ k) :=
  isBigO_iff_isBigOWith.2 <| hfg.isBigOWith.imp fun _c h => h.comp_tendsto hk

Composition Preserves Big-O Relation Under Filter Convergence

Informal description

Let $f : \alpha \to E$ and $g : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If $f$ is big-O of $g$ along $l$ (i.e., $f =O[l] g$), and $k : \beta \to \alpha$ is a function such that $k$ tends to $l$ along a filter $l'$ on $\beta$, then the composition $f \circ k$ is big-O of $g \circ k$ along $l'$ (i.e., $(f \circ k) =O[l'] (g \circ k)$).

Asymptotics.IsLittleO.comp_tendsto theorem

(hfg : f =o[l] g) {k : β → α} {l' : Filter β} (hk : Tendsto k l' l) : (f ∘ k) =o[l'] (g ∘ k)

Full source

theorem IsLittleO.comp_tendsto (hfg : f =o[l] g) {k : β → α} {l' : Filter β} (hk : Tendsto k l' l) :
    (f ∘ k) =o[l'] (g ∘ k) :=
  IsLittleO.of_isBigOWith fun _c cpos => (hfg.forall_isBigOWith cpos).comp_tendsto hk

Composition Preserves Little-o Relation Under Tendsto

Informal description

Let $f : \alpha \to E$ and $g : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If $f = o[l] g$ (i.e., $f$ is little-o of $g$ along $l$), and $k : \beta \to \alpha$ is a function such that $k$ tends to $l$ along a filter $l'$ on $\beta$, then the composition $f \circ k$ is little-o of $g \circ k$ along $l'$.

Asymptotics.isBigOWith_map theorem

{k : β → α} {l : Filter β} : IsBigOWith c (map k l) f g ↔ IsBigOWith c l (f ∘ k) (g ∘ k)

Full source

@[simp]
theorem isBigOWith_map {k : β → α} {l : Filter β} :
    IsBigOWithIsBigOWith c (map k l) f g ↔ IsBigOWith c l (f ∘ k) (g ∘ k) := by
  simp only [IsBigOWith_def]
  exact eventually_map

Big-O Relation Preservation under Function Composition: $f = O[\text{map } k \ l] g \leftrightarrow f \circ k = O[l] g \circ k$

Informal description

For a function $k : \beta \to \alpha$, a filter $l$ on $\beta$, and functions $f, g : \alpha \to E$ where $E$ is a normed space, the following are equivalent: 1. There exists a constant $c > 0$ such that $\|f(x)\| \leq c \|g(x)\|$ for all $x$ in the pushforward filter $\text{map } k \ l$; 2. There exists a constant $c > 0$ such that $\|f(k(y))\| \leq c \|g(k(y))\|$ for all $y$ in the filter $l$. In other words, $f$ is big-O of $g$ with constant $c$ along $\text{map } k \ l$ if and only if $f \circ k$ is big-O of $g \circ k$ with the same constant $c$ along $l$.

Asymptotics.isBigO_map theorem

{k : β → α} {l : Filter β} : f =O[map k l] g ↔ (f ∘ k) =O[l] (g ∘ k)

Full source

@[simp]
theorem isBigO_map {k : β → α} {l : Filter β} : f =O[map k l] gf =O[map k l] g ↔ (f ∘ k) =O[l] (g ∘ k) := by
  simp only [IsBigO_def, isBigOWith_map]

Big-O Relation under Function Composition: $f \circ k = O[l] g \circ k \leftrightarrow f = O[\text{map } k \ l] g$

Informal description

For functions $f, g : \alpha \to E$ and a map $k : \beta \to \alpha$, the relation $f = O[\text{map } k \ l] g$ holds if and only if the composition $f \circ k = O[l] g \circ k$ holds in the filter $l$ on $\beta$. In other words, $f$ is big-O of $g$ along the pushforward filter $\text{map } k \ l$ if and only if the precomposition of $f$ and $g$ with $k$ satisfies the big-O relation in the original filter $l$.

Asymptotics.isLittleO_map theorem

{k : β → α} {l : Filter β} : f =o[map k l] g ↔ (f ∘ k) =o[l] (g ∘ k)

Full source

@[simp]
theorem isLittleO_map {k : β → α} {l : Filter β} : f =o[map k l] gf =o[map k l] g ↔ (f ∘ k) =o[l] (g ∘ k) := by
  simp only [IsLittleO_def, isBigOWith_map]

Little-o Relation under Function Composition: $f \circ k = o[l] g \circ k \leftrightarrow f = o[\text{map } k \ l] g$

Informal description

For functions $f, g : \alpha \to E$ and a map $k : \beta \to \alpha$, the relation $f = o[\text{map } k \ l] g$ holds if and only if the composition $f \circ k = o[l] g \circ k$ holds in the filter $l$ on $\beta$. In other words, $f$ is little-o of $g$ along the pushforward filter $\text{map } k \ l$ if and only if the precomposition of $f$ and $g$ with $k$ satisfies the little-o relation in the original filter $l$.

Asymptotics.IsBigOWith.mono theorem

(h : IsBigOWith c l' f g) (hl : l ≤ l') : IsBigOWith c l f g

Full source

theorem IsBigOWith.mono (h : IsBigOWith c l' f g) (hl : l ≤ l') : IsBigOWith c l f g :=
  IsBigOWith.of_bound <| hl h.bound

Big-O Relation is Preserved Under Filter Refinement

Informal description

Let $f : \alpha \to E$ and $g : \alpha \to F$ be functions to normed spaces, and let $l, l'$ be filters on $\alpha$. If $f$ is big-O of $g$ with constant $c$ along $l'$ (i.e., $\text{IsBigOWith}(c, l', f, g)$ holds) and $l$ is a finer filter than $l'$ (i.e., $l \leq l'$), then $f$ is big-O of $g$ with constant $c$ along $l$ (i.e., $\text{IsBigOWith}(c, l, f, g)$ holds).

Asymptotics.IsBigO.mono theorem

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

Full source

theorem IsBigO.mono (h : f =O[l'] g) (hl : l ≤ l') : f =O[l] g :=
  isBigO_iff_isBigOWith.2 <| h.isBigOWith.imp fun _c h => h.mono hl

Big-O Relation is Preserved Under Filter Refinement

Informal description

Let $f : \alpha \to E$ and $g : \alpha \to F$ be functions to normed spaces, and let $l, l'$ be filters on $\alpha$. If $f$ is big-O of $g$ along $l'$ (i.e., $f =O[l'] g$) and $l$ is a finer filter than $l'$ (i.e., $l \leq l'$), then $f$ is big-O of $g$ along $l$ (i.e., $f =O[l] g$).

Asymptotics.IsLittleO.mono theorem

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

Full source

theorem IsLittleO.mono (h : f =o[l'] g) (hl : l ≤ l') : f =o[l] g :=
  IsLittleO.of_isBigOWith fun _c cpos => (h.forall_isBigOWith cpos).mono hl

Little-o Relation is Preserved Under Filter Refinement

Informal description

Let $f : \alpha \to E$ and $g : \alpha \to F$ be functions to normed spaces, and let $l, l'$ be filters on $\alpha$. If $f$ is little-o of $g$ along $l'$ (i.e., $f = o[l'] g$) and $l$ is a finer filter than $l'$ (i.e., $l \leq l'$), then $f$ is little-o of $g$ along $l$ (i.e., $f = o[l] g$).

Asymptotics.IsBigOWith.trans theorem

(hfg : IsBigOWith c l f g) (hgk : IsBigOWith c' l g k) (hc : 0 ≤ c) : IsBigOWith (c * c') l f k

Full source

theorem IsBigOWith.trans (hfg : IsBigOWith c l f g) (hgk : IsBigOWith c' l g k) (hc : 0 ≤ c) :
    IsBigOWith (c * c') l f k := by
  simp only [IsBigOWith_def] at *
  filter_upwards [hfg, hgk] with x hx hx'
  calc
    ‖f x‖ ≤ c * ‖g x‖ := hx
    _ ≤ c * (c' * ‖k x‖) := by gcongr
    _ = c * c' * ‖k x‖ := (mul_assoc _ _ _).symm

Transitivity of Big-O With Constants: $\text{IsBigOWith}(c, l, f, g) \land \text{IsBigOWith}(c', l, g, k) \to \text{IsBigOWith}(c \cdot c', l, f, k)$

Informal description

Let $f : \alpha \to E$, $g : \alpha \to F$, and $k : \alpha \to G$ be functions to normed spaces, and let $l$ be a filter on $\alpha$. Suppose that: 1. There exists a constant $c \geq 0$ such that $\|f(x)\| \leq c \|g(x)\|$ for all $x$ in $l$ eventually. 2. There exists a constant $c' \geq 0$ such that $\|g(x)\| \leq c' \|k(x)\|$ for all $x$ in $l$ eventually. Then, there exists a constant $c \cdot c' \geq 0$ such that $\|f(x)\| \leq c \cdot c' \|k(x)\|$ for all $x$ in $l$ eventually.

Asymptotics.IsBigO.trans theorem

{f : α → E} {g : α → F'} {k : α → G} (hfg : f =O[l] g) (hgk : g =O[l] k) : f =O[l] k

Full source

@[trans]
theorem IsBigO.trans {f : α → E} {g : α → F'} {k : α → G} (hfg : f =O[l] g) (hgk : g =O[l] k) :
    f =O[l] k :=
  let ⟨_c, cnonneg, hc⟩ := hfg.exists_nonneg
  let ⟨_c', hc'⟩ := hgk.isBigOWith
  (hc.trans hc' cnonneg).isBigO

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

Informal description

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

Asymptotics.transIsBigOIsBigO instance

: @Trans (α → E) (α → F') (α → G) (· =O[l] ·) (· =O[l] ·) (· =O[l] ·)

Full source

instance transIsBigOIsBigO :
    @Trans (α → E) (α → F') (α → G) (· =O[l] ·) (· =O[l] ·) (· =O[l] ·) where
  trans := IsBigO.trans

Transitivity of Big-O Relations

Informal description

The big-O relation `=O[l]` is transitive. That is, for functions $f : \alpha \to E$, $g : \alpha \to F'$, and $k : \alpha \to G$ to normed spaces and a filter $l$ on $\alpha$, if $f =O[l] g$ and $g =O[l] k$, then $f =O[l] k$.

Asymptotics.IsLittleO.trans_isBigOWith theorem

(hfg : f =o[l] g) (hgk : IsBigOWith c l g k) (hc : 0 < c) : f =o[l] k

Full source

theorem IsLittleO.trans_isBigOWith (hfg : f =o[l] g) (hgk : IsBigOWith c l g k) (hc : 0 < c) :
    f =o[l] k := by
  simp only [IsLittleO_def] at *
  intro c' c'pos
  have : 0 < c' / c := div_pos c'pos hc
  exact ((hfg this).trans hgk this.le).congr_const (div_mul_cancel₀ _ hc.ne')

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

Informal description

Let $f : \alpha \to E$, $g : \alpha \to F$, and $k : \alpha \to G$ be functions to normed spaces, and let $l$ be a filter on $\alpha$. Suppose that: 1. $f = o[l] g$ (i.e., $f$ is little-o of $g$ with respect to $l$) 2. There exists a constant $c > 0$ such that $\|g(x)\| \leq c \|k(x)\|$ for all $x$ in $l$ eventually. Then $f = o[l] k$ (i.e., $f$ is little-o of $k$ with respect to $l$).

Asymptotics.IsLittleO.trans_isBigO theorem

{f : α → E} {g : α → F} {k : α → G'} (hfg : f =o[l] g) (hgk : g =O[l] k) : f =o[l] k

Full source

@[trans]
theorem IsLittleO.trans_isBigO {f : α → E} {g : α → F} {k : α → G'} (hfg : f =o[l] g)
    (hgk : g =O[l] k) : f =o[l] k :=
  let ⟨_c, cpos, hc⟩ := hgk.exists_pos
  hfg.trans_isBigOWith hc cpos

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

Informal description

Let $f : \alpha \to E$, $g : \alpha \to F$, and $k : \alpha \to G'$ be functions to normed spaces, and let $l$ be a filter on $\alpha$. If $f$ is little-o of $g$ with respect to $l$ (i.e., $f = o[l] g$) and $g$ is big-O of $k$ with respect to $l$ (i.e., $g = O[l] k$), then $f$ is little-o of $k$ with respect to $l$ (i.e., $f = o[l] k$).

Asymptotics.transIsLittleOIsBigO instance

: @Trans (α → E) (α → F) (α → G') (· =o[l] ·) (· =O[l] ·) (· =o[l] ·)

Full source

instance transIsLittleOIsBigO :
    @Trans (α → E) (α → F) (α → G') (· =o[l] ·) (· =O[l] ·) (· =o[l] ·) where
  trans := IsLittleO.trans_isBigO

Transitivity of Little-o and Big-O Relations

Informal description

The relation $\cdot =o[l] \cdot$ is transitive with $\cdot =O[l] \cdot$ in the sense that if $f =o[l] g$ and $g =O[l] k$, then $f =o[l] k$ for functions $f : \alpha \to E$, $g : \alpha \to F$, and $k : \alpha \to G'$ with respect to a filter $l$ on $\alpha$.

Asymptotics.IsBigOWith.trans_isLittleO theorem

(hfg : IsBigOWith c l f g) (hgk : g =o[l] k) (hc : 0 < c) : f =o[l] k

Full source

theorem IsBigOWith.trans_isLittleO (hfg : IsBigOWith c l f g) (hgk : g =o[l] k) (hc : 0 < c) :
    f =o[l] k := by
  simp only [IsLittleO_def] at *
  intro c' c'pos
  have : 0 < c' / c := div_pos c'pos hc
  exact (hfg.trans (hgk this) hc.le).congr_const (mul_div_cancel₀ _ hc.ne')

Transitivity of Big-O With and Little-O: $\text{IsBigOWith}(c, l, f, g) \land g = o[l] k \to f = o[l] k$

Informal description

Let $f : \alpha \to E$, $g : \alpha \to F$, and $k : \alpha \to G$ be functions to normed spaces, and let $l$ be a filter on $\alpha$. Suppose that: 1. There exists a constant $c > 0$ such that $\|f(x)\| \leq c \|g(x)\|$ for all $x$ in $l$ eventually. 2. The function $g$ is little-o of $k$ with respect to $l$, i.e., $g = o[l] k$. Then, $f$ is little-o of $k$ with respect to $l$, i.e., $f = o[l] k$.

Asymptotics.IsBigO.trans_isLittleO theorem

{f : α → E} {g : α → F'} {k : α → G} (hfg : f =O[l] g) (hgk : g =o[l] k) : f =o[l] k

Full source

@[trans]
theorem IsBigO.trans_isLittleO {f : α → E} {g : α → F'} {k : α → G} (hfg : f =O[l] g)
    (hgk : g =o[l] k) : f =o[l] k :=
  let ⟨_c, cpos, hc⟩ := hfg.exists_pos
  hc.trans_isLittleO hgk cpos

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

Informal description

Let $f : \alpha \to E$, $g : \alpha \to F'$, and $k : \alpha \to G$ be functions mapping to normed spaces, and let $l$ be a filter on $\alpha$. If $f$ is 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$ is little o of $k$ along $l$ (i.e., for every $\epsilon > 0$, $\|g(x)\| \leq \epsilon \|k(x)\|$ for all $x$ in some neighborhood in $l$), then $f$ is little o of $k$ along $l$.

Asymptotics.transIsBigOIsLittleO instance

: @Trans (α → E) (α → F') (α → G) (· =O[l] ·) (· =o[l] ·) (· =o[l] ·)

Full source

instance transIsBigOIsLittleO :
    @Trans (α → E) (α → F') (α → G) (· =O[l] ·) (· =o[l] ·) (· =o[l] ·) where
  trans := IsBigO.trans_isLittleO

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

Informal description

The relation $\cdot =O[l] \cdot$ is transitive with respect to $\cdot =o[l] \cdot$ in the following sense: for functions $f : \alpha \to E$, $g : \alpha \to F'$, and $k : \alpha \to G$ between normed spaces and a filter $l$ on $\alpha$, if $f =O[l] g$ and $g =o[l] k$, then $f =o[l] k$.

Asymptotics.IsLittleO.trans theorem

{f : α → E} {g : α → F} {k : α → G} (hfg : f =o[l] g) (hgk : g =o[l] k) : f =o[l] k

Full source

@[trans]
theorem IsLittleO.trans {f : α → E} {g : α → F} {k : α → G} (hfg : f =o[l] g) (hgk : g =o[l] k) :
    f =o[l] k :=
  hfg.trans_isBigOWith hgk.isBigOWith one_pos

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

Informal description

Let $f : \alpha \to E$, $g : \alpha \to F$, and $k : \alpha \to G$ be functions between 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$) and $g$ is little-o of $k$ along $l$ (i.e., $g = o[l] k$), then $f$ is little-o of $k$ along $l$ (i.e., $f = o[l] k$).

Asymptotics.transIsLittleOIsLittleO instance

: @Trans (α → E) (α → F) (α → G) (· =o[l] ·) (· =o[l] ·) (· =o[l] ·)

Full source

instance transIsLittleOIsLittleO :
    @Trans (α → E) (α → F) (α → G) (· =o[l] ·) (· =o[l] ·) (· =o[l] ·) where
  trans := IsLittleO.trans

Transitivity of Little-o Relations

Informal description

The little-o relation `=o[l]` is transitive. That is, for functions $f : \alpha \to E$, $g : \alpha \to F$, and $k : \alpha \to G$ between normed spaces and a filter $l$ on $\alpha$, if $f = o[l] g$ and $g = o[l] k$, then $f = o[l] k$.

Filter.Eventually.trans_isBigO theorem

 {f : α → E} {g : α → F'} {k : α → G} (hfg : ∀ᶠ x in l, ‖f x‖ ≤ ‖g x‖) (hgk : g =O[l] k) : f =O[l] k

Full source

theorem _root_.Filter.Eventually.trans_isBigO {f : α → E} {g : α → F'} {k : α → G}
    (hfg : ∀ᶠ x in l, ‖f x‖ ≤ ‖g x‖) (hgk : g =O[l] k) : f =O[l] k :=
  (IsBigO.of_bound' hfg).trans hgk

Transitivity of Big-O Relations via Pointwise Norm Comparison

Informal description

Let $f : \alpha \to E$, $g : \alpha \to F'$, and $k : \alpha \to G$ be functions mapping to normed spaces, and let $l$ be a filter on $\alpha$. If there exists a neighborhood in $l$ where $\|f(x)\| \leq \|g(x)\|$ for all $x$, and $g =O[l] k$, then $f =O[l] k$.

Filter.Eventually.isBigO theorem

{f : α → E} {g : α → ℝ} {l : Filter α} (hfg : ∀ᶠ x in l, ‖f x‖ ≤ g x) : f =O[l] g

Full source

/-- See also `Asymptotics.IsBigO.of_norm_eventuallyLE`, which is the same lemma
stated using `Filter.EventuallyLE` instead of `Filter.Eventually`. -/
theorem _root_.Filter.Eventually.isBigO {f : α → E} {g : α → ℝ} {l : Filter α}
    (hfg : ∀ᶠ x in l, ‖f x‖ ≤ g x) : f =O[l] g :=
  .of_norm_eventuallyLE hfg

Big-O condition from eventual pointwise norm bound

Informal description

Let $f : \alpha \to E$ be a function and $g : \alpha \to \mathbb{R}$ be a real-valued function, where $E$ is a normed space. If there exists a neighborhood determined by the filter $l$ such that for all $x$ in this neighborhood, the norm of $f(x)$ is bounded by $g(x)$, i.e., $\|f(x)\| \leq g(x)$, then $f$ is big O of $g$ along $l$, denoted $f =O[l] g$.

Asymptotics.isBigOWith_of_le' theorem

(hfg : ∀ x, ‖f x‖ ≤ c * ‖g x‖) : IsBigOWith c l f g

Full source

theorem isBigOWith_of_le' (hfg : ∀ x, ‖f x‖ ≤ c * ‖g x‖) : IsBigOWith c l f g :=
  IsBigOWith.of_bound <| univ_mem' hfg

Pointwise Norm Bound Implies Big-O with Constant $c$

Informal description

For any constant $c \geq 0$, any filter $l$, and any functions $f$ and $g$ mapping to normed spaces, if for all $x$ the norm of $f(x)$ is bounded by $c$ times the norm of $g(x)$, then $f$ is big-O of $g$ along $l$ with constant $c$. That is, if $\|f(x)\| \leq c \|g(x)\|$ for all $x$, then $\text{IsBigOWith}(c, l, f, g)$ holds.

Asymptotics.isBigOWith_of_le theorem

(hfg : ∀ x, ‖f x‖ ≤ ‖g x‖) : IsBigOWith 1 l f g

Full source

theorem isBigOWith_of_le (hfg : ∀ x, ‖f x‖ ≤ ‖g x‖) : IsBigOWith 1 l f g :=
  isBigOWith_of_le' l fun x => by
    rw [one_mul]
    exact hfg x

Pointwise Norm Bound Implies Big-O with Constant 1

Informal description

For any filter $l$ and functions $f$ and $g$ mapping to normed spaces, if for all $x$ the norm of $f(x)$ is bounded by the norm of $g(x)$, then $f$ is big-O of $g$ along $l$ with constant $1$. That is, if $\|f(x)\| \leq \|g(x)\|$ for all $x$, then $\text{IsBigOWith}(1, l, f, g)$ holds.

Asymptotics.isBigO_of_le' theorem

(hfg : ∀ x, ‖f x‖ ≤ c * ‖g x‖) : f =O[l] g

Full source

theorem isBigO_of_le' (hfg : ∀ x, ‖f x‖ ≤ c * ‖g x‖) : f =O[l] g :=
  (isBigOWith_of_le' l hfg).isBigO

Pointwise Norm Bound Implies Big-O Relation

Informal description

For any constant $c \geq 0$, any filter $l$, and any functions $f$ and $g$ mapping to normed spaces, if for all $x$ the norm of $f(x)$ is bounded by $c$ times the norm of $g(x)$, then $f$ is big-O of $g$ along $l$. That is, if $\|f(x)\| \leq c \|g(x)\|$ for all $x$, then $f =O[l] g$ holds.

Asymptotics.isBigO_of_le theorem

(hfg : ∀ x, ‖f x‖ ≤ ‖g x‖) : f =O[l] g

Full source

theorem isBigO_of_le (hfg : ∀ x, ‖f x‖ ≤ ‖g x‖) : f =O[l] g :=
  (isBigOWith_of_le l hfg).isBigO

Pointwise Norm Bound Implies Big-O Relation

Informal description

For any functions $f$ and $g$ mapping to normed spaces and any filter $l$, if $\|f(x)\| \leq \|g(x)\|$ holds for all $x$, then $f$ is big-O of $g$ along $l$, denoted $f =O[l] g$.

Asymptotics.isBigOWith_refl theorem

(f : α → E) (l : Filter α) : IsBigOWith 1 l f f

Full source

theorem isBigOWith_refl (f : α → E) (l : Filter α) : IsBigOWith 1 l f f :=
  isBigOWith_of_le l fun _ => le_rfl

Reflexivity of Big-O with Constant 1: $\|f\| \leq 1 \cdot \|f\|$

Informal description

For any function $f \colon \alpha \to E$ mapping to a normed space $E$ and any filter $l$ on $\alpha$, the relation $\text{IsBigOWith}(1, l, f, f)$ holds. That is, $f$ is big-O of itself along $l$ with constant $1$, meaning $\|f(x)\| \leq 1 \cdot \|f(x)\|$ for all $x$ in the domain of $f$.

Asymptotics.isBigO_refl theorem

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

Full source

theorem isBigO_refl (f : α → E) (l : Filter α) : f =O[l] f :=
  (isBigOWith_refl f l).isBigO

Reflexivity of Big-O: $f =O[l] f$

Informal description

For any function $f \colon \alpha \to E$ mapping to a normed space $E$ and any filter $l$ on $\alpha$, the function $f$ is big-O of itself along $l$, denoted $f =O[l] f$.

Filter.EventuallyEq.isBigO theorem

{f₁ f₂ : α → E} (hf : f₁ =ᶠ[l] f₂) : f₁ =O[l] f₂

Full source

theorem _root_.Filter.EventuallyEq.isBigO {f₁ f₂ : α → E} (hf : f₁ =ᶠ[l] f₂) : f₁ =O[l] f₂ :=
  hf.trans_isBigO (isBigO_refl _ _)

Big-O Preservation under Eventual Equality

Informal description

For any two functions $f_1, f_2 : \alpha \to E$ mapping to a normed space $E$, if $f_1$ is eventually equal to $f_2$ along a filter $l$ on $\alpha$ (i.e., $f_1 =ᶠ[l] f_2$), then $f_1$ is big-O of $f_2$ along $l$ (i.e., $f_1 =O[l] f_2$).

Asymptotics.IsBigOWith.trans_le theorem

(hfg : IsBigOWith c l f g) (hgk : ∀ x, ‖g x‖ ≤ ‖k x‖) (hc : 0 ≤ c) : IsBigOWith c l f k

Full source

theorem IsBigOWith.trans_le (hfg : IsBigOWith c l f g) (hgk : ∀ x, ‖g x‖ ≤ ‖k x‖) (hc : 0 ≤ c) :
    IsBigOWith c l f k :=
  (hfg.trans (isBigOWith_of_le l hgk) hc).congr_const <| mul_one c

Transitivity of Big-O With Pointwise Norm Bound: $\text{IsBigOWith}(c, l, f, g) \land (\forall x, \|g(x)\| \leq \|k(x)\|) \to \text{IsBigOWith}(c, l, f, k)$

Informal description

Let $f : \alpha \to E$, $g : \alpha \to F$, and $k : \alpha \to G$ be functions to normed spaces, and let $l$ be a filter on $\alpha$. Suppose that: 1. There exists a constant $c \geq 0$ such that $\|f(x)\| \leq c \|g(x)\|$ for all $x$ in $l$ eventually. 2. For all $x$, $\|g(x)\| \leq \|k(x)\|$. Then, there exists a constant $c \geq 0$ such that $\|f(x)\| \leq c \|k(x)\|$ for all $x$ in $l$ eventually.

Asymptotics.IsBigO.trans_le theorem

(hfg : f =O[l] g') (hgk : ∀ x, ‖g' x‖ ≤ ‖k x‖) : f =O[l] k

Full source

theorem IsBigO.trans_le (hfg : f =O[l] g') (hgk : ∀ x, ‖g' x‖ ≤ ‖k x‖) : f =O[l] k :=
  hfg.trans (isBigO_of_le l hgk)

Transitivity of Big-O with Pointwise Norm Bound: $f = O(g') \land \|g'\| \leq \|k\| \Rightarrow f = O(k)$

Informal description

Let $f : \alpha \to E$, $g' : \alpha \to F$, and $k : \alpha \to G$ be functions mapping to normed spaces, and let $l$ be a filter on $\alpha$. If $f$ is big-O of $g'$ along $l$ (i.e., $f = O(g')$ at $l$) and for all $x$, the norm of $g'(x)$ is bounded by the norm of $k(x)$ (i.e., $\|g'(x)\| \leq \|k(x)\|$), then $f$ is big-O of $k$ along $l$ (i.e., $f = O(k)$ at $l$).

Asymptotics.IsLittleO.trans_le theorem

(hfg : f =o[l] g) (hgk : ∀ x, ‖g x‖ ≤ ‖k x‖) : f =o[l] k

Full source

theorem IsLittleO.trans_le (hfg : f =o[l] g) (hgk : ∀ x, ‖g x‖ ≤ ‖k x‖) : f =o[l] k :=
  hfg.trans_isBigOWith (isBigOWith_of_le _ hgk) zero_lt_one

Transitivity of Little-o with Pointwise Norm Bound: $f = o(g) \land \|g\| \leq \|k\| \Rightarrow f = o(k)$

Informal description

Let $f$, $g$, and $k$ be functions mapping to normed spaces, and let $l$ be a filter. If $f$ is little-o of $g$ with respect to $l$ (i.e., $f = o[l] g$), and for all $x$ the norm of $g(x)$ is bounded by the norm of $k(x)$ (i.e., $\|g(x)\| \leq \|k(x)\|$), then $f$ is little-o of $k$ with respect to $l$ (i.e., $f = o[l] k$).

Asymptotics.isLittleO_irrefl' theorem

(h : ∃ᶠ x in l, ‖f' x‖ ≠ 0) : ¬f' =o[l] f'

Full source

theorem isLittleO_irrefl' (h : ∃ᶠ x in l, ‖f' x‖ ≠ 0) : ¬f' =o[l] f' := by
  intro ho
  rcases ((ho.bound one_half_pos).and_frequently h).exists with ⟨x, hle, hne⟩
  rw [one_div, ← div_eq_inv_mul] at hle
  exact (half_lt_self (lt_of_le_of_ne (norm_nonneg _) hne.symm)).not_le hle

Non-reflexivity of little-o relation for non-vanishing functions

Informal description

If there exists a frequently occurring set of points $x$ in the filter $l$ where the norm of $f'(x)$ is nonzero, then $f'$ is not little-o of itself with respect to $l$. That is, $\neg (f' = o[l] f')$.

Asymptotics.isLittleO_irrefl theorem

(h : ∃ᶠ x in l, f'' x ≠ 0) : ¬f'' =o[l] f''

Full source

theorem isLittleO_irrefl (h : ∃ᶠ x in l, f'' x ≠ 0) : ¬f'' =o[l] f'' :=
  isLittleO_irrefl' <| h.mono fun _x => norm_ne_zero_iff.mpr

Non-reflexivity of little-o for non-vanishing functions

Informal description

If a function $f''$ is nonzero frequently (i.e., on a set that intersects every neighborhood in the filter $l$), then $f''$ cannot be asymptotically dominated by itself in the little-o sense with respect to $l$. That is, $\neg (f'' = o[l] f'')$.

Asymptotics.IsBigO.not_isLittleO theorem

(h : f'' =O[l] g') (hf : ∃ᶠ x in l, f'' x ≠ 0) : ¬g' =o[l] f''

Full source

theorem IsBigO.not_isLittleO (h : f'' =O[l] g') (hf : ∃ᶠ x in l, f'' x ≠ 0) :
    ¬g' =o[l] f'' := fun h' =>
  isLittleO_irrefl hf (h.trans_isLittleO h')

Big-O Implies Not Little-O for Non-Vanishing Functions

Informal description

Let $f''$ and $g'$ be functions from a type $\alpha$ to normed spaces, and let $l$ be a filter on $\alpha$. If $f''$ is 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 $f''$ is nonzero frequently along $l$, then $g'$ cannot be little o of $f''$ along $l$.

Asymptotics.IsLittleO.not_isBigO theorem

(h : f'' =o[l] g') (hf : ∃ᶠ x in l, f'' x ≠ 0) : ¬g' =O[l] f''

Full source

theorem IsLittleO.not_isBigO (h : f'' =o[l] g') (hf : ∃ᶠ x in l, f'' x ≠ 0) :
    ¬g' =O[l] f'' := fun h' =>
  isLittleO_irrefl hf (h.trans_isBigO h')

Non-reversibility of Little-o and Big-O: $f = o(g) \Rightarrow \neg(g = O(f))$ for non-vanishing $f$

Informal description

Let $f''$ and $g'$ be functions from a type $\alpha$ to normed spaces $E$ and $F$ respectively, and let $l$ be a filter on $\alpha$. If $f''$ is little-o of $g'$ with respect to $l$ (i.e., $f'' = o[l] g'$) and $f''$ is nonzero frequently in $l$ (i.e., $\exists^l x, f''(x) \neq 0$), then $g'$ is not big-O of $f''$ with respect to $l$ (i.e., $\neg (g' = O[l] f'')$).

Asymptotics.isBigOWith_bot theorem

: IsBigOWith c ⊥ f g

Full source

@[simp]
theorem isBigOWith_bot : IsBigOWith c ⊥ f g :=
  IsBigOWith.of_bound <| trivial

Big-O Bound Holds for Bottom Filter

Informal description

For any constant $C$ and functions $f$ and $g$ mapping to normed spaces, the relation $\text{IsBigOWith}(C, \bot, f, g)$ holds, where $\bot$ denotes the bottom filter. This means that $f$ is bounded by $C \cdot g$ with respect to the bottom filter.

Asymptotics.isBigO_bot theorem

: f =O[⊥] g

Full source

@[simp]
theorem isBigO_bot : f =O[⊥] g :=
  (isBigOWith_bot 1 f g).isBigO

Big-O Relation Holds for Bottom Filter

Informal description

For any functions $f$ and $g$ mapping into normed spaces, $f$ is big O of $g$ with respect to the bottom filter $\bot$.

Asymptotics.isLittleO_bot theorem

: f =o[⊥] g

Full source

@[simp]
theorem isLittleO_bot : f =o[⊥] g :=
  IsLittleO.of_isBigOWith fun c _ => isBigOWith_bot c f g

Little-o Relation Holds for Bottom Filter

Informal description

For any functions $f$ and $g$ mapping into normed spaces, $f$ is little-o of $g$ with respect to the bottom filter $\bot$.

Asymptotics.isBigOWith_pure theorem

{x} : IsBigOWith c (pure x) f g ↔ ‖f x‖ ≤ c * ‖g x‖

Full source

@[simp]
theorem isBigOWith_pure {x} : IsBigOWithIsBigOWith c (pure x) f g ↔ ‖f x‖ ≤ c * ‖g x‖ :=
  isBigOWith_iff

Big-O Bound at a Point: $\|f(x)\| \leq c \cdot \|g(x)\|$

Informal description

For a given point $x$, a real constant $c$, and functions $f$ and $g$ mapping into normed spaces, the relation $\text{IsBigOWith}(c, \text{pure } x, f, g)$ holds if and only if the norm of $f(x)$ is bounded by $c$ times the norm of $g(x)$, i.e., $\|f(x)\| \leq c \cdot \|g(x)\|$.

Asymptotics.IsBigOWith.sup theorem

(h : IsBigOWith c l f g) (h' : IsBigOWith c l' f g) : IsBigOWith c (l ⊔ l') f g

Full source

theorem IsBigOWith.sup (h : IsBigOWith c l f g) (h' : IsBigOWith c l' f g) :
    IsBigOWith c (l ⊔ l') f g :=
  IsBigOWith.of_bound <| mem_sup.2 ⟨h.bound, h'.bound⟩

Supremum Filter Preserves Big-O Bound with Constant $C$

Informal description

Let $f : \alpha \to E$ and $g : \alpha \to F$ be functions from a type $\alpha$ to normed spaces $E$ and $F$ respectively. If there exists a constant $C \in \mathbb{R}$ such that: 1. $\|f(x)\| \leq C \|g(x)\|$ holds eventually along filter $l$, and 2. $\|f(x)\| \leq C \|g(x)\|$ holds eventually along filter $l'$, then $\|f(x)\| \leq C \|g(x)\|$ holds eventually along the supremum filter $l \sqcup l'$.

Asymptotics.IsBigOWith.sup' theorem

(h : IsBigOWith c l f g') (h' : IsBigOWith c' l' f g') : IsBigOWith (max c c') (l ⊔ l') f g'

Full source

theorem IsBigOWith.sup' (h : IsBigOWith c l f g') (h' : IsBigOWith c' l' f g') :
    IsBigOWith (max c c') (l ⊔ l') f g' :=
  IsBigOWith.of_bound <|
    mem_sup.2 ⟨(h.weaken <| le_max_left c c').bound, (h'.weaken <| le_max_right c c').bound⟩

Big-O Bound with Maximum Constant Preserved under Filter Supremum

Informal description

Let $f : \alpha \to E$ and $g' : \alpha \to F$ be functions from a type $\alpha$ to normed spaces $E$ and $F$ respectively, and let $l$ and $l'$ be filters on $\alpha$. If there exist real constants $c$ and $c'$ such that: 1. $\|f(x)\| \leq c \|g'(x)\|$ holds eventually along filter $l$, and 2. $\|f(x)\| \leq c' \|g'(x)\|$ holds eventually along filter $l'$, then $\|f(x)\| \leq \max(c, c') \|g'(x)\|$ holds eventually along the supremum filter $l \sqcup l'$.

Asymptotics.IsBigO.sup theorem

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

Full source

theorem IsBigO.sup (h : f =O[l] g') (h' : f =O[l'] g') : f =O[l ⊔ l'] g' :=
  let ⟨_c, hc⟩ := h.isBigOWith
  let ⟨_c', hc'⟩ := h'.isBigOWith
  (hc.sup' hc').isBigO

Big-O Relation Preserved under Filter Supremum

Informal description

Let $f : \alpha \to E$ and $g' : \alpha \to F$ be functions from a type $\alpha$ to normed spaces $E$ and $F$ respectively, and let $l$ and $l'$ be filters on $\alpha$. If $f$ is big O of $g'$ along $l$ and $f$ is big O of $g'$ along $l'$, then $f$ is big O of $g'$ along the supremum filter $l \sqcup l'$.

Asymptotics.IsLittleO.sup theorem

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

Full source

theorem IsLittleO.sup (h : f =o[l] g) (h' : f =o[l'] g) : f =o[l ⊔ l'] g :=
  IsLittleO.of_isBigOWith fun _c cpos => (h.forall_isBigOWith cpos).sup (h'.forall_isBigOWith cpos)

Little-o relation is preserved under filter supremum

Informal description

Let $f : \alpha \to E$ and $g : \alpha \to F$ be functions from a type $\alpha$ to normed spaces $E$ and $F$ respectively. If $f = o[l] g$ and $f = o[l'] g$, then $f = o[l \sqcup l'] g$, where $l \sqcup l'$ is the supremum of the filters $l$ and $l'$.

Asymptotics.isBigO_sup theorem

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

Full source

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

Big-O condition under filter supremum: $f = O[l \sqcup l'] g' \leftrightarrow f = O[l] g' \land f = O[l'] g'$

Informal description

For functions $f : \alpha \to E$ and $g' : \alpha \to F$ to normed spaces and filters $l, l'$ on $\alpha$, the relation $f = O[l \sqcup l'] g'$ holds if and only if both $f = O[l] g'$ and $f = O[l'] g'$ hold.

Asymptotics.isLittleO_sup theorem

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

Full source

@[simp]
theorem isLittleO_sup : f =o[l ⊔ l'] gf =o[l ⊔ l'] g ↔ f =o[l] g ∧ f =o[l'] g :=
  ⟨fun h => ⟨h.mono le_sup_left, h.mono le_sup_right⟩, fun h => h.1.sup h.2⟩

Little-o condition under filter supremum: $f = o[l \sqcup l'] g \leftrightarrow f = o[l] g \land f = o[l'] g$

Informal description

For functions $f : \alpha \to E$ and $g : \alpha \to F$ to normed spaces and filters $l, l'$ on $\alpha$, the relation $f = o[l \sqcup l'] g$ holds if and only if both $f = o[l] g$ and $f = o[l'] g$ hold.

Asymptotics.isBigOWith_insert theorem

 [TopologicalSpace α] {x : α} {s : Set α} {C : ℝ} {g : α → E} {g' : α → F} (h : ‖g x‖ ≤ C * ‖g' x‖) :
  IsBigOWith C (𝓝[insert x s] x) g g' ↔ IsBigOWith C (𝓝[s] x) g g'

Full source

theorem isBigOWith_insert [TopologicalSpace α] {x : α} {s : Set α} {C : ℝ} {g : α → E} {g' : α → F}
    (h : ‖g x‖ ≤ C * ‖g' x‖) : IsBigOWithIsBigOWith C (𝓝[insert x s] x) g g' ↔
    IsBigOWith C (𝓝[s] x) g g' := by
  simp_rw [IsBigOWith_def, nhdsWithin_insert, eventually_sup, eventually_pure, h, true_and]

Equivalence of Big-O Conditions at Inserted Point

Informal description

Let $\alpha$ be a topological space, $x \in \alpha$, $s \subseteq \alpha$, $C \in \mathbb{R}$, and $g : \alpha \to E$, $g' : \alpha \to F$ be functions to normed spaces. If $\|g(x)\| \leq C \cdot \|g'(x)\|$, then the following are equivalent: 1. There exists a neighborhood of $x$ in $\{x\} \cup s$ where $\|g(y)\| \leq C \cdot \|g'(y)\|$ for all $y$ in this neighborhood. 2. There exists a neighborhood of $x$ in $s$ where $\|g(y)\| \leq C \cdot \|g'(y)\|$ for all $y$ in this neighborhood.

Asymptotics.IsBigOWith.insert theorem

 [TopologicalSpace α] {x : α} {s : Set α} {C : ℝ} {g : α → E} {g' : α → F} (h1 : IsBigOWith C (𝓝[s] x) g g')
  (h2 : ‖g x‖ ≤ C * ‖g' x‖) : IsBigOWith C (𝓝[insert x s] x) g g'

Full source

protected theorem IsBigOWith.insert [TopologicalSpace α] {x : α} {s : Set α} {C : ℝ} {g : α → E}
    {g' : α → F} (h1 : IsBigOWith C (𝓝[s] x) g g') (h2 : ‖g x‖ ≤ C * ‖g' x‖) :
    IsBigOWith C (𝓝[insert x s] x) g g' :=
  (isBigOWith_insert h2).mpr h1

Extension of Big-O Condition to Inserted Point

Informal description

Let $\alpha$ be a topological space, $x \in \alpha$, $s \subseteq \alpha$, $C \in \mathbb{R}$, and $g : \alpha \to E$, $g' : \alpha \to F$ be functions to normed spaces. If: 1. $g$ is big-O of $g'$ with constant $C$ in the neighborhood filter of $x$ within $s$, and 2. $\|g(x)\| \leq C \cdot \|g'(x)\|$, then $g$ is big-O of $g'$ with constant $C$ in the neighborhood filter of $x$ within $\{x\} \cup s$.

Asymptotics.isLittleO_insert theorem

 [TopologicalSpace α] {x : α} {s : Set α} {g : α → E'} {g' : α → F'} (h : g x = 0) :
  g =o[𝓝[insert x s] x] g' ↔ g =o[𝓝[s] x] g'

Full source

theorem isLittleO_insert [TopologicalSpace α] {x : α} {s : Set α} {g : α → E'} {g' : α → F'}
    (h : g x = 0) : g =o[𝓝[insert x s] x] g'g =o[𝓝[insert x s] x] g' ↔ g =o[𝓝[s] x] g' := by
  simp_rw [IsLittleO_def]
  refine forall_congr' fun c => forall_congr' fun hc => ?_
  rw [isBigOWith_insert]
  rw [h, norm_zero]
  exact mul_nonneg hc.le (norm_nonneg _)

Equivalence of Little-o Conditions at Inserted Point when $g(x) = 0$

Informal description

Let $\alpha$ be a topological space, $x \in \alpha$, $s \subseteq \alpha$, and $g : \alpha \to E'$, $g' : \alpha \to F'$ be functions to normed spaces. If $g(x) = 0$, then the following are equivalent: 1. $g$ is little-o of $g'$ as $y$ approaches $x$ within $\{x\} \cup s$. 2. $g$ is little-o of $g'$ as $y$ approaches $x$ within $s$.

Asymptotics.IsLittleO.insert theorem

 [TopologicalSpace α] {x : α} {s : Set α} {g : α → E'} {g' : α → F'} (h1 : g =o[𝓝[s] x] g') (h2 : g x = 0) :
  g =o[𝓝[insert x s] x] g'

Full source

protected theorem IsLittleO.insert [TopologicalSpace α] {x : α} {s : Set α} {g : α → E'}
    {g' : α → F'} (h1 : g =o[𝓝[s] x] g') (h2 : g x = 0) : g =o[𝓝[insert x s] x] g' :=
  (isLittleO_insert h2).mpr h1

Extension of Little-o Condition to Inserted Point when $g(x) = 0$

Informal description

Let $\alpha$ be a topological space, $x \in \alpha$, $s \subseteq \alpha$, and $g : \alpha \to E'$, $g' : \alpha \to F'$ be functions to normed spaces. If: 1. $g$ is little-o of $g'$ as $y$ approaches $x$ within $s$, and 2. $g(x) = 0$, then $g$ is little-o of $g'$ as $y$ approaches $x$ within $\{x\} \cup s$.

Asymptotics.isBigOWith_norm_right theorem

: (IsBigOWith c l f fun x => ‖g' x‖) ↔ IsBigOWith c l f g'

Full source

@[simp]
theorem isBigOWith_norm_right : (IsBigOWith c l f fun x => ‖g' x‖) ↔ IsBigOWith c l f g' := by
  simp only [IsBigOWith_def, norm_norm]

Equivalence of Big-O With Norm and Big-O With Function: $\text{IsBigOWith}(c, l, f, \|g'\|) \leftrightarrow \text{IsBigOWith}(c, l, f, g')$

Informal description

For a real constant $c$, a filter $l$, and functions $f$ and $g'$ mapping into normed spaces, the relation $\text{IsBigOWith}(c, l, f, \|g'\|)$ holds if and only if $\text{IsBigOWith}(c, l, f, g')$ holds. In other words, $f$ is bounded by $c$ times the norm of $g'$ along $l$ if and only if $f$ is bounded by $c$ times $g'$ itself along $l$.

Asymptotics.isBigOWith_abs_right theorem

: (IsBigOWith c l f fun x => |u x|) ↔ IsBigOWith c l f u

Full source

@[simp]
theorem isBigOWith_abs_right : (IsBigOWith c l f fun x => |u x|) ↔ IsBigOWith c l f u :=
  @isBigOWith_norm_right _ _ _ _ _ _ f u l

Equivalence of Big-O With Absolute Value and Big-O With Function: $\text{IsBigOWith}(c, l, f, |u|) \leftrightarrow \text{IsBigOWith}(c, l, f, u)$

Informal description

For a real constant $c$, a filter $l$, and functions $f$ and $u$ mapping into normed spaces, the relation $\text{IsBigOWith}(c, l, f, |u|)$ holds if and only if $\text{IsBigOWith}(c, l, f, u)$ holds. In other words, $f$ is bounded by $c$ times the absolute value of $u$ along $l$ if and only if $f$ is bounded by $c$ times $u$ itself along $l$.

Asymptotics.isBigO_norm_right theorem

: (f =O[l] fun x => ‖g' x‖) ↔ f =O[l] g'

Full source

@[simp]
theorem isBigO_norm_right : (f =O[l] fun x => ‖g' x‖) ↔ f =O[l] g' := by
  simp only [IsBigO_def]
  exact exists_congr fun _ => isBigOWith_norm_right

Equivalence of Big-O with Norm and Big-O with Function: $f =O[l] \|g'\| \leftrightarrow f =O[l] g'$

Informal description

For functions $f$ and $g'$ mapping into normed spaces and a filter $l$, the relation $f =O[l] \|g'\|$ holds if and only if $f =O[l] g'$ holds. In other words, $f$ is big-O of the norm of $g'$ along $l$ if and only if $f$ is big-O of $g'$ itself along $l$.

Asymptotics.isBigO_abs_right theorem

: (f =O[l] fun x => |u x|) ↔ f =O[l] u

Full source

@[simp]
theorem isBigO_abs_right : (f =O[l] fun x => |u x|) ↔ f =O[l] u :=
  @isBigO_norm_right _ _ ℝ _ _ _ _ _

Equivalence of Big-O with Absolute Value and Big-O with Function: $f =O[l] |u| \leftrightarrow f =O[l] u$

Informal description

For functions $f$ and $u$ mapping into normed spaces and a filter $l$, the relation $f =O[l] |u|$ holds if and only if $f =O[l] u$ holds. In other words, $f$ is big-O of the absolute value of $u$ along $l$ if and only if $f$ is big-O of $u$ itself along $l$.

Asymptotics.isLittleO_norm_right theorem

: (f =o[l] fun x => ‖g' x‖) ↔ f =o[l] g'

Full source

@[simp]
theorem isLittleO_norm_right : (f =o[l] fun x => ‖g' x‖) ↔ f =o[l] g' := by
  simp only [IsLittleO_def]
  exact forall₂_congr fun _ _ => isBigOWith_norm_right

Equivalence of Little-o Relations with Norm and Original Function

Informal description

For functions $f : \alpha \to E$ and $g' : \alpha \to F$ where $E$ and $F$ are normed spaces, and a filter $l$ on $\alpha$, the following are equivalent: 1. $f = o[l] (\lambda x, \|g'(x)\|)$ 2. $f = o[l] g'$ In other words, $f$ is little-o of the norm of $g'$ along $l$ if and only if $f$ is little-o of $g'$ itself along $l$.

Asymptotics.isLittleO_abs_right theorem

: (f =o[l] fun x => |u x|) ↔ f =o[l] u

Full source

@[simp]
theorem isLittleO_abs_right : (f =o[l] fun x => |u x|) ↔ f =o[l] u :=
  @isLittleO_norm_right _ _ ℝ _ _ _ _ _

Equivalence of Little-o Relations with Absolute Value and Original Function

Informal description

For functions $f : \alpha \to E$ and $u : \alpha \to \mathbb{R}$ where $E$ is a normed space, and a filter $l$ on $\alpha$, the following are equivalent: 1. $f = o[l] (\lambda x, |u(x)|)$ 2. $f = o[l] u$ In other words, $f$ is little-o of the absolute value of $u$ along $l$ if and only if $f$ is little-o of $u$ itself along $l$.

Asymptotics.isBigOWith_norm_left theorem

: IsBigOWith c l (fun x => ‖f' x‖) g ↔ IsBigOWith c l f' g

Full source

@[simp]
theorem isBigOWith_norm_left : IsBigOWithIsBigOWith c l (fun x => ‖f' x‖) g ↔ IsBigOWith c l f' g := by
  simp only [IsBigOWith_def, norm_norm]

Norm Equivalence in Big-O With Constant: $\|f'\| =_{O(c,l)} g \leftrightarrow f' =_{O(c,l)} g$

Informal description

For a real constant $c$, a filter $l$, and functions $f'$ and $g$ mapping to normed spaces, the following are equivalent: 1. The function $\lambda x, \|f'(x)\|$ is eventually bounded by $c \cdot \|g(x)\|$ along $l$. 2. The function $f'$ is eventually bounded by $c \cdot \|g(x)\|$ along $l$. In other words, $\text{IsBigOWith}(c, l, \lambda x \|f'(x)\|, g) \leftrightarrow \text{IsBigOWith}(c, l, f', g)$.

Asymptotics.isBigOWith_abs_left theorem

: IsBigOWith c l (fun x => |u x|) g ↔ IsBigOWith c l u g

Full source

@[simp]
theorem isBigOWith_abs_left : IsBigOWithIsBigOWith c l (fun x => |u x|) g ↔ IsBigOWith c l u g :=
  @isBigOWith_norm_left _ _ _ _ _ _ g u l

Absolute Value Equivalence in Big-O With Constant: $|u| =_{O(c,l)} g \leftrightarrow u =_{O(c,l)} g$

Informal description

For a real constant $c$, a filter $l$, and functions $u$ and $g$ mapping to normed spaces, the following are equivalent: 1. The function $\lambda x, |u(x)|$ is eventually bounded by $c \cdot \|g(x)\|$ along $l$. 2. The function $u$ is eventually bounded by $c \cdot \|g(x)\|$ along $l$. In other words, $\text{IsBigOWith}(c, l, \lambda x |u(x)|, g) \leftrightarrow \text{IsBigOWith}(c, l, u, g)$.

Asymptotics.isBigO_norm_left theorem

: (fun x => ‖f' x‖) =O[l] g ↔ f' =O[l] g

Full source

@[simp]
theorem isBigO_norm_left : (fun x => ‖f' x‖) =O[l] g(fun x => ‖f' x‖) =O[l] g ↔ f' =O[l] g := by
  simp only [IsBigO_def]
  exact exists_congr fun _ => isBigOWith_norm_left

Norm Equivalence in Big-O: $\|f'\| =_{O(l)} g \leftrightarrow f' =_{O(l)} g$

Informal description

For functions $f'$ and $g$ mapping to normed spaces and a filter $l$, the following are equivalent: 1. The function $\lambda x, \|f'(x)\|$ is big-O of $g$ along $l$. 2. The function $f'$ is big-O of $g$ along $l$. In other words, $(\lambda x \|f'(x)\|) =_{O(l)} g \leftrightarrow f' =_{O(l)} g$.

Asymptotics.isBigO_abs_left theorem

: (fun x => |u x|) =O[l] g ↔ u =O[l] g

Full source

@[simp]
theorem isBigO_abs_left : (fun x => |u x|) =O[l] g(fun x => |u x|) =O[l] g ↔ u =O[l] g :=
  @isBigO_norm_left _ _ _ _ _ g u l

Absolute Value Equivalence in Big-O: $|u| = O_l(g) \leftrightarrow u = O_l(g)$

Informal description

For functions $u$ and $g$ mapping to normed spaces and a filter $l$, the following are equivalent: 1. The function $\lambda x, |u(x)|$ is big-O of $g$ along $l$. 2. The function $u$ is big-O of $g$ along $l$. In other words, $(\lambda x, |u(x)|) = O_l(g) \leftrightarrow u = O_l(g)$.

Asymptotics.isLittleO_norm_left theorem

: (fun x => ‖f' x‖) =o[l] g ↔ f' =o[l] g

Full source

@[simp]
theorem isLittleO_norm_left : (fun x => ‖f' x‖) =o[l] g(fun x => ‖f' x‖) =o[l] g ↔ f' =o[l] g := by
  simp only [IsLittleO_def]
  exact forall₂_congr fun _ _ => isBigOWith_norm_left

Norm Equivalence in Little-o: $\|f'\| = o[l] g \leftrightarrow f' = o[l] g$

Informal description

For functions $f' : \alpha \to E$ and $g : \alpha \to F$ where $E$ and $F$ are normed spaces, and a filter $l$ on $\alpha$, the following are equivalent: 1. The function $\lambda x, \|f'(x)\|$ is little-o of $g$ along $l$. 2. The function $f'$ is little-o of $g$ along $l$. In other words, $(\lambda x \|f'(x)\|) = o[l] g \leftrightarrow f' = o[l] g$.

Asymptotics.isLittleO_abs_left theorem

: (fun x => |u x|) =o[l] g ↔ u =o[l] g

Full source

@[simp]
theorem isLittleO_abs_left : (fun x => |u x|) =o[l] g(fun x => |u x|) =o[l] g ↔ u =o[l] g :=
  @isLittleO_norm_left _ _ _ _ _ g u l

Absolute Value Equivalence in Little-o: $|u| = o[l] g \leftrightarrow u = o[l] g$

Informal description

For a function $u : \alpha \to \mathbb{R}$ and a function $g : \alpha \to F$ where $F$ is a normed space, and a filter $l$ on $\alpha$, the following are equivalent: 1. The function $\lambda x, |u(x)|$ is little-o of $g$ along $l$. 2. The function $u$ is little-o of $g$ along $l$. In other words, $(\lambda x, |u(x)|) = o[l] g \leftrightarrow u = o[l] g$.

Asymptotics.isBigOWith_norm_norm theorem

: (IsBigOWith c l (fun x => ‖f' x‖) fun x => ‖g' x‖) ↔ IsBigOWith c l f' g'

Full source

theorem isBigOWith_norm_norm :
    (IsBigOWith c l (fun x => ‖f' x‖) fun x => ‖g' x‖) ↔ IsBigOWith c l f' g' :=
  isBigOWith_norm_left.trans isBigOWith_norm_right

Norm Equivalence in Big-O With Constant: $\|f'\| =_{O(c,l)} \|g'\| \leftrightarrow f' =_{O(c,l)} g'$

Informal description

For a real constant $c$, a filter $l$, and functions $f'$ and $g'$ mapping into normed spaces, the following are equivalent: 1. The function $\lambda x, \|f'(x)\|$ is eventually bounded by $c \cdot \|g'(x)\|$ along $l$. 2. The function $f'$ is eventually bounded by $c \cdot g'$ along $l$. In other words, $\text{IsBigOWith}(c, l, \lambda x \|f'(x)\|, \lambda x \|g'(x)\|) \leftrightarrow \text{IsBigOWith}(c, l, f', g')$.

Asymptotics.isBigOWith_abs_abs theorem

: (IsBigOWith c l (fun x => |u x|) fun x => |v x|) ↔ IsBigOWith c l u v

Full source

theorem isBigOWith_abs_abs :
    (IsBigOWith c l (fun x => |u x|) fun x => |v x|) ↔ IsBigOWith c l u v :=
  isBigOWith_abs_left.trans isBigOWith_abs_right

Equivalence of Big-O With Absolute Values and Big-O With Functions: $|u| =_{O(c,l)} |v| \leftrightarrow u =_{O(c,l)} v$

Informal description

For a real constant $c$, a filter $l$, and functions $u$ and $v$ mapping into normed spaces, the following are equivalent: 1. The function $\lambda x, |u(x)|$ is eventually bounded by $c \cdot |v(x)|$ along $l$. 2. The function $u$ is eventually bounded by $c \cdot v$ along $l$. In other words, $\text{IsBigOWith}(c, l, \lambda x |u(x)|, \lambda x |v(x)|) \leftrightarrow \text{IsBigOWith}(c, l, u, v)$.

Asymptotics.isBigO_norm_norm theorem

: ((fun x => ‖f' x‖) =O[l] fun x => ‖g' x‖) ↔ f' =O[l] g'

Full source

theorem isBigO_norm_norm : ((fun x => ‖f' x‖) =O[l] fun x => ‖g' x‖) ↔ f' =O[l] g' :=
  isBigO_norm_left.trans isBigO_norm_right

Norm Equivalence in Big-O: $\|f'\| =_{O(l)} \|g'\| \leftrightarrow f' =_{O(l)} g'$

Informal description

For functions $f'$ and $g'$ mapping into normed spaces and a filter $l$, the following are equivalent: 1. The function $\lambda x, \|f'(x)\|$ is big-O of $\lambda x, \|g'(x)\|$ along $l$. 2. The function $f'$ is big-O of $g'$ along $l$. In other words, $(\lambda x, \|f'(x)\|) =_{O(l)} (\lambda x, \|g'(x)\|) \leftrightarrow f' =_{O(l)} g'$.

Asymptotics.isBigO_abs_abs theorem

: ((fun x => |u x|) =O[l] fun x => |v x|) ↔ u =O[l] v

Full source

theorem isBigO_abs_abs : ((fun x => |u x|) =O[l] fun x => |v x|) ↔ u =O[l] v :=
  isBigO_abs_left.trans isBigO_abs_right

Equivalence of Big-O with Absolute Values: $|u| = O_l(|v|) \leftrightarrow u = O_l(v)$

Informal description

For functions $u$ and $v$ mapping into normed spaces and a filter $l$, the following are equivalent: 1. The function $\lambda x, |u(x)|$ is big-O of $\lambda x, |v(x)|$ along $l$. 2. The function $u$ is big-O of $v$ along $l$. In other words, $(\lambda x, |u(x)|) = O_l (\lambda x, |v(x)|) \leftrightarrow u = O_l v$.

Asymptotics.isLittleO_norm_norm theorem

: ((fun x => ‖f' x‖) =o[l] fun x => ‖g' x‖) ↔ f' =o[l] g'

Full source

theorem isLittleO_norm_norm : ((fun x => ‖f' x‖) =o[l] fun x => ‖g' x‖) ↔ f' =o[l] g' :=
  isLittleO_norm_left.trans isLittleO_norm_right

Norm Equivalence in Little-o: $\|f'\| = o[l] \|g'\| \leftrightarrow f' = o[l] g'$

Informal description

For functions $f' : \alpha \to E$ and $g' : \alpha \to F$ where $E$ and $F$ are normed spaces, and a filter $l$ on $\alpha$, the following are equivalent: 1. The function $\lambda x, \|f'(x)\|$ is little-o of $\lambda x, \|g'(x)\|$ along $l$. 2. The function $f'$ is little-o of $g'$ along $l$. In other words, $(\lambda x, \|f'(x)\|) = o[l] (\lambda x, \|g'(x)\|) \leftrightarrow f' = o[l] g'$.

Asymptotics.isLittleO_abs_abs theorem

: ((fun x => |u x|) =o[l] fun x => |v x|) ↔ u =o[l] v

Full source

theorem isLittleO_abs_abs : ((fun x => |u x|) =o[l] fun x => |v x|) ↔ u =o[l] v :=
  isLittleO_abs_left.trans isLittleO_abs_right

Absolute Value Equivalence in Little-o: $|u| = o[l] |v| \leftrightarrow u = o[l] v$

Informal description

For real-valued functions $u, v : \alpha \to \mathbb{R}$ and a filter $l$ on $\alpha$, the following are equivalent: 1. The function $\lambda x, |u(x)|$ is little-o of $\lambda x, |v(x)|$ along $l$. 2. The function $u$ is little-o of $v$ along $l$. In other words, $|u| = o[l] |v| \leftrightarrow u = o[l] v$.

Asymptotics.isBigOWith_neg_right theorem

: (IsBigOWith c l f fun x => -g' x) ↔ IsBigOWith c l f g'

Full source

@[simp]
theorem isBigOWith_neg_right : (IsBigOWith c l f fun x => -g' x) ↔ IsBigOWith c l f g' := by
  simp only [IsBigOWith_def, norm_neg]

Negation Invariance of Big-O Bound: $\text{IsBigOWith}(c, l, f, -g') \leftrightarrow \text{IsBigOWith}(c, l, f, g')$

Informal description

For a real constant $c$, a filter $l$, and functions $f$ and $g'$, the relation $\text{IsBigOWith}(c, l, f, \lambda x, -g'(x))$ holds if and only if $\text{IsBigOWith}(c, l, f, g')$ holds. In other words, the big-O bound with constant $c$ is unchanged when the function $g'$ is negated.

Asymptotics.isBigO_neg_right theorem

: (f =O[l] fun x => -g' x) ↔ f =O[l] g'

Full source

@[simp]
theorem isBigO_neg_right : (f =O[l] fun x => -g' x) ↔ f =O[l] g' := by
  simp only [IsBigO_def]
  exact exists_congr fun _ => isBigOWith_neg_right

Negation Invariance of Big-O Relation: $f =O[l] (-g') \leftrightarrow f =O[l] g'$

Informal description

For functions $f$ and $g'$ and a filter $l$, the relation $f =O[l] (-g')$ holds if and only if $f =O[l] g'$ holds. In other words, the big-O relation is unchanged when the function $g'$ is negated.

Asymptotics.isLittleO_neg_right theorem

: (f =o[l] fun x => -g' x) ↔ f =o[l] g'

Full source

@[simp]
theorem isLittleO_neg_right : (f =o[l] fun x => -g' x) ↔ f =o[l] g' := by
  simp only [IsLittleO_def]
  exact forall₂_congr fun _ _ => isBigOWith_neg_right

Negation Invariance of Little-o Relation: $f = o[l] (-g') \leftrightarrow f = o[l] g'$

Informal description

For functions $f$ and $g'$ defined on a common domain with a filter $l$, and taking values in normed spaces, the relation $f = o[l] (-g')$ holds if and only if $f = o[l] g'$. In other words, the little-o asymptotic relation is invariant under negation of the function $g'$.

Asymptotics.isBigOWith_neg_left theorem

: IsBigOWith c l (fun x => -f' x) g ↔ IsBigOWith c l f' g

Full source

@[simp]
theorem isBigOWith_neg_left : IsBigOWithIsBigOWith c l (fun x => -f' x) g ↔ IsBigOWith c l f' g := by
  simp only [IsBigOWith_def, norm_neg]

Negation Invariance of Big-O With Constant $c$

Informal description

For a real constant $c$, a filter $l$ on a type $\alpha$, and functions $f' : \alpha \to E$ and $g : \alpha \to F$ where $E$ and $F$ are normed spaces, the following are equivalent: 1. The function $-f'$ is eventually bounded by $c \cdot g$ along $l$ (i.e., $\text{IsBigOWith}(c, l, -f', g)$ holds). 2. The function $f'$ is eventually bounded by $c \cdot g$ along $l$ (i.e., $\text{IsBigOWith}(c, l, f', g)$ holds). In other words, $\| -f'(x) \| \leq c \cdot \| g(x) \|$ for all $x$ in $l$ eventually if and only if $\| f'(x) \| \leq c \cdot \| g(x) \|$ for all $x$ in $l$ eventually.

Asymptotics.isBigO_neg_left theorem

: (fun x => -f' x) =O[l] g ↔ f' =O[l] g

Full source

@[simp]
theorem isBigO_neg_left : (fun x => -f' x) =O[l] g(fun x => -f' x) =O[l] g ↔ f' =O[l] g := by
  simp only [IsBigO_def]
  exact exists_congr fun _ => isBigOWith_neg_left

Negation Invariance of Big-O Relation: $-f' =O[l] g \leftrightarrow f' =O[l] g$

Informal description

For functions $f' : \alpha \to E$ and $g : \alpha \to F$ where $E$ and $F$ are normed spaces, and a filter $l$ on $\alpha$, the following are equivalent: 1. The function $-f'$ is big O of $g$ along $l$ (i.e., $-f' =O[l] g$). 2. The function $f'$ is big O of $g$ along $l$ (i.e., $f' =O[l] g$). In other words, $\| -f'(x) \|$ is eventually bounded by a constant multiple of $\| g(x) \|$ along $l$ if and only if $\| f'(x) \|$ is eventually bounded by the same constant multiple of $\| g(x) \|$ along $l$.

Asymptotics.isLittleO_neg_left theorem

: (fun x => -f' x) =o[l] g ↔ f' =o[l] g

Full source

@[simp]
theorem isLittleO_neg_left : (fun x => -f' x) =o[l] g(fun x => -f' x) =o[l] g ↔ f' =o[l] g := by
  simp only [IsLittleO_def]
  exact forall₂_congr fun _ _ => isBigOWith_neg_left

Negation Invariance of Little-o Relation: $-f' = o[l] g \leftrightarrow f' = o[l] g$

Informal description

For functions $f' : \alpha \to E$ and $g : \alpha \to F$ where $E$ and $F$ are normed spaces, and a filter $l$ on $\alpha$, the following are equivalent: 1. The function $-f'$ is little-o of $g$ along $l$ (i.e., $-f' = o[l] g$). 2. The function $f'$ is little-o of $g$ along $l$ (i.e., $f' = o[l] g$). In other words, $\| -f'(x) \| = o(\| g(x) \|)$ as $x$ approaches $l$ if and only if $\| f'(x) \| = o(\| g(x) \|)$ as $x$ approaches $l$.

Asymptotics.isBigOWith_fst_prod theorem

: IsBigOWith 1 l f' fun x => (f' x, g' x)

Full source

theorem isBigOWith_fst_prod : IsBigOWith 1 l f' fun x => (f' x, g' x) :=
  isBigOWith_of_le l fun _x => le_max_left _ _

First Component is Big-O of Pair with Constant 1

Informal description

For any filter $l$ and functions $f' : \alpha \to E$ and $g' : \alpha \to F$ where $E$ and $F$ are normed spaces, the function $f'$ is big-O with constant $1$ of the function $x \mapsto (f'(x), g'(x))$ along $l$. That is, there exists a constant $C = 1$ such that for all $x$ in $l$ eventually, $\|f'(x)\| \leq \max(\|f'(x)\|, \|g'(x)\|)$.

Asymptotics.isBigOWith_snd_prod theorem

: IsBigOWith 1 l g' fun x => (f' x, g' x)

Full source

theorem isBigOWith_snd_prod : IsBigOWith 1 l g' fun x => (f' x, g' x) :=
  isBigOWith_of_le l fun _x => le_max_right _ _

Second Component is Big-O of Product Function with Constant 1

Informal description

For functions $f' : \alpha \to E$ and $g' : \alpha \to F$ where $E$ and $F$ are normed spaces, and a filter $l$ on $\alpha$, the function $g'$ is big-O of the second component of the product function $(f', g')$ along $l$ with constant $1$. That is, there exists a constant $C = 1$ such that for all $x$ in $l$ eventually, $\|g'(x)\| \leq \|(f'(x), g'(x))\|$.

Asymptotics.isBigO_fst_prod theorem

: f' =O[l] fun x => (f' x, g' x)

Full source

theorem isBigO_fst_prod : f' =O[l] fun x => (f' x, g' x) :=
  isBigOWith_fst_prod.isBigO

First Component is Big-O of Pair Function

Informal description

For functions $f' : \alpha \to E$ and $g' : \alpha \to F$ where $E$ and $F$ are normed spaces, and a filter $l$ on $\alpha$, the function $f'$ is big-O of the function $x \mapsto (f'(x), g'(x))$ along $l$. That is, there exists a constant $C > 0$ such that $\|f'(x)\| \leq C \max(\|f'(x)\|, \|g'(x)\|)$ for all $x$ in some neighborhood determined by $l$.

Asymptotics.isBigO_snd_prod theorem

: g' =O[l] fun x => (f' x, g' x)

Full source

theorem isBigO_snd_prod : g' =O[l] fun x => (f' x, g' x) :=
  isBigOWith_snd_prod.isBigO

Second Component is Big-O of Product Function

Informal description

For functions $f' : \alpha \to E$ and $g' : \alpha \to F$ where $E$ and $F$ are normed spaces, and a filter $l$ on $\alpha$, the function $g'$ is big-O of the product function $x \mapsto (f'(x), g'(x))$ along $l$. That is, there exists a constant $C > 0$ such that $\|g'(x)\| \leq C \max(\|f'(x)\|, \|g'(x)\|)$ for all $x$ in some neighborhood determined by $l$.

Asymptotics.isBigO_fst_prod' theorem

{f' : α → E' × F'} : (fun x => (f' x).1) =O[l] f'

Full source

theorem isBigO_fst_prod' {f' : α → E' × F'} : (fun x => (f' x).1) =O[l] f' := by
  simpa [IsBigO_def, IsBigOWith_def] using isBigO_fst_prod (E' := E') (F' := F')

First Component is Big-O of Product Function

Informal description

For any function $f' : \alpha \to E' \times F'$ mapping to the product of normed spaces $E'$ and $F'$, the first component function $x \mapsto (f'(x)).1$ is big-O of $f'$ along the filter $l$. That is, there exists a constant $C > 0$ such that $\|(f'(x)).1\| \leq C \max(\|(f'(x)).1\|, \|(f'(x)).2\|)$ for all $x$ in some neighborhood determined by $l$.

Asymptotics.isBigO_snd_prod' theorem

{f' : α → E' × F'} : (fun x => (f' x).2) =O[l] f'

Full source

theorem isBigO_snd_prod' {f' : α → E' × F'} : (fun x => (f' x).2) =O[l] f' := by
  simpa [IsBigO_def, IsBigOWith_def] using isBigO_snd_prod (E' := E') (F' := F')

Second Component is Big-O of Product Function (Generalized)

Informal description

For any function $f' : \alpha \to E' \times F'$ where $E'$ and $F'$ are normed spaces, and for any filter $l$ on $\alpha$, the second component function $x \mapsto (f'(x)).2$ is big-O of $f'$ along $l$. That is, there exists a constant $C > 0$ such that $\|(f'(x)).2\| \leq C \|f'(x)\|$ for all $x$ in some neighborhood determined by $l$, where $\|f'(x)\| = \max(\|(f'(x)).1\|, \|(f'(x)).2\|)$.

Asymptotics.IsBigOWith.prod_rightl theorem

(h : IsBigOWith c l f g') (hc : 0 ≤ c) : IsBigOWith c l f fun x => (g' x, k' x)

Full source

theorem IsBigOWith.prod_rightl (h : IsBigOWith c l f g') (hc : 0 ≤ c) :
    IsBigOWith c l f fun x => (g' x, k' x) :=
  (h.trans isBigOWith_fst_prod hc).congr_const (mul_one c)

Big-O Bound Preserved Under Right Product Extension with Constant $c$

Informal description

Let $f : \alpha \to E$, $g' : \alpha \to F$, and $k' : \alpha \to G$ be functions to normed spaces, and let $l$ be a filter on $\alpha$. If there exists a constant $c \geq 0$ such that $\|f(x)\| \leq c \|g'(x)\|$ for all $x$ in $l$ eventually, then there exists a constant $c \geq 0$ such that $\|f(x)\| \leq c \max(\|g'(x)\|, \|k'(x)\|)$ for all $x$ in $l$ eventually.

Asymptotics.IsBigO.prod_rightl theorem

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

Full source

theorem IsBigO.prod_rightl (h : f =O[l] g') : f =O[l] fun x => (g' x, k' x) :=
  let ⟨_c, cnonneg, hc⟩ := h.exists_nonneg
  (hc.prod_rightl k' cnonneg).isBigO

Big-O relation preserved under right product extension with $g'$

Informal description

Let $f : \alpha \to E$ and $g', k' : \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$, then $f$ is also big-O of the function $x \mapsto (g'(x), k'(x))$ along $l$.

Asymptotics.IsLittleO.prod_rightl theorem

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

Full source

theorem IsLittleO.prod_rightl (h : f =o[l] g') : f =o[l] fun x => (g' x, k' x) :=
  IsLittleO.of_isBigOWith fun _c cpos => (h.forall_isBigOWith cpos).prod_rightl k' cpos.le

Little-o relation preserved under right product extension with $g'$

Informal description

Let $f : \alpha \to E$ and $g', k' : \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$, then $f$ is also little-o of the function $x \mapsto (g'(x), k'(x))$ along $l$.

Asymptotics.IsBigOWith.prod_rightr theorem

(h : IsBigOWith c l f g') (hc : 0 ≤ c) : IsBigOWith c l f fun x => (f' x, g' x)

Full source

theorem IsBigOWith.prod_rightr (h : IsBigOWith c l f g') (hc : 0 ≤ c) :
    IsBigOWith c l f fun x => (f' x, g' x) :=
  (h.trans isBigOWith_snd_prod hc).congr_const (mul_one c)

Big-O bound with constant $c$ for $f$ relative to the second component of a product function

Informal description

Asymptotics.IsBigO.prod_rightr theorem

(h : f =O[l] g') : f =O[l] fun x => (f' x, g' x)

Full source

theorem IsBigO.prod_rightr (h : f =O[l] g') : f =O[l] fun x => (f' x, g' x) :=
  let ⟨_c, cnonneg, hc⟩ := h.exists_nonneg
  (hc.prod_rightr f' cnonneg).isBigO

Big-O Relation Preserved Under Pairing with Auxiliary Function

Informal description

Let $f : \alpha \to E$ and $g', f' : \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$ (i.e., $f = O[l] g'$), then $f$ is also big-O of the function $x \mapsto (f'(x), g'(x))$ along $l$.

Asymptotics.IsLittleO.prod_rightr theorem

(h : f =o[l] g') : f =o[l] fun x => (f' x, g' x)

Full source

theorem IsLittleO.prod_rightr (h : f =o[l] g') : f =o[l] fun x => (f' x, g' x) :=
  IsLittleO.of_isBigOWith fun _c cpos => (h.forall_isBigOWith cpos).prod_rightr f' cpos.le

Little-o relation preserved under pairing with auxiliary function

Informal description

Let $f : \alpha \to E$ and $g', f' : \alpha \to F$ be functions to normed spaces, and let $l$ be a filter on $\alpha$. If $f$ is little-o of $g'$ with respect to $l$ (i.e., $f = o[l] g'$), then $f$ is also little-o of the function $x \mapsto (f'(x), g'(x))$ with respect to $l$.

Asymptotics.IsBigO.fiberwise_right theorem

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

Full source

protected theorem IsBigO.fiberwise_right :
    f =O[l ×ˢ l'] g → ∀ᶠ a in l, (f ⟨a, ·⟩) =O[l'] (g ⟨a, ·⟩) := by
  simp only [isBigO_iff, eventually_iff, mem_prod_iff]
  rintro ⟨c, t₁, ht₁, t₂, ht₂, ht⟩
  exact mem_of_superset ht₁ fun _ ha ↦ ⟨c, mem_of_superset ht₂ fun _ hb ↦ ht ⟨ha, hb⟩⟩

Fiberwise Big-O Relation Along Product Filter

Informal description

Let $f$ and $g$ be functions such that $f = O[l \times l'] g$ (i.e., $f$ is big-O of $g$ with respect to the product filter $l \times l'$). Then for almost all $a$ in $l$, the function $f(a, \cdot)$ is big-O of $g(a, \cdot)$ with respect to the filter $l'$.

Asymptotics.IsBigO.fiberwise_left theorem

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

Full source

protected theorem IsBigO.fiberwise_left :
    f =O[l ×ˢ l'] g → ∀ᶠ b in l', (f ⟨·, b⟩) =O[l] (g ⟨·, b⟩) := by
  simp only [isBigO_iff, eventually_iff, mem_prod_iff]
  rintro ⟨c, t₁, ht₁, t₂, ht₂, ht⟩
  exact mem_of_superset ht₂ fun _ hb ↦ ⟨c, mem_of_superset ht₁ fun _ ha ↦ ht ⟨ha, hb⟩⟩

Fiberwise Big-O Relation in First Variable

Informal description

Let $f$ and $g$ be functions such that $f = O[l \times l'] g$ (i.e., $f$ is big-O of $g$ with respect to the product filter $l \times l'$). Then for almost all $b$ in the filter $l'$, the function $x \mapsto f(x, b)$ is big-O of $x \mapsto g(x, b)$ with respect to the filter $l$.

Asymptotics.IsBigO.comp_fst theorem

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

Full source

protected theorem IsBigO.comp_fst : f =O[l] g → (f ∘ Prod.fst) =O[l ×ˢ l'] (g ∘ Prod.fst) := by
  simp only [isBigO_iff, eventually_prod_iff]
  exact fun ⟨c, hc⟩ ↦ ⟨c, _, hc, fun _ ↦ True, eventually_true l', fun {_} h {_} _ ↦ h⟩

Big-O relation preserved under first component composition

Informal description

Let $f$ and $g$ be functions such that $f = O[l] g$ (i.e., $f$ is big-O of $g$ with respect to filter $l$). Then the composition $f \circ \pi_1$ is big-O of $g \circ \pi_1$ with respect to the product filter $l \times l'$, where $\pi_1$ denotes the projection onto the first component.

Asymptotics.IsBigO.comp_snd theorem

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

Full source

protected theorem IsBigO.comp_snd : f =O[l] g → (f ∘ Prod.snd) =O[l' ×ˢ l] (g ∘ Prod.snd) := by
  simp only [isBigO_iff, eventually_prod_iff]
  exact fun ⟨c, hc⟩ ↦ ⟨c, fun _ ↦ True, eventually_true l', _, hc, fun _ ↦ id⟩

Big-O relation preserved under second component composition

Informal description

Let $f$ and $g$ be functions such that $f = O[l] g$ (i.e., $f$ is big-O of $g$ with respect to filter $l$). Then the composition $f \circ \text{snd}$ is big-O of $g \circ \text{snd}$ with respect to the product filter $l' \times l$, where $\text{snd}$ denotes the projection onto the second component.

Asymptotics.IsLittleO.comp_fst theorem

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

Full source

protected theorem IsLittleO.comp_fst : f =o[l] g → (f ∘ Prod.fst) =o[l ×ˢ l'] (g ∘ Prod.fst) := by
  simp only [isLittleO_iff, eventually_prod_iff]
  exact fun h _ hc ↦ ⟨_, h hc, fun _ ↦ True, eventually_true l', fun {_} h {_} _ ↦ h⟩

Little-o relation preserved under first component composition

Informal description

Let $f$ and $g$ be functions such that $f = o[l] g$ (i.e., $f$ is little-o of $g$ with respect to filter $l$). Then the composition $f \circ \text{fst}$ is little-o of $g \circ \text{fst}$ with respect to the product filter $l \times l'$, where $\text{fst}$ denotes the projection onto the first component.

Asymptotics.IsLittleO.comp_snd theorem

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

Full source

protected theorem IsLittleO.comp_snd : f =o[l] g → (f ∘ Prod.snd) =o[l' ×ˢ l] (g ∘ Prod.snd) := by
  simp only [isLittleO_iff, eventually_prod_iff]
  exact fun h _ hc ↦ ⟨fun _ ↦ True, eventually_true l', _, h hc, fun _ ↦ id⟩

Little-o relation preserved under second component composition

Informal description

Let $f$ and $g$ be functions such that $f = o[l] g$ (i.e., $f$ is little-o of $g$ with respect to filter $l$). Then the composition $f \circ \text{snd}$ is little-o of $g \circ \text{snd}$ with respect to the product filter $l' \times l$, where $\text{snd}$ denotes the projection onto the second component.

Asymptotics.IsBigOWith.prod_left_same theorem

(hf : IsBigOWith c l f' k') (hg : IsBigOWith c l g' k') : IsBigOWith c l (fun x => (f' x, g' x)) k'

Full source

theorem IsBigOWith.prod_left_same (hf : IsBigOWith c l f' k') (hg : IsBigOWith c l g' k') :
    IsBigOWith c l (fun x => (f' x, g' x)) k' := by
  rw [isBigOWith_iff] at *; filter_upwards [hf, hg] with x using max_le

Simultaneous Big-O Bound for Product of Functions with Same Constant

Informal description

Let $E$ and $F$ be normed spaces, $l$ a filter on a type $\alpha$, and $f', g' : \alpha \to E$, $k' : \alpha \to F$ functions. If there exists a constant $c \in \mathbb{R}$ such that $\|f'(x)\| \leq c \cdot \|k'(x)\|$ and $\|g'(x)\| \leq c \cdot \|k'(x)\|$ hold eventually for $x$ in $l$, then the product function $x \mapsto (f'(x), g'(x))$ satisfies $\|(f'(x), g'(x))\| \leq c \cdot \|k'(x)\|$ eventually for $x$ in $l$.

Asymptotics.IsBigOWith.prod_left theorem

(hf : IsBigOWith c l f' k') (hg : IsBigOWith c' l g' k') : IsBigOWith (max c c') l (fun x => (f' x, g' x)) k'

Full source

theorem IsBigOWith.prod_left (hf : IsBigOWith c l f' k') (hg : IsBigOWith c' l g' k') :
    IsBigOWith (max c c') l (fun x => (f' x, g' x)) k' :=
  (hf.weaken <| le_max_left c c').prod_left_same (hg.weaken <| le_max_right c c')

Big-O Bound for Product of Functions with Maximum Constant

Informal description

Let $E$ and $F$ be normed spaces, $l$ a filter on a type $\alpha$, and $f', g' : \alpha \to E$, $k' : \alpha \to F$ functions. If there exist real constants $c$ and $c'$ such that $\|f'(x)\| \leq c \cdot \|k'(x)\|$ and $\|g'(x)\| \leq c' \cdot \|k'(x)\|$ hold eventually for $x$ in $l$, then the product function $x \mapsto (f'(x), g'(x))$ satisfies $\|(f'(x), g'(x))\| \leq \max(c, c') \cdot \|k'(x)\|$ eventually for $x$ in $l$.

Asymptotics.IsBigOWith.prod_left_fst theorem

(h : IsBigOWith c l (fun x => (f' x, g' x)) k') : IsBigOWith c l f' k'

Full source

theorem IsBigOWith.prod_left_fst (h : IsBigOWith c l (fun x => (f' x, g' x)) k') :
    IsBigOWith c l f' k' :=
  (isBigOWith_fst_prod.trans h zero_le_one).congr_const <| one_mul c

First Component Bound in Product Big-O Relation

Informal description

Let $E$ and $F$ be normed spaces, $l$ a filter on a type $\alpha$, and $f' : \alpha \to E$, $g' : \alpha \to F$, $k' : \alpha \to G$ functions. If there exists a constant $c \in \mathbb{R}$ such that $\|(f'(x), g'(x))\| \leq c \cdot \|k'(x)\|$ holds eventually for $x$ in $l$, then $\|f'(x)\| \leq c \cdot \|k'(x)\|$ also holds eventually for $x$ in $l$.

Asymptotics.IsBigOWith.prod_left_snd theorem

(h : IsBigOWith c l (fun x => (f' x, g' x)) k') : IsBigOWith c l g' k'

Full source

theorem IsBigOWith.prod_left_snd (h : IsBigOWith c l (fun x => (f' x, g' x)) k') :
    IsBigOWith c l g' k' :=
  (isBigOWith_snd_prod.trans h zero_le_one).congr_const <| one_mul c

Second Component of Product Function is Big-O With Same Constant

Informal description

Asymptotics.isBigOWith_prod_left theorem

: IsBigOWith c l (fun x => (f' x, g' x)) k' ↔ IsBigOWith c l f' k' ∧ IsBigOWith c l g' k'

Full source

theorem isBigOWith_prod_left :
    IsBigOWithIsBigOWith c l (fun x => (f' x, g' x)) k' ↔ IsBigOWith c l f' k' ∧ IsBigOWith c l g' k' :=
  ⟨fun h => ⟨h.prod_left_fst, h.prod_left_snd⟩, fun h => h.1.prod_left_same h.2⟩

Equivalence of Product Big-O Bound with Componentwise Bounds

Informal description

Let $E$ and $F$ be normed spaces, $l$ a filter on a type $\alpha$, and $f' : \alpha \to E$, $g' : \alpha \to F$, $k' : \alpha \to G$ functions. For any real constant $c \geq 0$, the following are equivalent: 1. The product function $x \mapsto (f'(x), g'(x))$ satisfies $\|(f'(x), g'(x))\| \leq c \|k'(x)\|$ for all $x$ in $l$ eventually. 2. Both $\|f'(x)\| \leq c \|k'(x)\|$ and $\|g'(x)\| \leq c \|k'(x)\|$ hold for all $x$ in $l$ eventually.

Asymptotics.IsBigO.prod_left theorem

(hf : f' =O[l] k') (hg : g' =O[l] k') : (fun x => (f' x, g' x)) =O[l] k'

Full source

theorem IsBigO.prod_left (hf : f' =O[l] k') (hg : g' =O[l] k') : (fun x => (f' x, g' x)) =O[l] k' :=
  let ⟨_c, hf⟩ := hf.isBigOWith
  let ⟨_c', hg⟩ := hg.isBigOWith
  (hf.prod_left hg).isBigO

Big-O relation for product of functions: $(f', g') =O[l] k'$ when $f' =O[l] k'$ and $g' =O[l] k'$

Informal description

Asymptotics.IsBigO.prod_left_fst theorem

: (fun x => (f' x, g' x)) =O[l] k' → f' =O[l] k'

Full source

theorem IsBigO.prod_left_fst : (fun x => (f' x, g' x)) =O[l] k' → f' =O[l] k' :=
  IsBigO.trans isBigO_fst_prod

First Component of Big-O Product Relation Implies Componentwise Big-O

Informal description

Let $E$ and $F$ be normed spaces, $l$ a filter on a type $\alpha$, and $f' : \alpha \to E$, $g' : \alpha \to F$, $k' : \alpha \to G$ functions. If the product function $x \mapsto (f'(x), g'(x))$ is big-O of $k'$ along $l$ (i.e., $\|(f'(x), g'(x))\| \leq C \|k'(x)\|$ eventually for some constant $C$), then the first component function $f'$ is big-O of $k'$ along $l$ (i.e., $\|f'(x)\| \leq C \|k'(x)\|$ eventually).

Asymptotics.IsBigO.prod_left_snd theorem

: (fun x => (f' x, g' x)) =O[l] k' → g' =O[l] k'

Full source

theorem IsBigO.prod_left_snd : (fun x => (f' x, g' x)) =O[l] k' → g' =O[l] k' :=
  IsBigO.trans isBigO_snd_prod

Second Component Preserves Big-O Relation for Product Function

Informal description

For functions $f' : \alpha \to E$, $g' : \alpha \to F$, and $k' : \alpha \to G$ where $E$, $F$, and $G$ are normed spaces, and a filter $l$ on $\alpha$, if the product function $x \mapsto (f'(x), g'(x))$ is big-O of $k'$ along $l$, then the second component function $g'$ is big-O of $k'$ along $l$.

Asymptotics.isBigO_prod_left theorem

: (fun x => (f' x, g' x)) =O[l] k' ↔ f' =O[l] k' ∧ g' =O[l] k'

Full source

@[simp]
theorem isBigO_prod_left : (fun x => (f' x, g' x)) =O[l] k'(fun x => (f' x, g' x)) =O[l] k' ↔ f' =O[l] k' ∧ g' =O[l] k' :=
  ⟨fun h => ⟨h.prod_left_fst, h.prod_left_snd⟩, fun h => h.1.prod_left h.2⟩

Big-O Equivalence for Product Function: $(f', g') =O[l] k'$ $\leftrightarrow$ $f' =O[l] k'$ and $g' =O[l] k'$

Informal description

Let $E$ and $F$ be normed spaces, $l$ a filter on a type $\alpha$, and $f' : \alpha \to E$, $g' : \alpha \to F$, $k' : \alpha \to G$ functions. The product function $x \mapsto (f'(x), g'(x))$ is big-O of $k'$ along $l$ (i.e., $\|(f'(x), g'(x))\| \leq C \|k'(x)\|$ eventually for some constant $C$) if and only if both $f'$ is big-O of $k'$ along $l$ and $g'$ is big-O of $k'$ along $l$.

Asymptotics.IsLittleO.prod_left theorem

(hf : f' =o[l] k') (hg : g' =o[l] k') : (fun x => (f' x, g' x)) =o[l] k'

Full source

theorem IsLittleO.prod_left (hf : f' =o[l] k') (hg : g' =o[l] k') :
    (fun x => (f' x, g' x)) =o[l] k' :=
  IsLittleO.of_isBigOWith fun _c hc =>
    (hf.forall_isBigOWith hc).prod_left_same (hg.forall_isBigOWith hc)

Little-o relation for product of functions

Informal description

Let $E$ and $F$ be normed spaces, $l$ a filter on a type $\alpha$, and $f', g' : \alpha \to E$, $k' : \alpha \to F$ functions. If $f' = o[l] k'$ and $g' = o[l] k'$, then the product function $x \mapsto (f'(x), g'(x))$ satisfies $(f', g') = o[l] k'$.

Asymptotics.IsLittleO.prod_left_fst theorem

: (fun x => (f' x, g' x)) =o[l] k' → f' =o[l] k'

Full source

theorem IsLittleO.prod_left_fst : (fun x => (f' x, g' x)) =o[l] k' → f' =o[l] k' :=
  IsBigO.trans_isLittleO isBigO_fst_prod

First Component of Little-o Product is Little-o

Informal description

Let $E$ and $F$ be normed spaces, $l$ a filter on a type $\alpha$, and $f' : \alpha \to E$, $g' : \alpha \to F$, $k' : \alpha \to G$ functions. If the product function $x \mapsto (f'(x), g'(x))$ is little-o of $k'$ along $l$, then $f'$ is little-o of $k'$ along $l$.

Asymptotics.IsLittleO.prod_left_snd theorem

: (fun x => (f' x, g' x)) =o[l] k' → g' =o[l] k'

Full source

theorem IsLittleO.prod_left_snd : (fun x => (f' x, g' x)) =o[l] k' → g' =o[l] k' :=
  IsBigO.trans_isLittleO isBigO_snd_prod

Second Component of Little-o Product Relation

Informal description

Let $E$ and $F$ be normed spaces, $l$ a filter on a type $\alpha$, and $f' : \alpha \to E$, $g' : \alpha \to F$, $k' : \alpha \to G$ functions. If the product function $x \mapsto (f'(x), g'(x))$ is little-o of $k'$ along $l$, then the second component function $g'$ is little-o of $k'$ along $l$.

Asymptotics.isLittleO_prod_left theorem

: (fun x => (f' x, g' x)) =o[l] k' ↔ f' =o[l] k' ∧ g' =o[l] k'

Full source

@[simp]
theorem isLittleO_prod_left : (fun x => (f' x, g' x)) =o[l] k'(fun x => (f' x, g' x)) =o[l] k' ↔ f' =o[l] k' ∧ g' =o[l] k' :=
  ⟨fun h => ⟨h.prod_left_fst, h.prod_left_snd⟩, fun h => h.1.prod_left h.2⟩

Little-o Product Relation: $(f', g') = o[l] k' \leftrightarrow f' = o[l] k' \land g' = o[l] k'$

Informal description

Let $E$ and $F$ be normed spaces, $l$ a filter on a type $\alpha$, and $f' : \alpha \to E$, $g' : \alpha \to F$, $k' : \alpha \to G$ functions. The product function $x \mapsto (f'(x), g'(x))$ is little-o of $k'$ along $l$ if and only if both $f'$ is little-o of $k'$ along $l$ and $g'$ is little-o of $k'$ along $l$.

Asymptotics.IsBigOWith.add theorem

 (h₁ : IsBigOWith c₁ l f₁ g) (h₂ : IsBigOWith c₂ l f₂ g) : IsBigOWith (c₁ + c₂) l (fun x => f₁ x + f₂ x) g

Full source

theorem IsBigOWith.add (h₁ : IsBigOWith c₁ l f₁ g) (h₂ : IsBigOWith c₂ l f₂ g) :
    IsBigOWith (c₁ + c₂) l (fun x => f₁ x + f₂ x) g := by
  rw [IsBigOWith_def] at *
  filter_upwards [h₁, h₂] with x hx₁ hx₂ using
    calc
      ‖f₁ x + f₂ x‖ ≤ c₁ * ‖g x‖ + c₂ * ‖g x‖ := norm_add_le_of_le hx₁ hx₂
      _ = (c₁ + c₂) * ‖g x‖ := (add_mul _ _ _).symm

Sum of Big-O Bounds with Constants $c_1$ and $c_2$ is Big-O with Constant $c_1 + c_2$

Informal description

Let $f_1, f_2 : \alpha \to E$ and $g : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If there exist constants $c_1, c_2 \in \mathbb{R}$ such that $\|f_1(x)\| \leq c_1 \|g(x)\|$ and $\|f_2(x)\| \leq c_2 \|g(x)\|$ for all $x$ in $l$ eventually, then the sum $f_1 + f_2$ satisfies $\|(f_1 + f_2)(x)\| \leq (c_1 + c_2) \|g(x)\|$ for all $x$ in $l$ eventually.

Asymptotics.IsBigO.add theorem

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

Full source

theorem IsBigO.add (h₁ : f₁ =O[l] g) (h₂ : f₂ =O[l] g) : (fun x => f₁ x + f₂ x) =O[l] g :=
  let ⟨_c₁, hc₁⟩ := h₁.isBigOWith
  let ⟨_c₂, hc₂⟩ := h₂.isBigOWith
  (hc₁.add hc₂).isBigO

Sum of Big-O Functions is Big-O

Informal description

Let $f_1, f_2 : \alpha \to E$ and $g : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If $f_1$ is big O of $g$ along $l$ and $f_2$ is big O of $g$ along $l$, then the sum $f_1 + f_2$ is big O of $g$ along $l$.

Asymptotics.IsLittleO.add theorem

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

Full source

theorem IsLittleO.add (h₁ : f₁ =o[l] g) (h₂ : f₂ =o[l] g) : (fun x => f₁ x + f₂ x) =o[l] g :=
  IsLittleO.of_isBigOWith fun c cpos =>
    ((h₁.forall_isBigOWith <| half_pos cpos).add (h₂.forall_isBigOWith <|
      half_pos cpos)).congr_const (add_halves c)

Sum of Little-o Functions is Little-o

Informal description

Let $f_1, f_2 : \alpha \to E$ and $g : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If $f_1 = o[l] g$ and $f_2 = o[l] g$, then their sum satisfies $f_1 + f_2 = o[l] g$.

Asymptotics.IsLittleO.add_add theorem

 (h₁ : f₁ =o[l] g₁) (h₂ : f₂ =o[l] g₂) : (fun x => f₁ x + f₂ x) =o[l] fun x => ‖g₁ x‖ + ‖g₂ x‖

Full source

theorem IsLittleO.add_add (h₁ : f₁ =o[l] g₁) (h₂ : f₂ =o[l] g₂) :
    (fun x => f₁ x + f₂ x) =o[l] fun x => ‖g₁ x‖ + ‖g₂ x‖ := by
  refine (h₁.trans_le fun x => ?_).add (h₂.trans_le ?_) <;> simp [abs_of_nonneg, add_nonneg]

Sum of Little-o Functions is Little-o of Norm Sum

Informal description

Let $f_1, f_2 : \alpha \to E$ and $g_1, g_2 : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If $f_1 = o[l] g_1$ and $f_2 = o[l] g_2$, then the sum $f_1 + f_2$ is little-o of the function $x \mapsto \|g_1(x)\| + \|g_2(x)\|$ along $l$.

Asymptotics.IsBigO.add_isLittleO theorem

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

Full source

theorem IsBigO.add_isLittleO (h₁ : f₁ =O[l] g) (h₂ : f₂ =o[l] g) : (fun x => f₁ x + f₂ x) =O[l] g :=
  h₁.add h₂.isBigO

Sum of Big-O and Little-o Functions is Big-O

Informal description

Let $f_1, f_2 : \alpha \to E$ and $g : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If $f_1$ is big-O of $g$ along $l$ and $f_2$ is little-o of $g$ along $l$, then their sum $f_1 + f_2$ is big-O of $g$ along $l$.

Asymptotics.IsLittleO.add_isBigO theorem

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

Full source

theorem IsLittleO.add_isBigO (h₁ : f₁ =o[l] g) (h₂ : f₂ =O[l] g) : (fun x => f₁ x + f₂ x) =O[l] g :=
  h₁.isBigO.add h₂

Sum of Little-o and Big-O Functions is Big-O

Informal description

Let $f_1, f_2 : \alpha \to E$ and $g : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If $f_1$ is little-o of $g$ along $l$ and $f_2$ is big-O of $g$ along $l$, then the sum $f_1 + f_2$ is big-O of $g$ along $l$.

Asymptotics.IsBigOWith.add_isLittleO theorem

 (h₁ : IsBigOWith c₁ l f₁ g) (h₂ : f₂ =o[l] g) (hc : c₁ < c₂) : IsBigOWith c₂ l (fun x => f₁ x + f₂ x) g

Full source

theorem IsBigOWith.add_isLittleO (h₁ : IsBigOWith c₁ l f₁ g) (h₂ : f₂ =o[l] g) (hc : c₁ < c₂) :
    IsBigOWith c₂ l (fun x => f₁ x + f₂ x) g :=
  (h₁.add (h₂.forall_isBigOWith (sub_pos.2 hc))).congr_const (add_sub_cancel _ _)

Sum of Big-O and Little-o Functions is Big-O with Larger Constant

Informal description

Let $f_1, f_2 : \alpha \to E$ and $g : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If there exists a constant $c_1 \in \mathbb{R}$ such that $\|f_1(x)\| \leq c_1 \|g(x)\|$ for all $x$ in $l$ eventually, and $f_2 = o[l] g$, then for any $c_2 > c_1$, the sum $f_1 + f_2$ satisfies $\|(f_1 + f_2)(x)\| \leq c_2 \|g(x)\|$ for all $x$ in $l$ eventually.

Asymptotics.IsLittleO.add_isBigOWith theorem

 (h₁ : f₁ =o[l] g) (h₂ : IsBigOWith c₁ l f₂ g) (hc : c₁ < c₂) : IsBigOWith c₂ l (fun x => f₁ x + f₂ x) g

Full source

theorem IsLittleO.add_isBigOWith (h₁ : f₁ =o[l] g) (h₂ : IsBigOWith c₁ l f₂ g) (hc : c₁ < c₂) :
    IsBigOWith c₂ l (fun x => f₁ x + f₂ x) g :=
  (h₂.add_isLittleO h₁ hc).congr_left fun _ => add_comm _ _

Sum of Little-o and Big-O With Functions is Big-O With Larger Constant

Informal description

Let $f_1, f_2 : \alpha \to E$ and $g : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If $f_1 = o[l] g$ and there exists a constant $c_1 \in \mathbb{R}$ such that $\|f_2(x)\| \leq c_1 \|g(x)\|$ for all $x$ in $l$ eventually, then for any $c_2 > c_1$, the sum $f_1 + f_2$ satisfies $\|(f_1 + f_2)(x)\| \leq c_2 \|g(x)\|$ for all $x$ in $l$ eventually.

Asymptotics.IsBigOWith.sub theorem

 (h₁ : IsBigOWith c₁ l f₁ g) (h₂ : IsBigOWith c₂ l f₂ g) : IsBigOWith (c₁ + c₂) l (fun x => f₁ x - f₂ x) g

Full source

theorem IsBigOWith.sub (h₁ : IsBigOWith c₁ l f₁ g) (h₂ : IsBigOWith c₂ l f₂ g) :
    IsBigOWith (c₁ + c₂) l (fun x => f₁ x - f₂ x) g := by
  simpa only [sub_eq_add_neg] using h₁.add h₂.neg_left

Difference of Big-O Bounds with Constants $c_1$ and $c_2$ is Big-O with Constant $c_1 + c_2$

Informal description

Let $f_1, f_2 : \alpha \to E$ and $g : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If there exist constants $c_1, c_2 \in \mathbb{R}$ such that $\|f_1(x)\| \leq c_1 \|g(x)\|$ and $\|f_2(x)\| \leq c_2 \|g(x)\|$ for all $x$ in $l$ eventually, then the difference $f_1 - f_2$ satisfies $\|(f_1 - f_2)(x)\| \leq (c_1 + c_2) \|g(x)\|$ for all $x$ in $l$ eventually.

Asymptotics.IsBigOWith.sub_isLittleO theorem

 (h₁ : IsBigOWith c₁ l f₁ g) (h₂ : f₂ =o[l] g) (hc : c₁ < c₂) : IsBigOWith c₂ l (fun x => f₁ x - f₂ x) g

Full source

theorem IsBigOWith.sub_isLittleO (h₁ : IsBigOWith c₁ l f₁ g) (h₂ : f₂ =o[l] g) (hc : c₁ < c₂) :
    IsBigOWith c₂ l (fun x => f₁ x - f₂ x) g := by
  simpa only [sub_eq_add_neg] using h₁.add_isLittleO h₂.neg_left hc

Difference of Big-O and Little-o Functions is Big-O with Larger Constant

Informal description

Let $f_1, f_2 : \alpha \to E$ and $g : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If there exists a constant $c_1 \in \mathbb{R}$ such that $\|f_1(x)\| \leq c_1 \|g(x)\|$ for all $x$ in $l$ eventually, and $f_2 = o[l] g$, then for any $c_2 > c_1$, the difference $f_1 - f_2$ satisfies $\|(f_1 - f_2)(x)\| \leq c_2 \|g(x)\|$ for all $x$ in $l$ eventually.

Asymptotics.IsBigO.sub theorem

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

Full source

theorem IsBigO.sub (h₁ : f₁ =O[l] g) (h₂ : f₂ =O[l] g) : (fun x => f₁ x - f₂ x) =O[l] g := by
  simpa only [sub_eq_add_neg] using h₁.add h₂.neg_left

Difference of Big-O Functions is Big-O

Informal description

Let $f_1, f_2 : \alpha \to E$ and $g : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If $f_1$ is big O of $g$ along $l$ and $f_2$ is big O of $g$ along $l$, then the difference $f_1 - f_2$ is big O of $g$ along $l$.

Asymptotics.IsLittleO.sub theorem

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

Full source

theorem IsLittleO.sub (h₁ : f₁ =o[l] g) (h₂ : f₂ =o[l] g) : (fun x => f₁ x - f₂ x) =o[l] g := by
  simpa only [sub_eq_add_neg] using h₁.add h₂.neg_left

Difference of Little-o Functions is Little-o

Informal description

Let $f_1, f_2 : \alpha \to E$ and $g : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If $f_1 = o[l] g$ and $f_2 = o[l] g$, then their difference satisfies $f_1 - f_2 = o[l] g$.

Asymptotics.IsBigO.add_iff_left theorem

(h₂ : f₂ =O[l] g) : (fun x => f₁ x + f₂ x) =O[l] g ↔ (f₁ =O[l] g)

Full source

theorem IsBigO.add_iff_left (h₂ : f₂ =O[l] g) : (fun x => f₁ x + f₂ x) =O[l] g(fun x => f₁ x + f₂ x) =O[l] g ↔ (f₁ =O[l] g):=
  ⟨fun h ↦ h.sub h₂ |>.congr (fun _ ↦ add_sub_cancel_right _ _) (fun _ ↦ rfl), fun h ↦ h.add h₂⟩

Sum of Big-O Functions is Big-O if and only if First Function is Big-O

Informal description

Let $f_1, f_2 : \alpha \to E$ and $g : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If $f_2$ is big O of $g$ along $l$ (i.e., $f_2 =O[l] g$), then the sum $f_1 + f_2$ is big O of $g$ along $l$ if and only if $f_1$ is big O of $g$ along $l$.

Asymptotics.IsBigO.add_iff_right theorem

(h₁ : f₁ =O[l] g) : (fun x => f₁ x + f₂ x) =O[l] g ↔ (f₂ =O[l] g)

Full source

theorem IsBigO.add_iff_right (h₁ : f₁ =O[l] g) : (fun x => f₁ x + f₂ x) =O[l] g(fun x => f₁ x + f₂ x) =O[l] g ↔ (f₂ =O[l] g):=
  ⟨fun h ↦ h.sub h₁ |>.congr (fun _ ↦ (eq_sub_of_add_eq' rfl).symm) (fun _ ↦ rfl), fun h ↦ h₁.add h⟩

Big-O Sum Equivalence: $f_1 + f_2 =O[l] g \leftrightarrow f_2 =O[l] g$ when $f_1 =O[l] g$

Informal description

Let $f_1, f_2 : \alpha \to E$ and $g : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If $f_1$ is big O of $g$ along $l$ (i.e., $f_1 =O[l] g$), then the sum $f_1 + f_2$ is big O of $g$ along $l$ if and only if $f_2$ is big O of $g$ along $l$.

Asymptotics.IsLittleO.add_iff_left theorem

(h₂ : f₂ =o[l] g) : (fun x => f₁ x + f₂ x) =o[l] g ↔ (f₁ =o[l] g)

Full source

theorem IsLittleO.add_iff_left (h₂ : f₂ =o[l] g) : (fun x => f₁ x + f₂ x) =o[l] g(fun x => f₁ x + f₂ x) =o[l] g ↔ (f₁ =o[l] g):=
  ⟨fun h ↦ h.sub h₂ |>.congr (fun _ ↦ add_sub_cancel_right _ _) (fun _ ↦ rfl), fun h ↦ h.add h₂⟩

Little-o Sum Equivalence: $f_1 + f_2 = o[l] g \leftrightarrow f_1 = o[l] g$ when $f_2 = o[l] g$

Informal description

Let $f_1, f_2 : \alpha \to E$ and $g : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If $f_2 = o[l] g$, then the sum $f_1 + f_2 = o[l] g$ if and only if $f_1 = o[l] g$.

Asymptotics.IsLittleO.add_iff_right theorem

(h₁ : f₁ =o[l] g) : (fun x => f₁ x + f₂ x) =o[l] g ↔ (f₂ =o[l] g)

Full source

theorem IsLittleO.add_iff_right (h₁ : f₁ =o[l] g) : (fun x => f₁ x + f₂ x) =o[l] g(fun x => f₁ x + f₂ x) =o[l] g ↔ (f₂ =o[l] g):=
  ⟨fun h ↦ h.sub h₁ |>.congr (fun _ ↦ (eq_sub_of_add_eq' rfl).symm) (fun _ ↦ rfl), fun h ↦ h₁.add h⟩

Little-o Sum Equivalence: $f_1 + f_2 = o[l] g \leftrightarrow f_2 = o[l] g$ when $f_1 = o[l] g$

Informal description

Let $f_1, f_2 : \alpha \to E$ and $g : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If $f_1 = o[l] g$, then the sum $f_1 + f_2 = o[l] g$ if and only if $f_2 = o[l] g$.

Asymptotics.IsBigO.sub_iff_left theorem

(h₂ : f₂ =O[l] g) : (fun x => f₁ x - f₂ x) =O[l] g ↔ (f₁ =O[l] g)

Full source

theorem IsBigO.sub_iff_left (h₂ : f₂ =O[l] g) : (fun x => f₁ x - f₂ x) =O[l] g(fun x => f₁ x - f₂ x) =O[l] g ↔ (f₁ =O[l] g):=
  ⟨fun h ↦ h.add h₂ |>.congr (fun _ ↦ sub_add_cancel ..) (fun _ ↦ rfl), fun h ↦ h.sub h₂⟩

Big-O Difference Criterion: $f_1 - f_2 =O[l] g \leftrightarrow f_1 =O[l] g$ when $f_2 =O[l] g$

Informal description

Let $f_1, f_2 : \alpha \to E$ and $g : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If $f_2$ is big O of $g$ along $l$ (i.e., $f_2 =O[l] g$), then the difference $f_1 - f_2$ is big O of $g$ along $l$ if and only if $f_1$ is big O of $g$ along $l$.

Asymptotics.IsBigO.sub_iff_right theorem

(h₁ : f₁ =O[l] g) : (fun x => f₁ x - f₂ x) =O[l] g ↔ (f₂ =O[l] g)

Full source

theorem IsBigO.sub_iff_right (h₁ : f₁ =O[l] g) : (fun x => f₁ x - f₂ x) =O[l] g(fun x => f₁ x - f₂ x) =O[l] g ↔ (f₂ =O[l] g):=
  ⟨fun h ↦ h₁.sub h |>.congr (fun _ ↦ sub_sub_self ..) (fun _ ↦ rfl), fun h ↦ h₁.sub h⟩

Big-O condition for difference of functions (right version)

Informal description

Let $f_1, f_2 : \alpha \to E$ and $g : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If $f_1$ is big O of $g$ along $l$ (i.e., $f_1 =O[l] g$), then the difference $f_1 - f_2$ is big O of $g$ along $l$ if and only if $f_2$ is big O of $g$ along $l$. In other words: $$(f_1 - f_2 =O[l] g) \leftrightarrow (f_2 =O[l] g)$$

Asymptotics.IsLittleO.sub_iff_left theorem

(h₂ : f₂ =o[l] g) : (fun x => f₁ x - f₂ x) =o[l] g ↔ (f₁ =o[l] g)

Full source

theorem IsLittleO.sub_iff_left (h₂ : f₂ =o[l] g) : (fun x => f₁ x - f₂ x) =o[l] g(fun x => f₁ x - f₂ x) =o[l] g ↔ (f₁ =o[l] g):=
  ⟨fun h ↦ h.add h₂ |>.congr (fun _ ↦ sub_add_cancel ..) (fun _ ↦ rfl), fun h ↦ h.sub h₂⟩

Difference of Little-o Functions is Little-o if and only if First Function is Little-o

Informal description

Let $f_1, f_2 : \alpha \to E$ and $g : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If $f_2 = o[l] g$, then the difference $f_1 - f_2 = o[l] g$ if and only if $f_1 = o[l] g$. Here, $f = o[l] g$ means that for every $c > 0$, there exists a neighborhood in $l$ such that for all $x$ in this neighborhood, $\|f(x)\| \leq c \|g(x)\|$.

Asymptotics.IsLittleO.sub_iff_right theorem

(h₁ : f₁ =o[l] g) : (fun x => f₁ x - f₂ x) =o[l] g ↔ (f₂ =o[l] g)

Full source

theorem IsLittleO.sub_iff_right (h₁ : f₁ =o[l] g) : (fun x => f₁ x - f₂ x) =o[l] g(fun x => f₁ x - f₂ x) =o[l] g ↔ (f₂ =o[l] g):=
  ⟨fun h ↦ h₁.sub h |>.congr (fun _ ↦ sub_sub_self ..) (fun _ ↦ rfl), fun h ↦ h₁.sub h⟩

Equivalence of Little-o Conditions for Differences: $f_1 - f_2 = o[l] g \leftrightarrow f_2 = o[l] g$ under $f_1 = o[l] g$

Informal description

Let $f_1, f_2 : \alpha \to E$ and $g : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If $f_1 = o[l] g$, then the difference $f_1 - f_2$ satisfies $f_1 - f_2 = o[l] g$ if and only if $f_2 = o[l] g$.

Asymptotics.IsBigOWith.symm theorem

(h : IsBigOWith c l (fun x => f₁ x - f₂ x) g) : IsBigOWith c l (fun x => f₂ x - f₁ x) g

Full source

theorem IsBigOWith.symm (h : IsBigOWith c l (fun x => f₁ x - f₂ x) g) :
    IsBigOWith c l (fun x => f₂ x - f₁ x) g :=
  h.neg_left.congr_left fun _x => neg_sub _ _

Symmetry of Big-O With Relation for Differences: $\text{IsBigOWith}(c, l, f_1 - f_2, g) \leftrightarrow \text{IsBigOWith}(c, l, f_2 - f_1, g)$

Informal description

Let $E$ and $F$ be normed spaces, $l$ a filter on a type $\alpha$, and $g : \alpha \to F$ a function. For any real constant $c$ and functions $f_1, f_2 : \alpha \to E$, if the difference $f_1 - f_2$ satisfies $\text{IsBigOWith}(c, l, f_1 - f_2, g)$, then the reversed difference $f_2 - f_1$ also satisfies $\text{IsBigOWith}(c, l, f_2 - f_1, g)$. In other words, if $\|f_1(x) - f_2(x)\| \leq c \|g(x)\|$ holds eventually for $x$ in $l$, then $\|f_2(x) - f_1(x)\| \leq c \|g(x)\|$ also holds eventually.

Asymptotics.isBigOWith_comm theorem

: IsBigOWith c l (fun x => f₁ x - f₂ x) g ↔ IsBigOWith c l (fun x => f₂ x - f₁ x) g

Full source

theorem isBigOWith_comm :
    IsBigOWithIsBigOWith c l (fun x => f₁ x - f₂ x) g ↔ IsBigOWith c l (fun x => f₂ x - f₁ x) g :=
  ⟨IsBigOWith.symm, IsBigOWith.symm⟩

Commutativity of Big-O With Relation for Differences: $\text{IsBigOWith}(c, l, f_1 - f_2, g) \leftrightarrow \text{IsBigOWith}(c, l, f_2 - f_1, g)$

Informal description

For a real constant $c$, a filter $l$ on a type $\alpha$, and functions $f_1, f_2 : \alpha \to E$ and $g : \alpha \to F$ where $E$ and $F$ are normed spaces, the following are equivalent: 1. $\text{IsBigOWith}(c, l, f_1 - f_2, g)$ 2. $\text{IsBigOWith}(c, l, f_2 - f_1, g)$ In other words, the difference $f_1 - f_2$ satisfies the big-O bound with constant $c$ if and only if the reversed difference $f_2 - f_1$ satisfies the same bound.

Asymptotics.IsBigO.symm theorem

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

Full source

theorem IsBigO.symm (h : (fun x => f₁ x - f₂ x) =O[l] g) : (fun x => f₂ x - f₁ x) =O[l] g :=
  h.neg_left.congr_left fun _x => neg_sub _ _

Symmetry of Big-O Relation for Differences: $f_1 - f_2 =O[l] g \leftrightarrow f_2 - f_1 =O[l] g$

Informal description

Let $f_1, f_2 : \alpha \to E$ and $g : \alpha \to F$ be functions, and let $l$ be a filter on $\alpha$. If the difference $f_1 - f_2$ is big-O of $g$ along $l$ (i.e., $f_1 - f_2 =O[l] g$), then the reversed difference $f_2 - f_1$ is also big-O of $g$ along $l$ (i.e., $f_2 - f_1 =O[l] g$).

Asymptotics.isBigO_comm theorem

: (fun x => f₁ x - f₂ x) =O[l] g ↔ (fun x => f₂ x - f₁ x) =O[l] g

Full source

theorem isBigO_comm : (fun x => f₁ x - f₂ x) =O[l] g(fun x => f₁ x - f₂ x) =O[l] g ↔ (fun x => f₂ x - f₁ x) =O[l] g :=
  ⟨IsBigO.symm, IsBigO.symm⟩

Commutativity of Big-O Relation for Differences: $f_1 - f_2 =O[l] g \leftrightarrow f_2 - f_1 =O[l] g$

Informal description

For functions $f_1, f_2 : \alpha \to E$ and $g : \alpha \to F$ where $E$ and $F$ are normed spaces, and a filter $l$ on $\alpha$, the difference $f_1 - f_2$ is big-O of $g$ along $l$ if and only if the reversed difference $f_2 - f_1$ is big-O of $g$ along $l$. In other words, $f_1 - f_2 =O[l] g \leftrightarrow f_2 - f_1 =O[l] g$.

Asymptotics.IsLittleO.symm theorem

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

Full source

theorem IsLittleO.symm (h : (fun x => f₁ x - f₂ x) =o[l] g) : (fun x => f₂ x - f₁ x) =o[l] g := by
  simpa only [neg_sub] using h.neg_left

Symmetry of Little-o Relation for Differences

Informal description

Let $f₁, f₂ : \alpha \to E$ and $g : \alpha \to F$ be functions, and let $l$ be a filter on $\alpha$. If the difference $f₁ - f₂$ is little-o of $g$ with respect to $l$, then the difference $f₂ - f₁$ is also little-o of $g$ with respect to $l$. In other words, if $f₁ - f₂ = o[l] g$, then $f₂ - f₁ = o[l] g$.

Asymptotics.isLittleO_comm theorem

: (fun x => f₁ x - f₂ x) =o[l] g ↔ (fun x => f₂ x - f₁ x) =o[l] g

Full source

theorem isLittleO_comm : (fun x => f₁ x - f₂ x) =o[l] g(fun x => f₁ x - f₂ x) =o[l] g ↔ (fun x => f₂ x - f₁ x) =o[l] g :=
  ⟨IsLittleO.symm, IsLittleO.symm⟩

Commutativity of Little-o Relation for Differences

Informal description

For functions $f₁, f₂ : \alpha \to E$ and $g : \alpha \to F$ with respect to a filter $l$ on $\alpha$, the difference $f₁ - f₂$ is little-o of $g$ if and only if the difference $f₂ - f₁$ is little-o of $g$. In other words, $f₁ - f₂ = o[l] g \leftrightarrow f₂ - f₁ = o[l] g$.

Asymptotics.IsBigOWith.triangle theorem

 (h₁ : IsBigOWith c l (fun x => f₁ x - f₂ x) g) (h₂ : IsBigOWith c' l (fun x => f₂ x - f₃ x) g) :
  IsBigOWith (c + c') l (fun x => f₁ x - f₃ x) g

Full source

theorem IsBigOWith.triangle (h₁ : IsBigOWith c l (fun x => f₁ x - f₂ x) g)
    (h₂ : IsBigOWith c' l (fun x => f₂ x - f₃ x) g) :
    IsBigOWith (c + c') l (fun x => f₁ x - f₃ x) g :=
  (h₁.add h₂).congr_left fun _x => sub_add_sub_cancel _ _ _

Triangle Inequality for Big-O Bounds with Constants $c$ and $c'$

Informal description

Let $f_1, f_2, f_3 : \alpha \to E$ and $g : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If there exist constants $c, c' \in \mathbb{R}$ such that $\|f_1(x) - f_2(x)\| \leq c \|g(x)\|$ and $\|f_2(x) - f_3(x)\| \leq c' \|g(x)\|$ for all $x$ in $l$ eventually, then the difference $f_1(x) - f_3(x)$ satisfies $\|f_1(x) - f_3(x)\| \leq (c + c') \|g(x)\|$ for all $x$ in $l$ eventually.

Asymptotics.IsBigO.triangle theorem

 (h₁ : (fun x => f₁ x - f₂ x) =O[l] g) (h₂ : (fun x => f₂ x - f₃ x) =O[l] g) : (fun x => f₁ x - f₃ x) =O[l] g

Full source

theorem IsBigO.triangle (h₁ : (fun x => f₁ x - f₂ x) =O[l] g)
    (h₂ : (fun x => f₂ x - f₃ x) =O[l] g) : (fun x => f₁ x - f₃ x) =O[l] g :=
  (h₁.add h₂).congr_left fun _x => sub_add_sub_cancel _ _ _

Triangle Inequality for Big-O Relations

Informal description

Let $f_1, f_2, f_3 : \alpha \to E$ and $g : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If the difference $f_1 - f_2$ is big-O of $g$ along $l$ (i.e., $f_1 - f_2 =O[l] g$) and the difference $f_2 - f_3$ is big-O of $g$ along $l$ (i.e., $f_2 - f_3 =O[l] g$), then the difference $f_1 - f_3$ is big-O of $g$ along $l$ (i.e., $f_1 - f_3 =O[l] g$).

Asymptotics.IsLittleO.triangle theorem

 (h₁ : (fun x => f₁ x - f₂ x) =o[l] g) (h₂ : (fun x => f₂ x - f₃ x) =o[l] g) : (fun x => f₁ x - f₃ x) =o[l] g

Full source

theorem IsLittleO.triangle (h₁ : (fun x => f₁ x - f₂ x) =o[l] g)
    (h₂ : (fun x => f₂ x - f₃ x) =o[l] g) : (fun x => f₁ x - f₃ x) =o[l] g :=
  (h₁.add h₂).congr_left fun _x => sub_add_sub_cancel _ _ _

Triangle Inequality for Little-o Asymptotics

Informal description

Let $f_1, f_2, f_3 : \alpha \to E$ and $g : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If $f_1 - f_2 = o[l] g$ and $f_2 - f_3 = o[l] g$, then $f_1 - f_3 = o[l] g$.

Asymptotics.IsBigO.congr_of_sub theorem

(h : (fun x => f₁ x - f₂ x) =O[l] g) : f₁ =O[l] g ↔ f₂ =O[l] g

Full source

theorem IsBigO.congr_of_sub (h : (fun x => f₁ x - f₂ x) =O[l] g) : f₁ =O[l] gf₁ =O[l] g ↔ f₂ =O[l] g :=
  ⟨fun h' => (h'.sub h).congr_left fun _x => sub_sub_cancel _ _, fun h' =>
    (h.add h').congr_left fun _x => sub_add_cancel _ _⟩

Big-O Equivalence under Function Difference: $f_1 =O[l] g \leftrightarrow f_2 =O[l] g$ when $f_1 - f_2 =O[l] g$

Informal description

Let $f_1, f_2 : \alpha \to E$ and $g : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If the difference $f_1 - f_2$ is big-O of $g$ along $l$ (i.e., $f_1 - f_2 =O[l] g$), then $f_1$ is big-O of $g$ along $l$ if and only if $f_2$ is big-O of $g$ along $l$.

Asymptotics.IsLittleO.congr_of_sub theorem

(h : (fun x => f₁ x - f₂ x) =o[l] g) : f₁ =o[l] g ↔ f₂ =o[l] g

Full source

theorem IsLittleO.congr_of_sub (h : (fun x => f₁ x - f₂ x) =o[l] g) : f₁ =o[l] gf₁ =o[l] g ↔ f₂ =o[l] g :=
  ⟨fun h' => (h'.sub h).congr_left fun _x => sub_sub_cancel _ _, fun h' =>
    (h.add h').congr_left fun _x => sub_add_cancel _ _⟩

Little-o Equivalence Under Function Difference

Informal description

Let $f_1, f_2 : \alpha \to E$ and $g : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If $f_1 - f_2 = o[l] g$, then $f_1 = o[l] g$ if and only if $f_2 = o[l] g$.

Asymptotics.isLittleO_zero theorem

: (fun _x => (0 : E')) =o[l] g'

Full source

theorem isLittleO_zero : (fun _x => (0 : E')) =o[l] g' :=
  IsLittleO.of_bound fun c hc =>
    univ_mem' fun x => by simpa using mul_nonneg hc.le (norm_nonneg <| g' x)

Zero function is $o(g')$ for any $g'$

Informal description

For any filter $l$ and any function $g'$ with codomain in a normed space $E'$, the zero function is little-o of $g'$ along $l$. That is, the zero function grows asymptotically slower than $g'$ as the argument approaches the limit defined by $l$.

Asymptotics.isBigOWith_zero theorem

(hc : 0 ≤ c) : IsBigOWith c l (fun _x => (0 : E')) g'

Full source

theorem isBigOWith_zero (hc : 0 ≤ c) : IsBigOWith c l (fun _x => (0 : E')) g' :=
  IsBigOWith.of_bound <| univ_mem' fun x => by simpa using mul_nonneg hc (norm_nonneg <| g' x)

Zero Function is Big-O with Constant $c \geq 0$

Informal description

For any real constant $c \geq 0$, any filter $l$, and any function $g'$ with codomain in a normed space $E'$, the zero function satisfies $\text{IsBigOWith}(c, l, 0, g')$. That is, the zero function is bounded by $c$ times $g'$ along $l$.

Asymptotics.isBigOWith_zero' theorem

: IsBigOWith 0 l (fun _x => (0 : E')) g

Full source

theorem isBigOWith_zero' : IsBigOWith 0 l (fun _x => (0 : E')) g :=
  IsBigOWith.of_bound <| univ_mem' fun x => by simp

Zero Function is Big-O with Constant Zero

Informal description

For any filter $l$ and any function $g$ with codomain in a normed space, the zero function satisfies $\text{IsBigOWith}(0, l, 0, g)$. That is, the zero function is bounded by $0$ times $g$ along $l$.

Asymptotics.isBigO_zero theorem

: (fun _x => (0 : E')) =O[l] g

Full source

theorem isBigO_zero : (fun _x => (0 : E')) =O[l] g :=
  isBigO_iff_isBigOWith.2 ⟨0, isBigOWith_zero' _ _⟩

Zero Function is Big-O of Any Function

Informal description

The zero function is big O of any function $g$ along any filter $l$. That is, $0 =O[l] g$.

Asymptotics.isBigO_refl_left theorem

: (fun x => f' x - f' x) =O[l] g'

Full source

theorem isBigO_refl_left : (fun x => f' x - f' x) =O[l] g' :=
  (isBigO_zero g' l).congr_left fun _x => (sub_self _).symm

Big-O of Zero Difference Function

Informal description

For any function $f'$ and filter $l$, the function $x \mapsto f'(x) - f'(x)$ is big-O of any function $g'$ along $l$, i.e., $0 =O[l] g'$.

Asymptotics.isLittleO_refl_left theorem

: (fun x => f' x - f' x) =o[l] g'

Full source

theorem isLittleO_refl_left : (fun x => f' x - f' x) =o[l] g' :=
  (isLittleO_zero g' l).congr_left fun _x => (sub_self _).symm

Zero Difference Function is Little-o of Any Function

Informal description

For any function $f'$ and filter $l$, the function $x \mapsto f'(x) - f'(x)$ is little-o of any function $g'$ along $l$, i.e., $0 =o[l] g'$.

Asymptotics.isBigOWith_zero_right_iff theorem

: (IsBigOWith c l f'' fun _x => (0 : F')) ↔ f'' =ᶠ[l] 0

Full source

@[simp]
theorem isBigOWith_zero_right_iff : (IsBigOWith c l f'' fun _x => (0 : F')) ↔ f'' =ᶠ[l] 0 := by
  simp only [IsBigOWith_def, exists_prop, norm_zero, mul_zero,
    norm_le_zero_iff, EventuallyEq, Pi.zero_apply]

Big-O with Zero Right-Hand Side Characterization: $\text{IsBigOWith}(c, l, f'', 0) \leftrightarrow f'' =_l 0$

Informal description

For a real constant $c$, a filter $l$, and a function $f''$ mapping to a normed space $F'$, the relation $\text{IsBigOWith}(c, l, f'', 0)$ holds if and only if $f''$ is eventually equal to zero along the filter $l$.

Asymptotics.isBigO_zero_right_iff theorem

: (f'' =O[l] fun _x => (0 : F')) ↔ f'' =ᶠ[l] 0

Full source

@[simp]
theorem isBigO_zero_right_iff : (f'' =O[l] fun _x => (0 : F')) ↔ f'' =ᶠ[l] 0 :=
  ⟨fun h =>
    let ⟨_c, hc⟩ := h.isBigOWith
    isBigOWith_zero_right_iff.1 hc,
    fun h => (isBigOWith_zero_right_iff.2 h : IsBigOWith 1 _ _ _).isBigO⟩

Big-O with Zero Right-Hand Side Characterization: $f'' =O[l] 0 \leftrightarrow f'' =_l 0$

Informal description

For a function $f''$ mapping to a normed space $F'$ and a filter $l$, the relation $f'' =O[l] 0$ holds if and only if $f''$ is eventually equal to zero along the filter $l$.

Asymptotics.isLittleO_zero_right_iff theorem

: (f'' =o[l] fun _x => (0 : F')) ↔ f'' =ᶠ[l] 0

Full source

@[simp]
theorem isLittleO_zero_right_iff : (f'' =o[l] fun _x => (0 : F')) ↔ f'' =ᶠ[l] 0 :=
  ⟨fun h => isBigO_zero_right_iff.1 h.isBigO,
   fun h => IsLittleO.of_isBigOWith fun _c _hc => isBigOWith_zero_right_iff.2 h⟩

Little-o with Zero Right-Hand Side Characterization: $f'' = o[l] 0 \leftrightarrow f'' =_l 0$

Informal description

For a function $f''$ mapping to a normed space $F'$ and a filter $l$, the relation $f'' = o[l] 0$ holds if and only if $f''$ is eventually equal to zero along the filter $l$.

Asymptotics.isBigOWith_const_const theorem

(c : E) {c' : F''} (hc' : c' ≠ 0) (l : Filter α) : IsBigOWith (‖c‖ / ‖c'‖) l (fun _x : α => c) fun _x => c'

Full source

theorem isBigOWith_const_const (c : E) {c' : F''} (hc' : c' ≠ 0) (l : Filter α) :
    IsBigOWith (‖c‖ / ‖c'‖) l (fun _x : α => c) fun _x => c' := by
  simp only [IsBigOWith_def]
  apply univ_mem'
  intro x
  rw [mem_setOf, div_mul_cancel₀ _ (norm_ne_zero_iff.mpr hc')]

Big-O Bound for Constant Functions: $\|c\| \leq (\|c\| / \|c'\|) \cdot \|c'\|$ when $c' \neq 0$

Informal description

Let $E$ and $F''$ be normed spaces, $c \in E$, and $c' \in F''$ with $c' \neq 0$. For any filter $l$ on a type $\alpha$, the constant function $(\lambda x \mapsto c)$ is big-O of the constant function $(\lambda x \mapsto c')$ along $l$ with constant $\|c\| / \|c'\|$. That is, there exists a constant $C = \|c\| / \|c'\|$ such that for all $x$ in the domain eventually, $\|c\| \leq C \cdot \|c'\|$.

Asymptotics.isBigO_const_const theorem

(c : E) {c' : F''} (hc' : c' ≠ 0) (l : Filter α) : (fun _x : α => c) =O[l] fun _x => c'

Full source

theorem isBigO_const_const (c : E) {c' : F''} (hc' : c' ≠ 0) (l : Filter α) :
    (fun _x : α => c) =O[l] fun _x => c' :=
  (isBigOWith_const_const c hc' l).isBigO

Big-O Relation for Constant Functions: $c =O[l] c'$ when $c' \neq 0$

Informal description

Let $E$ and $F''$ be normed spaces, $c \in E$, and $c' \in F''$ with $c' \neq 0$. For any filter $l$ on a type $\alpha$, the constant function $(\lambda x \mapsto c)$ is big-O of the constant function $(\lambda x \mapsto c')$ along $l$.

Asymptotics.isBigO_const_const_iff theorem

{c : E''} {c' : F''} (l : Filter α) [l.NeBot] : ((fun _x : α => c) =O[l] fun _x => c') ↔ c' = 0 → c = 0

Full source

@[simp]
theorem isBigO_const_const_iff {c : E''} {c' : F''} (l : Filter α) [l.NeBot] :
    ((fun _x : α => c) =O[l] fun _x => c') ↔ c' = 0 → c = 0 := by
  rcases eq_or_ne c' 0 with (rfl | hc')
  · simp [EventuallyEq]
  · simp [hc', isBigO_const_const _ hc']

Big-O Relation for Constant Functions: $c =O[l] c'$ if and only if $c' = 0 \Rightarrow c = 0$

Informal description

Let $E''$ and $F''$ be normed spaces, $c \in E''$, $c' \in F''$, and $l$ be a non-trivial filter on $\alpha$. The constant function $(\lambda x \mapsto c)$ is big-O of the constant function $(\lambda x \mapsto c')$ along $l$ if and only if $c' = 0$ implies $c = 0$.

Asymptotics.isBigO_pure theorem

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

Full source

@[simp]
theorem isBigO_pure {x} : f'' =O[pure x] g''f'' =O[pure x] g'' ↔ g'' x = 0 → f'' x = 0 :=
  calc
    f'' =O[pure x] g'' ↔ (fun _y : α => f'' x) =O[pure x] fun _ => g'' x := isBigO_congr rfl rfl
    _ ↔ g'' x = 0 → f'' x = 0 := isBigO_const_const_iff _

Big-O Relation at a Point: $f'' =O[\text{pure }x] g''$ iff $g''(x) = 0 \Rightarrow f''(x) = 0$

Informal description

For functions $f''$ and $g''$ and a point $x$, the relation $f'' =O[\text{pure }x] g''$ holds if and only if $g''(x) = 0$ implies $f''(x) = 0$.

Asymptotics.isBigOWith_const_mul_self theorem

(c : R) (f : α → R) (l : Filter α) : IsBigOWith ‖c‖ l (fun x => c * f x) f

Full source

theorem isBigOWith_const_mul_self (c : R) (f : α → R) (l : Filter α) :
    IsBigOWith ‖c‖ l (fun x => c * f x) f :=
  isBigOWith_of_le' _ fun _x => norm_mul_le _ _

Big-O bound for scalar multiplication: $\text{IsBigOWith}(\|c\|, l, (c \cdot f), f)$

Informal description

For any scalar $c$ in a seminormed ring $R$, any function $f \colon \alpha \to R$, and any filter $l$ on $\alpha$, the function $x \mapsto c \cdot f(x)$ is big-O of $f$ along $l$ with constant $\|c\|$. That is, $\text{IsBigOWith}(\|c\|, l, (x \mapsto c \cdot f(x)), f)$ holds.

Asymptotics.isBigO_const_mul_self theorem

(c : R) (f : α → R) (l : Filter α) : (fun x => c * f x) =O[l] f

Full source

theorem isBigO_const_mul_self (c : R) (f : α → R) (l : Filter α) : (fun x => c * f x) =O[l] f :=
  (isBigOWith_const_mul_self c f l).isBigO

Big-O relation for scalar multiplication: $(c \cdot f) =O[l] f$

Informal description

For any scalar $c$ in a seminormed ring $R$, any function $f \colon \alpha \to R$, and any filter $l$ on $\alpha$, the function $x \mapsto c \cdot f(x)$ is big-O of $f$ along $l$. That is, $(c \cdot f) =O[l] f$.

Asymptotics.IsBigOWith.const_mul_left theorem

{f : α → R} (h : IsBigOWith c l f g) (c' : R) : IsBigOWith (‖c'‖ * c) l (fun x => c' * f x) g

Full source

theorem IsBigOWith.const_mul_left {f : α → R} (h : IsBigOWith c l f g) (c' : R) :
    IsBigOWith (‖c'‖ * c) l (fun x => c' * f x) g :=
  (isBigOWith_const_mul_self c' f l).trans h (norm_nonneg c')

Left scalar multiplication preserves big-O bound: $\text{IsBigOWith}(c, l, f, g) \Rightarrow \text{IsBigOWith}(\|c'\| \cdot c, l, (c' \cdot f), g)$

Informal description

Let $f \colon \alpha \to \mathbb{R}$ and $g \colon \alpha \to \mathbb{R}$ be functions, and let $l$ be a filter on $\alpha$. If there exists a constant $c \geq 0$ such that $\|f(x)\| \leq c \|g(x)\|$ for all $x$ in $l$ eventually, then for any real constant $c'$, 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_mul_left theorem

{f : α → R} (h : f =O[l] g) (c' : R) : (fun x => c' * f x) =O[l] g

Full source

theorem IsBigO.const_mul_left {f : α → R} (h : f =O[l] g) (c' : R) : (fun x => c' * f x) =O[l] g :=
  let ⟨_c, hc⟩ := h.isBigOWith
  (hc.const_mul_left c').isBigO

Left scalar multiplication preserves big-O relation: $(c' \cdot f) =O[l] g$ if $f =O[l] g$

Informal description

Let $f \colon \alpha \to \mathbb{R}$ and $g \colon \alpha \to \mathbb{R}$ be functions, 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 real constant $c'$, the function $x \mapsto c' \cdot f(x)$ is also big-O of $g$ along $l$, i.e., $(c' \cdot f) =O[l] g$.

Asymptotics.isBigOWith_self_const_mul' theorem

(u : Rˣ) (f : α → R) (l : Filter α) : IsBigOWith ‖(↑u⁻¹ : R)‖ l f fun x => ↑u * f x

Full source

theorem isBigOWith_self_const_mul' (u : Rˣ) (f : α → R) (l : Filter α) :
    IsBigOWith ‖(↑u⁻¹ : R)‖ l f fun x => ↑u * f x :=
  (isBigOWith_const_mul_self ↑u⁻¹ (fun x ↦ ↑u * f x) l).congr_left
    fun x ↦ u.inv_mul_cancel_left (f x)

Big-O relation between $f$ and $u \cdot f$ with constant $\|u^{-1}\|$

Informal description

Let $R$ be a seminormed ring, $u$ be a unit in $R$, $f \colon \alpha \to R$ be a function, and $l$ be a filter on $\alpha$. Then the relation $\text{IsBigOWith}(\|u^{-1}\|, l, f, (x \mapsto u \cdot f(x)))$ holds, meaning that $f$ is big-O of $u \cdot f$ along $l$ with constant $\|u^{-1}\|$.

Asymptotics.isBigOWith_self_const_mul theorem

{c : S} (hc : c ≠ 0) (f : α → S) (l : Filter α) : IsBigOWith ‖c‖⁻¹ l f fun x ↦ c * f x

Full source

theorem isBigOWith_self_const_mul {c : S} (hc : c ≠ 0) (f : α → S) (l : Filter α) :
    IsBigOWith ‖c‖‖c‖⁻¹ l f fun x ↦ c * f x := by
  simp [IsBigOWith, inv_mul_cancel_left₀ (norm_ne_zero_iff.mpr hc)]

Big-O relation between $f$ and $c \cdot f$ with constant $\|c\|^{-1}$

Informal description

Let $S$ be a normed field, $c \in S$ be a nonzero element, $f \colon \alpha \to S$ be a function, and $l$ be a filter on $\alpha$. Then the relation $\text{IsBigOWith}(\|c\|^{-1}, l, f, (x \mapsto c \cdot f(x)))$ holds, meaning that $f$ is big-O of $c \cdot f$ along $l$ with constant $\|c\|^{-1}$.

Asymptotics.isBigO_self_const_mul' theorem

{c : R} (hc : IsUnit c) (f : α → R) (l : Filter α) : f =O[l] fun x => c * f x

Full source

theorem isBigO_self_const_mul' {c : R} (hc : IsUnit c) (f : α → R) (l : Filter α) :
    f =O[l] fun x => c * f x :=
  let ⟨u, hu⟩ := hc
  hu ▸ (isBigOWith_self_const_mul' u f l).isBigO

Big-O relation between $f$ and $c \cdot f$ for unit $c$

Informal description

Let $R$ be a seminormed ring, $f \colon \alpha \to R$ be a function, $l$ be a filter on $\alpha$, and $c \in R$ be a unit. Then $f$ is big-O of the function $x \mapsto c \cdot f(x)$ along $l$, i.e., $f =O[l] (x \mapsto c \cdot f(x))$.

Asymptotics.isBigO_self_const_mul theorem

{c : S} (hc : c ≠ 0) (f : α → S) (l : Filter α) : f =O[l] fun x ↦ c * f x

Full source

theorem isBigO_self_const_mul {c : S} (hc : c ≠ 0) (f : α → S) (l : Filter α) :
    f =O[l] fun x ↦ c * f x :=
  (isBigOWith_self_const_mul hc f l).isBigO

Big-O relation between $f$ and $c \cdot f$ for nonzero $c$

Informal description

Let $S$ be a normed field, $f \colon \alpha \to S$ be a function, $l$ be a filter on $\alpha$, and $c \in S$ be a nonzero element. Then $f$ is big-O of the function $x \mapsto c \cdot f(x)$ along $l$, i.e., $f =O[l] (x \mapsto c \cdot f(x))$.

Asymptotics.isBigO_const_mul_left_iff' theorem

{f : α → R} {c : R} (hc : IsUnit c) : (fun x => c * f x) =O[l] g ↔ f =O[l] g

Full source

theorem isBigO_const_mul_left_iff' {f : α → R} {c : R} (hc : IsUnit c) :
    (fun x => c * f x) =O[l] g(fun x => c * f x) =O[l] g ↔ f =O[l] g :=
  ⟨(isBigO_self_const_mul' hc f l).trans, fun h => h.const_mul_left c⟩

Equivalence of Big-O Relations Under Left Multiplication by a Unit: $(c \cdot f) = O_l(g) \leftrightarrow f = O_l(g)$ for unit $c$

Informal description

Let $R$ be a seminormed ring, $f \colon \alpha \to R$ be a function, $g \colon \alpha \to S$ be another function (where $S$ is a normed space), $l$ be a filter on $\alpha$, and $c \in R$ be a unit. Then the 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: $$ (\lambda x, c \cdot f(x)) = O_l(g) \leftrightarrow f = O_l(g) $$

Asymptotics.isBigO_const_mul_left_iff theorem

{f : α → S} {c : S} (hc : c ≠ 0) : (fun x => c * f x) =O[l] g ↔ f =O[l] g

Full source

theorem isBigO_const_mul_left_iff {f : α → S} {c : S} (hc : c ≠ 0) :
    (fun x => c * f x) =O[l] g(fun x => c * f x) =O[l] g ↔ f =O[l] g :=
  ⟨(isBigO_self_const_mul hc f l).trans, (isBigO_const_mul_self c f l).trans⟩

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

Informal description

Let $S$ be a normed field, $f \colon \alpha \to S$ and $g \colon \alpha \to F$ be functions, $l$ be a filter on $\alpha$, and $c \in S$ be a nonzero element. Then the 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$, i.e., $$(c \cdot f) =O[l] g \leftrightarrow f =O[l] g.$$

Asymptotics.IsLittleO.const_mul_left theorem

{f : α → R} (h : f =o[l] g) (c : R) : (fun x => c * f x) =o[l] g

Full source

theorem IsLittleO.const_mul_left {f : α → R} (h : f =o[l] g) (c : R) : (fun x => c * f x) =o[l] g :=
  (isBigO_const_mul_self c f l).trans_isLittleO h

Little-o Preservation under Scalar Multiplication: $(c \cdot f) = o[l] g$ if $f = o[l] g$

Informal description

Let $f \colon \alpha \to R$ and $g \colon \alpha \to S$ be functions, where $R$ is a seminormed ring and $S$ is a normed space. If $f$ is little-o of $g$ along a filter $l$ (i.e., $f = o[l] g$), then for any constant $c \in R$, the function $x \mapsto c \cdot f(x)$ is also little-o of $g$ along $l$ (i.e., $(c \cdot f) = o[l] g$).

Asymptotics.isLittleO_const_mul_left_iff' theorem

{f : α → R} {c : R} (hc : IsUnit c) : (fun x => c * f x) =o[l] g ↔ f =o[l] g

Full source

theorem isLittleO_const_mul_left_iff' {f : α → R} {c : R} (hc : IsUnit c) :
    (fun x => c * f x) =o[l] g(fun x => c * f x) =o[l] g ↔ f =o[l] g :=
  ⟨(isBigO_self_const_mul' hc f l).trans_isLittleO, fun h => h.const_mul_left c⟩

Equivalence of Little-o Relations under Scalar Multiplication by a Unit: $(c \cdot f) = o[l] g \leftrightarrow f = o[l] g$ for unit $c$

Informal description

Let $R$ be a seminormed ring, $f \colon \alpha \to R$ and $g \colon \alpha \to F$ be functions, $l$ be a filter on $\alpha$, and $c \in R$ be a unit. Then the 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$, i.e., $(c \cdot f) = o[l] g \leftrightarrow f = o[l] g$.

Asymptotics.isLittleO_const_mul_left_iff theorem

{f : α → S} {c : S} (hc : c ≠ 0) : (fun x => c * f x) =o[l] g ↔ f =o[l] g

Full source

theorem isLittleO_const_mul_left_iff {f : α → S} {c : S} (hc : c ≠ 0) :
    (fun x => c * f x) =o[l] g(fun x => c * f x) =o[l] g ↔ f =o[l] g :=
  ⟨(isBigO_self_const_mul hc f l).trans_isLittleO, (isBigO_const_mul_self c f l).trans_isLittleO⟩

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

Informal description

Let $S$ be a normed field, $f \colon \alpha \to S$ be a function, $g \colon \alpha \to F$ be another function, $l$ be a filter on $\alpha$, and $c \in S$ be a nonzero element. Then the 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.IsBigOWith.of_const_mul_right theorem

{g : α → R} {c : R} (hc' : 0 ≤ c') (h : IsBigOWith c' l f fun x => c * g x) : IsBigOWith (c' * ‖c‖) l f g

Full source

theorem IsBigOWith.of_const_mul_right {g : α → R} {c : R} (hc' : 0 ≤ c')
    (h : IsBigOWith c' l f fun x => c * g x) : IsBigOWith (c' * ‖c‖) l f g :=
  h.trans (isBigOWith_const_mul_self c g l) hc'

Big-O bound transformation under scalar multiplication: $\text{IsBigOWith}(c', l, f, c \cdot g) \to \text{IsBigOWith}(c' \cdot \|c\|, l, f, g)$

Informal description

Asymptotics.IsBigO.of_const_mul_right theorem

{g : α → R} {c : R} (h : f =O[l] fun x => c * g x) : f =O[l] g

Full source

theorem IsBigO.of_const_mul_right {g : α → R} {c : R} (h : f =O[l] fun x => c * g x) : f =O[l] g :=
  let ⟨_c, cnonneg, hc⟩ := h.exists_nonneg
  (hc.of_const_mul_right cnonneg).isBigO

Big-O relation preserved under scalar multiplication: $f =O[l] (c \cdot g) \implies f =O[l] g$

Informal description

Let $f : \alpha \to E$ and $g : \alpha \to R$ be functions, where $E$ is a normed space and $R$ is a seminormed ring. If $f$ is big-O of $x \mapsto c \cdot g(x)$ along filter $l$ for some constant $c \in R$, then $f$ is big-O of $g$ along $l$.

Asymptotics.IsBigOWith.const_mul_right' theorem

 {g : α → R} {u : Rˣ} {c' : ℝ} (hc' : 0 ≤ c') (h : IsBigOWith c' l f g) :
  IsBigOWith (c' * ‖(↑u⁻¹ : R)‖) l f fun x => ↑u * g x

Full source

theorem IsBigOWith.const_mul_right' {g : α → R} {u : Rˣ} {c' : ℝ} (hc' : 0 ≤ c')
    (h : IsBigOWith c' l f g) : IsBigOWith (c' * ‖(↑u⁻¹ : R)‖) l f fun x => ↑u * g x :=
  h.trans (isBigOWith_self_const_mul' _ _ _) hc'

Big-O relation between $f$ and $u \cdot g$ with constant $c' \cdot \|u^{-1}\|$

Informal description

Let $R$ be a seminormed ring, $u$ be a unit in $R$, $f \colon \alpha \to R$ and $g \colon \alpha \to R$ be functions, and $l$ be a filter on $\alpha$. Given a nonnegative real constant $c' \geq 0$, if $f$ is big-O of $g$ along $l$ with constant $c'$, then $f$ is big-O of the function $x \mapsto u \cdot g(x)$ along $l$ with constant $c' \cdot \|u^{-1}\|$.

Asymptotics.IsBigOWith.const_mul_right theorem

 {g : α → S} {c : S} (hc : c ≠ 0) {c' : ℝ} (hc' : 0 ≤ c') (h : IsBigOWith c' l f g) :
  IsBigOWith (c' * ‖c‖⁻¹) l f fun x => c * g x

Full source

theorem IsBigOWith.const_mul_right {g : α → S} {c : S} (hc : c ≠ 0) {c' : ℝ} (hc' : 0 ≤ c')
    (h : IsBigOWith c' l f g) : IsBigOWith (c' * ‖c‖‖c‖⁻¹) l f fun x => c * g x :=
  h.trans (isBigOWith_self_const_mul hc g l) hc'

Big-O relation between $f$ and $c \cdot g$ with constant $c' \cdot \|c\|^{-1}$

Informal description

Let $S$ be a normed field, $f : \alpha \to E$ and $g : \alpha \to S$ be functions, $l$ be a filter on $\alpha$, and $c \in S$ be a nonzero element. Suppose there exists a nonnegative real constant $c'$ such that $\text{IsBigOWith}(c', l, f, g)$ holds. Then, the relation $\text{IsBigOWith}(c' \cdot \|c\|^{-1}, l, f, (x \mapsto c \cdot g(x)))$ holds, i.e., $f$ is big-O of $c \cdot g$ along $l$ with constant $c' \cdot \|c\|^{-1}$.

Asymptotics.IsBigO.const_mul_right' theorem

{g : α → R} {c : R} (hc : IsUnit c) (h : f =O[l] g) : f =O[l] fun x => c * g x

Full source

theorem IsBigO.const_mul_right' {g : α → R} {c : R} (hc : IsUnit c) (h : f =O[l] g) :
    f =O[l] fun x => c * g x :=
  h.trans (isBigO_self_const_mul' hc g l)

Big-O Relation Preserved Under Right Multiplication by Unit

Informal description

Let $R$ be a seminormed ring, $f \colon \alpha \to E$ and $g \colon \alpha \to R$ be functions, $l$ be a filter on $\alpha$, and $c \in R$ be a unit. If $f$ is big-O of $g$ along $l$ (i.e., $f =O[l] g$), then $f$ is also big-O of the function $x \mapsto c \cdot g(x)$ along $l$ (i.e., $f =O[l] (x \mapsto c \cdot g(x))$).

Asymptotics.IsBigO.const_mul_right theorem

{g : α → S} {c : S} (hc : c ≠ 0) (h : f =O[l] g) : f =O[l] fun x => c * g x

Full source

theorem IsBigO.const_mul_right {g : α → S} {c : S} (hc : c ≠ 0) (h : f =O[l] g) :
    f =O[l] fun x => c * g x :=
  match h.exists_nonneg with
  | ⟨_, hd, hd'⟩ => (hd'.const_mul_right hc hd).isBigO

Big-O Relation Preserved Under Right Multiplication by Nonzero Constant

Informal description

Let $S$ be a normed field, $f : \alpha \to E$ and $g : \alpha \to S$ be functions, and $l$ be a filter on $\alpha$. If $f$ is big O of $g$ along $l$ (i.e., $f =O[l] g$) and $c \in S$ is a nonzero element, then $f$ is also big O of the function $x \mapsto c \cdot g(x)$ along $l$ (i.e., $f =O[l] (x \mapsto c \cdot g(x))$).

Asymptotics.isBigO_const_mul_right_iff' theorem

{g : α → R} {c : R} (hc : IsUnit c) : (f =O[l] fun x => c * g x) ↔ f =O[l] g

Full source

theorem isBigO_const_mul_right_iff' {g : α → R} {c : R} (hc : IsUnit c) :
    (f =O[l] fun x => c * g x) ↔ f =O[l] g :=
  ⟨fun h => h.of_const_mul_right, fun h => h.const_mul_right' hc⟩

Equivalence of Big-O Relations Under Right Multiplication by Unit

Informal description

Let $R$ be a seminormed ring, $f \colon \alpha \to E$ and $g \colon \alpha \to R$ be functions, $l$ be a filter on $\alpha$, and $c \in R$ be a unit. Then the following equivalence holds: \[ f =O[l] (x \mapsto c \cdot g(x)) \quad \text{if and only if} \quad f =O[l] g. \]

Asymptotics.isBigO_const_mul_right_iff theorem

{g : α → S} {c : S} (hc : c ≠ 0) : (f =O[l] fun x => c * g x) ↔ f =O[l] g

Full source

theorem isBigO_const_mul_right_iff {g : α → S} {c : S} (hc : c ≠ 0) :
    (f =O[l] fun x => c * g x) ↔ f =O[l] g :=
  ⟨fun h ↦ h.of_const_mul_right, fun h ↦ h.const_mul_right hc⟩

Equivalence of Big-O Relations Under Right Multiplication by Nonzero Constant

Informal description

Let $S$ be a normed field, $f : \alpha \to E$ and $g : \alpha \to S$ be functions, and $l$ be a filter on $\alpha$. For any nonzero constant $c \in S$, the following equivalence holds: \[ f =O[l] (x \mapsto c \cdot g(x)) \quad \text{if and only if} \quad f =O[l] g. \]

Asymptotics.IsLittleO.of_const_mul_right theorem

{g : α → R} {c : R} (h : f =o[l] fun x => c * g x) : f =o[l] g

Full source

theorem IsLittleO.of_const_mul_right {g : α → R} {c : R} (h : f =o[l] fun x => c * g x) :
    f =o[l] g :=
  h.trans_isBigO (isBigO_const_mul_self c g l)

Little-o relation preserved under scalar multiplication: $f = o(c \cdot g) \Rightarrow f = o(g)$

Informal description

Let $f \colon \alpha \to E$ and $g \colon \alpha \to R$ be functions, where $E$ is a normed space and $R$ is a seminormed ring. Let $l$ be a filter on $\alpha$ and $c \in R$. If $f$ is little-o of $x \mapsto c \cdot g(x)$ along $l$, then $f$ is little-o of $g$ along $l$. In other words, if $f = o[l] (c \cdot g)$, then $f = o[l] g$.

Asymptotics.IsLittleO.const_mul_right' theorem

{g : α → R} {c : R} (hc : IsUnit c) (h : f =o[l] g) : f =o[l] fun x => c * g x

Full source

theorem IsLittleO.const_mul_right' {g : α → R} {c : R} (hc : IsUnit c) (h : f =o[l] g) :
    f =o[l] fun x => c * g x :=
  h.trans_isBigO (isBigO_self_const_mul' hc g l)

Little-o relation preserved under right multiplication by a unit

Informal description

Let $R$ be a seminormed ring, $f, g \colon \alpha \to R$ be functions, $l$ be a filter on $\alpha$, and $c \in R$ be a unit. If $f$ is little-o of $g$ along $l$ (i.e., $f = o[l] g$), then $f$ is also little-o of the function $x \mapsto c \cdot g(x)$ along $l$ (i.e., $f = o[l] (x \mapsto c \cdot g(x))$).

Asymptotics.IsLittleO.const_mul_right theorem

{g : α → S} {c : S} (hc : c ≠ 0) (h : f =o[l] g) : f =o[l] fun x => c * g x

Full source

theorem IsLittleO.const_mul_right {g : α → S} {c : S} (hc : c ≠ 0) (h : f =o[l] g) :
    f =o[l] fun x => c * g x :=
  h.trans_isBigO <| isBigO_self_const_mul hc g l

Little-o Preservation under Right Multiplication by Nonzero Constant: $f = o(g) \Rightarrow f = o(c \cdot g)$ for $c \neq 0$

Informal description

Let $f : \alpha \to E$ and $g : \alpha \to S$ be functions to normed spaces, where $S$ is a normed field. Let $l$ be a filter on $\alpha$ and $c \in S$ be a nonzero element. If $f$ is little-o of $g$ with respect to $l$ (i.e., $f = o[l] g$), then $f$ is also little-o of the function $x \mapsto c \cdot g(x)$ with respect to $l$ (i.e., $f = o[l] (x \mapsto c \cdot g(x))$).

Asymptotics.isLittleO_const_mul_right_iff' theorem

{g : α → R} {c : R} (hc : IsUnit c) : (f =o[l] fun x => c * g x) ↔ f =o[l] g

Full source

theorem isLittleO_const_mul_right_iff' {g : α → R} {c : R} (hc : IsUnit c) :
    (f =o[l] fun x => c * g x) ↔ f =o[l] g :=
  ⟨fun h => h.of_const_mul_right, fun h => h.const_mul_right' hc⟩

Equivalence of Little-o Relations Under Right Multiplication by a Unit: $f = o(c \cdot g) \Leftrightarrow f = o(g)$

Informal description

Let $R$ be a seminormed ring, $f, g \colon \alpha \to R$ be functions, $l$ be a filter on $\alpha$, and $c \in R$ be a unit. Then $f$ is little-o of the function $x \mapsto c \cdot g(x)$ along $l$ if and only if $f$ is little-o of $g$ along $l$. In other words: $$ f = o[l] (c \cdot g) \Leftrightarrow f = o[l] g $$

Asymptotics.isLittleO_const_mul_right_iff theorem

{g : α → S} {c : S} (hc : c ≠ 0) : (f =o[l] fun x => c * g x) ↔ f =o[l] g

Full source

theorem isLittleO_const_mul_right_iff {g : α → S} {c : S} (hc : c ≠ 0) :
    (f =o[l] fun x => c * g x) ↔ f =o[l] g :=
  ⟨fun h ↦ h.of_const_mul_right, fun h ↦ h.trans_isBigO (isBigO_self_const_mul hc g l)⟩

Little-o relation equivalence under scalar multiplication: $f = o(c \cdot g) \leftrightarrow f = o(g)$ for $c \neq 0$

Informal description

Let $f : \alpha \to E$ and $g : \alpha \to S$ be functions, where $E$ is a normed space and $S$ is a normed field. Let $l$ be a filter on $\alpha$ and $c \in S$ be a nonzero element. Then $f$ is little-o of $x \mapsto c \cdot g(x)$ along $l$ if and only if $f$ is little-o of $g$ along $l$. In other words, $f = o[l] (c \cdot g) \leftrightarrow f = o[l] g$.

Asymptotics.IsBigOWith.mul theorem

 {f₁ f₂ : α → R} {g₁ g₂ : α → S} {c₁ c₂ : ℝ} (h₁ : IsBigOWith c₁ l f₁ g₁) (h₂ : IsBigOWith c₂ l f₂ g₂) :
  IsBigOWith (c₁ * c₂) l (fun x => f₁ x * f₂ x) fun x => g₁ x * g₂ x

Full source

theorem IsBigOWith.mul {f₁ f₂ : α → R} {g₁ g₂ : α → S} {c₁ c₂ : ℝ} (h₁ : IsBigOWith c₁ l f₁ g₁)
    (h₂ : IsBigOWith c₂ l f₂ g₂) :
    IsBigOWith (c₁ * c₂) l (fun x => f₁ x * f₂ x) fun x => g₁ x * g₂ x := by
  simp only [IsBigOWith_def] at *
  filter_upwards [h₁, h₂] with _ hx₁ hx₂
  apply le_trans (norm_mul_le _ _)
  convert mul_le_mul hx₁ hx₂ (norm_nonneg _) (le_trans (norm_nonneg _) hx₁) using 1
  rw [norm_mul, mul_mul_mul_comm]

Product of Big-O Functions: $\text{IsBigOWith}(c_1, l, f_1, g_1) \land \text{IsBigOWith}(c_2, l, f_2, g_2) \implies \text{IsBigOWith}(c_1 c_2, l, f_1 f_2, g_1 g_2)$

Informal description

Let $f_1, f_2 : \alpha \to R$ and $g_1, g_2 : \alpha \to S$ be functions, where $R$ and $S$ are normed spaces, and let $l$ be a filter on $\alpha$. If there exist constants $c_1, c_2 \in \mathbb{R}$ such that $f_1$ is big-O of $g_1$ along $l$ with constant $c_1$ (i.e., $\|f_1(x)\| \leq c_1 \|g_1(x)\|$ eventually) and $f_2$ is big-O of $g_2$ along $l$ with constant $c_2$ (i.e., $\|f_2(x)\| \leq c_2 \|g_2(x)\|$ eventually), then the product function $x \mapsto f_1(x) f_2(x)$ is big-O of the product function $x \mapsto g_1(x) g_2(x)$ along $l$ with constant $c_1 c_2$ (i.e., $\|f_1(x) f_2(x)\| \leq c_1 c_2 \|g_1(x) g_2(x)\|$ eventually).

Asymptotics.IsBigO.mul theorem

 {f₁ f₂ : α → R} {g₁ g₂ : α → S} (h₁ : f₁ =O[l] g₁) (h₂ : f₂ =O[l] g₂) :
  (fun x => f₁ x * f₂ x) =O[l] fun x => g₁ x * g₂ x

Full source

theorem IsBigO.mul {f₁ f₂ : α → R} {g₁ g₂ : α → S} (h₁ : f₁ =O[l] g₁) (h₂ : f₂ =O[l] g₂) :
    (fun x => f₁ x * f₂ x) =O[l] fun x => g₁ x * g₂ x :=
  let ⟨_c, hc⟩ := h₁.isBigOWith
  let ⟨_c', hc'⟩ := h₂.isBigOWith
  (hc.mul hc').isBigO

Product of Big-O Functions: $(f_1 =O[l] g_1) \land (f_2 =O[l] g_2) \implies (f_1 f_2) =O[l] (g_1 g_2)$

Informal description

Let $f_1, f_2 : \alpha \to R$ and $g_1, g_2 : \alpha \to S$ be functions, where $R$ and $S$ are normed spaces, and let $l$ be a filter on $\alpha$. If $f_1$ is big-O of $g_1$ along $l$ (i.e., $f_1 =O[l] g_1$) and $f_2$ is big-O of $g_2$ along $l$ (i.e., $f_2 =O[l] g_2$), then the product function $x \mapsto f_1(x) f_2(x)$ is big-O of the product function $x \mapsto g_1(x) g_2(x)$ along $l$ (i.e., $(f_1 \cdot f_2) =O[l] (g_1 \cdot g_2)$).

Asymptotics.IsBigO.mul_isLittleO theorem

 {f₁ f₂ : α → R} {g₁ g₂ : α → S} (h₁ : f₁ =O[l] g₁) (h₂ : f₂ =o[l] g₂) :
  (fun x => f₁ x * f₂ x) =o[l] fun x => g₁ x * g₂ x

Full source

theorem IsBigO.mul_isLittleO {f₁ f₂ : α → R} {g₁ g₂ : α → S} (h₁ : f₁ =O[l] g₁) (h₂ : f₂ =o[l] g₂) :
    (fun x => f₁ x * f₂ x) =o[l] fun x => g₁ x * g₂ x := by
  simp only [IsLittleO_def] at *
  intro c cpos
  rcases h₁.exists_pos with ⟨c', c'pos, hc'⟩
  exact (hc'.mul (h₂ (div_pos cpos c'pos))).congr_const (mul_div_cancel₀ _ (ne_of_gt c'pos))

Product of Big-O and Little-o Functions: $(f_1 =O[l] g_1) \land (f_2 =o[l] g_2) \implies (f_1 f_2) =o[l] (g_1 g_2)$

Informal description

Let $f_1, f_2 : \alpha \to R$ and $g_1, g_2 : \alpha \to S$ be functions, where $R$ and $S$ are normed spaces, and let $l$ be a filter on $\alpha$. If $f_1$ is big-O of $g_1$ along $l$ (i.e., $f_1 =O[l] g_1$) and $f_2$ is little-o of $g_2$ along $l$ (i.e., $f_2 =o[l] g_2$), then the product function $x \mapsto f_1(x) f_2(x)$ is little-o of the product function $x \mapsto g_1(x) g_2(x)$ along $l$ (i.e., $(f_1 \cdot f_2) =o[l] (g_1 \cdot g_2)$).

Asymptotics.IsLittleO.mul theorem

 {f₁ f₂ : α → R} {g₁ g₂ : α → S} (h₁ : f₁ =o[l] g₁) (h₂ : f₂ =o[l] g₂) : (fun x ↦ f₁ x * f₂ x) =o[l] fun x ↦ g₁ x * g₂ x

Full source

theorem IsLittleO.mul {f₁ f₂ : α → R} {g₁ g₂ : α → S} (h₁ : f₁ =o[l] g₁) (h₂ : f₂ =o[l] g₂) :
    (fun x ↦ f₁ x * f₂ x) =o[l] fun x ↦ g₁ x * g₂ x :=
  h₁.mul_isBigO h₂.isBigO

Product of Little-o Functions: $(f_1 = o[l] g_1) \land (f_2 = o[l] g_2) \implies (f_1 f_2) = o[l] (g_1 g_2)$

Informal description

Let $f_1, f_2 : \alpha \to R$ and $g_1, g_2 : \alpha \to S$ be functions, where $R$ and $S$ are normed spaces, and let $l$ be a filter on $\alpha$. If $f_1$ is little-o of $g_1$ along $l$ (i.e., $f_1 = o[l] g_1$) and $f_2$ is little-o of $g_2$ along $l$ (i.e., $f_2 = o[l] g_2$), then the product function $x \mapsto f_1(x) f_2(x)$ is little-o of the product function $x \mapsto g_1(x) g_2(x)$ along $l$ (i.e., $(f_1 \cdot f_2) = o[l] (g_1 \cdot g_2)$).

Asymptotics.IsBigOWith.pow' theorem

 [NormOneClass S] {f : α → R} {g : α → S} (h : IsBigOWith c l f g) :
  ∀ n : ℕ, IsBigOWith (Nat.casesOn n ‖(1 : R)‖ fun n ↦ c ^ (n + 1)) l (fun x => f x ^ n) fun x => g x ^ n

Full source

theorem IsBigOWith.pow' [NormOneClass S] {f : α → R} {g : α → S} (h : IsBigOWith c l f g) :
    ∀ n : ℕ, IsBigOWith (Nat.casesOn n ‖(1 : R)‖ fun n ↦ c ^ (n + 1))
      l (fun x => f x ^ n) fun x => g x ^ n
  | 0 => by
    have : Nontrivial S := NormOneClass.nontrivial
    simpa using isBigOWith_const_const (1 : R) (one_ne_zero' S) l
  | 1 => by simpa
  | n + 2 => by simpa [pow_succ] using (IsBigOWith.pow' h (n + 1)).mul h

Big-O Preservation under Powers: $\text{IsBigOWith}(c, l, f, g) \implies \text{IsBigOWith}(c^{n+1}, l, f^n, g^n)$ for $n \geq 1$

Informal description

Let $R$ and $S$ be normed spaces with $S$ satisfying $\|1_S\| = 1$. Given functions $f : \alpha \to R$ and $g : \alpha \to S$ such that $f$ is big-O of $g$ along a filter $l$ with constant $c$ (i.e., $\|f(x)\| \leq c \|g(x)\|$ eventually holds), then for any natural number $n$, the function $x \mapsto f(x)^n$ is big-O of $x \mapsto g(x)^n$ along $l$ with constant $\|1_R\|$ when $n = 0$ and $c^{n+1}$ when $n \geq 1$.

Asymptotics.IsBigOWith.pow theorem

 [NormOneClass R] [NormOneClass S] {f : α → R} {g : α → S} (h : IsBigOWith c l f g) :
  ∀ n : ℕ, IsBigOWith (c ^ n) l (fun x => f x ^ n) fun x => g x ^ n

Full source

theorem IsBigOWith.pow [NormOneClass R] [NormOneClass S]
    {f : α → R} {g : α → S} (h : IsBigOWith c l f g) :
    ∀ n : ℕ, IsBigOWith (c ^ n) l (fun x => f x ^ n) fun x => g x ^ n
  | 0 => by simpa using h.pow' 0
  | n + 1 => h.pow' (n + 1)

Big-O bound for powers: $\|f\| \leq c \|g\| \implies \|f^n\| \leq c^n \|g^n\|$ in normed spaces with $\|1\| = 1$

Informal description

Let $R$ and $S$ be normed spaces with $\|1_R\| = 1$ and $\|1_S\| = 1$. Given functions $f : \alpha \to R$ and $g : \alpha \to S$ such that $\|f(x)\| \leq c \|g(x)\|$ holds for all $x$ in some neighborhood determined by the filter $l$ (i.e., $\text{IsBigOWith}(c, l, f, g)$ holds), then for any natural number $n$, the function $x \mapsto f(x)^n$ satisfies $\|f(x)^n\| \leq c^n \|g(x)^n\|$ in the same neighborhood (i.e., $\text{IsBigOWith}(c^n, l, f^n, g^n)$ holds).

Asymptotics.IsBigOWith.of_pow theorem

 [NormOneClass S] {n : ℕ} {f : α → S} {g : α → R} (h : IsBigOWith c l (f ^ n) (g ^ n)) (hn : n ≠ 0) (hc : c ≤ c' ^ n)
  (hc' : 0 ≤ c') : IsBigOWith c' l f g

Full source

theorem IsBigOWith.of_pow [NormOneClass S] {n : ℕ} {f : α → S} {g : α → R}
    (h : IsBigOWith c l (f ^ n) (g ^ n)) (hn : n ≠ 0) (hc : c ≤ c' ^ n) (hc' : 0 ≤ c') :
    IsBigOWith c' l f g :=
  IsBigOWith.of_bound <| (h.weaken hc).bound.mono fun x hx ↦
    le_of_pow_le_pow_left₀ hn (by positivity) <|
      calc
        ‖f x‖ ^ n = ‖f x ^ n‖ := (norm_pow _ _).symm
        _ ≤ c' ^ n * ‖g x ^ n‖ := hx
        _ ≤ c' ^ n * ‖g x‖ ^ n := by gcongr; exact norm_pow_le' _ hn.bot_lt
        _ = (c' * ‖g x‖) ^ n := (mul_pow _ _ _).symm

Big-O Bound for Functions via Their Powers: $\|f^n\| \leq c \|g^n\| \implies \|f\| \leq c' \|g\|$ when $c \leq c'^n$ and $n \neq 0$

Informal description

Let $S$ be a normed space with $\|1\| = 1$, and let $n$ be a nonzero natural number. Suppose $f: \alpha \to S$ and $g: \alpha \to \mathbb{R}$ are functions such that $\|f^n(x)\| \leq c \|g^n(x)\|$ holds for all $x$ in some neighborhood determined by the filter $l$ (i.e., $\text{IsBigOWith}(c, l, f^n, g^n)$ holds). If $c \leq c'^n$ and $c' \geq 0$, then $\|f(x)\| \leq c' \|g(x)\|$ holds for all $x$ in the same neighborhood (i.e., $\text{IsBigOWith}(c', l, f, g)$ holds).

Asymptotics.IsBigO.pow theorem

[NormOneClass S] {f : α → R} {g : α → S} (h : f =O[l] g) (n : ℕ) : (fun x => f x ^ n) =O[l] fun x => g x ^ n

Full source

theorem IsBigO.pow [NormOneClass S] {f : α → R} {g : α → S} (h : f =O[l] g) (n : ℕ) :
    (fun x => f x ^ n) =O[l] fun x => g x ^ n :=
  let ⟨_C, hC⟩ := h.isBigOWith
  isBigO_iff_isBigOWith.2 ⟨_, hC.pow' n⟩

Preservation of Big-O Relation under Powers: $f =O[l] g \implies f^n =O[l] g^n$

Informal description

Let $R$ and $S$ be normed spaces with $\|1_S\| = 1$. Given functions $f : \alpha \to R$ and $g : \alpha \to S$ such that $f$ is big-O of $g$ along a filter $l$ (i.e., $f =O[l] g$), then for any natural number $n$, the function $x \mapsto f(x)^n$ is big-O of $x \mapsto g(x)^n$ along $l$.

Asymptotics.IsLittleO.pow theorem

{f : α → R} {g : α → S} (h : f =o[l] g) {n : ℕ} (hn : 0 < n) : (fun x => f x ^ n) =o[l] fun x => g x ^ n

Full source

theorem IsLittleO.pow {f : α → R} {g : α → S} (h : f =o[l] g) {n : ℕ} (hn : 0 < n) :
    (fun x => f x ^ n) =o[l] fun x => g x ^ n := by
  obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn.ne'; clear hn
  induction n with
  | zero => simpa only [pow_one]
  | succ n ihn => convert ihn.mul h <;> simp [pow_succ]

Little-o relation preserved under powers: $f = o[l] g \implies f^n = o[l] g^n$ for $n > 0$

Informal description

Let $R$ and $S$ be normed spaces, and let $f : \alpha \to R$ and $g : \alpha \to S$ be functions. If $f$ is little-o of $g$ along a filter $l$ (i.e., $f = o[l] g$) and $n$ is a positive natural number, then the $n$-th power of $f$ is little-o of the $n$-th power of $g$ along $l$ (i.e., $f^n = o[l] g^n$).

Asymptotics.IsLittleO.of_pow theorem

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

Full source

theorem IsLittleO.of_pow [NormOneClass S] {f : α → S} {g : α → R} {n : ℕ}
    (h : (f ^ n) =o[l] (g ^ n)) (hn : n ≠ 0) : f =o[l] g :=
  IsLittleO.of_isBigOWith fun _c hc => (h.def' <| pow_pos hc _).of_pow hn le_rfl hc.le

Little-o relation preserved under taking roots: $f^n = o(g^n) \implies f = o(g)$ for $n \neq 0$

Informal description

Let $S$ be a normed space with $\|1_S\| = 1$, and let $R$ be another normed space. For functions $f: \alpha \to S$ and $g: \alpha \to R$, if the $n$-th power of $f$ is little-o of the $n$-th power of $g$ along a filter $l$ (i.e., $f^n = o[l] g^n$) for some nonzero natural number $n$, then $f$ is little-o of $g$ along $l$ (i.e., $f = o[l] g$).

Asymptotics.IsBigOWith.inv_rev theorem

 {f : α → 𝕜} {g : α → 𝕜'} (h : IsBigOWith c l f g) (h₀ : ∀ᶠ x in l, f x = 0 → g x = 0) :
  IsBigOWith c l (fun x => (g x)⁻¹) fun x => (f x)⁻¹

Full source

theorem IsBigOWith.inv_rev {f : α → 𝕜} {g : α → 𝕜'} (h : IsBigOWith c l f g)
    (h₀ : ∀ᶠ x in l, f x = 0 → g x = 0) : IsBigOWith c l (fun x => (g x)⁻¹) fun x => (f x)⁻¹ := by
  refine IsBigOWith.of_bound (h.bound.mp (h₀.mono fun x h₀ hle => ?_))
  rcases eq_or_ne (f x) 0 with hx | hx
  · simp only [hx, h₀ hx, inv_zero, norm_zero, mul_zero, le_rfl]
  · have hc : 0 < c := pos_of_mul_pos_left ((norm_pos_iff.2 hx).trans_le hle) (norm_nonneg _)
    replace hle := inv_anti₀ (norm_pos_iff.2 hx) hle
    simpa only [norm_inv, mul_inv, ← div_eq_inv_mul, div_le_iff₀ hc] using hle

Reciprocal Reversal of Big-O Bound: $\|g^{-1}\| \leq c\|f^{-1}\|$ under $\|f\| \leq c\|g\|$ and non-vanishing condition

Informal description

Let $f: \alpha \to \mathbb{K}$ and $g: \alpha \to \mathbb{K}'$ be functions where $\mathbb{K}$ and $\mathbb{K}'$ are normed division rings, and let $l$ be a filter on $\alpha$. If $f$ is bounded by $g$ with constant $c$ along $l$ (i.e., $\|f(x)\| \leq c\|g(x)\|$ eventually in $l$) and $g(x) = 0$ whenever $f(x) = 0$ eventually in $l$, then the reciprocals satisfy $\|g(x)^{-1}\| \leq c\|f(x)^{-1}\|$ eventually in $l$.

Asymptotics.IsBigO.inv_rev theorem

 {f : α → 𝕜} {g : α → 𝕜'} (h : f =O[l] g) (h₀ : ∀ᶠ x in l, f x = 0 → g x = 0) :
  (fun x => (g x)⁻¹) =O[l] fun x => (f x)⁻¹

Full source

theorem IsBigO.inv_rev {f : α → 𝕜} {g : α → 𝕜'} (h : f =O[l] g)
    (h₀ : ∀ᶠ x in l, f x = 0 → g x = 0) : (fun x => (g x)⁻¹) =O[l] fun x => (f x)⁻¹ :=
  let ⟨_c, hc⟩ := h.isBigOWith
  (hc.inv_rev h₀).isBigO

Reciprocal Reversal of Big-O Relation: $g^{-1} =O[l] f^{-1}$ under $f =O[l] g$ and non-vanishing condition

Informal description

Let $f : \alpha \to \mathbb{K}$ and $g : \alpha \to \mathbb{K}'$ be functions where $\mathbb{K}$ and $\mathbb{K}'$ are normed division rings, and let $l$ be a filter on $\alpha$. If $f$ is big O of $g$ along $l$ (i.e., $f =O[l] g$) and $g(x) = 0$ whenever $f(x) = 0$ eventually in $l$, then the reciprocal function $x \mapsto (g(x))^{-1}$ is big O of the reciprocal function $x \mapsto (f(x))^{-1}$ along $l$.

Asymptotics.IsLittleO.inv_rev theorem

 {f : α → 𝕜} {g : α → 𝕜'} (h : f =o[l] g) (h₀ : ∀ᶠ x in l, f x = 0 → g x = 0) :
  (fun x => (g x)⁻¹) =o[l] fun x => (f x)⁻¹

Full source

theorem IsLittleO.inv_rev {f : α → 𝕜} {g : α → 𝕜'} (h : f =o[l] g)
    (h₀ : ∀ᶠ x in l, f x = 0 → g x = 0) : (fun x => (g x)⁻¹) =o[l] fun x => (f x)⁻¹ :=
  IsLittleO.of_isBigOWith fun _c hc => (h.def' hc).inv_rev h₀

Reciprocal Reversal of Little-o Relation: $(g^{-1}) = o[l] (f^{-1})$ under $f = o[l] g$ and non-vanishing condition

Informal description

Let $f: \alpha \to \mathbb{K}$ and $g: \alpha \to \mathbb{K}'$ be functions where $\mathbb{K}$ and $\mathbb{K}'$ are normed division rings, and let $l$ be a filter on $\alpha$. If $f = o[l] g$ (i.e., $f$ is little-o of $g$ along $l$) and $g(x) = 0$ whenever $f(x) = 0$ eventually in $l$, then the reciprocals satisfy $(g^{-1}) = o[l] (f^{-1})$.

Asymptotics.IsBigOWith.sum theorem

(h : ∀ i ∈ s, IsBigOWith (C i) l (A i) g) : IsBigOWith (∑ i ∈ s, C i) l (fun x => ∑ i ∈ s, A i x) g

Full source

theorem IsBigOWith.sum (h : ∀ i ∈ s, IsBigOWith (C i) l (A i) g) :
    IsBigOWith (∑ i ∈ s, C i) l (fun x => ∑ i ∈ s, A i x) g := by
  induction s using Finset.cons_induction with
  | empty => simp only [isBigOWith_zero', Finset.sum_empty, forall_true_iff]
  | cons i s is IH =>
    simp only [is, Finset.sum_cons, Finset.forall_mem_cons] at h ⊢
    exact h.1.add (IH h.2)

Sum of Big-O Bounds with Constants $C_i$ is Big-O with Constant $\sum C_i$

Informal description

Let $s$ be a finite set, and for each $i \in s$, let $A_i : \alpha \to E$ and $g : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. Suppose that for each $i \in s$, there exists a constant $C_i \in \mathbb{R}$ such that $\|A_i(x)\| \leq C_i \|g(x)\|$ for all $x$ in $l$ eventually. Then the sum $\sum_{i \in s} A_i$ satisfies $\left\|\sum_{i \in s} A_i(x)\right\| \leq \left(\sum_{i \in s} C_i\right) \|g(x)\|$ for all $x$ in $l$ eventually.

Asymptotics.IsBigO.sum theorem

(h : ∀ i ∈ s, A i =O[l] g) : (fun x => ∑ i ∈ s, A i x) =O[l] g

Full source

theorem IsBigO.sum (h : ∀ i ∈ s, A i =O[l] g) : (fun x => ∑ i ∈ s, A i x) =O[l] g := by
  simp only [IsBigO_def] at *
  choose! C hC using h
  exact ⟨_, IsBigOWith.sum hC⟩

Sum of Big-O Functions is Big-O

Informal description

Let $s$ be a finite set, and for each $i \in s$, let $A_i : \alpha \to E$ and $g : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If for each $i \in s$, the function $A_i$ is big O of $g$ along $l$, then the sum $\sum_{i \in s} A_i$ is also big O of $g$ along $l$.

Asymptotics.IsLittleO.sum theorem

(h : ∀ i ∈ s, A i =o[l] g') : (fun x => ∑ i ∈ s, A i x) =o[l] g'

Full source

theorem IsLittleO.sum (h : ∀ i ∈ s, A i =o[l] g') : (fun x => ∑ i ∈ s, A i x) =o[l] g' := by
  simp only [← Finset.sum_apply]
  exact Finset.sum_induction A (· =o[l] g') (fun _ _ ↦ .add) (isLittleO_zero ..) h

Sum of Little-o Functions is Little-o

Informal description

Let $s$ be a finite set, and for each $i \in s$, let $A_i : \alpha \to E$ and $g' : \alpha \to F$ be functions between normed spaces, and let $l$ be a filter on $\alpha$. If for each $i \in s$, the function $A_i$ is little-o of $g'$ along $l$, then the sum $\sum_{i \in s} A_i$ is also little-o of $g'$ along $l$.

Asymptotics.IsBigOWith.eventually_mul_div_cancel theorem

(h : IsBigOWith c l u v) : u / v * v =ᶠ[l] u

Full source

theorem IsBigOWith.eventually_mul_div_cancel (h : IsBigOWith c l u v) : u / v * v =ᶠ[l] u :=
  Eventually.mono h.bound fun y hy => div_mul_cancel_of_imp fun hv => by simpa [hv] using hy

Eventual Cancellation Property for Big-O Bounded Functions

Informal description

Let $u$ and $v$ be functions from a type $\alpha$ to a normed division ring, and let $l$ be a filter on $\alpha$. If there exists a constant $C$ such that $\text{IsBigOWith}(C, l, u, v)$ holds (i.e., $\|u(x)\| \leq C\|v(x)\|$ for all $x$ in $l$ eventually), then the equality $(u/v) \cdot v = u$ holds eventually along $l$.

Asymptotics.IsBigO.eventually_mul_div_cancel theorem

(h : u =O[l] v) : u / v * v =ᶠ[l] u

Full source

/-- If `u = O(v)` along `l`, then `(u / v) * v = u` eventually at `l`. -/
theorem IsBigO.eventually_mul_div_cancel (h : u =O[l] v) : u / v * v =ᶠ[l] u :=
  let ⟨_c, hc⟩ := h.isBigOWith
  hc.eventually_mul_div_cancel

Eventual Cancellation Property for Big-O Bounded Functions

Informal description

Let $u$ and $v$ be functions from a type $\alpha$ to a normed division ring, and let $l$ be a filter on $\alpha$. If $u =O[l] v$ (i.e., $u$ is big O of $v$ along $l$), then the equality $(u/v) \cdot v = u$ holds eventually along $l$.

Asymptotics.IsLittleO.eventually_mul_div_cancel theorem

(h : u =o[l] v) : u / v * v =ᶠ[l] u

Full source

/-- If `u = o(v)` along `l`, then `(u / v) * v = u` eventually at `l`. -/
theorem IsLittleO.eventually_mul_div_cancel (h : u =o[l] v) : u / v * v =ᶠ[l] u :=
  (h.forall_isBigOWith zero_lt_one).eventually_mul_div_cancel

Eventual Cancellation Property for Little-o Bounded Functions

Informal description

Let $u$ and $v$ be functions from a type $\alpha$ to a normed division ring, and let $l$ be a filter on $\alpha$. If $u = o[l] v$ (i.e., $u$ is little-o of $v$ along $l$), then the equality $(u/v) \cdot v = u$ holds eventually along $l$.