Theory Cauchy.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)))"
by (induct xs) (auto simp: mean_def)
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 have
"… = (len + 1)*∑:xs / (len * (1+len))"
by (smt (verit, best) lnez add_divide_distrib divide_divide_eq_left
nonzero_divide_mult_cancel_left times_divide_eq_left)
also from l1nez have "… = ∑:xs / len"
by (simp add: add.commute)
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:
assumes "xs ≠ []" "0 < x" and mgt0: "0 < mean xs"
shows "0 < mean (x # xs)"
proof -
have lxsgt0: "length xs ≠ 0"
using assms by simp
from mgt0 have xsgt0: "0 < ∑:xs"
by (simp add: assms list_sum_mean)
with ‹x>0› have "∑:(x#xs) > 0" by simp
thus ?thesis
using mean_def by force
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
by simp
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 xs_ne a_ne_m Cons have
"length (list_neq (remove1 a xs) m) < length (list_neq xs m)"
by simp
then show ?thesis
by (simp add: a_ne_x)
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))))"
by (induct xs) (auto simp:field_simps)
lemma list_eq_prod [simp]:
fixes xs::"real list"
shows "∏:(list_eq xs m) = (m ^ (length (list_eq xs m)))"
by (induct xs) auto
lemma sum_list_split:
fixes xs::"real list"
shows "∑:xs = (∑:(list_neq xs m) + ∑:(list_eq xs m))"
by (induct xs) auto
lemma prod_list_split:
fixes xs::"real list"
shows "∏:xs = (∏:(list_neq xs m) * ∏:(list_eq xs m))"
by (induct xs) auto
lemma sum_list_length_split:
fixes xs::"real list"
shows "length xs = length (list_neq xs m) + length (list_eq xs m)"
by (induct xs) auto
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)))"
by (metis of_nat_add sum_list_length_split)
also have "… = ∑:xs"
by (simp add: list_sum_mean [symmetric])
finally show False
by (metis nless_le sum_list_split)
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)))"
by (metis of_nat_add sum_list_length_split)
also have "… = ∑:xs"
by (simp add: list_sum_mean [symmetric])
finally show False
by (metis less_irrefl sum_list_split)
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 ∈ set xs" "b ∈ set xs" "a ≠ b"
shows "het xs > 0"
unfolding het_def
by (metis (mono_tags, lifting) assms filter_empty_conv length_greater_0_conv)
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)"
by (auto simp: pos_def)
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)"
by (metis assms notin_set_remove1 pos_def)
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)
then show ?case
proof cases
assume xse: "xs = []"
thus ?thesis
using Cons.prems mean_def by auto
next
assume xsne: "xs ≠ []"
show ?thesis
by (meson Cons.hyps Cons.prems mean_gt_0 pos_cons xsne)
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))"
by (metis mult_1)
also have "… = (mean x) ^ (length (list_eq x (mean x)))" by simp
finally have "∏:x = (mean x) ^ (length x)"
by (metis add_0 lz sum_list_length_split)
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:
assumes "pos x" "het x = 0"
shows "gmean x = mean x"
proof -
have "root (length x) (∏:x) = root (length x) ((mean x)^(length x))"
by (simp add: assms pos_imp_ne prod_list_het0)
also have "… = mean x"
by (simp add: ‹pos x› order.order_iff_strict pos_imp_ne pos_mean
real_root_power_cancel)
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
have mem : "α ∈ set(remove1 β xs) ∧ β ∈ set(remove1 α xs) ∧ remove1 α xs ≠ [] ∧ (remove1 β xs) ≠ []"
by (metis α_mem β_mem el_neq empty_iff in_set_remove1 list.set(1))
from nl have nl_pos: "pos new_list"
by (metis b_pos lo m_pos mem pos_cons pos_imp_rmv_pos pos_single pos_xs)
with mem nl lo bdef α_mem β_mem
have s_eq_s: "∑:new_list = ∑:xs"
by (simp add: sum_list_rmv1)
then have eq_mean: "mean new_list = mean xs"
by (metis One_nat_def Suc_pred α_mem length_Cons length_pos_if_in_set
length_remove1 list_mean_eq_iff lo mem nl)
have gt_gmean: "gmean new_list > gmean xs"
proof -
have mb_gt_gt: "m*b > α*β"
using α_gt β_lt bdef le_diff_imp_gt_prod by force
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 nl have
nlne: "new_list ≠ []" by simp
moreover from pos_asm lo have
"∏:left_over > 0"
using α_pos β_pos mult_pos_pos xsprod zero_less_mult_pos2 by auto
ultimately show "gmean new_list > gmean xs"
using s_eq_s eq_mean list_gmean_gt_iff list_sum_mean m
m_pos pos_asm xsne by force
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 left_over m)"
using assms(1) eq_mean nl by auto
also have
"… < length (list_neq (remove1 α xs) m)"
by (metis β_ne_m list_neq_remove1 lo mem)
also have "… < length (list_neq xs m)"
by (metis α_mem α_ne_m list_neq_remove1)
also have "… = het xs"
using het_def m by presburger
finally show "het new_list < het xs" .
next
assume bnm: "b≠m"
with het_def have
"het new_list = length (b#(list_neq left_over m))"
using eq_mean m nl by force
also have "… = 1 + length (list_neq (remove1 β (remove1 α xs)) m)"
using lo by auto
also have "… < 1 + length (list_neq (remove1 α xs) m)"
by (metis β_ne_m add_strict_left_mono list_neq_remove1 mem)
finally have "het new_list ≤ length (list_neq (remove1 α xs) m)"
by simp
also have "… < length (list_neq xs m)"
by (metis α_mem α_ne_m list_neq_remove1)
also have "… = het xs"
using het_def m by presburger
finally show ?thesis .
qed
then show ?thesis
using γ_eq_def eq_mean gt_gmean list_sum_mean nl_pos pos_mean s_eq_s
by fastforce
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:
shows "p = het x ⟹ p > 0 ⟹ pos x ⟹
(∃y. gmean y > gmean x ∧ γ_eq (x,y) ∧ het y = 0 ∧ pos y)"
proof (induct p arbitrary: x rule: nat_less_induct)
case (1 n x)
then have "het x > 0" and "pos x" by auto
with new_list_gt_gmean obtain β where
β_def: "gmean β > gmean x ∧ γ_eq (x,β) ∧ het β < het x ∧ pos β"
using γ_eq_sym by blast
then obtain b where bdef: "b = het β" by simp
with 1 β_def have "b < n" by auto
then show ?case
by (smt (verit, best) "1.hyps" β_def γ_eq_trans bdef not_gr_zero)
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
ultimately obtain α where
"gmean α > gmean z ∧ γ_eq (z,α) ∧ het α = 0 ∧ pos α"
using assms existence_of_het0 by blast
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"
by (metis CauchysMeanTheorem CauchysMeanTheorem_Eq assms nless_le)
end