English
The radius is monotone with respect to coefficient-wise majorization: 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
/-- The left inverse does not depend on the zeroth coefficient of a formal multilinear
series. -/
theorem leftInv_removeZero (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) :
p.removeZero.leftInv i x = p.leftInv i x := by
ext1 n
induction n using Nat.strongRec' with
| _ n IH
match n with
| 0 =>
simp -- if one replaces `simp` with `refl`, the proof times out in the kernel.
| 1 =>
simp -- TODO: why?
| n + 2 =>
simp only [leftInv, neg_inj]
refine Finset.sum_congr rfl fun c cuniv => ?_
rcases c with ⟨c, hc⟩
ext v
simp [IH _ hc]
