English
In a Banach algebra A over a nontrivially normed field 𝕜, for any a ∈ A the function z ↦ inverse(1 − z a) has a convergent power-series representation in a disk of radius ‖a‖₊⁻¹, with coefficients given by appropriate multilinear maps; in particular, (1 − z a)⁻¹ = ∑_{n=0}^∞ z^n a^n for |z| < ‖a‖₊⁻¹.
Русский
В банаховой алгебре A над не нулевым полем 𝕜 функция z ↦ (1 − z a)⁻¹ имеет совпадающее представление в виде степенного ряда в окружности радиуса ‖a‖₊⁻¹; в частности, (1 − z a)⁻¹ = ∑_{n=0}^∞ z^n a^n при |z| < ‖a‖₊⁻¹.
LaTeX
$$$\\text{HasFPowerSeriesOnBall}\\left( z \\mapsto (1 - z \\cdot a)^{-1},\\; n \\mapsto \\text{ContinuousMultilinearMap.mkPiRing } 𝕜 (\\text{Fin } n) (a^n)\\right) \\\\ \\text{with radius } ‖a‖_{+}^{-1}$$$
Lean4
/-- In a Banach algebra `A` over a nontrivially normed field `𝕜`, for any `a : A` the
power series with coefficients `a ^ n` represents the function `(1 - z • a)⁻¹` in a disk of
radius `‖a‖₊⁻¹`. -/
theorem hasFPowerSeriesOnBall_inverse_one_sub_smul [HasSummableGeomSeries A] (a : A) :
HasFPowerSeriesOnBall (fun z : 𝕜 => Ring.inverse (1 - z • a))
(fun n => ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (a ^ n)) 0 ‖a‖₊⁻¹ :=
{ r_le :=
by
refine le_of_forall_nnreal_lt fun r hr => le_radius_of_bound_nnreal _ (max 1 ‖(1 : A)‖₊) fun n => ?_
rw [← norm_toNNReal, norm_mkPiRing, norm_toNNReal]
rcases n with - | n
· simp only [le_refl, mul_one, or_true, le_max_iff, pow_zero]
· refine le_trans (le_trans (mul_le_mul_right' (nnnorm_pow_le' a n.succ_pos) (r ^ n.succ)) ?_) (le_max_left _ _)
by_cases h : ‖a‖₊ = 0
· simp only [h, zero_mul, zero_le', pow_succ']
· rw [← coe_inv h, coe_lt_coe, NNReal.lt_inv_iff_mul_lt h] at hr
simpa only [← mul_pow, mul_comm] using pow_le_one' hr.le n.succ
r_pos := ENNReal.inv_pos.mpr coe_ne_top
hasSum := fun {y} hy =>
by
have norm_lt : ‖y • a‖ < 1 := by
by_cases h : ‖a‖₊ = 0
· simp only [nnnorm_eq_zero.mp h, norm_zero, zero_lt_one, smul_zero]
· have nnnorm_lt : ‖y‖₊ < ‖a‖₊⁻¹ := by
simpa only [← coe_inv h, mem_ball_zero_iff, Metric.emetric_ball_nnreal] using hy
rwa [← coe_nnnorm, ← Real.lt_toNNReal_iff_coe_lt, Real.toNNReal_one, nnnorm_smul, ←
NNReal.lt_inv_iff_mul_lt h]
simpa [← smul_pow, (summable_geometric_of_norm_lt_one norm_lt).hasSum_iff] using
(NormedRing.inverse_one_sub _ norm_lt).symm }
