Theory CauchysMeanTheorem
chapter ‹Cauchy's Mean Theorem›
theory CauchysMeanTheorem
imports Complex_Main
begin
section ‹Abstract›
text ‹The following document presents a proof of Cauchy's Mean
theorem formalised in the Isabelle/Isar theorem proving system.
{\em Theorem}: For any collection of positive real numbers the
geometric mean is always less than or equal to the arithmetic mean. In
mathematical terms: $$\sqrt[n]{x_1 x_2 \dots x_n} \leq \frac{x_1 +
\dots + x_n}{n}$$ We will use the term {\em mean} to denote the
arithmetic mean and {\em gmean} to denote the geometric mean.
{\em Informal Proof}:
This proof is based on the proof presented in [1]. First we need an
auxiliary lemma (the proof of which is presented formally below) that
states:
Given two pairs of numbers of equal sum, the pair with the greater
product is the pair with the least difference. Using this lemma we now
present the proof -
Given any collection $C$ of positive numbers with mean $M$ and product
$P$ and with some element not equal to M we can choose two elements
from the collection, $a$ and $b$ where $a>M$ and $b<M$. Remove these
elements from the collection and replace them with two new elements,
$a'$ and $b'$ such that $a' = M$ and $a' + b' = a + b$. This new
collection $C'$ now has a greater product $P'$ but equal mean with
respect to $C$. We can continue in this fashion until we have a
collection $C_n$ such that $P_n > P$ and $M_n = M$, but $C_n$ has all
its elements equal to $M$ and thus $P_n = M^n$. Using the definition
of geometric and arithmetic means above we can see that for any
collection of positive elements $E$ it is always true that gmean E
$\leq$ mean E. QED.
[1] Dorrie, H. "100 Great Problems of Elementary Mathematics." 1965, Dover.
›
section ‹Formal proof›
subsection ‹Collection sum and product›
text ‹The finite collections of numbers will be modelled as
lists. We then define sum and product operations over these lists.›
subsubsection ‹Sum and product definitions›
notation (input) sum_list ("∑:_" [999] 998)
notation (input) prod_list ("∏:_" [999] 998)
subsubsection ‹Properties of sum and product›
text ‹We now present some useful properties of sum and product over
collections.›
text ‹These lemmas just state that if all the elements in a
collection $C$ are less (greater than) than some value $m$, then the
sum will less than (greater than) $m*length(C)$.›
lemma sum_list_mono_lt [rule_format]:
fixes xs::"real list"
shows "xs ≠ [] ∧ (∀x∈ set xs. x < m)
⟶ ((∑:xs) < (m*(real (length xs))))"
proof (induct xs)
case Nil show ?case by simp
next
case (Cons y ys)
{
assume ant: "y#ys ≠ [] ∧ (∀x∈set(y#ys). x < m)"
hence ylm: "y < m" by simp
have "∑:(y#ys) < m * real (length (y#ys))"
proof cases
assume "ys ≠ []"
moreover with ant have "∀x∈set ys. x < m" by simp
moreover with calculation Cons have "∑:ys < m*real (length ys)" by simp
hence "∑:ys + y < m*real(length ys) + y" by simp
with ylm have "∑:(y#ys) < m*(real(length ys) + 1)" by(simp add:field_simps)
then have "∑:(y#ys) < m*(real(length ys + 1))"
by (simp add: algebra_simps)
hence "∑:(y#ys) < m*(real (length(y#ys)))" by simp
thus ?thesis .
next
assume "¬ (ys ≠ [])"
hence "ys = []" by simp
with ylm show ?thesis by simp
qed
}
thus ?case by simp
qed
lemma sum_list_mono_gt [rule_format]:
fixes xs::"real list"
shows "xs ≠ [] ∧ (∀x∈set xs. x > m)
⟶ ((∑:xs) > (m*(real (length xs))))"
txt ‹proof omitted›
proof (induct xs)
case Nil show ?case by simp
next
case (Cons y ys)
{
assume ant: "y#ys ≠ [] ∧ (∀x∈set(y#ys). x > m)"
hence ylm: "y > m" by simp
have "∑:(y#ys) > m * real (length (y#ys))"
proof cases
assume "ys ≠ []"
moreover with ant have "∀x∈set ys. x > m" by simp
moreover with calculation Cons have "∑:ys > m*real (length ys)" by simp
hence "∑:ys + y > m*real(length ys) + y" by simp
with ylm have "∑:(y#ys) > m*(real(length ys) + 1)" by(simp add:field_simps)
then have "∑:(y#ys) > m*(real(length ys + 1))"
by (simp add: algebra_simps)
hence "∑:(y#ys) > m*(real (length(y#ys)))" by simp
thus ?thesis .
next
assume "¬ (ys ≠ [])"
hence "ys = []" by simp
with ylm show ?thesis by simp
qed
}
thus ?case by simp
qed
text ‹If $a$ is in $C$ then the sum of the collection $D$ where $D$
is $C$ with $a$ removed is the sum of $C$ minus $a$.›
lemma sum_list_rmv1:
"a ∈ set xs ⟹ ∑:(remove1 a xs) = ∑:xs - (a :: 'a :: ab_group_add)"
by (induct xs) auto
text ‹A handy addition and division distribution law over collection
sums.›
lemma list_sum_distrib_aux:
shows "(∑:xs/(n :: 'a :: archimedean_field) + ∑:xs) = (1 + (1/n)) * ∑:xs"
proof (induct xs)
case Nil show ?case by simp
next
case (Cons x xs)
show ?case
proof -
have
"∑:(x#xs)/n = x/n + ∑:xs/n"
by (simp add: add_divide_distrib)
also with Cons have
"… = x/n + (1+1/n)*∑:xs - ∑:xs"
by simp
finally have
"∑:(x#xs) / n + ∑:(x#xs) = x/n + (1+1/n)*∑:xs - ∑:xs + ∑:(x#xs)"
by simp
also have
"… = x/n + (1+(1/n)- 1)*∑:xs + ∑:(x#xs)"
by (subst mult_1_left [symmetric, of "∑:xs"]) (simp add: field_simps)
also have
"… = x/n + (1/n)*∑:xs + ∑:(x#xs)"
by simp
also have
"… = (1/n)*∑:(x#xs) + 1*∑:(x#xs)" by(simp add: divide_simps)
finally show ?thesis by (simp add: field_simps)
qed
qed
lemma remove1_retains_prod:
fixes a and xs::"'a :: comm_ring_1 list"
shows "a : set xs ⟶ ∏:xs = ∏:(remove1 a xs) * a"
(is "?P xs")
proof (induct xs)
case Nil
show ?case by simp
next
case (Cons aa list)
assume plist: "?P list"
show "?P (aa#list)"
proof
assume aml: "a : set(aa#list)"
show "∏:(aa # list) = ∏:remove1 a (aa # list) * a"
proof (cases)
assume aeq: "a = aa"
hence
"remove1 a (aa#list) = list"
by simp
hence
"∏:(remove1 a (aa#list)) = ∏:list"
by simp
moreover with aeq have
"∏:(aa#list) = ∏:list * a"
by simp
ultimately show
"∏:(aa#list) = ∏:remove1 a (aa # list) * a"
by simp
next
assume naeq: "a ≠ aa"
with aml have aml2: "a : set list" by simp
from naeq have
"remove1 a (aa#list) = aa#(remove1 a list)"
by simp
moreover hence
"∏:(remove1 a (aa#list)) = aa * ∏:(remove1 a list)"
by simp
moreover from aml2 plist have
"∏:list = ∏:(remove1 a list) * a"
by simp
ultimately show
"∏:(aa#list) = ∏:remove1 a (aa # list) * a"
by simp
qed
qed
qed
text ‹The final lemma of this section states that if all elements
are positive and non-zero then the product of these elements is also
positive and non-zero.›
lemma el_gt0_imp_prod_gt0 [rule_format]:
fixes xs::"'a :: archimedean_field list"
shows "∀y. y : set xs ⟶ y > 0 ⟹ ∏:xs > 0"
proof (induct xs)
case Nil show ?case by simp
next
case (Cons a xs)
have exp: "∏:(a#xs) = ∏:xs * a" by simp
with Cons have "a > 0" by simp
with exp Cons show ?case by simp
qed
subsection ‹Auxiliary lemma›
text ‹This section presents a proof of the auxiliary lemma required
for this theorem.›
lemma prod_exp:
fixes x::real
shows "4*(x*y) = (x+y)^2 - (x-y)^2"
by (simp add: power2_diff power2_sum)
lemma abs_less_imp_sq_less [rule_format]:
fixes x::real and y::real and z::real and w::real
assumes diff: "abs (x-y) < abs (z-w)"
shows "(x-y)^2 < (z-w)^2"
proof cases
assume "x=y"
hence "abs (x-y) = 0" by simp
moreover with diff have "abs(z-w) > 0" by simp
hence "(z-w)^2 > 0" by simp
ultimately show ?thesis by auto
next
assume "x≠y"
hence "abs (x - y) > 0" by simp
with diff have "(abs (x-y))^2 < (abs (z-w))^2"
by - (drule power_strict_mono [where a="abs (x-y)" and n=2 and b="abs (z-w)"], auto)
thus ?thesis by simp
qed
text ‹The required lemma (phrased slightly differently than in the
informal proof.) Here we show that for any two pairs of numbers with
equal sums the pair with the least difference has the greater
product.›
lemma le_diff_imp_gt_prod [rule_format]:
fixes x::real and y::real and z::real and w::real
assumes diff: "abs (x-y) < abs (z-w)" and sum: "x+y = z+w"
shows "x*y > z*w"
proof -
from sum have "(x+y)^2 = (z+w)^2" by simp
moreover from diff have "(x-y)^2 < (z-w)^2" by (rule abs_less_imp_sq_less)
ultimately have "(x+y)^2 - (x-y)^2 > (z+w)^2 - (z-w)^2" by auto
thus "x*y > z*w" by (simp only: prod_exp [symmetric])
qed
subsection ‹Mean and GMean›
text ‹Now we introduce definitions and properties of arithmetic and
geometric means over collections of real numbers.›
subsubsection ‹Definitions›
text ‹{\em Arithmetic mean}›
definition
mean :: "(real list)⇒real" where
"mean s = (∑:s / real (length s))"
text ‹{\em Geometric mean}›
definition
gmean :: "(real list)⇒real" where
"gmean s = root (length s) (∏:s)"
subsubsection ‹Properties›
text ‹Here we present some trivial properties of {\em mean} and {\em gmean}.›
lemma list_sum_mean:
fixes xs::"real list"
shows "∑:xs = ((mean xs) * (real (length xs)))"
apply (induct_tac xs)
apply simp
apply clarsimp
apply (unfold mean_def)
apply clarsimp
done
lemma list_mean_eq_iff:
fixes one::"real list" and two::"real list"
assumes
se: "( ∑:one = ∑:two )" and
le: "(length one = length two)"
shows "(mean one = mean two)"
proof -
from se le have
"(∑:one / real (length one)) = (∑:two / real (length two))"
by auto
thus ?thesis unfolding mean_def .
qed
lemma list_gmean_gt_iff:
fixes one::"real list" and two::"real list"
assumes
gz1: "∏:one > 0" and gz2: "∏:two > 0" and
ne1: "one ≠ []" and ne2: "two ≠ []" and
pe: "(∏:one > ∏:two)" and
le: "(length one = length two)"
shows "(gmean one > gmean two)"
unfolding gmean_def
using le ne2 pe by simp
text ‹This slightly more complicated lemma shows that for every non-empty collection with mean $M$, adding another element $a$ where $a=M$ results in a new list with the same mean $M$.›
lemma list_mean_cons [rule_format]:
fixes xs::"real list"
shows "xs ≠ [] ⟶ mean ((mean xs)#xs) = mean xs"
proof
assume lne: "xs ≠ []"
obtain len where ld: "len = real (length xs)" by simp
with lne have lgt0: "len > 0" by simp
hence lnez: "len ≠ 0" by simp
from lgt0 have l1nez: "len + 1 ≠ 0" by simp
from ld have mean: "mean xs = ∑:xs / len" unfolding mean_def by simp
with ld of_nat_add of_int_1 mean_def
have "mean ((mean xs)#xs) = (∑:xs/len + ∑:xs) / (1+len)"
by simp
also from list_sum_distrib_aux[of xs] have
"… = (1 + (1/len))*∑:xs / (1+len)" by simp
also with lnez have
"… = (len + 1)*∑:xs / (len * (1+len))"
apply -
apply (drule mult_divide_mult_cancel_left
[symmetric, where c="len" and a="(1 + 1 / len) * ∑:xs" and b="1+len"])
apply (clarsimp simp:field_simps)
done
also from l1nez have "… = ∑:xs / len"
apply (subst mult.commute [where a="len"])
apply (drule mult_divide_mult_cancel_left
[where c="len+1" and a="∑:xs" and b="len"])
by (simp add: ac_simps ac_simps)
finally show "mean ((mean xs)#xs) = mean xs" by (simp add: mean)
qed
text ‹For a non-empty collection with positive mean, if we add a positive number to the collection then the mean remains positive.›
lemma mean_gt_0 [rule_format]:
"xs≠[] ∧ 0 < x ∧ 0 < (mean xs) ⟶ 0 < (mean (x#xs))"
proof
assume a: "xs ≠ [] ∧ 0 < x ∧ 0 < mean xs"
hence xgt0: "0 < x" and mgt0: "0 < mean xs" by auto
from a have lxsgt0: "length xs ≠ 0" by simp
from mgt0 have xsgt0: "0 < ∑:xs"
proof -
have "mean xs = ∑:xs / real (length xs)" unfolding mean_def by simp
hence "∑:xs = mean xs * real (length xs)" by simp
moreover from lxsgt0 have "real (length xs) > 0" by simp
moreover with calculation lxsgt0 mgt0 show ?thesis by auto
qed
with xgt0 have "∑:(x#xs) > 0" by simp
thus "0 < (mean (x#xs))"
proof -
assume "0 < ∑:(x#xs)"
moreover have "real (length (x#xs)) > 0" by simp
ultimately show ?thesis unfolding mean_def by simp
qed
qed
subsection ‹‹list_neq›, ‹list_eq››
text ‹This section presents a useful formalisation of the act of removing all the elements from a collection that are equal (not equal) to a particular value. We use this to extract all the non-mean elements from a collection as is required by the proof.›
subsubsection ‹Definitions›
text ‹‹list_neq› and ‹list_eq› just extract elements from a collection that are not equal (or equal) to some value.›
abbreviation
list_neq :: "('a list) ⇒ 'a ⇒ ('a list)" where
"list_neq xs el == filter (λx. x≠el) xs"
abbreviation
list_eq :: "('a list) ⇒ 'a ⇒ ('a list)" where
"list_eq xs el == filter (λx. x=el) xs"
subsubsection ‹Properties›
text ‹This lemma just proves a required fact about ‹list_neq›, {\em remove1} and {\em length}.›
lemma list_neq_remove1 [rule_format]:
shows "a≠m ∧ a : set xs
⟶ length (list_neq (remove1 a xs) m) < length (list_neq xs m)"
(is "?A xs ⟶ ?B xs" is "?P xs")
proof (induct xs)
case Nil show ?case by simp
next
case (Cons x xs)
note ‹?P xs›
{
assume a: "?A (x#xs)"
hence
a_ne_m: "a≠m" and
a_mem_x_xs: "a : set(x#xs)"
by auto
have b: "?B (x#xs)"
proof cases
assume "xs = []"
with a_ne_m a_mem_x_xs show ?thesis
apply (cases "x=a")
by auto
next
assume xs_ne: "xs ≠ []"
with a_ne_m a_mem_x_xs show ?thesis
proof cases
assume "a=x" with a_ne_m show ?thesis by simp
next
assume a_ne_x: "a≠x"
with a_mem_x_xs have a_mem_xs: "a : set xs" by simp
with xs_ne a_ne_m Cons have
rel: "length (list_neq (remove1 a xs) m) < length (list_neq xs m)"
by simp
show ?thesis
proof cases
assume x_e_m: "x=m"
with Cons xs_ne a_ne_m a_mem_xs show ?thesis by simp
next
assume x_ne_m: "x≠m"
from a_ne_x have
"remove1 a (x#xs) = x#(remove1 a xs)"
by simp
hence
"length (list_neq (remove1 a (x#xs)) m) =
length (list_neq (x#(remove1 a xs)) m)"
by simp
also with x_ne_m have
"… = 1 + length (list_neq (remove1 a xs) m)"
by simp
finally have
"length (list_neq (remove1 a (x#xs)) m) =
1 + length (list_neq (remove1 a xs) m)"
by simp
moreover with x_ne_m a_ne_x have
"length (list_neq (x#xs) m) =
1 + length (list_neq xs m)"
by simp
moreover with rel show ?thesis by simp
qed
qed
qed
}
thus "?P (x#xs)" by simp
qed
text ‹We now prove some facts about ‹list_eq›, ‹list_neq›, length, sum and product.›
lemma list_eq_sum [simp]:
fixes xs::"real list"
shows "∑:(list_eq xs m) = (m * (real (length (list_eq xs m))))"
apply (induct_tac xs)
apply simp
apply (simp add:field_simps)
done
lemma list_eq_prod [simp]:
fixes xs::"real list"
shows "∏:(list_eq xs m) = (m ^ (length (list_eq xs m)))"
apply (induct_tac xs)
apply simp
apply clarsimp
done
lemma sum_list_split:
fixes xs::"real list"
shows "∑:xs = (∑:(list_neq xs m) + ∑:(list_eq xs m))"
apply (induct xs)
apply simp
apply clarsimp
done
lemma prod_list_split:
fixes xs::"real list"
shows "∏:xs = (∏:(list_neq xs m) * ∏:(list_eq xs m))"
apply (induct xs)
apply simp
apply clarsimp
done
lemma sum_list_length_split:
fixes xs::"real list"
shows "length xs = length (list_neq xs m) + length (list_eq xs m)"
apply (induct xs)
apply simp+
done
subsection ‹Element selection›
text ‹We now show that given after extracting all the elements not equal to the mean there exists one that is greater then (or less than) the mean.›
lemma pick_one_gt:
fixes xs::"real list" and m::real
defines m: "m ≡ (mean xs)" and neq: "noteq ≡ list_neq xs m"
assumes asum: "noteq≠[]"
shows "∃e. e : set noteq ∧ e > m"
proof (rule ccontr)
let ?m = "(mean xs)"
let ?neq = "list_neq xs ?m"
let ?eq = "list_eq xs ?m"
from list_eq_sum have "(∑:?eq) = ?m * (real (length ?eq))" by simp
from asum have neq_ne: " ?neq ≠ []" unfolding m neq .
assume not_el: "¬(∃e. e : set noteq ∧ m < e)"
hence not_el_exp: "¬(∃e. e : set ?neq ∧ ?m < e)" unfolding m neq .
hence "∀e. ¬(e : set ?neq) ∨ ¬(e > ?m)" by simp
hence "∀e. e : set ?neq ⟶ ¬(e > ?m)" by blast
hence "∀e. e : set ?neq ⟶ e ≤ ?m" by (simp add: linorder_not_less)
hence "∀e. e : set ?neq ⟶ e < ?m" by (simp add:order_le_less)
with assms sum_list_mono_lt have "(∑:?neq) < ?m * (real (length ?neq))" by blast
hence
"(∑:?neq) + (∑:?eq) < ?m * (real (length ?neq)) + (∑:?eq)" by simp
also have
"… = (?m * ((real (length ?neq) + (real (length ?eq)))))"
by (simp add:field_simps)
also have
"… = (?m * (real (length xs)))"
apply (subst of_nat_add [symmetric])
by (simp add: sum_list_length_split [symmetric])
also have
"… = ∑:xs"
by (simp add: list_sum_mean [symmetric])
also from not_el calculation show False by (simp only: sum_list_split [symmetric])
qed
lemma pick_one_lt:
fixes xs::"real list" and m::real
defines m: "m ≡ (mean xs)" and neq: "noteq ≡ list_neq xs m"
assumes asum: "noteq≠[]"
shows "∃e. e : set noteq ∧ e < m"
proof (rule ccontr)
let ?m = "(mean xs)"
let ?neq = "list_neq xs ?m"
let ?eq = "list_eq xs ?m"
from list_eq_sum have "(∑:?eq) = ?m * (real (length ?eq))" by simp
from asum have neq_ne: " ?neq ≠ []" unfolding m neq .
assume not_el: "¬(∃e. e : set noteq ∧ m > e)"
hence not_el_exp: "¬(∃e. e : set ?neq ∧ ?m > e)" unfolding m neq .
hence "∀e. ¬(e : set ?neq) ∨ ¬(e < ?m)" by simp
hence "∀e. e : set ?neq ⟶ ¬(e < ?m)" by blast
hence "∀e. e : set ?neq ⟶ e ≥ ?m" by (simp add: linorder_not_less)
hence "∀e. e : set ?neq ⟶ e > ?m" by (auto simp: order_le_less)
with assms sum_list_mono_gt have "(∑:?neq) > ?m * (real (length ?neq))" by blast
hence
"(∑:?neq) + (∑:?eq) > ?m * (real (length ?neq)) + (∑:?eq)" by simp
also have
"(?m * (real (length ?neq)) + (∑:?eq)) =
(?m * (real (length ?neq)) + (?m * (real (length ?eq))))"
by simp
also have
"… = (?m * ((real (length ?neq) + (real (length ?eq)))))"
by (simp add:field_simps)
also have
"… = (?m * (real (length xs)))"
apply (subst of_nat_add [symmetric])
by (simp add: sum_list_length_split [symmetric])
also have
"… = ∑:xs"
by (simp add: list_sum_mean [symmetric])
also from not_el calculation show False by (simp only: sum_list_split [symmetric])
qed
subsection ‹Abstract properties›
text ‹In order to maintain some comprehension of the following proofs we now introduce some properties of collections.›
subsubsection ‹Definitions›
text ‹{\em het}: The heterogeneity of a collection is the number of elements not equal to its mean. A heterogeneity of zero implies the all the elements in the collection are the same (i.e. homogeneous).›
definition
het :: "real list ⇒ nat" where
"het l = length (list_neq l (mean l))"
lemma het_gt_0_imp_noteq_ne: "het l > 0 ⟹ list_neq l (mean l) ≠ []"
unfolding het_def by simp
lemma het_gt_0I: assumes a: "a ∈ set xs" and b: "b ∈ set xs" and neq: "a ≠ b"
shows "het xs > 0"
proof (rule ccontr)
assume "¬ ?thesis"
hence "het xs = 0" by auto
from this[unfolded het_def] have "list_neq xs (mean xs) = []" by simp
from arg_cong[OF this, of set] have mean: "⋀ x. x ∈ set xs ⟹ x = mean xs" by auto
from mean[OF a] mean[OF b] neq show False by auto
qed
text ‹‹γ-eq›: Two lists are $\gamma$-equivalent if and only
if they both have the same number of elements and the same arithmetic
means.›
definition
γ_eq :: "((real list)*(real list)) ⇒ bool" where
"γ_eq a ⟷ mean (fst a) = mean (snd a) ∧ length (fst a) = length (snd a)"
text ‹‹γ_eq› is transitive and symmetric.›
lemma γ_eq_sym: "γ_eq (a,b) = γ_eq (b,a)"
unfolding γ_eq_def by auto
lemma γ_eq_trans:
"γ_eq (x,y) ⟹ γ_eq (y,z) ⟹ γ_eq (x,z)"
unfolding γ_eq_def by simp
text ‹{\em pos}: A list is positive if all its elements are greater than 0.›
definition
pos :: "real list ⇒ bool" where
"pos l ⟷ (if l=[] then False else ∀e. e : set l ⟶ e > 0)"
lemma pos_empty [simp]: "pos [] = False" unfolding pos_def by simp
lemma pos_single [simp]: "pos [x] = (x > 0)" unfolding pos_def by simp
lemma pos_imp_ne: "pos xs ⟹ xs≠[]" unfolding pos_def by auto
lemma pos_cons [simp]:
"xs ≠ [] ⟶ pos (x#xs) =
(if (x>0) then pos xs else False)"
(is "?P x xs" is "?A xs ⟶ ?S x xs")
proof (simp add: if_split, rule impI)
assume xsne: "xs ≠ []"
hence pxs_simp:
"pos xs = (∀e. e : set xs ⟶ e > 0)"
unfolding pos_def by simp
show
"(0 < x ⟶ pos (x # xs) = pos xs) ∧
(¬ 0 < x ⟶ ¬ pos (x # xs))"
proof
{
assume xgt0: "0 < x"
{
assume pxs: "pos xs"
with pxs_simp have "∀e. e : set xs ⟶ e > 0" by simp
with xgt0 have "∀e. e : set (x#xs) ⟶ e > 0" by simp
hence "pos (x#xs)" unfolding pos_def by simp
}
moreover
{
assume pxxs: "pos (x#xs)"
hence "∀e. e : set (x#xs) ⟶ e > 0" unfolding pos_def by simp
hence "∀e. e : set xs ⟶ e > 0" by simp
with xsne have "pos xs" unfolding pos_def by simp
}
ultimately have "pos (x # xs) = pos xs"
apply -
apply (rule iffI)
apply auto
done
}
thus "0 < x ⟶ pos (x # xs) = pos xs" by simp
next
{
assume xngt0: "¬ (0<x)"
{
assume pxs: "pos xs"
with pxs_simp have "∀e. e : set xs ⟶ e > 0" by simp
with xngt0 have "¬ (∀e. e : set (x#xs) ⟶ e > 0)" by auto
hence "¬ (pos (x#xs))" unfolding pos_def by simp
}
moreover
{
assume pxxs: "¬pos xs"
with xsne have "¬ (∀e. e : set xs ⟶ e > 0)" unfolding pos_def by simp
hence "¬ (∀e. e : set (x#xs) ⟶ e > 0)" by auto
hence "¬ (pos (x#xs))" unfolding pos_def by simp
}
ultimately have "¬ pos (x#xs)" by auto
}
thus "¬ 0 < x ⟶ ¬ pos (x # xs)" by simp
qed
qed
subsubsection ‹Properties›
text ‹Here we prove some non-trivial properties of the abstract properties.›
text ‹Two lemmas regarding {\em pos}. The first states the removing
an element from a positive collection (of more than 1 element) results
in a positive collection. The second asserts that the mean of a
positive collection is positive.›
lemma pos_imp_rmv_pos:
assumes "(remove1 a xs)≠[]" "pos xs" shows "pos (remove1 a xs)"
proof -
from assms have pl: "pos xs" and rmvne: "(remove1 a xs)≠[]" by auto
from pl have "xs ≠ []" by (rule pos_imp_ne)
with pl pos_def have "∀x. x : set xs ⟶ x > 0" by simp
hence "∀x. x : set (remove1 a xs) ⟶ x > 0"
using set_remove1_subset[of _ xs] by(blast)
with rmvne show "pos (remove1 a xs)" unfolding pos_def by simp
qed
lemma pos_mean: "pos xs ⟹ mean xs > 0"
proof (induct xs)
case Nil thus ?case by(simp add: pos_def)
next
case (Cons x xs)
show ?case
proof cases
assume xse: "xs = []"
hence "pos (x#xs) = (x > 0)" by simp
with Cons(2) have "x>0" by(simp)
with xse have "0 < mean (x#xs)" by(auto simp:mean_def)
thus ?thesis by simp
next
assume xsne: "xs ≠ []"
show ?thesis
proof cases
assume pxs: "pos xs"
with Cons(1) have z_le_mxs: "0 < mean xs" by(simp)
{
assume ass: "x > 0"
with ass z_le_mxs xsne have "0 < mean (x#xs)"
apply -
apply (rule mean_gt_0)
by simp
}
moreover
{
from xsne pxs have "0 < x"
proof cases
assume "0 < x" thus ?thesis by simp
next
assume "¬(0 < x)"
with xsne pos_cons have "pos (x#xs) = False" by simp
with Cons(2) show ?thesis by simp
qed
}
ultimately have "0 < mean (x#xs)" by simp
thus ?thesis by simp
next
assume npxs: "¬pos xs"
with xsne pos_cons have "pos (x#xs) = False" by simp
thus ?thesis using Cons(2) by simp
qed
qed
qed
text ‹We now show that homogeneity of a non-empty collection $x$
implies that its product is equal to ‹(mean x)^(length x)›.›
lemma prod_list_het0:
shows "x≠[] ∧ het x = 0 ⟹ ∏:x = (mean x) ^ (length x)"
proof -
assume "x≠[] ∧ het x = 0"
hence xne: "x≠[]" and hetx: "het x = 0" by auto
from hetx have lz: "length (list_neq x (mean x)) = 0" unfolding het_def .
hence "∏:(list_neq x (mean x)) = 1" by simp
with prod_list_split have "∏:x = ∏:(list_eq x (mean x))"
apply -
apply (drule meta_spec [of _ x])
apply (drule meta_spec [of _ "mean x"])
by simp
also with list_eq_prod have
"… = (mean x) ^ (length (list_eq x (mean x)))" by simp
also with calculation lz sum_list_length_split have
"∏:x = (mean x) ^ (length x)"
apply -
apply (drule meta_spec [of _ x])
apply (drule meta_spec [of _ "mean x"])
by simp
thus ?thesis by simp
qed
text ‹Furthermore we present an important result - that a
homogeneous collection has equal geometric and arithmetic means.›
lemma het_base:
shows "pos x ∧ het x = 0 ⟹ gmean x = mean x"
proof -
assume ass: "pos x ∧ het x = 0"
hence
xne: "x≠[]" and
hetx: "het x = 0" and
posx: "pos x"
by auto
from posx pos_mean have mxgt0: "mean x > 0" by simp
from xne have lxgt0: "length x > 0" by simp
with ass prod_list_het0 have
"root (length x) (∏:x) = root (length x) ((mean x)^(length x))"
by simp
also from lxgt0 mxgt0 real_root_power_cancel have "… = mean x" by auto
finally show "gmean x = mean x" unfolding gmean_def .
qed
subsection ‹Existence of a new collection›
text ‹We now present the largest and most important proof in this
document. Given any positive and non-homogeneous collection of real
numbers there exists a new collection that is $\gamma$-equivalent,
positive, has a strictly lower heterogeneity and a greater geometric
mean.›
lemma new_list_gt_gmean:
fixes xs :: "real list" and m :: real
and neq and eq
defines
m: "m ≡ mean xs" and
neq: "noteq ≡ list_neq xs m" and
eq: "eq ≡ list_eq xs m"
assumes pos_xs: "pos xs" and het_gt_0: "het xs > 0"
shows
"∃xs'. gmean xs' > gmean xs ∧ γ_eq (xs',xs) ∧
het xs' < het xs ∧ pos xs'"
proof -
from pos_xs pos_imp_ne have
pos_els: "∀y. y : set xs ⟶ y > 0" by (unfold pos_def, simp)
with el_gt0_imp_prod_gt0[of xs] have pos_asm: "∏:xs > 0" by simp
from neq het_gt_0 het_gt_0_imp_noteq_ne m have
neqne: "noteq ≠ []" by simp
txt ‹Pick two elements from xs, one greater than m, one less than m.›
from assms pick_one_gt neqne obtain α where
α_def: "α : set noteq ∧ α > m" unfolding neq m by auto
from assms pick_one_lt neqne obtain β where
β_def: "β : set noteq ∧ β < m" unfolding neq m by auto
from α_def β_def have α_gt: "α > m" and β_lt: "β < m" by auto
from α_def β_def have el_neq: "β ≠ α" by simp
from neqne neq have xsne: "xs ≠ []" by auto
from β_def have β_mem: "β : set xs" by (auto simp: neq)
from α_def have α_mem: "α : set xs" by (auto simp: neq)
from pos_xs pos_def xsne α_mem β_mem α_def β_def have
α_pos: "α > 0" and β_pos: "β > 0" by auto
obtain left_over where lo: "left_over = (remove1 β (remove1 α xs))" by simp
obtain b where bdef: "m + b = α + β"
by (drule meta_spec [of _ "α + β - m"], simp)
from m pos_xs pos_def pos_mean have m_pos: "m > 0" by simp
with bdef α_pos β_pos α_gt β_lt have b_pos: "b > 0" by simp
obtain new_list where nl: "new_list = m#b#(left_over)" by auto
from el_neq β_mem α_mem have "β : set xs ∧ α : set xs ∧ β ≠ α" by simp
hence "α : set (remove1 β xs) ∧ β : set(remove1 α xs)" by (auto simp add: in_set_remove1)
moreover hence "(remove1 α xs) ≠ [] ∧ (remove1 β xs) ≠ []" by (auto)
ultimately have
mem : "α : set(remove1 β xs) ∧ β : set(remove1 α xs) ∧
(remove1 α xs) ≠ [] ∧ (remove1 β xs) ≠ []" by simp
from nl have nl_pos: "pos new_list"
proof cases
assume "left_over = []"
with nl b_pos m_pos show ?thesis by simp
next
assume lone: "left_over ≠ []"
from mem pos_imp_rmv_pos pos_xs have "pos (remove1 α xs)" by simp
with lo lone pos_imp_rmv_pos have "pos left_over" by simp
with lone mem nl m_pos b_pos show ?thesis by simp
qed
with mem nl lo bdef α_mem β_mem
have "∑:new_list = ∑:xs"
apply clarsimp
apply (subst sum_list_rmv1)
apply simp
apply (subst sum_list_rmv1)
apply simp
apply clarsimp
done
moreover from lo nl β_mem α_mem mem have
leq: "length new_list = length xs"
apply -
apply (erule conjE)+
apply (clarsimp)
apply (subst length_remove1, simp)
apply (simp add: length_remove1)
apply (auto dest!:length_pos_if_in_set)
done
ultimately have eq_mean: "mean new_list = mean xs" by (rule list_mean_eq_iff)
have gt_gmean: "gmean new_list > gmean xs"
proof -
from bdef α_gt β_lt have "abs (m - b) < abs (α - β)" by arith
moreover from bdef have "m+b = α+β" .
ultimately have mb_gt_gt: "m*b > α*β" by (rule le_diff_imp_gt_prod)
moreover from nl have
"∏:new_list = ∏:left_over * (m*b)" by auto
moreover
from lo α_mem β_mem mem remove1_retains_prod[where 'a = real] have
xsprod: "∏:xs = ∏:left_over * (α*β)" by auto
moreover from xsne have
"xs ≠ []" .
moreover from nl have
nlne: "new_list ≠ []" by simp
moreover from pos_asm lo have
"∏:left_over > 0"
proof -
from pos_asm have "∏:xs > 0" .
moreover
from xsprod have "∏:xs = ∏:left_over * (α*β)" .
ultimately have "∏:left_over * (α*β) > 0" by simp
moreover
from pos_els α_mem β_mem have "α > 0" and "β > 0" by auto
hence "α*β > 0" by simp
ultimately show "∏:left_over > 0"
apply -
apply (rule zero_less_mult_pos2 [where a="(α * β)"])
by auto
qed
ultimately have "∏:new_list > ∏:xs"
by simp
moreover with pos_asm nl have "∏:new_list > 0" by auto
moreover from calculation pos_asm xsne nlne leq list_gmean_gt_iff
show "gmean new_list > gmean xs" by simp
qed
from β_lt have β_ne_m: "β ≠ m" by simp
from mem have
β_mem_rmv_α: "β : set (remove1 α xs)" and rmv_α_ne: "(remove1 α xs) ≠ []" by auto
from α_def have α_ne_m: "α ≠ m" by simp
have lt_het: "het new_list < het xs"
proof cases
assume bm: "b=m"
with het_def have
"het new_list = length (list_neq new_list (mean new_list))"
by simp
also with m nl eq_mean have
"… = length (list_neq (m#b#(left_over)) m)"
by simp
also with bm have
"… = length (list_neq left_over m)"
by simp
also with lo β_def α_def have
"… = length (list_neq (remove1 β (remove1 α xs)) m)"
by simp
also from β_ne_m β_mem_rmv_α rmv_α_ne have
"… < length (list_neq (remove1 α xs) m)"
apply -
apply (rule list_neq_remove1)
by simp
also from α_mem α_ne_m xsne have
"… < length (list_neq xs m)"
apply -
apply (rule list_neq_remove1)
by simp
also with m het_def have "… = het xs" by simp
finally show "het new_list < het xs" .
next
assume bnm: "b≠m"
with het_def have
"het new_list = length (list_neq new_list (mean new_list))"
by simp
also with m nl eq_mean have
"… = length (list_neq (m#b#(left_over)) m)"
by simp
also with bnm have
"… = length (b#(list_neq left_over m))"
by simp
also have
"… = 1 + length (list_neq left_over m)"
by simp
also with lo β_def α_def have
"… = 1 + length (list_neq (remove1 β (remove1 α xs)) m)"
by simp
also from β_ne_m β_mem_rmv_α rmv_α_ne have
"… < 1 + length (list_neq (remove1 α xs) m)"
apply -
apply (simp only: nat_add_left_cancel_less)
apply (rule list_neq_remove1)
by simp
finally have
"het new_list ≤ length (list_neq (remove1 α xs) m)"
by simp
also from α_mem α_ne_m xsne have "… < length (list_neq xs m)"
apply -
apply (rule list_neq_remove1)
by simp
also with m het_def have "… = het xs" by simp
finally show "het new_list < het xs" .
qed
from γ_eq_def lt_het gt_gmean eq_mean leq nl_pos show ?thesis by auto
qed
text ‹Furthermore we show that for all non-homogeneous positive
collections there exists another collection that is
$\gamma$-equivalent, positive, has a greater geometric mean {\em and}
is homogeneous.›
lemma existence_of_het0 [rule_format]:
shows "∀x. p = het x ∧ p > 0 ∧ pos x ⟶
(∃y. gmean y > gmean x ∧ γ_eq (x,y) ∧ het y = 0 ∧ pos y)"
(is "?Q p" is "∀x. (?A x p ⟶ ?S x)")
proof (induct p rule: nat_less_induct)
fix n
assume ind: "∀m<n. ?Q m"
{
fix x
assume ass: "?A x n"
hence "het x > 0" and "pos x" by auto
with new_list_gt_gmean have
"∃y. gmean y > gmean x ∧ γ_eq (x,y) ∧ het y < het x ∧ pos y"
apply -
apply (drule meta_spec [of _ x])
apply (drule meta_mp)
apply assumption
apply (drule meta_mp)
apply assumption
apply (subst(asm) γ_eq_sym)
apply simp
done
then obtain β where
β_def: "gmean β > gmean x ∧ γ_eq (x,β) ∧ het β < het x ∧ pos β" ..
then obtain b where bdef: "b = het β" by simp
with ass β_def have "b < n" by auto
with ind have "?Q b" by simp
with β_def have
ind2: "b = het β ∧ 0 < b ∧ pos β ⟶
(∃y. gmean β < gmean y ∧ γ_eq (β, y) ∧ het y = 0 ∧ pos y)" by simp
{
assume "¬(0<b)"
hence "b=0" by simp
with bdef have "het β = 0" by simp
with β_def have "?S x" by auto
}
moreover
{
assume "0 < b"
with bdef ind2 β_def have "?S β" by simp
then obtain γ where
"gmean β < gmean γ ∧ γ_eq (β, γ) ∧ het γ = 0 ∧ pos γ" ..
with β_def have "gmean x < gmean γ ∧ γ_eq (x,γ) ∧ het γ = 0 ∧ pos γ"
apply clarsimp
apply (rule γ_eq_trans)
by auto
hence "?S x" by auto
}
ultimately have "?S x" by auto
}
thus "?Q n" by simp
qed
subsection ‹Cauchy's Mean Theorem›
text ‹We now present the final proof of the theorem. For any
positive collection we show that its geometric mean is less than or
equal to its arithmetic mean.›
theorem CauchysMeanTheorem:
fixes z::"real list"
assumes "pos z"
shows "gmean z ≤ mean z"
proof -
from ‹pos z› have zne: "z≠[]" by (rule pos_imp_ne)
show "gmean z ≤ mean z"
proof cases
assume "het z = 0"
with ‹pos z› zne het_base have "gmean z = mean z" by simp
thus ?thesis by simp
next
assume "het z ≠ 0"
hence "het z > 0" by simp
moreover obtain k where "k = het z" by simp
moreover with calculation ‹pos z› existence_of_het0 have
"∃y. gmean y > gmean z ∧ γ_eq (z,y) ∧ het y = 0 ∧ pos y" by auto
then obtain α where
"gmean α > gmean z ∧ γ_eq (z,α) ∧ het α = 0 ∧ pos α" ..
with het_base γ_eq_def pos_imp_ne have
"mean z = mean α" and
"gmean α > gmean z" and
"gmean α = mean α" by auto
hence "gmean z < mean z" by simp
thus ?thesis by simp
qed
qed
text ‹In the equality version we prove that the geometric mean
is identical to the arithmetic mean iff the collection is
homogeneous.›
theorem CauchysMeanTheorem_Eq:
fixes z::"real list"
assumes "pos z"
shows "gmean z = mean z ⟷ het z = 0"
proof
assume "het z = 0"
with het_base[of z] ‹pos z› show "gmean z = mean z" by auto
next
assume eq: "gmean z = mean z"
show "het z = 0"
proof (rule ccontr)
assume "het z ≠ 0"
hence "het z > 0" by auto
moreover obtain k where "k = het z" by simp
moreover with calculation ‹pos z› existence_of_het0 have
"∃y. gmean y > gmean z ∧ γ_eq (z,y) ∧ het y = 0 ∧ pos y" by auto
then obtain α where
"gmean α > gmean z ∧ γ_eq (z,α) ∧ het α = 0 ∧ pos α" ..
with het_base γ_eq_def pos_imp_ne have
"mean z = mean α" and
"gmean α > gmean z" and
"gmean α = mean α" by auto
hence "gmean z < mean z" by simp
thus False using eq by auto
qed
qed
corollary CauchysMeanTheorem_Less:
fixes z::"real list"
assumes "pos z" and "het z > 0"
shows "gmean z < mean z"
using
CauchysMeanTheorem[OF ‹pos z›]
CauchysMeanTheorem_Eq[OF ‹pos z›]
‹het z > 0›
by auto
end