[?] Obtain a proof of this result?

Questions
1

I’m seeking a proof that the sum shown below evaluates to shown result.

In[1]:= factorialPowerOneHalf[k_] := FactorialPower[1/2, k]

In[2]:= f[n_, k_] := Binomial[n, k]*factorialPowerOneHalf[k]*factorialPowerOneHalf[n - k]

In[3]:= Sum[f[n, k], {k, 0, n}]

Out[3]= FactorialPower[1, n]

I’m confident Mathematica is correct, but I’m interested to see the proof. Is there any way Mathematica can help me find the proof?

2

What you have is a special case of something analogous to the binomial expansion but with factorial powers rather than integer powers.

(a+b)_n = \sum_{j=0}^n \binom{n}{j} (a)_j (b)_{n-j}

with a=b={1\over 2} .

See Wiki Falling and rising factorials.

3

Thank you. I recognize the relation of my problem to the Binomial Expansion:

In[18]:= FullSimplify[
 Binomial[n, k] FactorialPower[1/2, k] FactorialPower[1/2, n - k] == 
  n!*Binomial[1/2, k]*Binomial[1/2, n - k]]

Out[18]= True

and that equation I can prove easily.

Curiously—but not essentially to my line of inquiry—Mathematica doesn’t solve the sum when I express it more like the Binomial Expansion:

In[13]:= FullSimplify[n!*Binomial[1/2, k]*Binomial[1/2, n - k]]

Out[13]= Binomial[1/2, k] Binomial[1/2, -k + n] n!

or more simply:

In[13]:= FullSimplify[Binomial[1/2, k]*Binomial[1/2, n - k]]

Out[13]= Binomial[1/2, k] Binomial[1/2, -k + n] n!

I could solve my problem (finding a proof as described in my initial post) by working through an analysis textbook; but what I’m really after is a proof that doesn’t rely on derivatives. A proof modeled after (e.g.) Rudin would make heavy use of derivatives and Taylor’s Theorem, which I’m trying to avoid.

I was hoping Mathematica could help me find such a proof, but my hope is a long shot, as Mathematica seems to excel at calculating true answers, but less so at providing proofs.

4

Because your example was a special case of the more general expansion, it wasn’t clear that you were aware of that identity. In the link I used the “Sheffer Sequence” is referenced and a search on that term might find some established proofs. Wolfram MathWorld gives a blurb on the Sheffer Sequence.

I’m not sure what you would expect from Mathematica. If FullSimplify ended up with FactorialPower[1, n], how would the “black box” function FullSimplify be considered a proof?

5

Thanks for the additional references. “Sheffer Sequence” is something I hadn’t heard of; I’ll research it. I’m not any expert in the Binomial Expansion; I’ve just seen it asserted, and I’ve browsed some analysis textbooks for their line of proof.

Software could show proofs. I wasn’t expecting Mathematica to be that software; I was just asking if it was.

6

P.S. To clarify why I’m not satisfied with Rudin’s proof (though I accept its validity):

The problem I’ve stated at the top entails only a finite sum of rational numbers. No infinite sums. No irrational numbers. No need to define the real numbers in order to state the problem. Yet Rudin’s proof depends on the theory of real numbers. I’m hoping to find a way to a proof that doesn’t depend on the theory of real numbers.

7

A proof by induction of Jim’s identity is probably what you want. Multiply by both sides by {((a - k), (b - (n - k)))} and use the fact that

FactorialPower[a, k + 1] == (a - k) FactorialPower[a, k]

etc. to get terms like

Binomial[n, k] FactorialPower[a, k + 1] FactorialPower[b, -k + n] 
Binomial[n, k] FactorialPower[a, k] FactorialPower[b, -k + n + 1]

Shift the index of the first type to get terms like

Binomial[n, k - 1] FactorialPower[a, k] FactorialPower[b, -k + n + 1]

Then use the binomial identity for Binomial[n, k - 1] Binomial[n, k] to write the LHS as a sum up to n + 1.

8

Thanks immensely.