Grace/Cumulus/Real/BinomialTheorem.g17

Imports

Declarations

binomialTerm.sequence theorem derivation
realPartialSum.shift_one theorem derivation
binomial.expansion theorem derivation
binomial.theorem theorem derivation
Source

1-- The binomial theorem: (A + B)^n is the sum over k ≤ n of2-- choose(n, k)·A^k·B^(n−k), by induction on n with Pascal's rule3-- 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.BinomialTheorem9import BinomialTerms10import FiniteSum1112theorem binomialTerm.sequence (A B : Real) (n : Nat)13  shows RealSequence(binomialTerm(A, B, n))14proof15  unfold RealSequence16  exact binomialTerm.function1718-- Splitting the first term off a partial sum.19theorem realPartialSum.shift_one (u : Set) (m : Nat)20  requires sequence : RealSequence(u)21  shows ∑ i < succ(m), u(i) = (u(0):R) + (∑ k < m, shiftedRealSequence(u, succ(0))(k):R)22proof23  have shifted := shiftedRealSequence.sequence at u, succ(0) with sequence24  have split := realPartialSum.split_at at u, succ(0), m with sequence25  have form : add(succ(0), m) = succ(m) by ring26  rw form at split27  have one := realPartialSum.succ at u, 028  have zero := realPartialSum.zero at u29  have firstReal := RealSequence.value at u, 0 with sequence30  have first : realPartialSum(u, succ(0)) = u(0)31    rw one32    linarith33  rw [split, first]34  rfl3536-- The expansion by induction on n, with the bound written as succ(n) so that37-- the induction cases unfold the partial sum directly.38theorem binomial.expansion (A B : Real) (n : Nat)39  shows (A + B) ^ n = ∑ i < succ(n), binomialTerm(A, B, n)(i)40proof41  induction n42  | zero =>43    have sequence := binomialTerm.sequence at A, B, 044    have zeroIndex := binomialTerm.zero_index at A, B, 045    have shift := realPartialSum.shift_one at binomialTerm(A, B, 0), 0 with sequence46    have empty := realPartialSum.zero at shiftedRealSequence(binomialTerm(A, B, 0), succ(0))47    have sumReal : (A + B) ∈ ℝ by typecheck48    rw [realPow.zero, shift, zeroIndex, realPow.zero, empty]49    ring50  | succ(m) using ih =>51    have termsM := binomialTerm.sequence at A, B, m52    have termsNext := binomialTerm.sequence at A, B, succ(m)53    have shiftedNext := shiftedRealSequence.sequence at binomialTerm(A, B, succ(m)), succ(0) with termsNext54    have shiftedM := shiftedRealSequence.sequence at binomialTerm(A, B, m), succ(0) with termsM55    have constantA := constantSequence.sequence at A56    have constantB := constantSequence.sequence at B57    have scaledM := mulSequence.sequence with constantA, termsM58    have scaledShift := mulSequence.sequence with constantB, shiftedM59    have combined := addSequence.sequence with scaledM, scaledShift60    have agree : ∀ k ∈ ℕ, k < succ(m) → shiftedRealSequence(binomialTerm(A, B, succ(m)), succ(0))(k) = addSequence(mulSequence(constantSequence(A), binomialTerm(A, B, m)), mulSequence(constantSequence(B), shiftedRealSequence(binomialTerm(A, B, m), succ(0))))(k)61      intros k hk hkm62      have kNat : Nat(k) by typecheck63      have form : add(succ(0), k) = succ(k) by ring64      have shiftValue := shiftedRealSequence.value at binomialTerm(A, B, succ(m)), succ(0), k with termsNext65      have shiftValueM := shiftedRealSequence.value at binomialTerm(A, B, m), succ(0), k with termsM66      rw form at shiftValue67      rw form at shiftValueM68      have aReal := RealSequence.value at constantSequence(A), k with constantA69      have bReal := RealSequence.value at constantSequence(B), k with constantB70      have aValue := constantSequence.value at A, k71      have bValue := constantSequence.value at B, k72      have termReal := binomialTerm.real at A, B, m, k73      have shiftReal := RealSequence.value at shiftedRealSequence(binomialTerm(A, B, m), succ(0)), k with shiftedM74      have scaledValue := mulSequence.value at constantSequence(A), binomialTerm(A, B, m), k with constantA, termsM, aReal, termReal75      have scaledShiftValue := mulSequence.value at constantSequence(B), shiftedRealSequence(binomialTerm(A, B, m), succ(0)), k with constantB, shiftedM, bReal, shiftReal76      have scaledReal := RealSequence.value at mulSequence(constantSequence(A), binomialTerm(A, B, m)), k with scaledM77      have scaledShiftReal := RealSequence.value at mulSequence(constantSequence(B), shiftedRealSequence(binomialTerm(A, B, m), succ(0))), k with scaledShift78      have sumValue := addSequence.value at mulSequence(constantSequence(A), binomialTerm(A, B, m)), mulSequence(constantSequence(B), shiftedRealSequence(binomialTerm(A, B, m), succ(0))), k with scaledM, scaledShift, scaledReal, scaledShiftReal79      have pascal := binomialTerm.pascal at A, B, m, k80      rw [shiftValue, sumValue, scaledValue, scaledShiftValue, aValue, bValue, shiftValueM, pascal]81      rfl82    have equal := realPartialSum.eq_prefix at shiftedRealSequence(binomialTerm(A, B, succ(m)), succ(0)), addSequence(mulSequence(constantSequence(A), binomialTerm(A, B, m)), mulSequence(constantSequence(B), shiftedRealSequence(binomialTerm(A, B, m), succ(0)))), succ(m) with shiftedNext, combined, agree83    have add := realPartialSum.add at mulSequence(constantSequence(A), binomialTerm(A, B, m)), mulSequence(constantSequence(B), shiftedRealSequence(binomialTerm(A, B, m), succ(0))), succ(m) with scaledM, scaledShift84    have scaleA := realPartialSum.scale at binomialTerm(A, B, m), succ(m), A with termsM85    have scaleB := realPartialSum.scale at shiftedRealSequence(binomialTerm(A, B, m), succ(0)), succ(m), B with shiftedM86    have shiftNext := realPartialSum.shift_one at binomialTerm(A, B, succ(m)), succ(m) with termsNext87    have shiftM := realPartialSum.shift_one at binomialTerm(A, B, m), succ(m) with termsM88    have stepM := realPartialSum.succ at binomialTerm(A, B, m), succ(m)89    have le : m ≤ m90      witness 091      ring92    have beyond := binomialTerm.beyond at A, B, m, m with le93    have firstNext := binomialTerm.succ_zero at A, B, m94    rw [realPow.succ, ih, shiftNext, firstNext, equal, add, scaleA, scaleB]95    rw shiftM at stepM96    have shiftSum : (∑ k < succ(m), shiftedRealSequence(binomialTerm(A, B, m), succ(0))(k):R) = (∑ i < succ(m), binomialTerm(A, B, m)(i):R) - (binomialTerm(A, B, m)(0):R) by linarith97    rw shiftSum98    ring99100-- The binomial theorem: (A + B)ⁿ = ∑ₖ₌₀ⁿ C(n, k) Aᵏ Bⁿ⁻ᵏ, the sum running101-- over the n + 1 indices below n + 1.102theorem binomial.theorem (A B : Real) (n : Nat)103  shows (A + B) ^ n = ∑ i < n + 1, binomialTerm(A, B, n)(i)104proof105  have bound : n + 1 = succ(n) := add.right_one at n106  rw bound107  exact binomial.expansion at A, B, n with *108