ArithmeticSeriesStarter

Arithmetic series

Open in Workbench View on GitHub

1-- Arithmetic series2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module ArithmeticSeriesStarter8import Grace.Cumulus.Real.ArithmeticSeries910-- Arbitrary real starting term and common difference; n + 1 terms.11theorem sum_formula (A D : Real, n : Nat)12  shows ∑ i < n + 1, arithmeticTerms(A, D)(i) =13    (((realNat(n):R) + (1:R)) * ((2:R) * A + (realNat(n):R) * D)) /14      (2:R)15proof16  exact arithmeticSeries.quotient at A, D, n with *1718-- 1 + 3 + ... + (2n - 1) = n², including n = 0.19theorem odd_numbers (n : Nat)20  shows ∑ i < n, arithmeticTerms(realOne, (2:R))(i) =21    (realNat(n):R) * (realNat(n):R)22proof23  exact arithmeticSeries.odd_sum at n with *2425theorem empty_sum (A D : Real)26  shows ∑ i < 0, arithmeticTerms(A, D)(i) = (0:R)27proof28  exact realPartialSum.zero2930theorem singleton_sum (A D : Real)31  shows ∑ i < 1, arithmeticTerms(A, D)(i) = A32proof33  have value := arithmeticTerms.value at A, D, 0 with *34  rw realPartialSum.succ35  rw realPartialSum.zero36  rw value37  rw realNat.zero38  ring39