English
If coefficients scale by a scalar, the radius scales accordingly: radius(p) ≤ radius(q) when ‖p n‖ ≤ ‖q n‖ for all n.
Русский
Если коэффициенты ограничиваются не больше, чем коэффициенты другой последовательности, радиус меньшего не больше радиуса большего.
LaTeX
$$$\\forall n,\\|p_n\\| \\le \\|q_n\\| \\Rightarrow radius(q) \\le radius(p).$$$
Lean4
theorem div_le_radius_compContinuousLinearMap (p : FormalMultilinearSeries 𝕜 F G) (u : E →L[𝕜] F) :
p.radius / ‖u‖ₑ ≤ (p.compContinuousLinearMap u).radius :=
by
obtain (rfl | h_zero) := eq_zero_or_nnnorm_pos u
· simp
rw [ENNReal.div_le_iff (by simpa using h_zero) (by simp)]
refine le_of_forall_nnreal_lt fun r hr ↦ ?_
rw [← ENNReal.div_le_iff (by simpa using h_zero) (by simp), enorm_eq_nnnorm, ← coe_div h_zero.ne']
obtain ⟨C, hC_pos, hC⟩ := p.norm_mul_pow_le_of_lt_radius hr
refine le_radius_of_bound _ C fun n ↦ ?_
calc
‖p.compContinuousLinearMap u n‖ * ↑(r / ‖u‖₊) ^ n ≤ ‖p n‖ * ‖u‖ ^ n * ↑(r / ‖u‖₊) ^ n :=
by
gcongr
exact nnnorm_compContinuousLinearMap_le p u n
_ = ‖p n‖ * r ^ n := by
simp only [NNReal.coe_div, coe_nnnorm, div_pow, mul_assoc]
rw [mul_div_cancel₀]
rw [← NNReal.coe_pos] at h_zero
positivity
_ ≤ C := hC n
