Grace/Cumulus/Real/PowerSums.g17

Open in Workbench Download source

Imports

ArithmeticSeries

Declarations

Source

1-- Sums of powers: closed forms for the sums of the first n squares and cubes,2-- and the sum of cubes as the square of the sum of the first n naturals3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Real.PowerSums9import ArithmeticSeries1011-- The squares and cubes of the naturals, as real sequences.12defgraph squareTerms (n ∈ ℕ) : ℝ := (realNat(n):R) * (realNat(n):R)13proof14  have typedN := nat.omega.backward at n with member15  have count := realNat.real at n with typedN16  exact realMulValue.real at realNat(n), realNat(n)1718defgraph cubeTerms (n ∈ ℕ) : ℝ := (realNat(n):R) * (realNat(n):R) * (realNat(n):R)19proof20  have typedN := nat.omega.backward at n with member21  have count := realNat.real at n with typedN22  have square := realMulValue.real at realNat(n), realNat(n)23  exact realMulValue.real at (realNat(n):R) * (realNat(n):R), realNat(n)2425theorem squareTerms.sequence26  shows RealSequence(squareTerms)27proof28  exact squareTerms.function2930theorem cubeTerms.sequence31  shows RealSequence(cubeTerms)32proof33  exact cubeTerms.function3435-- 6·(0² + 1² + ⋯ + (n−1)²) = n(n − 1)(2n − 1).36theorem powerSum.squares (n : Nat)37  shows (6:R) * (∑ i < n, squareTerms(i):R) =38    (realNat(n):R) * ((realNat(n):R) - (1:R)) * ((2:R) * (realNat(n):R) - (1:R))39proof40  induction n41  | zero =>42    rw [realPartialSum.zero, realNat.zero]43    ring44  | succ(k) using ih =>45    have sequence := squareTerms.sequence46    have count := realNat.real at k47    have value := squareTerms.value at k with *48    rw [realPartialSum.succ, value, realNat.succ]49    linear_combination ih5051-- 6·(1² + ⋯ + n²) = n(n + 1)(2n + 1).52theorem powerSum.squares_inclusive (n : Nat)53  shows (6:R) * (∑ i < n + 1, squareTerms(i):R) =54    (realNat(n):R) * ((realNat(n):R) + (1:R)) * ((2:R) * (realNat(n):R) + (1:R))55proof56  have bound : n + 1 = succ(n) := add.right_one at n57  rw bound58  have all := powerSum.squares at succ(n)59  rw realNat.succ at all60  linear_combination all6162-- 4·(0³ + 1³ + ⋯ + (n−1)³) = n²(n − 1)².63theorem powerSum.cubes (n : Nat)64  shows (4:R) * (∑ i < n, cubeTerms(i):R) =65    (realNat(n):R) * (realNat(n):R) * ((realNat(n):R) - (1:R)) * ((realNat(n):R) - (1:R))66proof67  induction n68  | zero =>69    rw [realPartialSum.zero, realNat.zero]70    ring71  | succ(k) using ih =>72    have sequence := cubeTerms.sequence73    have count := realNat.real at k74    have value := cubeTerms.value at k with *75    rw [realPartialSum.succ, value, realNat.succ]76    linear_combination ih7778-- 4·(1³ + ⋯ + n³) = n²(n + 1)².79theorem powerSum.cubes_inclusive (n : Nat)80  shows (4:R) * (∑ i < n + 1, cubeTerms(i):R) =81    (realNat(n):R) * (realNat(n):R) * ((realNat(n):R) + (1:R)) * ((realNat(n):R) + (1:R))82proof83  have bound : n + 1 = succ(n) := add.right_one at n84  rw bound85  have all := powerSum.cubes at succ(n)86  rw realNat.succ at all87  linear_combination all8889-- Nicomachus: 1³ + ⋯ + n³ = (1 + ⋯ + n)².90theorem powerSum.cubes_eq_square_of_sum (n : Nat)91  shows ∑ i < n + 1, cubeTerms(i) =92    (∑ i < n + 1, arithmeticTerms(realZero, realOne)(i):R) *93      (∑ i < n + 1, arithmeticTerms(realZero, realOne)(i):R)94proof95  have bound : n + 1 = succ(n) := add.right_one at n96  rw bound97  have cubes := powerSum.cubes_inclusive at n98  rw bound at cubes99  have gauss := arithmeticSeries.gauss at n100  rw bound at gauss101  have scaled : (4:R) * ((∑ i < succ(n), cubeTerms(i):R) - (∑ i < succ(n), arithmeticTerms(realZero, realOne)(i):R) * (∑ i < succ(n), arithmeticTerms(realZero, realOne)(i):R)) = (0:R)102    linear_combination cubes - ((2:R) * (∑ i < succ(n), arithmeticTerms(realZero, realOne)(i):R) + (realNat(n):R) * ((realNat(n):R) + (1:R))) * gauss103  have fourPositive : (0:R) < (4:R) by linarith104  have fourNonzero : (4:R) ≠ (0:R)105    intro zero106    rw zero at fourPositive107    linarith108  have cancel := realInvValue.mul_left with fourNonzero109  have identity : (∑ i < succ(n), cubeTerms(i):R) - (∑ i < succ(n), arithmeticTerms(realZero, realOne)(i):R) * (∑ i < succ(n), arithmeticTerms(realZero, realOne)(i):R) = realInvValue((4:R)) * ((4:R) * ((∑ i < succ(n), cubeTerms(i):R) - (∑ i < succ(n), arithmeticTerms(realZero, realOne)(i):R) * (∑ i < succ(n), arithmeticTerms(realZero, realOne)(i):R)))110    have rearrange : realInvValue((4:R)) * ((4:R) * ((∑ i < succ(n), cubeTerms(i):R) - (∑ i < succ(n), arithmeticTerms(realZero, realOne)(i):R) * (∑ i < succ(n), arithmeticTerms(realZero, realOne)(i):R))) = (realInvValue((4:R)) * (4:R)) * ((∑ i < succ(n), cubeTerms(i):R) - (∑ i < succ(n), arithmeticTerms(realZero, realOne)(i):R) * (∑ i < succ(n), arithmeticTerms(realZero, realOne)(i):R))111      ring112    have one := realMulValue.one_left at (∑ i < succ(n), cubeTerms(i):R) - (∑ i < succ(n), arithmeticTerms(realZero, realOne)(i):R) * (∑ i < succ(n), arithmeticTerms(realZero, realOne)(i):R)113    rw [rearrange, cancel, one]114    rfl115  rw scaled at identity116  have zero := realMulValue.zero_right at realInvValue((4:R))117  rw zero at identity118  linear_combination identity119