Grace/Cumulus/Real/BinomialTerms.g17

Open in Workbench Download source

Imports

Power · Natural · NumberTheory.BinomialVanishing

Declarations

Source

1-- The terms of the binomial expansion, choose(n, k)·A^k·B^(n−k), and the2-- Pascal recurrence they satisfy from one row to the next3-- 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.BinomialTerms9import Power10import Natural11import NumberTheory.BinomialVanishing1213defgraph binomialTerm (A B : Real) (n : Nat) (k ∈ ℕ) : ℝ := (realNat(n choose k):R) * (realPow(A, k) * realPow(B, sub(n, k)))14proof15  have kNat : Nat(k) by typecheck16  have coefficientNat : Nat(n choose k) by typecheck17  have coefficient := realNat.real at n choose k18  have powerA := realPow.real at A, k19  have subNat := sub.closed at n, k20  have powerB := realPow.real at B, sub(n, k)21  have product := realMulValue.real at A ^ k, B ^ sub(n, k)22  exact realMulValue.real at realNat(n choose k), A ^ k * B ^ sub(n, k)2324theorem binomialTerm.real (A B : Real) (n k : Nat)25  shows binomialTerm(A, B, n)(k) ∈ ℝ26proof27  have function := binomialTerm.function at A, B, n28  have kIn := nat.omega.forward at k with *29  exact FunctionBetween.apply_closed with function, kIn3031theorem binomialTerm.zero_index (A B : Real) (n : Nat)32  shows binomialTerm(A, B, n)(0) = B ^ n33proof34  have value := binomialTerm.value at A, B, n, (0:N)35  rw [value, choose.zero_right, realNat.one, realPow.zero, sub.zero_right]36  ring3738theorem binomialTerm.succ_zero (A B : Real) (n : Nat)39  shows binomialTerm(A, B, succ(n))(0) = B * binomialTerm(A, B, n)(0)40proof41  have first := binomialTerm.zero_index at A, B, succ(n)42  have second := binomialTerm.zero_index at A, B, n43  rw [first, second]44  exact realPow.succ4546theorem binomialTerm.beyond (A B : Real) (n k : Nat)47  requires le : n ≤ k48  shows binomialTerm(A, B, n)(succ(k)) = (0:R)49proof50  have value := binomialTerm.value at A, B, n, succ(k)51  have vanish := choose.vanishes with le52  rw [value, vanish, realNat.zero]53  exact realMulValue.zero_left5455-- Pascal's rule, term by term.56theorem binomialTerm.pascal (A B : Real) (n k : Nat)57  shows binomialTerm(A, B, succ(n))(succ(k)) = A * binomialTerm(A, B, n)(k) + B * binomialTerm(A, B, n)(succ(k))58proof59  have top := binomialTerm.value at A, B, succ(n), succ(k)60  have left := binomialTerm.value at A, B, n, k61  have right := binomialTerm.value at A, B, n, succ(k)62  have powerASucc := realPow.succ at A, k63  have coefficients := realNat.add at n choose k, n choose succ(k)64  rw [top, left, right, choose.succ_succ, coefficients, sub.succ_succ, powerASucc]65  have alternatives : k < n ∨ ¬k < n by tauto66  cases alternatives with below | notBelow67  . have nNat : Nat(n) by typecheck68    have peel := sub.succ_of_Less at k69    have step := peel with n, below70    have powerBStep := realPow.succ at B, sub(n, succ(k))71    rw [step, powerBStep]72    ring73  . have le := LessEqual.of_not_Less with notBelow74    have vanish := choose.vanishes with le75    rw [vanish, realNat.zero]76    ring77