-- The terms of the binomial expansion, choose(n, k)·A^k·B^(n−k), and the
-- Pascal recurrence they satisfy from one row to the next
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Real.BinomialTerms
import Power
import Natural
import NumberTheory.BinomialVanishing

defgraph binomialTerm (A B : Real) (n : Nat) (k ∈ ℕ) : ℝ := (realNat(n choose k):R) * (realPow(A, k) * realPow(B, sub(n, k)))
proof
  have kNat : Nat(k) by typecheck
  have coefficientNat : Nat(n choose k) by typecheck
  have coefficient := realNat.real at n choose k
  have powerA := realPow.real at A, k
  have subNat := sub.closed at n, k
  have powerB := realPow.real at B, sub(n, k)
  have product := realMulValue.real at A ^ k, B ^ sub(n, k)
  exact realMulValue.real at realNat(n choose k), A ^ k * B ^ sub(n, k)

theorem binomialTerm.real (A B : Real) (n k : Nat)
  shows binomialTerm(A, B, n)(k) ∈ ℝ
proof
  have function := binomialTerm.function at A, B, n
  have kIn := nat.omega.forward at k with *
  exact FunctionBetween.apply_closed with function, kIn

theorem binomialTerm.zero_index (A B : Real) (n : Nat)
  shows binomialTerm(A, B, n)(0) = B ^ n
proof
  have value := binomialTerm.value at A, B, n, (0:N)
  rw [value, choose.zero_right, realNat.one, realPow.zero, sub.zero_right]
  ring

theorem binomialTerm.succ_zero (A B : Real) (n : Nat)
  shows binomialTerm(A, B, succ(n))(0) = B * binomialTerm(A, B, n)(0)
proof
  have first := binomialTerm.zero_index at A, B, succ(n)
  have second := binomialTerm.zero_index at A, B, n
  rw [first, second]
  exact realPow.succ

theorem binomialTerm.beyond (A B : Real) (n k : Nat)
  requires le : n ≤ k
  shows binomialTerm(A, B, n)(succ(k)) = (0:R)
proof
  have value := binomialTerm.value at A, B, n, succ(k)
  have vanish := choose.vanishes with le
  rw [value, vanish, realNat.zero]
  exact realMulValue.zero_left

-- Pascal's rule, term by term.
theorem binomialTerm.pascal (A B : Real) (n k : Nat)
  shows binomialTerm(A, B, succ(n))(succ(k)) = A * binomialTerm(A, B, n)(k) + B * binomialTerm(A, B, n)(succ(k))
proof
  have top := binomialTerm.value at A, B, succ(n), succ(k)
  have left := binomialTerm.value at A, B, n, k
  have right := binomialTerm.value at A, B, n, succ(k)
  have powerASucc := realPow.succ at A, k
  have coefficients := realNat.add at n choose k, n choose succ(k)
  rw [top, left, right, choose.succ_succ, coefficients, sub.succ_succ, powerASucc]
  have alternatives : k < n ∨ ¬k < n by tauto
  cases alternatives with below | notBelow
  . have nNat : Nat(n) by typecheck
    have peel := sub.succ_of_Less at k
    have step := peel with n, below
    have powerBStep := realPow.succ at B, sub(n, succ(k))
    rw [step, powerBStep]
    ring
  . have le := LessEqual.of_not_Less with notBelow
    have vanish := choose.vanishes with le
    rw [vanish, realNat.zero]
    ring