Grace/Cumulus/Real/ArithmeticSeries.g17

Open in Workbench Download source

Imports

Natural · FiniteSum

Declarations

• arithmeticTerms defgraph
• arithmeticTerms.sequence theorem derivation
• arithmeticSeries.doubled theorem derivation
• arithmeticSeries.inclusive theorem derivation
• arithmeticSeries.first_last theorem derivation
• arithmeticSeries.gauss theorem derivation
• arithmeticSeries.odd_sum theorem derivation
• arithmeticSeries.quotient theorem derivation

Source

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 Grace.Cumulus.Real.ArithmeticSeries8import Natural9import FiniteSum1011defgraph arithmeticTerms (A D : Real) (n ∈ ℕ) : ℝ := A + (realNat(n):R) * D12proof13  have typedN := nat.omega.backward at n with member14  have count := realNat.real at n with typedN15  have term : Real((A:R) + (realNat(n):R) * (D:R))16    typecheck17  unfold Real at term18  exact term1920theorem arithmeticTerms.sequence (A D : Real)21  shows RealSequence(arithmeticTerms(A, D))22proof23  unfold RealSequence24  exact arithmeticTerms.function at A, D with *2526-- The first n terms, including the empty prefix when n = 0.27theorem arithmeticSeries.doubled (A D : Real, n : Nat)28  shows (2:R) * (∑ i < n, arithmeticTerms(A, D)(i):R) =29    (realNat(n):R) * ((2:R) * A + ((realNat(n):R) - (1:R)) * D)30proof31  induction n32  | zero =>33    rw [realPartialSum.zero, realNat.zero]34    ring35  | succ(k) using ih =>36    have sequence := arithmeticTerms.sequence at A, D with *37    have value := arithmeticTerms.value at A, D, k with *38    rw [realPartialSum.succ, value, realNat.succ]39    linear_combination ih4041-- Inclusive indexing matches a + (a+d) + ... + (a+n*d).42theorem arithmeticSeries.inclusive (A D : Real, n : Nat)43  shows (2:R) * (∑ i < n + 1, arithmeticTerms(A, D)(i):R) =44    ((realNat(n):R) + (1:R)) * ((2:R) * A + (realNat(n):R) * D)45proof46  have bound : n + 1 = succ(n) := add.right_one at n47  rw bound48  have sequence := arithmeticTerms.sequence at A, D with *49  have doubled := arithmeticSeries.doubled at A, D, succ(n) with *50  rw realNat.succ at doubled51  linear_combination doubled5253theorem arithmeticSeries.first_last (A D : Real, n : Nat)54  shows (2:R) * (∑ i < n + 1, arithmeticTerms(A, D)(i):R) =55    ((realNat(n):R) + (1:R)) * (A + (arithmeticTerms(A, D)[n]:R))56proof57  have bound : n + 1 = succ(n) := add.right_one at n58  rw bound59  have sequence := arithmeticTerms.sequence at A, D with *60  have value := arithmeticTerms.value at A, D, n with *61  have inclusive := arithmeticSeries.inclusive at A, D, n with *62  rw bound at inclusive63  rw value64  linear_combination inclusive6566theorem arithmeticSeries.gauss (n : Nat)67  shows (2:R) * (∑ i < n + 1, arithmeticTerms(realZero, realOne)(i):R) =68    (realNat(n):R) * ((realNat(n):R) + (1:R))69proof70  have bound : n + 1 = succ(n) := add.right_one at n71  rw bound72  have sequence := arithmeticTerms.sequence at realZero, realOne with *73  have inclusive := arithmeticSeries.inclusive at realZero, realOne, n with *74  rw bound at inclusive75  linear_combination inclusive7677theorem arithmeticSeries.odd_sum (n : Nat)78  shows ∑ k < n, arithmeticTerms(realOne, (2:R))(k) =79    (realNat(n):R) * (realNat(n):R)80proof81  have sequence := arithmeticTerms.sequence at realOne, (2:R) with *82  have prefix := realPartialSum.real with sequence83  have doubled := arithmeticSeries.doubled at realOne, (2:R), n with *84  apply realAddValue.double_cancel with prefix85  linear_combination doubled8687theorem arithmeticSeries.quotient (A D : Real, n : Nat)88  shows ∑ i < n + 1, arithmeticTerms(A, D)(i) =89    (((realNat(n):R) + (1:R)) * ((2:R) * A + (realNat(n):R) * D)) /90      (2:R)91proof92  have bound : n + 1 = succ(n) := add.right_one at n93  rw bound94  have sequence := arithmeticTerms.sequence at A, D with *95  have prefix := realPartialSum.real at arithmeticTerms(A, D), succ(n) with sequence96  have numerator : Real(((realNat(n):R) + (1:R)) * ((2:R) * A + (realNat(n):R) * D))97    typecheck98  have inclusive := arithmeticSeries.inclusive at A, D, n with *99  rw bound at inclusive100  apply realDiv.of_double_eq at ∑ i < succ(n), arithmeticTerms(A, D)(i),101    ((realNat(n):R) + (1:R)) * ((2:R) * A + (realNat(n):R) * D) with prefix, numerator102  linear_combination inclusive103