Shifting sums

Stream: Is there code for X?

[Vincent Beffara]

Do we have changes of indices in sums like this?

def Nci (n₀ : ℕ) : set ℕ := {n : ℕ | n₀ ≤ n}

lemma shift_sum {n₀ : ℕ} {a : ℕ → ℂ} {s : ℂ} (ha : has_sum (a ∘ (coe : Nci n₀ → ℕ)) s) :
  has_sum (λ n, a (n₀ + n)) s := sorry

Actually that might be an XY problem, what I need is

example {a : ℕ → ℂ} {s : ℂ} (ha : has_sum a s) (h'a : a 0 = 0) :
  has_sum (λ n, a (n + 1)) s

and I reached the above by following has_sum_subtype_iff_of_support_subsetbut that might be overly general for what I need.

[Yaël Dillies]

Nci is Ici

[Vincent Beffara]

Ah I thought Ici was for reals, should have thought a little more

[Vincent Beffara]

That will do for now, but feels like reinventing the wheel several times in a row:

def shift (n₀ : ℕ) : ℕ ≃ set.Ici n₀ := {
  to_fun := λ n, ⟨n₀ + n, by simp only [set.Ici, set.mem_set_of_eq, le_add_iff_nonneg_right, zero_le]⟩,
  inv_fun := λ n, n - n₀,
  left_inv := λ n, by simp only [subtype.coe_mk, add_tsub_cancel_left],
  right_inv := λ ⟨n, hn⟩, by simp only [subtype.coe_mk, subtype.mk_eq_mk]; linarith }

def shift' (n₀ : ℕ) : finset ℕ ≃ finset (set.Ici n₀) := {
  to_fun := finset.map (shift n₀),
  inv_fun := finset.map (shift n₀).symm,
  left_inv := λ s, by ext b; simp only [finset.mem_map_equiv, equiv.coe_eq_to_embedding,
    equiv.symm_symm, equiv.symm_apply_apply],
  right_inv := λ s, by ext b; simp only [finset.mem_map_equiv, equiv.coe_eq_to_embedding,
    equiv.symm_symm, equiv.apply_symm_apply] }

lemma tendsto_shift'_at_top {n₀ : ℕ} : tendsto (shift' n₀) at_top at_top :=
begin
  refine filter.tendsto_at_top_finset_of_monotone (λ s1 s2, finset.map_subset_map.mpr) _,
  rintro ⟨x, hx⟩,
  refine ⟨{x - n₀}, _⟩,
  simp only [shift', shift, equiv.coe_eq_to_embedding, equiv.coe_fn_mk, finset.map_singleton,
    equiv.to_embedding_apply, finset.mem_singleton, subtype.mk_eq_mk],
  linarith
end

lemma shift_sum {n₀ : ℕ} {a : ℕ → ℂ} {s : ℂ} (ha : has_sum (a ∘ (coe : set.Ici n₀ → ℕ)) s) :
  has_sum (λ n, a (n₀ + n)) s :=
begin
  simp only [has_sum] at ha ⊢,
  suffices : tendsto (((λ (s : finset ℕ), ∑ b in s, a (n₀ + b)) ∘ (shift' n₀).symm) ∘ (shift' n₀))
    at_top (𝓝 s),
  simpa only [comp.assoc _ (shift' n₀).symm (shift' n₀), equiv.symm_comp_self] using this,
  refine tendsto.comp _ tendsto_shift'_at_top,
  change tendsto (λ s, ∑ b in ((shift' n₀).symm s), a (n₀ + b)) at_top (𝓝 s),
  convert ha,
  funext s,
  simp only [shift', shift, equiv.coe_eq_to_embedding, equiv.coe_fn_symm_mk, finset.sum_map,
    equiv.to_embedding_apply, comp_app],
  congr,
  funext,
  congr,
  cases x,
  linarith
end

[Sebastien Gouezel]

You can look around docs#tsum_eq_zero_add