Arithmetic/Geometric Mean
-------------------------

------
Summary:
Higher Order
Unusual Induction Scheme
Extra lemmata required
Challenges Rippling

------
Definitions:

< (less) 
-------

nat -> nat -> bool 

(X < 0) = false 
(0 < (s Y)) = true 
((s X) < (s Y)) = (X < Y) 

* (times) 
---------

nat -> nat -> nat

(X * 0) = 0
(X * (s Y)) = ((X * Y) + X)

exp
---

nat -> nat -> nat 

(exp X 0) = 0 
(exp X (s Y)) = ((exp X Y) * X) 

leq 
---

nat -> nat -> bool 

(leq 0 Y) = true
(leq (s X) 0) = false 
(leq (s X) (s Y)) = (leq X Y) 

sum 
---

nat -> nat -> (nat -> nat) -> nat 

(sum X 0 F) = (F 0) 
((s Y) < X) -> (sum X (s Y) F) = 0
(not ((s Y) < X)) -> (sum (s Y) F) = ((F (s Y)) + (sum X Y F))

prod
----

nat -> nat -> (nat -> nat) -> nat 

(prod X 0 F) = (F 0) 
((s Y) < X) -> (prod X (s Y) F) = (s 0)
(not ((s Y) < X)) -> (prod X (s Y) F) = ((F (s Y)) * (prod X Y F))

root
----

------
Theorem

forall n:nat,a:(nat -> nat).  
	(leq (prod n a) (exp (div (sum n a) n) n))

--------
Comments:

This is essentially the same theorem as HOL001a but reformulated and
using a different step case in a way that makes the proof easier.
Reformulation is attributed to Shankar.

There are at least two possible induction schemes that can be used for
this proof.  One with the step cases (P(n) -> P(2n)) and (P(n) ->
P(2n - 1)) and (forall m. (m < n) -> P(m)) -> P(n)) with a casesplit
on odd and even numbers in the step case.  The discussion 
here is based upon a proof using the first of these.

It needs several lemmata (some given below)

(sum (2 * N) F) = (sum N F) + (sum N (lambda i. (F (N + i))))
(prod (2 * N) F) = (prod N F) * (prod N (lambda i. (F (N + i))))
(div X (Y * Z)) = (div (div X Z) Y)
(div (X + Y) Z) = (div X Z) + (div Y Z)
(root (X * Y) Z) = (root X (root Y Z))
(root X (Y * Z)) = (root X Y) * (root X Z)
((exp X N) = Y) = (X = (root N Y))

(root N X) is the nth root of X.  The inverse of exp.

Even with these lemmata the rewriting involved presents several
challenges to rippling (e.g. the "odd" step case does not appear to
make use of the annotations) - Louise Dennis

------
Source:

Alan Bundy
Edinburgh MRG Group Blue Book Note 951