changeOrigin_finite_of_finite — Mathlib

English

If p is finite, then for any m with n ≤ k+m, p.changeOriginSeries k m = 0.

Русский

Если p конечна, то для любого m с n ≤ k+m, p.changeOriginSeries k m = 0.

LaTeX

$$∀ {m}, n ≤ k+m → p.changeOriginSeries k m = 0$$

Lean4

/-- If `p` is a formal multilinear series such that `p m = 0` for `n ≤ m`, then
`p.changeOrigin x k = 0` for `n ≤ k`. -/
theorem changeOrigin_finite_of_finite (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (hn : ∀ (m : ℕ), n ≤ m → p m = 0)
    {k : ℕ} (hk : n ≤ k) : p.changeOrigin x k = 0 :=
  by
  rw [changeOrigin, p.changeOriginSeries_sum_eq_partialSum_of_finite hn]
  apply Finset.sum_eq_zero
  intro m hm
  rw [Finset.mem_range] at hm
  rw [p.changeOriginSeries_finite_of_finite hn k (le_add_of_le_left hk), ContinuousMultilinearMap.zero_apply]

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