(* Title: Cauchy's Mean Theorem Author: Benjamin Porter <Benjamin.Porter at gmail.com>, 2006 cleaned up a bit by Tobias Nipkow, 2007 Maintainer: Benjamin Porter <Benjamin.Porter at gmail.com> *) 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) ― ‹reductio ad absurdum› 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 ― ‹remove these elements from xs, and insert two new elements› 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 ― ‹prove that new list is positive› 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 ― ‹now show that the new list has the same mean as the old list› 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) ― ‹finally show that the new list has a greater gmean than the old list› 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 ― ‹auxiliary info› 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 ― ‹now show that new list is more homogeneous› 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 ― ‹thus thesis by existence of newlist› 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