changeOriginSeries_sum_eq_partialSum_of_finite

English

If p is a formal multilinear series and hn ensures p_m = 0 for n ≤ m, then for all x,y in E, (p.changeOrigin x).sum y = p.sum (x + y).

Русский

Если p—формальная многолинейная серия и hn гарантирует нулевые коэффициенты после n, тогда для любых x,y: (p.changeOrigin x).sum y = p.sum (x+y).

LaTeX

$$$\\forall x,y:\\; (p.changeOrigin x).sum y = p.sum (x+y)$$$

Lean4

theorem changeOriginSeries_sum_eq_partialSum_of_finite (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ}
    (hn : ∀ (m : ℕ), n ≤ m → p m = 0) (k : ℕ) :
    (p.changeOriginSeries k).sum = (p.changeOriginSeries k).partialSum (n - k) :=
  by
  ext x
  rw [partialSum, FormalMultilinearSeries.sum,
    tsum_eq_sum (f := fun m => p.changeOriginSeries k m (fun _ => x)) (s := Finset.range (n - k))]
  intro m hm
  rw [Finset.mem_range, not_lt] at hm
  rw [p.changeOriginSeries_finite_of_finite hn k (by rw [add_comm]; exact Nat.le_add_of_sub_le hm),
    ContinuousMultilinearMap.zero_apply]

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