Computation of an explicit sum

Stream: Is there code for X?

[Riccardo Brasca]

Working on the flt-project I need to prove something like

import algebra.big_operators.basic
import tactic.linarith

open_locale big_operators

open nat

namespace test

variables {R : Type*} [comm_ring R] {n : ℕ} (hn : 4 ≤ n)

include hn

def f (a : ℤ) : fin n → ℤ := λ x, if x = ⟨1, by linarith⟩ then a else
  if x = ⟨n.pred, pred_lt (by linarith)⟩ then -a else 0

example (x : R) (a : ℤ) : ∑ (j : fin n), f hn a j • x ^ (j : ℕ) =
  a * x ^ ((⟨1, by linarith⟩ : fin n) : ℕ) -
  ↑a * x ^ ((⟨n.pred, pred_lt (by linarith)⟩ : fin n) : ℕ) := sorry

end test

I can do it by hand, but later I will need a similar result with 4 terms, and this is already annoying enough... Does anyone see a smart way of doing it? Note that I don't care about the definition of f, I only need a function f : fin n → ℤ such that the example is true (but I cannot change the RHS).

[Floris van Doorn]

Is there a reason you work with fin in the first place, and not sum over docs#finset.range?

[Riccardo Brasca]

I think it's irrelevant, f can be defined on ℕ and one can use docs#finset.sum_range. In my application I have at some point to use fin because I need to identify the LHS with a linear combination of element of a basis, but I think I can use docs#finset.sum_range also for that.

[Riccardo Brasca]

The current proof is

import algebra.big_operators.basic
import tactic.linarith

open_locale big_operators

open nat finset

namespace test

variables {R : Type*} [comm_ring R] {n : ℕ} (hn : 4 ≤ n)

include hn

def f (a : ℤ) : fin n → ℤ := λ x, if x = ⟨1, by linarith⟩ then a else
  if x = ⟨n.pred, pred_lt (by linarith)⟩ then -a else 0

example (x : R) (a : ℤ) : ∑ (j : fin n), f hn a j • x ^ (j : ℕ) =
  a * x ^ ((⟨1, by linarith⟩ : fin n) : ℕ) -
  ↑a * x ^ ((⟨n.pred, pred_lt (by linarith)⟩ : fin n) : ℕ) :=
begin
  have hnotmem : (⟨n.pred, pred_lt (by linarith)⟩ : fin n) ∈ univ.erase (⟨1, by linarith⟩ : fin n),
  { refine mem_erase.2 ⟨λ h, _, mem_univ _⟩,
    simp only [fin.ext_iff, fin.coe_mk, nat.pred_eq_succ_iff] at h,
    linarith },
  rw [← insert_erase (mem_univ (⟨1, by linarith⟩ : fin n)), sum_insert, ← insert_erase hnotmem,
    sum_insert],
  suffices : ∀ i ∈ (univ.erase (⟨1, by linarith⟩ : fin n)).erase
    (⟨n.pred, pred_lt (by linarith)⟩ : fin n), f hn a i • x ^ (i : ℕ) = 0,
  { rw [sum_congr rfl this, sum_const_zero, add_zero],
    have hn2 : n ≠ 2 := λ _, by linarith,
    simp [f, hn2, sub_eq_add_neg] },
  intros i hi,
  suffices H : i ≠ ⟨1, by linarith⟩ ∧ i ≠ ⟨n.pred, pred_lt (by linarith)⟩, simp [H.1, H.2, f],
  exact ⟨λ heq, by simpa [heq] using hi,
    λ heq, by simpa [heq] using erase_subset_erase _ (erase_subset _ _) hi⟩,
  repeat { exact not_mem_erase _ _ }
end

end test

That's not that bad, but still...

[Riccardo Brasca]

(I can of course remove a lot of linarith, but that's not important)

[Floris van Doorn]

import algebra.big_operators.basic

open_locale big_operators

open nat finset

@[simp]
lemma finset.range_filter_eq {n m : ℕ} : (range n).filter (= m) = if m < n then {m} else ∅ :=
sorry

lemma ne_and_eq_iff_right {α} {a b c : α} (h : b ≠ c) : a ≠ b ∧ a = c ↔ a = c :=
and_iff_right_of_imp (λ h2, h2.symm ▸ h.symm)

namespace test

variables {R : Type*} [comm_ring R] {n : ℕ} (hn : 4 ≤ n)

include hn
def f (a : ℤ) : ℕ → ℤ := λ x, if x = 1 then a else if x = n.pred then -a else 0

example (x : R) (a : ℤ) : ∑ j in range n, f hn a j • x ^ (j : ℕ) = a * x ^ 1 - ↑a * x ^ n.pred :=
begin
  have h2n : 1 ≠ n.pred := sorry,
  have h3n : 1 < n := sorry,
  have h4n : n.pred < n := sorry,
  simp_rw [f, ite_smul, sum_ite, finset.filter_filter, ← ne.def, ne_and_eq_iff_right h2n,
    finset.range_filter_eq],
  simp [h3n, h4n, sub_eq_add_neg],
end

end test

[Floris van Doorn]

This can be repeated with more than 2 terms relatively easily. You just have to show linearly many assumptions i < n and quadratically many assumptions i ≠ j

[Riccardo Brasca]

Oooh, very nice!!

[Floris van Doorn]

Here is an example with 3 terms:

def f (a : ℤ) : ℕ → ℤ := λ x, if x = 1 then a else if x = 2 then 1 else if x = n.pred then -a else 0

example (x : R) (a : ℤ) : ∑ j in range n, f hn a j • x ^ (j : ℕ) = a * x ^ 1 + x ^ 2 - ↑a * x ^ n.pred :=
begin
  have h2n : 1 ≠ n.pred := sorry,
  have h12 : 1 ≠ 2 := sorry,
  have h5n : 2 ≠ n.pred := sorry,
  have h3n : 1 < n := sorry,
  have h6n : 2 < n := sorry,
  have h4n : n.pred < n := sorry,
  simp [f, ite_smul, sum_ite, finset.filter_filter, ← ne.def, and_assoc,
    ne_and_eq_iff_right h12, ne_and_eq_iff_right h5n, ne_and_eq_iff_right h2n,
    finset.range_filter_eq, *, sub_eq_add_neg, add_assoc],
end

[Riccardo Brasca]

Let me make sure I can use a function f : ℕ → ℤ, but thanks a lot!

[Floris van Doorn]

It should not be too hard to adapt this argument to fin, it will just get a whole lot uglier.