radius_compContinuousLinearMap_le

English

If the coefficients were constant, the radius would be infinite.

Русский

Если коэффициенты постоянны, радиус бесконечен.

LaTeX

$$$p.radius = \\infty$ if $p_n$ are constant in n.$$

Lean4

theorem radius_compContinuousLinearMap_le [Nontrivial F] (p : FormalMultilinearSeries 𝕜 F G) (u : E ≃L[𝕜] F) :
    (p.compContinuousLinearMap u.toContinuousLinearMap).radius ≤ ‖u.symm.toContinuousLinearMap‖ₑ * p.radius :=
  by
  have :=
    (p.compContinuousLinearMap u.toContinuousLinearMap).div_le_radius_compContinuousLinearMap
      u.symm.toContinuousLinearMap
  simp only [compContinuousLinearMap_comp, ContinuousLinearEquiv.coe_comp_coe_symm, compContinuousLinearMap_id] at this
  rwa [ENNReal.div_le_iff' (by simpa [DFunLike.ext_iff] using exists_ne 0) (by simp)] at this

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