-- Infinite series as limits of partial sums
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Real.Analysis.Series
import FiniteSum
import ExtremeValue

-- Section: Series
-- A series sums to S when its sequence of partial sums converges to S.
predicate SumsTo (u : Set) (S : Real) :=
  RealSequence(u) ∧ ConvergesTo(prefixSums(u), S)

predicate Summable (u : Set) := ∃ S ∈ ℝ, SumsTo(u, S)

theorem SumsTo.sequence (u : Set) (S : Real)
  requires sums : SumsTo(u, S)
  shows RealSequence(u)
proof
  simp [SumsTo]

theorem SumsTo.converges (u : Set) (S : Real)
  requires sums : SumsTo(u, S)
  shows ConvergesTo(prefixSums(u), S)
proof
  simp [SumsTo]

theorem SumsTo.of_converges (u : Set) (S : Real)
  requires sequence : RealSequence(u)
  requires converges : ConvergesTo(prefixSums(u), S)
  shows SumsTo(u, S)
proof
  constructor
  . exact sequence
  . exact converges

theorem SumsTo.unique (u : Set) (S T : Real)
  requires sumsS : SumsTo(u, S)
  requires sumsT : SumsTo(u, T)
  shows S = T
proof
  have convergesS := SumsTo.converges with sumsS
  have convergesT := SumsTo.converges with sumsT
  exact ConvergesTo.unique with convergesS, convergesT

theorem SumsTo.summable (u : Set) (S : Real)
  requires sums : SumsTo(u, S)
  shows Summable(u)
proof
  have realS : S ∈ ℝ by simp [Real]
  witness S
  constructor
  . exact realS
  . exact sums

-- Section: PartialSumAlgebra
-- The partial sums of a termwise sum are the sums of the partial sums.
theorem prefixSums.add (u v : Set, n : Nat)
  requires sequenceU : RealSequence(u)
  requires sequenceV : RealSequence(v)
  shows prefixSums(addSequence(u, v))[n] =
    addSequence(prefixSums(u), prefixSums(v))[n]
proof
  have added := addSequence.sequence with sequenceU, sequenceV
  have prefixesU := prefixSums.sequence with sequenceU
  have prefixesV := prefixSums.sequence with sequenceV
  have sumU := RealSequence.value at prefixSums(u), n with prefixesU
  have sumV := RealSequence.value at prefixSums(v), n with prefixesV
  have valueAdded := prefixSums.value at addSequence(u, v), n with added
  have valueU := prefixSums.value at u, n with sequenceU
  have valueV := prefixSums.value at v, n with sequenceV
  have combined := addSequence.value at prefixSums(u), prefixSums(v), n with
    prefixesU, prefixesV, sumU, sumV
  have linear := realPartialSum.add at u, v, n with sequenceU, sequenceV
  rw [valueAdded, combined, valueU, valueV, linear]
  rfl

theorem prefixSums.neg (u : Set, n : Nat)
  requires sequence : RealSequence(u)
  shows prefixSums(negSequence(u))[n] = negSequence(prefixSums(u))[n]
proof
  have negated := negSequence.sequence with sequence
  have prefixes := prefixSums.sequence with sequence
  have sumReal := RealSequence.value at prefixSums(u), n with prefixes
  have valueNegated := prefixSums.value at negSequence(u), n with negated
  have valueU := prefixSums.value at u, n with sequence
  have combined := negSequence.value at prefixSums(u), n with prefixes, sumReal
  have linear := realPartialSum.neg at u, n with sequence
  rw [valueNegated, combined, valueU, linear]
  rfl

theorem prefixSums.scale (u : Set, n : Nat, C : Real)
  requires sequence : RealSequence(u)
  shows prefixSums(mulSequence(constantSequence(C), u))[n] =
    mulSequence(constantSequence(C), prefixSums(u))[n]
proof
  have constants := constantSequence.sequence at C
  have scaled := mulSequence.sequence with constants, sequence
  have prefixes := prefixSums.sequence with sequence
  have constantReal := RealSequence.value at constantSequence(C), n with
    constants
  have sumReal := RealSequence.value at prefixSums(u), n with prefixes
  have valueScaled := prefixSums.value at
    mulSequence(constantSequence(C), u), n with scaled
  have valueU := prefixSums.value at u, n with sequence
  have combined := mulSequence.value at
    constantSequence(C), prefixSums(u), n with
      constants, prefixes, constantReal, sumReal
  have constant := constantSequence.value at C, n with *
  have linear := realPartialSum.scale at u, n, C with sequence
  rw [valueScaled, combined, valueU, linear, constant]
  rfl

-- Section: SeriesAlgebra
theorem SumsTo.add (u v : Set) (S T : Real)
  requires sumsU : SumsTo(u, S)
  requires sumsV : SumsTo(v, T)
  shows SumsTo(addSequence(u, v), S + T)
proof
  have sequenceU := SumsTo.sequence with sumsU
  have sequenceV := SumsTo.sequence with sumsV
  have convergesU := SumsTo.converges with sumsU
  have convergesV := SumsTo.converges with sumsV
  have added := addSequence.sequence with sequenceU, sequenceV
  have prefixes := prefixSums.sequence with added
  have limit := ConvergesTo.add with convergesU, convergesV
  have equal : ∀ n ∈ ℕ, prefixSums(addSequence(u, v))[n] =
      addSequence(prefixSums(u), prefixSums(v))[n]
    intros n naturalN
    have typedN : Nat(n) by exact nat.omega.backward at n with naturalN
    exact prefixSums.add with sequenceU, sequenceV
  have converges := ConvergesTo.of_equal_terms with prefixes, limit, equal
  exact SumsTo.of_converges with added, converges

theorem SumsTo.neg (u : Set) (S : Real)
  requires sums : SumsTo(u, S)
  shows SumsTo(negSequence(u), -S)
proof
  have sequence := SumsTo.sequence with sums
  have converges := SumsTo.converges with sums
  have negated := negSequence.sequence with sequence
  have prefixes := prefixSums.sequence with negated
  have limit := ConvergesTo.neg with converges
  have equal : ∀ n ∈ ℕ, prefixSums(negSequence(u))[n] =
      negSequence(prefixSums(u))[n]
    intros n naturalN
    have typedN : Nat(n) by exact nat.omega.backward at n with naturalN
    exact prefixSums.neg with sequence
  have convergesNegated := ConvergesTo.of_equal_terms with
    prefixes, limit, equal
  exact SumsTo.of_converges with negated, convergesNegated

theorem SumsTo.sub (u v : Set) (S T : Real)
  requires sumsU : SumsTo(u, S)
  requires sumsV : SumsTo(v, T)
  shows SumsTo(subSequence(u, v), S - T)
proof
  have negated := SumsTo.neg with sumsV
  have added := SumsTo.add with sumsU, negated
  unfold subSequence
  unfold realSubValue
  exact added

theorem SumsTo.scale (u : Set) (S C : Real)
  requires sums : SumsTo(u, S)
  shows SumsTo(mulSequence(constantSequence(C), u), C * S)
proof
  have sequence := SumsTo.sequence with sums
  have converges := SumsTo.converges with sums
  have constants := constantSequence.sequence at C
  have scaled := mulSequence.sequence with constants, sequence
  have prefixes := prefixSums.sequence with scaled
  have constantConverges := constantSequence.converges at C
  have limit := ConvergesTo.mul with constantConverges, converges
  have equal : ∀ n ∈ ℕ,
      prefixSums(mulSequence(constantSequence(C), u))[n] =
        mulSequence(constantSequence(C), prefixSums(u))[n]
    intros n naturalN
    have typedN : Nat(n) by exact nat.omega.backward at n with naturalN
    exact prefixSums.scale with sequence
  have convergesScaled := ConvergesTo.of_equal_terms with
    prefixes, limit, equal
  exact SumsTo.of_converges with scaled, convergesScaled

-- Section: FiniteSeries
-- Beyond the index N the partial sums of a vanishing sequence stay fixed.
theorem realPartialSum.eventually_zero (u : Set, N m : Nat)
  requires sequence : RealSequence(u)
  requires vanishing : ∀ n ∈ ℕ, N ≤ n → u[n] = (0:R)
  shows realPartialSum(u, add(N, m)) = ∑ i < N, u(i)
proof
  induction m
  | zero =>
    rw add.right_unit
    rfl
  | succ(k) using ih =>
    have index : Nat(add(N, k)) by typecheck
    have indexNatural := nat.omega.forward with index
    have after : N ≤ add(N, k) by exact LessEqual.add_right at N, k
    have term := vanishing with add(N, k), indexNatural, after
    have termReal := RealSequence.value at u, add(N, k) with sequence
    have prefixReal := realPartialSum.real at u, N with sequence
    rw [add.succ_right, realPartialSum.succ, ih]
    linarith

theorem SumsTo.of_eventually_zero (u : Set, N : Nat)
  requires sequence : RealSequence(u)
  requires vanishing : ∀ n ∈ ℕ, N ≤ n → u[n] = (0:R)
  shows SumsTo(u, ∑ i < N, u(i))
proof
  have prefixes := prefixSums.sequence with sequence
  have sumReal := realPartialSum.real at u, N with sequence
  have naturalN := nat.omega.forward at N with assumption
  apply SumsTo.of_converges with sequence
  constructor
  . exact prefixes
  . intros E realE positive
    witness N
    constructor
    . exact naturalN
    . intros n naturalIndex after
      have typedN : Nat(n) by exact nat.omega.backward at n with naturalIndex
      obtain ⟨m, typedM, split⟩ := after
      have value := prefixSums.value at u, n with sequence
      have fixed := realPartialSum.eventually_zero at u, N, m with
        sequence, vanishing
      rw split at fixed
      rw [value, fixed]
      exact openBall.center with positive

theorem SumsTo.zero
  shows SumsTo(constantSequence((0:R)), (0:R))
proof
  have sequence := constantSequence.sequence at (0:R)
  have vanishing : ∀ n ∈ ℕ, 0 ≤ n → constantSequence(0)[n] = (0:R)
    intros n naturalN after
    have typedN : Nat(n) by exact nat.omega.backward at n with naturalN
    exact constantSequence.value at (0:R), n with *
  have sums := SumsTo.of_eventually_zero at constantSequence(0), 0 with
    sequence, vanishing
  rwa realPartialSum.zero at sums

-- Section: Comparison
theorem SumsTo.le_of_le_terms (u v : Set) (S T : Real)
  requires sumsU : SumsTo(u, S)
  requires sumsV : SumsTo(v, T)
  requires ordered : PointwiseLE(u, v)
  shows S ≤ T
proof
  have sequenceU := SumsTo.sequence with sumsU
  have sequenceV := SumsTo.sequence with sumsV
  have convergesU := SumsTo.converges with sumsU
  have convergesV := SumsTo.converges with sumsV
  have bounded : ∀ k ∈ ℕ, (u[k]:R) ≤ (v[k]:R)
    intros k naturalK
    have view := ordered with k, naturalK
    exact realLe.characterization.backward with view
  have prefixOrdered : PointwiseLE(prefixSums(u), prefixSums(v))
    intros n naturalN
    have typedN : Nat(n) by exact nat.omega.backward at n with naturalN
    have valueU := prefixSums.value at u, n with sequenceU
    have valueV := prefixSums.value at v, n with sequenceV
    have comparison := realPartialSum.monotone at u, v, n with
      sequenceU, sequenceV, bounded
    rw [valueU, valueV]
    exact realLe.characterization.forward with comparison
  exact ConvergesTo.le_of_le_terms with convergesU, convergesV, prefixOrdered

theorem SumsTo.nonnegative (u : Set) (S : Real)
  requires sums : SumsTo(u, S)
  requires nonnegative : NonnegativeTerms(u)
  shows 0 ≤ S
proof
  have sequence := SumsTo.sequence with sums
  have ordered : PointwiseLE(constantSequence(0), u)
    intros n naturalN
    have typedN : Nat(n) by exact nat.omega.backward at n with naturalN
    have value := constantSequence.value at (0:R), n with *
    rw value
    exact nonnegative with n, naturalN
  exact SumsTo.le_of_le_terms with SumsTo.zero, sums, ordered

-- Section: Summability
theorem Summable.add (u v : Set)
  requires summableU : Summable(u)
  requires summableV : Summable(v)
  shows Summable(addSequence(u, v))
proof
  obtain ⟨S, realS, sumsU⟩ := summableU
  obtain ⟨T, realT, sumsV⟩ := summableV
  have typedS : Real(S) by exact realS
  have typedT : Real(T) by exact realT
  have sums := SumsTo.add with sumsU, sumsV
  exact SumsTo.summable with sums

theorem Summable.neg (u : Set)
  requires summable : Summable(u)
  shows Summable(negSequence(u))
proof
  obtain ⟨S, realS, sums⟩ := summable
  have typedS : Real(S) by exact realS
  have negated := SumsTo.neg with sums
  exact SumsTo.summable with negated

theorem Summable.sub (u v : Set)
  requires summableU : Summable(u)
  requires summableV : Summable(v)
  shows Summable(subSequence(u, v))
proof
  obtain ⟨S, realS, sumsU⟩ := summableU
  obtain ⟨T, realT, sumsV⟩ := summableV
  have typedS : Real(S) by exact realS
  have typedT : Real(T) by exact realT
  have sums := SumsTo.sub with sumsU, sumsV
  exact SumsTo.summable with sums

theorem Summable.scale (u : Set) (C : Real)
  requires summable : Summable(u)
  shows Summable(mulSequence(constantSequence(C), u))
proof
  obtain ⟨S, realS, sums⟩ := summable
  have typedS : Real(S) by exact realS
  have scaled := SumsTo.scale at u, S, C with sums
  exact SumsTo.summable with scaled

-- Section: Tails
-- Dropping the first k terms of a convergent sequence keeps its limit.
theorem ConvergesTo.shifted (u : Set) (L : Real, k : Nat)
  requires converges : ConvergesTo(u, L)
  shows ConvergesTo(shiftedRealSequence(u, k), L)
proof
  have sequence := ConvergesTo.sequence with converges
  have shifted := shiftedRealSequence.sequence at u, k with sequence
  constructor
  . exact shifted
  . intros E realE positive
    obtain ⟨N, naturalN, close⟩ := ConvergesTo.eventually with
      converges, positive
    witness N
    constructor
    . exact naturalN
    . intros n naturalIndex after
      have typedN : Nat(n) by exact nat.omega.backward at n with naturalIndex
      have typedBound : Nat(N) by exact nat.omega.backward at N with naturalN
      have index : Nat(add(k, n)) by typecheck
      have indexNatural := nat.omega.forward with index
      have below : N ≤ add(k, n) by arith
      have value := shiftedRealSequence.value at u, k, n with sequence
      rw value
      exact close with add(k, n), indexNatural, below

-- The terms of a convergent series tend to zero: each term is the
-- difference of two consecutive partial sums.
theorem SumsTo.terms_converge_zero (u : Set) (S : Real)
  requires sums : SumsTo(u, S)
  shows ConvergesTo(u, (0:R))
proof
  have sequence := SumsTo.sequence with sums
  have converges := SumsTo.converges with sums
  have prefixes := prefixSums.sequence with sequence
  have shifted := ConvergesTo.shifted at prefixSums(u), S, 1 with converges
  have limit := ConvergesTo.sub with shifted, converges
  have zero := realSubValue.self at S
  rw zero at limit
  have shiftedSequence := shiftedRealSequence.sequence at
    prefixSums(u), 1 with prefixes
  have equal : ∀ n ∈ ℕ, u[n] =
      subSequence(shiftedRealSequence(prefixSums(u), 1), prefixSums(u))[n]
    intros n naturalN
    have typedN : Nat(n) by exact nat.omega.backward at n with naturalN
    have shiftedReal := RealSequence.value at
      shiftedRealSequence(prefixSums(u), 1), n with shiftedSequence
    have prefixReal := RealSequence.value at prefixSums(u), n with prefixes
    have difference := subSequence.value at
      shiftedRealSequence(prefixSums(u), 1), prefixSums(u), n with
        shiftedSequence, prefixes, shiftedReal, prefixReal
    have shiftedValue := shiftedRealSequence.value at
      prefixSums(u), 1, n with prefixes
    have swap := add.commutative at n, 1
    have successor := add.right_one at n
    have next := prefixSums.value at u, succ(n) with sequence
    have current := prefixSums.value at u, n with sequence
    have term := RealSequence.value at u, n with sequence
    have sumReal := realPartialSum.real at u, n with sequence
    rw [difference, shiftedValue, swap, successor, next, current,
      realPartialSum.succ]
    ring
  exact ConvergesTo.of_equal_terms with sequence, limit, equal