radius_leftInv_pos_of_radius_pos — Mathlib

English

If ‖p_n‖ ≤ ‖q_n‖ for all n, then radius(q) ≤ radius(p).

Русский

Если ∥p_n∥ ≤ ∥q_n∥ для всех n, тогда radius(q) ≤ radius(p).

LaTeX

$$$\\forall n, \\|p_n\\| ≤ \\|q_n\\| \\Rightarrow q.radius ≤ p.radius.$$$

Lean4

/-- If a a formal multilinear series has a positive radius of convergence, then its left inverse
also has a positive radius of convergence. -/
theorem radius_leftInv_pos_of_radius_pos {p : FormalMultilinearSeries 𝕜 E F} {i : E ≃L[𝕜] F} {x : E} (hp : 0 < p.radius)
    (h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm i) : 0 < (p.leftInv i x).radius :=
  by
  rw [leftInv_eq_rightInv _ _ _ h]
  exact radius_rightInv_pos_of_radius_pos hp

Похожие утверждения