Auxiliary theorems about ContinuousLinearMap

Mostly about ContinuousLinearMap.IsInvertible and ContinuousLinearMap.inverse.

theorem ContinuousLinearMap.IsInvertible.eventually {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {α : Type u_4} {l : Filter α} [CompleteSpace E] {f₀ : E →L[𝕜] F} {f : α → E →L[𝕜] F} (hf₀ : f₀.IsInvertible) (hf : Filter.Tendsto f l (nhds f₀)) : ∀ᶠ (x : α) in l, (f x).IsInvertible

If a family of continuous linear maps converges to an invertible continuous linear map, then the maps are eventually invertible as well.

theorem ContinuousLinearMap.isBigO_inverse_sub_inverse {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {α : Type u_4} {l : Filter α} {f g : α → E →L[𝕜] F} (hf_inv : ∀ᶠ (a : α) in l, (f a).IsInvertible) (hf_bdd : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l fun (a : α) => ‖(f a).inverse‖) (hg_inv : ∀ᶠ (a : α) in l, (g a).IsInvertible) (hg_bdd : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l fun (a : α) => ‖(g a).inverse‖) : (fun (a : α) => (f a).inverse - (g a).inverse) =O[l] fun (a : α) => f a - g a

Consider two families of continuous linear maps, f a and g a.

Suppose that both of them are eventually invertible along a filter l, and the norms of their inverses are bounded. Then $$f^{-1}_a - g^{-1}_a = O(f_a - g_a)$$.

theorem ContinuousLinearMap.apply_sub_apply_isBigO {α : Type u_5} {𝕜 : Type u_6} {𝕝 : Type u_7} {E : Type u_8} {F : Type u_9} {G : Type u_10} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕝] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕝 F] [NormedAddCommGroup G] {σ : 𝕜 →+* 𝕝} [RingHomIsometric σ] {f₁ f₂ : α → E →SL[σ] F} {g₁ g₂ : α → E} {B : α → G} {l : Filter α} (hf_bdd : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l fun (x : α) => ‖f₁ x‖) (hf_sub : (fun (a : α) => f₁ a - f₂ a) =O[l] B) (hg_bdd : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l fun (x : α) => ‖g₂ x‖) (hg_sub : (fun (a : α) => g₁ a - g₂ a) =O[l] B) : (fun (a : α) => (f₁ a) (g₁ a) - (f₂ a) (g₂ a)) =O[l] B