-rw-r--r-- 7188 leangoppa-20230726/Goppadecoding/sum.lean raw
import Mathlib.Tactic

open BigOperators Finset

namespace Goppadecoding

section lemmas_sum

-- based on sum_flip in library but easier-to-use interface
theorem sum_flip_simpler {M: Type _} [AddCommMonoid M] {n: ℕ} (f: ℕ → M):
  ∑ x in range n, f x = ∑ x in range n, f (n-1-x) :=
by
  by_cases n0: n = 0
  . rw[n0]
    simp only [range_zero, sum_empty]
  have n1: (n-1)+1 = n := Nat.succ_pred n0
  calc
    _ = ∑ x in range ((n-1)+1), f x := by rw[n1]
    _ = ∑ x in range ((n-1)+1), f (n-1-x) := by rw[← sum_flip]
    _ = ∑ x in range n, f (n-1-x) := by rw[n1]

theorem sum_singleton_ite {U: Type _} [DecidableEq U] {S: Finset U} {M: Type _} [AddCommMonoid M] (m: M) {s: U}:
  s ∈ S → ∑ t in S, (if s = t then m else 0) = m := by
  intro sinS
  calc
    ∑ t in S, (if s = t then m else 0)
      = if s ∈ S then m else 0 := by apply sum_ite_eq
    _ = m := by simp only [sinS, ite_true]

theorem sum_ite_add_sum_ite {S: Type _} (P: S → Prop) {hp: DecidablePred P} [Fintype S] {M: Type _} [AddCommMonoid M] (f: S → M) (g: S → M):
  (∑ x, if P x then f x else 0) + (∑ x, if P x then 0 else g x)
  = ∑ x, if P x then f x else g x := by
    repeat rw[sum_ite]
    repeat rw[sum_const_zero]
    simp only [mem_univ, forall_true_left, add_zero, zero_add]

theorem sum_fin_eq_sum_range_lemma {U: Type _} (n: ℕ) (x: ℕ) (f: Fin (Nat.succ n + 1) → U):
  x ∈ range (n+1) → f (Fin.succ x) = f (x+1) := by
    simp only [mem_range]
    intro xn1
    apply congr_arg
    simp only [Fin.succ, Fin.ofNat_eq_val, Fin.coe_ofNat_eq_mod, Fin.eq_iff_veq]
    have xmodn1: x % (n+1) = x := Nat.mod_eq_of_lt xn1
    have x1: (x: Fin (Nat.succ n + 1)) + 1 = (x+1: ℕ) := by simp only [Nat.cast_add, Nat.cast_one]
    have xsuccn: x < Nat.succ n := by simp only [xn1]
    have x1succn1: x + 1 < Nat.succ n + 1 := by simp only [add_lt_add_iff_right, xsuccn]
    have x1succval: ((x+1: ℕ): Fin (Nat.succ n + 1)).val = (x + 1: ℕ) := Fin.val_cast_of_lt x1succn1
    rw[xmodn1,x1,x1succval]

-- similar to Finset.sum_fin_eq_sum_range
-- but uses the automatic %(n+1) cast
-- see also Finset.sum_range where function is defined on ℕ
theorem sum_fin_eq_sum_range {M: Type _} [AddCommMonoid M] (n: ℕ):
  ∀ (f: Fin (n+1) → M),
  ∑ j: Fin (n+1), f j = ∑ j in range (n+1), f j := by
    induction' n with n prevcase
    . intro f
      rw[Fin.sum_univ_succ f]
      simp only [Nat.zero_eq, univ_eq_empty, sum_empty, add_zero, zero_add, range_one, sum_singleton, Nat.cast_zero]
    . intro f
      rw[Fin.sum_univ_succ f]
      rw[sum_range_succ' (fun (x:ℕ) ↦ f x) (Nat.succ n)]
      simp only [Nat.cast_add, Nat.cast_one, Nat.cast_zero]
      rw[prevcase]
      simp only [Nat.succ_eq_add_one]
      rw[add_comm]
      have main: ∑ j in range (n+1), f (Fin.succ j) = ∑ j in range (n+1), f (j+1) := by
        apply sum_congr
        simp only
        intro x
        simp only [mem_range]
        intro xrange
        rw[sum_fin_eq_sum_range_lemma n x f]
        simp only [mem_range, xrange]
      rw[main]

theorem sum_range_mod {M: Type _} [AddCommMonoid M] (n: ℕ) (f: ℕ → ℕ → M):
  ∑ x in range n, f (x % n) x = ∑ x in range n, f x x := by
    apply sum_congr
    simp only
    intro x xrange
    have xn: x < n := List.mem_range.mp xrange
    have xmodn: x % n = x := by rw[Nat.mod_eq_of_lt xn]
    rw[xmodn]

theorem sum_range_ite {M: Type _} [AddCommMonoid M] {m: ℕ} {n: ℕ} (mn: m ≤ n) (f: ℕ → M):
  ∑ x in range n, (if x < m then f x else 0) = ∑ x in range m, f x := by
    let d:ℕ := n - m
    have md: n = m+d := Eq.symm (Nat.add_sub_of_le mn)
    rw[md]
    rw[sum_range_add]
    simp only [ge_iff_le, add_lt_iff_neg_left, not_lt_zero', ite_false, sum_const_zero, add_zero]
    apply sum_congr
    simp only
    intro x xrange
    have xm: x < m := List.mem_range.mp xrange
    simp only [xm, ite_true]

theorem sum_range_eq_sum_fin_ite {M: Type _} [AddCommMonoid M] {m: ℕ} {n: ℕ} (mn: m ≤ n) (f: ℕ → M):
  ∑ j in range m, f j = ∑ j: Fin n, if (j:ℕ) < m then f j else 0 := by
    rw[← sum_range (fun x ↦ if (x:ℕ) < m then f x else 0)]
    rw[sum_range_ite]
    linarith

theorem Ico_filter_not_lt {α: Type _} [LinearOrder α] [LocallyFiniteOrder α] (a b c : α) : ((Ico a b).filter fun x => ¬x < c) = Ico (max a c) b := by
  rw[← Ico_filter_le]
  simp only [not_lt, ge_iff_le, mem_Ico, and_imp, Ico_filter_le, le_max_iff]

theorem sum_Ico_ite_lt {M: Type _} [AddCommMonoid M] {n: ℕ} (f: ℕ → M):
  ∑ x in Ico 0 n, (if x < n then 0 else f x) = 0 := by
    apply sum_eq_zero
    simp only [ge_iff_le, nonpos_iff_eq_zero, Nat.Ico_zero_eq_range, mem_range, ite_eq_left_iff, not_lt]
    intro x xn
    contrapose
    intro _
    simp only [not_le, xn]

theorem sum_fin_ite_eq_sum_fin_ite_sub {M: Type _} [AddCommMonoid M] {m: ℕ} {n: ℕ} {mn: ℕ} (mplusn: mn = m+n) (f: ℕ → M):
  ∑ x: Fin mn, (if (x:ℕ) < m then f (x:ℕ) else 0) =
  ∑ y: Fin mn, (if (y:ℕ) < n then 0 else f ((y:ℕ) - n)) := by
    calc
      ∑ x: Fin mn, (if (x:ℕ) < m then f (x:ℕ) else 0)
        = ∑ x in range mn, (if x < m then f x else 0)
            := by rw[← sum_range (fun x ↦ if x < m then f x else 0)]
      _ = ∑ x in range (m+n), (if x < m then f x else 0)
            := by simp only [mplusn]
      _ = ∑ x in range m, (if x < m then f x else 0) + ∑ x in range n, (if (m + x) < m then f (m + x) else 0)
            := sum_range_add (fun x => if x < m then f x else 0) m n
      _ = ∑ x in range m, f x + ∑ x in range n, (if (m + x) < m then f (m + x) else 0)
            := by simp only [le_refl, sum_range_ite, add_lt_iff_neg_left, not_lt_zero', ite_false, sum_const_zero, add_zero]
      _ = ∑ x in range m, f x
            := by simp only [add_lt_iff_neg_left, not_lt_zero', ite_false, sum_const_zero, add_zero]
      _ = ∑ x in Ico 0 m, f x
            := by simp only [ge_iff_le, nonpos_iff_eq_zero, Nat.Ico_zero_eq_range]
      _ = ∑ y in Ico (0+n) (m+n), f (y-n)
            := by rw[← sum_Ico_add]; apply sum_congr; simp only [ge_iff_le, nonpos_iff_eq_zero, Nat.Ico_zero_eq_range]; simp only [ge_iff_le, nonpos_iff_eq_zero, Nat.Ico_zero_eq_range, mem_range, add_le_iff_nonpos_right, add_tsub_cancel_left, implies_true, forall_const]
      _ = ∑ y in Ico n mn, f (y-n)
            := by simp only [zero_add, ge_iff_le, add_le_iff_nonpos_left, nonpos_iff_eq_zero, mplusn]
      _ = ∑ y in Ico n mn, if y < n then 0 else f (y-n)
            := by rw[sum_ite,Ico_filter_lt,Ico_filter_not_lt]; simp only [ge_iff_le, min_le_iff, le_refl, or_true, Ico_eq_empty_of_le, sum_const_zero, max_self, zero_add]
      _ = ∑ y in Ico 0 n, (if y < n then 0 else f (y-n)) + ∑ y in Ico n mn, (if y < n then 0 else f (y-n))
            := by rw[sum_Ico_ite_lt,zero_add]
      _ = ∑ y in Ico 0 mn, if y < n then 0 else f (y-n)
            := by rw[sum_Ico_consecutive]; simp only [_root_.zero_le]; rw[mplusn]; apply le_add_self
      _ = ∑ y in range mn, if y < n then 0 else f (y-n)
            := by rw[Nat.Ico_zero_eq_range]
      _ = ∑ y: Fin mn, (if (y:ℕ) < n then 0 else f ((y:ℕ) - n))
            := by rw[sum_range]
    
end lemmas_sum