Mathlib.Analysis.NormedSpace.OperatorNorm.Asymptotics

ContinuousLinearMap.isBigOWith_id theorem

: IsBigOWith ‖f‖ l f fun x => x

Full source

theorem isBigOWith_id : IsBigOWith ‖f‖ l f fun x => x :=
  isBigOWith_of_le' _ f.le_opNorm

Operator Norm Asymptotic Bound: $f(x) = O(\|f\| \cdot \|x\|)$

Informal description

For any continuous semilinear map $f \colon E \to F$ between seminormed additive commutative groups and any filter $l$ on $E$, the function $f$ is asymptotically bounded by the identity function with constant $\|f\|$, i.e., $f(x) = O(\|f\| \cdot \|x\|)$ as $x \to l$.

ContinuousLinearMap.isBigO_id theorem

: f =O[l] fun x => x

Full source

theorem isBigO_id : f =O[l] fun x => x :=
  (f.isBigOWith_id l).isBigO

Asymptotic Bound of Continuous Linear Map: $f(x) = O(\|x\|)$

Informal description

For any continuous semilinear map $f \colon E \to F$ between seminormed additive commutative groups and any filter $l$ on $E$, the function $f$ is asymptotically bounded by the identity function, i.e., $f(x) = O(\|x\|)$ as $x \to l$.

ContinuousLinearMap.isBigOWith_comp theorem

 [RingHomIsometric σ₂₃] {α : Type*} (g : F →SL[σ₂₃] G) (f : α → F) (l : Filter α) :
  IsBigOWith ‖g‖ l (fun x' => g (f x')) f

Full source

theorem isBigOWith_comp [RingHomIsometric σ₂₃] {α : Type*} (g : F →SL[σ₂₃] G) (f : α → F)
    (l : Filter α) : IsBigOWith ‖g‖ l (fun x' => g (f x')) f :=
  (g.isBigOWith_id ⊤).comp_tendsto le_top

Asymptotic Bound for Composition of Continuous Semilinear Maps: $g \circ f(x) = O(\|g\| \cdot \|f(x)\|)$

Informal description

Let $E$, $F$, and $G$ be seminormed additive commutative groups, and let $\sigma_{23}$ be a ring homomorphism from $F$ to $G$ that is isometric. Given a continuous semilinear map $g \colon F \to_{\sigma_{23}} G$ and a function $f \colon \alpha \to F$ defined on some type $\alpha$, for any filter $l$ on $\alpha$, the composition $g \circ f$ satisfies the asymptotic bound $\|g \circ f(x)\| \leq \|g\| \cdot \|f(x)\|$ for all $x$ in a neighborhood of $l$. In other words, $g \circ f(x) = O(\|g\| \cdot \|f(x)\|)$ as $x \to l$.

ContinuousLinearMap.isBigO_comp theorem

 [RingHomIsometric σ₂₃] {α : Type*} (g : F →SL[σ₂₃] G) (f : α → F) (l : Filter α) : (fun x' => g (f x')) =O[l] f

Full source

theorem isBigO_comp [RingHomIsometric σ₂₃] {α : Type*} (g : F →SL[σ₂₃] G) (f : α → F)
    (l : Filter α) : (fun x' => g (f x')) =O[l] f :=
  (g.isBigOWith_comp f l).isBigO

Asymptotic Bound for Composition of Continuous Semilinear Maps: $g \circ f = O(f)$

Informal description

Let $E$, $F$, and $G$ be seminormed additive commutative groups, and let $\sigma_{23}$ be a ring homomorphism from $F$ to $G$ that is isometric. Given a continuous semilinear map $g \colon F \to_{\sigma_{23}} G$ and a function $f \colon \alpha \to F$ defined on some type $\alpha$, for any filter $l$ on $\alpha$, the composition $g \circ f$ is asymptotically bounded by $f$, i.e., $g(f(x)) = O(f(x))$ as $x \to l$.

ContinuousLinearMap.isBigOWith_sub theorem

(x : E) : IsBigOWith ‖f‖ l (fun x' => f (x' - x)) fun x' => x' - x

Full source

theorem isBigOWith_sub (x : E) :
    IsBigOWith ‖f‖ l (fun x' => f (x' - x)) fun x' => x' - x :=
  f.isBigOWith_comp _ l

Asymptotic Bound for Continuous Linear Map at Shifted Point: $f(x' - x) = O(\|f\| \cdot \|x' - x\|)$

Informal description

Let $E$ and $F$ be seminormed additive commutative groups, and let $f \colon E \to F$ be a continuous linear map. For any point $x \in E$ and any filter $l$ on $E$, the function $f(x' - x)$ satisfies the asymptotic bound $\|f(x' - x)\| \leq \|f\| \cdot \|x' - x\|$ for all $x'$ in a neighborhood of $l$. In other words, $f(x' - x) = O(\|f\| \cdot \|x' - x\|)$ as $x' \to l$.

ContinuousLinearMap.isBigO_sub theorem

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

Full source

theorem isBigO_sub (x : E) :
    (fun x' => f (x' - x)) =O[l] fun x' => x' - x :=
  f.isBigO_comp _ l

Asymptotic Bound for Continuous Linear Map at Shifted Point: $f(x' - x) = O(x' - x)$

Informal description

Let $E$ and $F$ be seminormed additive commutative groups, and let $f \colon E \to F$ be a continuous linear map. For any point $x \in E$ and any filter $l$ on $E$, the function $f(x' - x)$ is asymptotically bounded by $x' - x$, i.e., $f(x' - x) = O(x' - x)$ as $x' \to l$.

ContinuousLinearEquiv.isBigO_comp theorem

{α : Type*} (f : α → E) (l : Filter α) : (fun x' => e (f x')) =O[l] f

Full source

theorem isBigO_comp {α : Type*} (f : α → E) (l : Filter α) : (fun x' => e (f x')) =O[l] f :=
  (e : E →SL[σ₁₂] F).isBigO_comp f l

Asymptotic Bound for Composition with Continuous Linear Equivalence: $e \circ f = O(f)$

Informal description

Let $E$ and $F$ be seminormed additive commutative groups, and let $e \colon E \to F$ be a continuous linear equivalence. For any function $f \colon \alpha \to E$ defined on some type $\alpha$ and any filter $l$ on $\alpha$, the composition $e \circ f$ is asymptotically bounded by $f$, i.e., $e(f(x)) = O(f(x))$ as $x \to l$.

ContinuousLinearEquiv.isBigO_sub theorem

(l : Filter E) (x : E) : (fun x' => e (x' - x)) =O[l] fun x' => x' - x

Full source

theorem isBigO_sub (l : Filter E) (x : E) : (fun x' => e (x' - x)) =O[l] fun x' => x' - x :=
  (e : E →SL[σ₁₂] F).isBigO_sub l x

Asymptotic Bound for Continuous Linear Equivalence at Shifted Point: $e(x' - x) = O(x' - x)$

Informal description

Let $E$ and $F$ be seminormed additive commutative groups, and let $e \colon E \to F$ be a continuous linear equivalence. For any point $x \in E$ and any filter $l$ on $E$, the function $e(x' - x)$ is asymptotically bounded by $x' - x$, i.e., $e(x' - x) = O(x' - x)$ as $x' \to l$.

ContinuousLinearEquiv.isBigO_comp_rev theorem

{α : Type*} (f : α → E) (l : Filter α) : f =O[l] fun x' => e (f x')

Full source

theorem isBigO_comp_rev {α : Type*} (f : α → E) (l : Filter α) : f =O[l] fun x' => e (f x') :=
  (e.symm.isBigO_comp _ l).congr_left fun _ => e.symm_apply_apply _

Reverse Asymptotic Bound for Composition with Continuous Linear Equivalence: $f = O(e \circ f)$

Informal description

Let $E$ and $F$ be seminormed additive commutative groups, and let $e \colon E \to F$ be a continuous linear equivalence. For any function $f \colon \alpha \to E$ defined on some type $\alpha$ and any filter $l$ on $\alpha$, the function $f$ is asymptotically bounded by the composition $e \circ f$, i.e., $f(x) = O(e(f(x)))$ as $x \to l$.

ContinuousLinearEquiv.isBigO_sub_rev theorem

(l : Filter E) (x : E) : (fun x' => x' - x) =O[l] fun x' => e (x' - x)

Full source

theorem isBigO_sub_rev (l : Filter E) (x : E) : (fun x' => x' - x) =O[l] fun x' => e (x' - x) :=
  e.isBigO_comp_rev _ _

Reverse Asymptotic Bound for Shifted Difference under Continuous Linear Equivalence: $x' - x = O(e(x' - x))$

Informal description

Let $E$ and $F$ be seminormed additive commutative groups, and let $e \colon E \to F$ be a continuous linear equivalence. For any point $x \in E$ and any filter $l$ on $E$, the function $x' - x$ is asymptotically bounded by $e(x' - x)$, i.e., $x' - x = O(e(x' - x))$ as $x' \to l$.