Asymptotic statements about the operator norm #
This file contains lemmas about how operator norm on continuous linear maps interacts with IsBigO.
theorem
ContinuousLinearMap.isBigOWith_id
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_5}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[RingHomIsometric σ₁₂]
(f : E →SL[σ₁₂] F)
(l : Filter E)
:
Asymptotics.IsBigOWith ‖f‖ l ⇑f fun (x : E) => x
theorem
ContinuousLinearMap.isBigO_id
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_5}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[RingHomIsometric σ₁₂]
(f : E →SL[σ₁₂] F)
(l : Filter E)
:
theorem
ContinuousLinearMap.isBigOWith_comp
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{F : Type u_5}
{G : Type u_6}
[SeminormedAddCommGroup F]
[SeminormedAddCommGroup G]
[NontriviallyNormedField 𝕜₂]
[NontriviallyNormedField 𝕜₃]
[NormedSpace 𝕜₂ F]
[NormedSpace 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
[RingHomIsometric σ₂₃]
{α : Type u_7}
(g : F →SL[σ₂₃] G)
(f : α → F)
(l : Filter α)
:
Asymptotics.IsBigOWith ‖g‖ l (fun (x' : α) => g (f x')) f
theorem
ContinuousLinearMap.isBigO_comp
{𝕜₂ : Type u_2}
{𝕜₃ : Type u_3}
{F : Type u_5}
{G : Type u_6}
[SeminormedAddCommGroup F]
[SeminormedAddCommGroup G]
[NontriviallyNormedField 𝕜₂]
[NontriviallyNormedField 𝕜₃]
[NormedSpace 𝕜₂ F]
[NormedSpace 𝕜₃ G]
{σ₂₃ : 𝕜₂ →+* 𝕜₃}
[RingHomIsometric σ₂₃]
{α : Type u_7}
(g : F →SL[σ₂₃] G)
(f : α → F)
(l : Filter α)
:
theorem
ContinuousLinearMap.isBigOWith_sub
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_5}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[RingHomIsometric σ₁₂]
(f : E →SL[σ₁₂] F)
(l : Filter E)
(x : E)
:
Asymptotics.IsBigOWith ‖f‖ l (fun (x' : E) => f (x' - x)) fun (x' : E) => x' - x
theorem
ContinuousLinearMap.isBigO_sub
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_5}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
[RingHomIsometric σ₁₂]
(f : E →SL[σ₁₂] F)
(l : Filter E)
(x : E)
:
theorem
ContinuousLinearEquiv.isBigO_comp
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_5}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{σ₂₁ : 𝕜₂ →+* 𝕜}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
(e : E ≃SL[σ₁₂] F)
[RingHomIsometric σ₁₂]
{α : Type u_7}
(f : α → E)
(l : Filter α)
:
theorem
ContinuousLinearEquiv.isBigO_sub
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_5}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{σ₂₁ : 𝕜₂ →+* 𝕜}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
(e : E ≃SL[σ₁₂] F)
[RingHomIsometric σ₁₂]
(l : Filter E)
(x : E)
:
theorem
ContinuousLinearEquiv.isBigO_comp_rev
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_5}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{σ₂₁ : 𝕜₂ →+* 𝕜}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
(e : E ≃SL[σ₁₂] F)
[RingHomIsometric σ₂₁]
{α : Type u_7}
(f : α → E)
(l : Filter α)
:
theorem
ContinuousLinearEquiv.isBigO_sub_rev
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_4}
{F : Type u_5}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
{σ₁₂ : 𝕜 →+* 𝕜₂}
{σ₂₁ : 𝕜₂ →+* 𝕜}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
(e : E ≃SL[σ₁₂] F)
[RingHomIsometric σ₂₁]
(l : Filter E)
(x : E)
: