section‹Khovanskii's Theorem› text‹We formalise the proof of an important theorem in additive combinatorics due to Khovanskii, attesting that the cardinality of the set of all sums of $n$ many elements of $A$, where $A$ is a finite subset of an abelian group, is a polynomial in $n$ for all sufficiently large $n$. We follow a proof due to Nathanson and Ruzsa as presented in the notes “Introduction to Additive Combinatorics” by Timothy Gowers for the University of Cambridge.› theory Khovanskii imports Complex_Main FiniteProduct "HOL-Library.Equipollence" "Pluennecke_Ruzsa_Inequality.Pluennecke_Ruzsa_Inequality" "Bernoulli.Bernoulli" ― ‹sums of a fixed power are polynomials› "HOL-Analysis.Weierstrass_Theorems" ― ‹needed for polynomial function› "HOL-Library.List_Lenlexorder" ― ‹lexicographic ordering for the type @{typ ‹nat list›}› begin text ‹The sum of the elements of a list› abbreviation "σ ≡ sum_list" text ‹Related to the nsets of Ramsey.thy, but simpler› definition finsets :: "['a set, nat] ⇒ 'a set set" where "finsets A n ≡ {N. N ⊆ A ∧ card N = n}" lemma card_finsets: "finite N ⟹ card (finsets N k) = card N choose k" by (simp add: finsets_def n_subsets) lemma sorted_map_plus_iff [simp]: fixes a::"'a::linordered_cancel_ab_semigroup_add" shows "sorted (map ((+) a) xs) ⟷ sorted xs" by (induction xs) auto lemma distinct_map_plus_iff [simp]: fixes a::"'a::linordered_cancel_ab_semigroup_add" shows "distinct (map ((+) a) xs) ⟷ distinct xs" by (induction xs) auto subsection ‹Arithmetic operations on lists, pointwise on the elements› text ‹Weak type class properties. Cancellation is difficult to arrange because of complications when lists differ in length.› instantiation list :: (plus) plus begin definition "plus_list ≡ map2 (+)" instance.. end lemma length_plus_list [simp]: fixes xs :: "'a::plus list" shows "length (xs+ys) = min (length xs) (length ys)" by (simp add: plus_list_def) lemma plus_Nil [simp]: "[] + xs = []" by (simp add: plus_list_def) lemma plus_Cons: "(y # ys) + (x # xs) = (y+x) # (ys+xs)" by (simp add: plus_list_def) lemma nth_plus_list [simp]: fixes xs :: "'a::plus list" assumes "i < length xs" "i < length ys" shows "(xs+ys)!i = xs!i + ys!i" by (simp add: plus_list_def assms) instantiation list :: (minus) minus begin definition "minus_list ≡ map2 (-)" instance.. end lemma length_minus_list [simp]: fixes xs :: "'a::minus list" shows "length (xs-ys) = min (length xs) (length ys)" by (simp add: minus_list_def) lemma minus_Nil [simp]: "[] - xs = []" by (simp add: minus_list_def) lemma minus_Cons: "(y # ys) - (x # xs) = (y-x) # (ys-xs)" by (simp add: minus_list_def) lemma nth_minus_list [simp]: fixes xs :: "'a::minus list" assumes "i < length xs" "i < length ys" shows "(xs-ys)!i = xs!i - ys!i" by (simp add: minus_list_def assms) instance list :: (ab_semigroup_add) ab_semigroup_add proof have "map2 (+) (map2 (+) xs ys) zs = map2 (+) xs (map2 (+) ys zs)" for xs ys zs :: "'a list" proof (induction xs arbitrary: ys zs) case (Cons x xs) show ?case proof (cases "ys=[] ∨ zs=[]") case False then obtain y ys' z zs' where "ys = y#ys'" "zs = z # zs'" by (meson list.exhaust) then show ?thesis by (simp add: Cons add.assoc) qed auto qed auto then show "a + b + c = a + (b + c)" for a b c :: "'a list" by (auto simp: plus_list_def) next have "map2 (+) xs ys = map2 (+) ys xs" for xs ys :: "'a list" proof (induction xs arbitrary: ys) case (Cons x xs) show ?case proof (cases ys) case (Cons y ys') then show ?thesis by (simp add: Cons.IH add.commute) qed auto qed auto then show "a + b = b + a" for a b :: "'a list" by (auto simp: plus_list_def) qed subsection ‹The pointwise ordering on two equal-length lists of natural numbers› text ‹Gowers uses the usual symbol ($\le$) for his pointwise ordering. In our development, $\le$ is the lexicographic ordering and $\unlhd$ is the pointwise ordering.› definition pointwise_le :: "[nat list, nat list] ⇒ bool" (infixr "⊴" 50 ) where "x ⊴ y ≡ list_all2 (≤) x y" definition pointwise_less :: "[nat list, nat list] ⇒ bool" (infixr "⊲" 50 ) where "x ⊲ y ≡ x ⊴ y ∧ x ≠ y" lemma pointwise_le_iff_nth: "x ⊴ y ⟷ length x = length y ∧ (∀i < length x. x!i ≤ y!i)" by (simp add: list_all2_conv_all_nth pointwise_le_def) lemma pointwise_le_iff: "x ⊴ y ⟷ length x = length y ∧ (∀(i,j) ∈ set (zip x y). i≤j)" by (simp add: list_all2_iff pointwise_le_def) lemma pointwise_append_le_iff [simp]: "u@x ⊴ u@y ⟷ x ⊴ y" by (auto simp: pointwise_le_iff_nth nth_append) lemma pointwise_le_refl [iff]: "x ⊴ x" by (simp add: list.rel_refl pointwise_le_def) lemma pointwise_le_antisym: "⟦x ⊴ y; y ⊴ x⟧ ⟹ x=y" by (metis antisym list_all2_antisym pointwise_le_def) lemma pointwise_le_trans: "⟦x ⊴ y; y ⊴ z⟧ ⟹ x ⊴ z" by (smt (verit, del_insts) le_trans list_all2_trans pointwise_le_def) lemma pointwise_le_Nil [simp]: "Nil ⊴ x ⟷ x = Nil" by (simp add: pointwise_le_def) lemma pointwise_le_Nil2 [simp]: "x ⊴ Nil ⟷ x = Nil" by (simp add: pointwise_le_def) lemma pointwise_le_iff_less_equal: "x ⊴ y ⟷ x ⊲ y ∨ x = y" using pointwise_less_def by blast lemma pointwise_less_iff: "x ⊲ y ⟷ x ⊴ y ∧ (∃(i,j) ∈ set (zip x y). i<j)" using list_eq_iff_zip_eq pointwise_le_iff pointwise_less_def by fastforce lemma pointwise_less_iff2: "x ⊲ y ⟷ x ⊴ y ∧ (∃k < length x. x!k <y ! k)" unfolding pointwise_less_def pointwise_le_iff_nth by (fastforce intro!: nth_equalityI) lemma pointwise_less_Nil [simp]: "¬ Nil ⊲ x" by (simp add: pointwise_less_def) lemma pointwise_less_Nil2 [simp]: "¬ x ⊲ Nil" by (simp add: pointwise_less_def) lemma zero_pointwise_le_iff [simp]: "replicate r 0 ⊴ x ⟷ length x = r" by (auto simp: pointwise_le_iff_nth) lemma pointwise_le_imp_σ: assumes "xs ⊴ ys" shows "σ xs ≤ σ ys" using assms proof (induction ys arbitrary: xs) case Nil then show ?case by (simp add: pointwise_le_iff) next case (Cons y ys) then obtain x xs' where "x≤y" "xs = x#xs'" "xs' ⊴ ys" by (auto simp: pointwise_le_def list_all2_Cons2) then show ?case by (simp add: Cons.IH add_le_mono) qed lemma sum_list_plus: fixes xs :: "'a::comm_monoid_add list" assumes "length xs = length ys" shows "σ (xs + ys) = σ xs + σ ys" using assms by (simp add: plus_list_def case_prod_unfold sum_list_addf) lemma sum_list_minus: assumes "xs ⊴ ys" shows "σ (ys - xs) = σ ys - σ xs" using assms proof (induction ys arbitrary: xs) case (Cons y ys) then obtain x xs' where "x≤y" "xs = x#xs'" "xs' ⊴ ys" by (auto simp: pointwise_le_def list_all2_Cons2) then show ?case using pointwise_le_imp_σ by (auto simp: Cons minus_Cons) qed (auto simp: in_set_conv_nth) subsection ‹Pointwise minimum and maximum of a set of lists› definition min_pointwise :: "[nat, nat list set] ⇒ nat list" where "min_pointwise ≡ λr U. map (λi. Min ((λu. u!i) ` U)) [0..<r]" lemma min_pointwise_le: "⟦u ∈ U; finite U⟧ ⟹ min_pointwise (length u) U ⊴ u" by (simp add: min_pointwise_def pointwise_le_iff_nth) lemma min_pointwise_ge_iff: assumes "finite U" "U ≠ {}" "⋀u. u ∈ U ⟹ length u = r" "length x = r" shows "x ⊴ min_pointwise r U ⟷ (∀u ∈ U. x ⊴ u)" by (auto simp: min_pointwise_def pointwise_le_iff_nth assms) definition max_pointwise :: "[nat, nat list set] ⇒ nat list" where "max_pointwise ≡ λr U. map (λi. Max ((λu. u!i) ` U)) [0..<r]" lemma max_pointwise_ge: "⟦u ∈ U; finite U⟧ ⟹ u ⊴ max_pointwise (length u) U" by (simp add: max_pointwise_def pointwise_le_iff_nth) lemma max_pointwise_le_iff: assumes "finite U" "U ≠ {}" "⋀u. u ∈ U ⟹ length u = r" "length x = r" shows "max_pointwise r U ⊴ x ⟷ (∀u ∈ U. u ⊴ x)" by (auto simp: max_pointwise_def pointwise_le_iff_nth assms) lemma max_pointwise_mono: assumes "X' ⊆ X" "finite X" "X' ≠ {}" shows "max_pointwise r X' ⊴ max_pointwise r X" using assms by (simp add: max_pointwise_def pointwise_le_iff_nth Max_mono image_mono) lemma pointwise_le_plus: "⟦xs ⊴ ys; length ys ≤ length zs⟧ ⟹ xs ⊴ ys+zs" proof (induction xs arbitrary: ys zs) case (Cons x xs) then obtain y ys' z zs' where "ys = y#ys'" "zs = z#zs'" unfolding pointwise_le_iff by (metis Suc_le_length_iff le_refl length_Cons) with Cons show ?case by (auto simp: plus_list_def pointwise_le_def) qed (simp add: pointwise_le_iff) lemma pairwise_minus_cancel: "⟦z ⊴ x; z ⊴ y; x - z = y - z⟧ ⟹ x = y" unfolding pointwise_le_iff_nth by (metis eq_diff_iff nth_equalityI nth_minus_list) subsection ‹A locale to fix the finite subset @{term "A ⊆ G"}› locale Khovanskii = additive_abelian_group + fixes A :: "'a set" assumes AsubG: "A ⊆ G" and finA: "finite A" begin text ‹finite products of a group element› definition Gmult :: "'a ⇒ nat ⇒ 'a" where "Gmult a n ≡ (((⊕)a) ^^ n) 𝟬" lemma Gmult_0 [simp]: "Gmult a 0 = 𝟬" by (simp add: Gmult_def) lemma Gmult_1 [simp]: "a ∈ G ⟹ Gmult a (Suc 0) = a" by (simp add: Gmult_def) lemma Gmult_Suc [simp]: "Gmult a (Suc n) = a ⊕ Gmult a n" by (simp add: Gmult_def) lemma Gmult_in_G [simp,intro]: "a ∈ G ⟹ Gmult a n ∈ G" by (induction n) auto lemma Gmult_add_add: assumes "a ∈ G" shows "Gmult a (m+n) = Gmult a m ⊕ Gmult a n" by (induction m) (use assms local.associative in fastforce)+ lemma Gmult_add_diff: assumes "a ∈ G" shows "Gmult a (n+k) ⊖ Gmult a n = Gmult a k" by (metis Gmult_add_add Gmult_in_G assms commutative inverse_closed invertible invertible_left_inverse2) lemma Gmult_diff: assumes "a ∈ G" "n≤m" shows "Gmult a m ⊖ Gmult a n = Gmult a (m-n)" by (metis Gmult_add_diff assms le_add_diff_inverse) text ‹Mapping elements of @{term A} to their numeric subscript› abbreviation "idx ≡ to_nat_on A" text ‹The elements of @{term A} in order› definition aA :: "'a list" where "aA ≡ map (from_nat_into A) [0..<card A]" definition α :: "nat list ⇒ 'a" where "α ≡ λx. fincomp (λi. Gmult (aA!i) (x!i)) {..<card A}" text ‹The underlying assumption is @{term "length y = length x"}› definition useless:: "nat list ⇒ bool" where "useless x ≡ ∃y < x. σ y = σ x ∧ α y = α x ∧ length y = length x" abbreviation "useful x ≡ ¬ useless x" lemma alpha_replicate_0 [simp]: "α (replicate (card A) 0) = 𝟬" by (auto simp: α_def intro: fincomp_unit_eqI) lemma idx_less_cardA: assumes "a ∈ A" shows "idx a < card A" by (metis assms bij_betw_def finA imageI lessThan_iff to_nat_on_finite) lemma aA_idx_eq [simp]: assumes "a ∈ A" shows "aA ! (idx a) = a" by (simp add: aA_def assms countable_finite finA idx_less_cardA) lemma set_aA: "set aA = A" using bij_betw_from_nat_into_finite [OF finA] by (simp add: aA_def atLeast0LessThan bij_betw_def) lemma nth_aA_in_G [simp]: "i < card A ⟹ aA!i ∈ G" using AsubG aA_def set_aA by auto lemma alpha_in_G [iff]: "α x ∈ G" using nth_aA_in_G fincomp_closed by (simp add: α_def) lemma Gmult_in_PiG [simp]: "(λi. Gmult (aA!i) (f i)) ∈ {..<card A} → G" by simp lemma alpha_plus: assumes "length x = card A" "length y = card A" shows "α (x + y) = α x ⊕ α y" proof - have "α (x + y) = fincomp (λi. Gmult (aA!i) (map2 (+) x y!i)) {..<card A}" by (simp add: α_def plus_list_def) also have "… = fincomp (λi. Gmult (aA!i) (x!i + y!i)) {..<card A}" by (intro fincomp_cong'; simp add: assms) also have "… = fincomp (λi. Gmult (aA!i) (x!i) ⊕ Gmult (aA!i) (y!i)) {..<card A}" by (intro fincomp_cong'; simp add: Gmult_add_add) also have "… = α x ⊕ α y" by (simp add: α_def fincomp_comp) finally show ?thesis . qed lemma alpha_minus: assumes "y ⊴ x" "length y = card A" shows "α (x - y) = α x ⊖ α y" proof - have "α (x - y) = fincomp (λi. Gmult (aA!i) (map2 (-) x y!i)) {..<card A}" by (simp add: α_def minus_list_def) also have "… = fincomp (λi. Gmult (aA!i) (x!i - y!i)) {..<card A}" using assms by (intro fincomp_cong') (auto simp: pointwise_le_iff) also have "… = fincomp (λi. Gmult (aA!i) (x!i) ⊖ Gmult (aA!i) (y!i)) {..<card A}" using assms by (intro fincomp_cong') (simp add: pointwise_le_iff_nth Gmult_diff)+ also have "… = α x ⊖ α y" by (simp add: α_def fincomp_comp fincomp_inverse) finally show ?thesis . qed subsection ‹Adding one to a list element› definition list_incr :: "nat ⇒ nat list ⇒ nat list" where "list_incr i x ≡ x[i := Suc (x!i)]" lemma list_incr_Nil [simp]: "list_incr i [] = []" by (simp add: list_incr_def) lemma list_incr_Cons [simp]: "list_incr (Suc i) (k#ks) = k # list_incr i ks" by (simp add: list_incr_def) lemma sum_list_incr [simp]: "i < length x ⟹ σ (list_incr i x) = Suc (σ x)" by (auto simp: list_incr_def sum_list_update) lemma length_list_incr [simp]: "length (list_incr i x) = length x" by (auto simp: list_incr_def) lemma nth_le_list_incr: "i < card A ⟹ x!i ≤ list_incr (idx a) x!i" unfolding list_incr_def by (metis Suc_leD linorder_not_less list_update_beyond nth_list_update_eq nth_list_update_neq order_refl) lemma list_incr_nth_diff: "i < length x ⟹ list_incr j x!i - x!i = (if i = j then 1 else 0)" by (simp add: list_incr_def) subsection ‹The set of all @{term r}-tuples that sum to @{term n}› definition length_sum_set :: "nat ⇒ nat ⇒ nat list set" where "length_sum_set r n ≡ {x. length x = r ∧ σ x = n}" lemma length_sum_set_Nil [simp]: "length_sum_set 0 n = (if n=0 then {[]} else {})" by (auto simp: length_sum_set_def) lemma length_sum_set_Suc [simp]: "k#ks ∈ length_sum_set (Suc r) n ⟷ (∃m. ks ∈ length_sum_set r m ∧ n = m+k)" by (auto simp: length_sum_set_def) lemma length_sum_set_Suc_eqpoll: "length_sum_set (Suc r) n ≈ Sigma {..n} (λi. length_sum_set r (n-i))" (is "?L ≈ ?R") unfolding eqpoll_def proof let ?f = "(λl. (hd l, tl l))" show "bij_betw ?f ?L ?R" proof (intro bij_betw_imageI) show "inj_on ?f ?L" by (force simp: inj_on_def length_sum_set_def intro: list.expand) show "?f ` ?L = ?R" by (force simp: length_sum_set_def length_Suc_conv) qed qed lemma finite_length_sum_set: "finite (length_sum_set r n)" proof (induction r arbitrary: n) case 0 then show ?case by (auto simp: length_sum_set_def) next case (Suc r) then show ?case using length_sum_set_Suc_eqpoll eqpoll_finite_iff by blast qed lemma card_length_sum_set: "card (length_sum_set (Suc r) n) = (∑i≤n. card (length_sum_set r (n-i)))" proof - have "card (length_sum_set (Suc r) n) = card (Sigma {..n} (λi. length_sum_set r (n-i)))" by (metis eqpoll_finite_iff eqpoll_iff_card finite_length_sum_set length_sum_set_Suc_eqpoll) also have "… = (∑i≤n. card (length_sum_set r (n-i)))" by (simp add: finite_length_sum_set) finally show ?thesis . qed lemma sum_up_index_split': assumes "N ≤ n" shows "(∑i≤n. f i) = (∑i≤n-N. f i) + (∑i=Suc (n-N)..n. f i)" by (metis assms diff_add sum_up_index_split) lemma sum_invert: "N ≤ n ⟹ (∑i = Suc (n - N)..n. f (n - i)) = (∑j<N. f j)" proof (induction N) case (Suc N) then show ?case apply (auto simp: Suc_diff_Suc) by (metis sum.atLeast_Suc_atMost Suc_leD add.commute diff_diff_cancel diff_le_self) qed auto lemma sum_diff_split: assumes "N ≤ n" shows "(∑i≤n - N. real (n - i) ^ j) = (∑i≤n. real i ^ j) - (∑i<N. real i ^ j)" proof - have inj: "inj_on ((-) n) {N..n}" by (auto simp: inj_on_def) have "(∑i≤n - N. real (n - i) ^ j) = (∑i∈(-) n ` {N..n}. real (n - i) ^ j)" proof (rule sum.cong) have "⋀x. x ≤ n - N ⟹ ∃m≥N. m ≤ n ∧ x = n - m" by (metis assms diff_diff_cancel diff_le_mono2 diff_le_self le_trans) then show "{..n - N} = (-) n ` {N..n}" by (auto simp: image_iff Bex_def) qed auto also have "… = (∑i=N..n. real i ^ j)" using sum.reindex [OF inj, of "λi. real (n - i) ^ j", symmetric] by (simp add: ) also have "… = (∑i≤n. real i ^ j) - (∑i<N. real i ^ j)" proof (cases N) case 0 then show ?thesis using atMost_atLeast0 by auto next case (Suc N') then show ?thesis using assms sum_up_index_split [of _ N' "n-N'"] by (smt (verit, best) Suc_diff_le add_Suc_shift diff_Suc_Suc le_add_diff_inverse lessThan_Suc_atMost) qed finally show ?thesis . qed lemma real_polynomial_function_length_sum_set: "∃p. real_polynomial_function p ∧ (∀n>0. real (card (length_sum_set r n)) = p (real n))" proof (induction r) case 0 have "∀n>0. real (card (length_sum_set 0 n)) = 0" by auto then show ?case by blast next case (Suc r) then obtain p where poly: "real_polynomial_function p" and p: "⋀n. n>0 ⟹ real (card (length_sum_set r n)) = p (real n)" by blast then obtain a n where p_eq: "p = (λx. ∑i≤n. a i * x ^ i)" using real_polynomial_function_iff_sum by auto define q where "q ≡ λx. ∑j≤n. a j * ((bernpoly (Suc j) (1 + x) - bernpoly (Suc j) 0) / (1 + real j) - 0 ^ j)" have rp_q: "real_polynomial_function q" by (fastforce simp: bernpoly_def p_eq q_def) have q_eq: "(∑x≤n - 1. p (real (n - x))) = q (real n)" if "n>0" for n using that by (simp add: p_eq q_def sum.swap sum_diff_split add.commute sum_of_powers flip: sum_distrib_left) define p' where "p' ≡ λx. q x + real (card (length_sum_set r 0))" have "real_polynomial_function p'" using rp_q by (force simp: p'_def) moreover have "(∑x≤n - Suc 0. p (real (n - x))) + real (card (length_sum_set r 0)) = p' (real n)" if "n>0" for n using that q_eq by (auto simp: p'_def) ultimately show ?case unfolding card_length_sum_set by (force simp: sum_up_index_split' [of 1] p sum_invert) qed lemma all_zeroes_replicate: "length_sum_set r 0 = {replicate r 0}" by (auto simp: length_sum_set_def replicate_eqI) lemma length_sum_set_Suc_eq_UN: "length_sum_set r (Suc n) = (⋃i<r. list_incr i ` length_sum_set r n)" proof - have "∃i<r. x ∈ list_incr i ` length_sum_set r n" if "σ x = Suc n" and "r = length x" for x proof - have "x ≠ replicate r 0" using that by (metis sum_list_replicate Zero_not_Suc mult_zero_right) then obtain i where i: "i < r" "x!i ≠ 0" by (metis ‹r = length x› in_set_conv_nth replicate_eqI) with that have "x[i := x!i - 1] ∈ length_sum_set r n" by (simp add: sum_list_update length_sum_set_def) with i that show ?thesis unfolding list_incr_def by force qed then show ?thesis by (auto simp: length_sum_set_def Bex_def) qed lemma alpha_list_incr: assumes "a ∈ A" "x ∈ length_sum_set (card A) n" shows "α (list_incr (idx a) x) = a ⊕ α x" proof - have lenx: "length x = card A" using assms length_sum_set_def by blast have "α (list_incr (idx a) x) ⊖ α x = fincomp (λi. Gmult (aA!i) (list_incr (idx a) x!i) ⊖ Gmult (aA!i) (x!i)) {..<card A}" by (simp add: α_def fincomp_comp fincomp_inverse) also have "… = fincomp (λi. Gmult (aA!i) (list_incr (idx a) x!i - x!i)) {..<card A}" by (intro fincomp_cong; simp add: Gmult_diff nth_le_list_incr) also have "… = fincomp (λi. if i = idx a then (aA!i) else 𝟬) {..<card A}" by (intro fincomp_cong'; simp add: list_incr_nth_diff lenx) also have "… = a" using assms by (simp add: fincomp_singleton_swap idx_less_cardA) finally have "α (list_incr (idx a) x) ⊖ α x = a" . then show ?thesis by (metis alpha_in_G associative inverse_closed invertible invertible_left_inverse right_unit) qed lemma sumset_iterated_enum: defines "r ≡ card A" shows "sumset_iterated A n = α ` length_sum_set r n" proof (induction n) case 0 then show ?case by (simp add: all_zeroes_replicate r_def) next case (Suc n) have eq: "{..<r} = idx ` A" by (metis bij_betw_def finA r_def to_nat_on_finite) have "sumset_iterated A (Suc n) = (⋃a∈A. (λi. a ⊕ α i) ` length_sum_set r n)" using AsubG by (auto simp: Suc sumset) also have "… = (⋃a∈A. (λi. α (list_incr (idx a) i)) ` length_sum_set r n)" by (simp add: alpha_list_incr r_def) also have "… = α ` length_sum_set r (Suc n)" by (simp add: image_UN image_comp length_sum_set_Suc_eq_UN eq) finally show ?case . qed subsection ‹Lemma 2.7 in Gowers's notes› text‹The following lemma corresponds to a key fact about the cardinality of the set of all sums of $n$ many elements of $A$, stated before Gowers's Lemma 2.7.› lemma card_sumset_iterated_length_sum_set_useful: defines "r ≡ card A" shows "card(sumset_iterated A n) = card (length_sum_set r n ∩ {x. useful x})" (is "card ?L = card ?R") proof - have "α x ∈ α ` (length_sum_set r n ∩ {x. useful x})" if "x ∈ length_sum_set r n" for x proof - define y where "y ≡ LEAST y. y ∈ length_sum_set r n ∧ α y = α x" have y: "y ∈ length_sum_set (card A) n ∧ α y = α x" by (metis (mono_tags, lifting) LeastI r_def y_def that) moreover have "useful y" proof (clarsimp simp: useless_def) show False if "σ z = σ y" "length z = length y" and "z < y" "α z = α y" for z using that Least_le length_sum_set_def not_less_Least r_def y y_def by fastforce qed ultimately show ?thesis unfolding image_iff length_sum_set_def r_def by (smt (verit) Int_Collect) qed then have "sumset_iterated A n = α ` (length_sum_set r n ∩ {x. useful x})" by (auto simp: sumset_iterated_enum length_sum_set_def r_def) moreover have "inj_on α (length_sum_set r n ∩ {x. useful x})" apply (simp add: image_iff length_sum_set_def r_def inj_on_def useless_def Ball_def) by (metis linorder_less_linear) ultimately show ?thesis by (simp add: card_image length_sum_set_def) qed text‹The following lemma corresponds to Lemma 2.7 in Gowers's notes.› lemma useless_leq_useless: defines "r ≡ card A" assumes "useless x" and "x ⊴ y" and "length x = r" shows "useless y " proof - have leny: "length y = r" using pointwise_le_iff assms by auto obtain x' where "x'< x" and σx': "σ x' = σ x" and αx': "α x' = α x" and lenx': "length x' = length x" using assms useless_def by blast obtain i where "i < card A" and xi: "x'!i < x!i" and takex': "take i x' = take i x" using ‹x'<x› lenx' assms by (auto simp: list_less_def lenlex_def elim!: lex_take_index) define y' where "y' ≡ y+x'-x" have leny': "length y' = length y" using assms lenx' pointwise_le_iff by (simp add: y'_def) have "x!i ≤ y!i" using ‹x ⊴ y› ‹i < card A› assms by (simp add: pointwise_le_iff_nth) then have "y'!i < y!i" using ‹i < card A› assms lenx' xi pointwise_le_iff by (simp add: y'_def plus_list_def minus_list_def) moreover have "take i y' = take i y" proof (intro nth_equalityI) show "length (take i y') = length (take i y)" by (simp add: leny') show "⋀k. k < length (take i y') ⟹ take i y' ! k = take i y!k" using takex' by (simp add: y'_def plus_list_def minus_list_def take_map take_zip) qed ultimately have "y' < y" using leny' ‹i < card A› assms pointwise_le_iff by (auto simp: list_less_def lenlex_def lexord_lex lexord_take_index_conv) moreover have "σ y' = σ y" using assms by (simp add: σx' lenx' leny pointwise_le_plus sum_list_minus sum_list_plus y'_def) moreover have "α y' = α y" using assms lenx' αx' leny by (fastforce simp: y'_def pointwise_le_plus alpha_minus alpha_plus local.associative) ultimately show ?thesis using leny' useless_def by blast qed inductive_set minimal_elements for U where "⟦x ∈ U; ⋀y. y ∈ U ⟹ ¬ y ⊲ x⟧ ⟹ x ∈ minimal_elements U" lemma pointwise_less_imp_σ: assumes "xs ⊲ ys" shows "σ xs < σ ys" proof - have eq: "length ys = length xs" and "xs ⊴ ys" using assms by (auto simp: pointwise_le_iff pointwise_less_iff) have "∀k<length xs. xs!k ≤ ys!k" using ‹xs ⊴ ys› list_all2_nthD pointwise_le_def by auto moreover have "∃k<length xs. xs!k < ys!k" using assms pointwise_less_iff2 by force ultimately show ?thesis by (force simp: eq sum_list_sum_nth intro: sum_strict_mono_ex1) qed lemma wf_measure_σ: "wf (inv_image less_than σ)" by blast lemma WFP: "wfP (⊲)" by (auto simp: wfP_def pointwise_less_imp_σ intro: wf_subset [OF wf_measure_σ]) text‹The following is a direct corollary of the above lemma, i.e. a corollary of Lemma 2.7 in Gowers's notes.› corollary useless_iff: assumes "length x = card A" shows "useless x ⟷ (∃x' ∈ minimal_elements (Collect useless). x' ⊴ x)" (is "_=?R") proof assume "useless x" obtain z where z: "useless z" "z ⊴ x" and zmin: "⋀y. y ⊲ z ⟹ y ⊴ x ⟹ useful y" using wfE_min [to_pred, where Q = "{z. useless z ∧ z ⊴ x}", OF WFP] by (metis (no_types, lifting) ‹useless x› mem_Collect_eq pointwise_le_refl) then show ?R by (smt (verit) mem_Collect_eq minimal_elements.intros pointwise_le_trans pointwise_less_def) next assume ?R with useless_leq_useless minimal_elements.cases show "useless x" by (metis assms mem_Collect_eq pointwise_le_iff) qed subsection ‹The set of minimal elements of a set of $r$-tuples is finite› text‹The following general finiteness claim corresponds to Lemma 2.8 in Gowers's notes and is key to the main proof.› lemma minimal_elements_set_tuples_finite: assumes Ur: "⋀x. x ∈ U ⟹ length x = r" shows "finite (minimal_elements U)" using assms proof (induction r arbitrary: U) case 0 then have "U ⊆ {[]}" by auto then show ?case by (metis finite.simps minimal_elements.cases finite_subset subset_eq) next case (Suc r) show ?case proof (cases "U={}") case True with Suc.IH show ?thesis by blast next case False then obtain u where u: "u ∈ U" and zmin: "⋀y. y ⊲ u ⟹ y ∉ U" using wfE_min [to_pred, where Q = "U", OF WFP] by blast define V where "V = {v ∈ U. ¬ u ⊴ v}" define VF where "VF ≡ λi t. {v ∈ V. v!i = t}" have [simp]: "length v = Suc r" if "v ∈ VF i t" for v i t using that by (simp add: Suc.prems VF_def V_def) have *: "∃i≤r. v!i < u!i" if "v ∈ V" for v using that u Suc.prems by (force simp: V_def pointwise_le_iff_nth not_le less_Suc_eq_le) with u have "minimal_elements U ≤ insert u (⋃i≤r. ⋃t < u!i. minimal_elements (VF i t))" by (force simp: VF_def V_def minimal_elements.simps pointwise_less_def) moreover have "finite (minimal_elements (VF i t))" if "i≤r" "t < u!i" for i t proof - define delete where "delete ≡ λv::nat list. take i v @ drop (Suc i) v" ― ‹deletion of @{term i}› have len_delete[simp]: "length (delete u) = r" if "u ∈ VF i t" for u using Suc.prems VF_def V_def ‹i ≤ r› delete_def that by auto have nth_delete: "delete u!k = (if k<i then u!k else u!Suc k)" if "u ∈ VF i t" "k<r" for u k using that by (simp add: delete_def nth_append) have delete_le_iff [simp]: "delete u ⊴ delete v ⟷ u ⊴ v" if "u ∈ VF i t" "v ∈ VF i t" for u v proof assume "delete u ⊴ delete v" then have "∀j. (j < i ⟶ u!j ≤ v!j) ∧ (j < r ⟶ i ≤ j ⟶ u!Suc j ≤ v!Suc j)" using that ‹i ≤ r› by (force simp: pointwise_le_iff_nth nth_delete split: if_split_asm cong: conj_cong) then show "u ⊴ v" using that ‹i ≤ r› apply (simp add: pointwise_le_iff_nth VF_def) by (metis eq_iff le_Suc_eq less_Suc_eq_0_disj linorder_not_less) next assume "u ⊴ v" then show "delete u ⊴ delete v" using that by (simp add: pointwise_le_iff_nth nth_delete) qed then have delete_eq_iff: "delete u = delete v ⟷ u = v" if "u ∈ VF i t" "v ∈ VF i t" for u v by (metis that pointwise_le_antisym pointwise_le_refl) have delete_less_iff: "delete u ⊲ delete v ⟷ u ⊲ v" if "u ∈ VF i t" "v ∈ VF i t" for u v by (metis delete_le_iff pointwise_le_antisym pointwise_less_def that) have "length (delete v) = r" if "v ∈ V" for v using id_take_nth_drop Suc.prems V_def ‹i ≤ r› delete_def that by auto then have "finite (minimal_elements (delete ` V))" by (metis (mono_tags, lifting) Suc.IH image_iff) moreover have "inj_on delete (minimal_elements (VF i t))" by (simp add: delete_eq_iff inj_on_def minimal_elements.simps) moreover have "delete ` (minimal_elements (VF i t)) ⊆ minimal_elements (delete ` (VF i t))" by (auto simp: delete_less_iff minimal_elements.simps) ultimately show ?thesis by (metis (mono_tags, lifting) Suc.IH image_iff inj_on_finite len_delete) qed ultimately show ?thesis by (force elim: finite_subset) qed qed subsection ‹Towards Lemma 2.9 in Gowers's notes› text ‹Increasing sequences› fun augmentum :: "nat list ⇒ nat list" where "augmentum [] = []" | "augmentum (n#ns) = n # map ((+)n) (augmentum ns)" definition dementum:: "nat list ⇒ nat list" where "dementum xs ≡ xs - (0#xs)" lemma dementum_Nil [simp]: "dementum [] = []" by (simp add: dementum_def) lemma zero_notin_augmentum [simp]: "0 ∉ set ns ⟹ 0 ∉ set (augmentum ns)" by (induction ns) auto lemma length_augmentum [simp]:"length (augmentum xs) = length xs" by (induction xs) auto lemma sorted_augmentum [simp]: "0 ∉ set ns ⟹ sorted (augmentum ns)" by (induction ns) auto lemma distinct_augmentum [simp]: "0 ∉ set ns ⟹ distinct (augmentum ns)" by (induction ns) (simp_all add: image_iff) lemma augmentum_subset_sum_list: "set (augmentum ns) ⊆ {..σ ns}" by (induction ns) auto lemma sum_list_augmentum: "σ ns ∈ set (augmentum ns) ⟷ length ns > 0" by (induction ns) auto lemma length_dementum [simp]: "length (dementum xs) = length xs" by (simp add: dementum_def) lemma sorted_imp_pointwise: assumes "sorted (xs@[n])" shows "0 # xs ⊴ xs @ [n]" using assms by (simp add: pointwise_le_iff_nth nth_Cons' nth_append sorted_append sorted_wrt_append sorted_wrt_nth_less) lemma sum_list_dementum: assumes "sorted (xs@[n])" shows "σ (dementum (xs@[n])) = n" proof - have "dementum (xs@[n]) = (xs@[n]) - (0 # xs)" by (rule nth_equalityI; simp add: nth_append dementum_def nth_Cons') then show ?thesis by (simp add: sum_list_minus sorted_imp_pointwise assms) qed lemma augmentum_cancel: "map ((+)k) (augmentum ns) - (k # map ((+)k) (augmentum ns)) = ns" proof (induction ns arbitrary: k) case Nil then show ?case by simp next case (Cons n ns) have "(+) k ∘ (+) n = (+) (k+n)" by auto then show ?case by (simp add: minus_Cons Cons) qed lemma dementum_augmentum [simp]: assumes "0 ∉ set ns" shows "(dementum ∘ sorted_list_of_set) ((set ∘ augmentum) ns) = ns" (is "?L ns = _") using assms augmentum_cancel [of 0] by (simp add: dementum_def map_idI sorted_list_of_set.idem_if_sorted_distinct) lemma dementum_nonzero: assumes ns: "sorted_wrt (<) ns" and 0: "0 ∉ set ns" shows "0 ∉ set (dementum ns)" unfolding dementum_def minus_list_def using sorted_wrt_nth_less [OF ns] 0 by (auto simp: in_set_conv_nth image_iff set_zip nth_Cons' dest: leD) lemma nth_augmentum [simp]: "i < length ns ⟹ augmentum ns!i = (∑j≤i. ns!j)" proof (induction ns arbitrary: i) case Nil then show ?case by simp next case (Cons a ns) show ?case proof (cases "i=0") case False then have "augmentum (a # ns)!i = a + sum ((!) ns) {..i-1}" using Cons.IH Cons.prems by auto also have "… = a + (∑j∈{0<..i}. ns!(j-1))" using sum.reindex [of Suc "{..i - Suc 0}" "λj. ns!(j-1)", symmetric] False by (simp add: image_Suc_atMost atLeastSucAtMost_greaterThanAtMost del: sum.cl_ivl_Suc) also have "… = (∑j = 0..i. if j=0 then a else ns!(j-1))" by (simp add: sum.head) also have "… = sum ((!) (a # ns)) {..i}" by (simp add: nth_Cons' atMost_atLeast0) finally show ?thesis . qed auto qed lemma augmentum_dementum [simp]: assumes "0 ∉ set ns" "sorted ns" shows "augmentum (dementum ns) = ns" proof (rule nth_equalityI) fix i assume "i < length (augmentum (dementum ns))" then have i: "i < length ns" by simp show "augmentum (dementum ns)!i = ns!i" proof (cases "i=0") case True then show ?thesis using nth_augmentum dementum_def i by auto next case False have ns_le: "⋀j. ⟦0 < j; j ≤ i⟧ ⟹ ns ! (j - Suc 0) ≤ ns ! j" using ‹sorted ns› i by (simp add: sorted_iff_nth_mono) have "augmentum (dementum ns)!i = (∑j≤i. ns!j - (if j = 0 then 0 else ns!(j-1)))" using i by (simp add: dementum_def nth_Cons') also have "… = (∑j=0..i. if j = 0 then ns!0 else ns!j - ns!(j-1))" by (smt (verit, del_insts) diff_zero sum.cong atMost_atLeast0) also have "… = ns!0 + (∑j∈{0<..i}. ns!j - ns!(j-1))" by (simp add: sum.head) also have "… = ns!0 + ((∑j∈{0<..i}. ns!j) - (∑j∈{0<..i}. ns!(j-1)))" by (auto simp: ns_le intro: sum_subtractf_nat) also have "… = ns!0 + (∑j∈{0<..i}. ns!j) - (∑j∈{0<..i}. ns!(j-1))" proof - have "(∑j∈{0<..i}. ns ! (j - 1)) ≤ sum ((!) ns) {0<..i}" by (metis One_nat_def greaterThanAtMost_iff ns_le sum_mono) then show ?thesis by simp qed also have "… = ns!0 + (∑j∈{0<..i}. ns!j) - (∑j≤i-Suc 0. ns!j)" using sum.reindex [of Suc "{..i - Suc 0}" "λj. ns!(j-1)", symmetric] False by (simp add: image_Suc_atMost atLeastSucAtMost_greaterThanAtMost) also have "… = (∑j=0..i. ns!j) - (∑j≤i-Suc 0. ns!j)" by (simp add: sum.head [of 0 i]) also have "… = (∑j=0..i-Suc 0. ns!j) + ns!i - (∑j≤i-Suc 0. ns!j)" by (metis False Suc_pred less_Suc0 not_less_eq sum.atLeast0_atMost_Suc) also have "… = ns!i" by (simp add: atLeast0AtMost) finally show "augmentum (dementum ns)!i = ns!i" . qed qed auto text‹The following lemma corresponds to Lemma 2.9 in Gowers's notes. The proof involves introducing bijective maps between r-tuples that fulfill certain properties/r-tuples and subsets of naturals, so as to show the cardinality claim. › lemma bound_sum_list_card: assumes "r > 0" and n: "n ≥ σ x'" and lenx': "length x' = r" defines "S ≡ {x. x' ⊴ x ∧ σ x = n}" shows "card S = (n - σ x' + r - 1) choose (r-1)" proof- define m where "m ≡ n - σ x'" define f where "f ≡ λx::nat list. x - x'" have f: "bij_betw f S (length_sum_set r m)" proof (intro bij_betw_imageI) show "inj_on f S" using pairwise_minus_cancel by (force simp: S_def f_def inj_on_def) have "⋀x. x ∈ S ⟹ f x ∈ length_sum_set r m" by (simp add: S_def f_def length_sum_set_def lenx' m_def pointwise_le_iff sum_list_minus) moreover have "x ∈ f ` S" if "x ∈ length_sum_set r m" for x proof have x[simp]: "length x = r" "σ x = m" using that by (auto simp: length_sum_set_def) have "x = x' + x - x'" by (rule nth_equalityI; simp add: lenx') then show "x = f (x' + x)" unfolding f_def by fastforce have "x' ⊴ x' + x" by (simp add: lenx' pointwise_le_plus) moreover have "σ (x' + x) = n" by (simp add: lenx' m_def n sum_list_plus) ultimately show "x' + x ∈ S" using S_def by blast qed ultimately show "f ` S = length_sum_set r m" by auto qed define g where "g ≡ λx::nat list. map Suc x" define g' where "g' ≡ λx::nat list. x - replicate (length x) 1" define T where "T ≡ length_sum_set r (m+r) ∩ lists(-{0})" have g: "bij_betw g (length_sum_set r m) T" proof (intro bij_betw_imageI) show "inj_on g (length_sum_set r m)" by (auto simp: g_def inj_on_def) have "⋀x. x ∈ length_sum_set r m ⟹ g x ∈ T" by (auto simp: g_def length_sum_set_def sum_list_Suc T_def) moreover have "x ∈ g ` length_sum_set r m" if "x ∈ T" for x proof have [simp]: "length x = r" using length_sum_set_def that T_def by auto have r1_x: "replicate r (Suc 0) ⊴ x" using that unfolding T_def pointwise_le_iff_nth by (simp add: lists_def in_listsp_conv_set Suc_leI) show "x = g (g' x)" using that by (intro nth_equalityI) (auto simp: g_def g'_def T_def) show "g' x ∈ length_sum_set r m" using that T_def by (simp add: g'_def r1_x sum_list_minus length_sum_set_def sum_list_replicate) qed ultimately show "g ` (length_sum_set r m) = T" by auto qed define U where "U ≡ (insert (m+r)) ` finsets {0<..<m+r} (r-1)" have h: "bij_betw (set ∘ augmentum) T U" proof (intro bij_betw_imageI) show "inj_on ((set ∘ augmentum)) T" unfolding inj_on_def T_def by (metis ComplD IntE dementum_augmentum in_listsD insertI1) have "(set ∘ augmentum) t ∈ U" if "t ∈ T" for t proof - have t: "length t = r" "σ t = m+r" "0 ∉ set t" using that by (force simp: T_def length_sum_set_def)+ then have mrt: "m + r ∈ set (augmentum t)" by (metis ‹r>0› sum_list_augmentum) then have "set (augmentum t) = insert (m + r) (set (augmentum t) - {m + r})" by blast moreover have "set (augmentum t) - {m + r} ∈ finsets {0<..<m + r} (r - Suc 0)" apply (auto simp: finsets_def mrt distinct_card t) by (metis atMost_iff augmentum_subset_sum_list le_eq_less_or_eq subsetD t(2)) ultimately show ?thesis by (metis One_nat_def U_def comp_apply imageI) qed moreover have "u ∈ (set ∘ augmentum) ` T" if "u ∈ U" for u proof from that obtain N where u: "u = insert (m + r) N" and Nsub: "N ⊆ {0<..<m + r}" and [simp]: "card N = r - Suc 0" by (auto simp: U_def finsets_def) have [simp]: "0 ∉ N" "m+r ∉ N" "finite N" using finite_subset Nsub by auto have [simp]: "card u = r" using Nsub ‹r>0› by (auto simp: u card_insert_if) have ssN: "sorted (sorted_list_of_set N @ [m + r])" using Nsub by (simp add: less_imp_le_nat sorted_wrt_append subset_eq) have so_u_N: "sorted_list_of_set u = insort (m+r) (sorted_list_of_set N)" by (simp add: u) also have "… = sorted_list_of_set N @ [m+r]" using Nsub by (force intro: sorted_insort_is_snoc) finally have so_u: "sorted_list_of_set u = sorted_list_of_set N @ [m+r]" . have 0: "0 ∉ set (sorted_list_of_set u)" by (simp add: ‹r>0› set_insort_key so_u_N) show "u = (set ∘ augmentum) ((dementum ∘ sorted_list_of_set)u)" using 0 so_u ssN u by force have sortd_wrt_u: "sorted_wrt (<) (sorted_list_of_set u)" by simp show "(dementum ∘ sorted_list_of_set) u ∈ T" apply (simp add: T_def length_sum_set_def) using sum_list_dementum [OF ssN] sortd_wrt_u 0 by (force simp: so_u dementum_nonzero)+ qed ultimately show "(set ∘ augmentum) ` T = U" by auto qed obtain φ where "bij_betw φ S U" by (meson bij_betw_trans f g h) moreover have "card U = (n - σ x' + r-1) choose (r-1)" proof - have "inj_on (insert (m + r)) (finsets {0<..<m + r} (r - Suc 0))" by (simp add: inj_on_def finsets_def subset_iff) (meson insert_ident order_less_le) then have "card U = card (finsets {0<..<m + r} (r - 1))" unfolding U_def by (simp add: card_image) also have "… = (n - σ x' + r-1) choose (r-1)" by (simp add: card_finsets m_def) finally show ?thesis . qed ultimately show ?thesis by (metis bij_betw_same_card) qed subsection ‹Towards the main theorem› lemma extend_tuple: assumes "σ xs ≤ n" "length xs ≠ 0" obtains ys where "σ ys = n" "xs ⊴ ys" proof - obtain x xs' where xs: "xs = x#xs'" using assms list.exhaust by auto define y where "y ≡ x + n - σ xs" show thesis proof show "σ (y#xs') = n" using assms xs y_def by auto show "xs ⊴ y#xs'" using assms y_def pointwise_le_def xs by auto qed qed lemma extend_preserving: assumes "σ xs ≤ n" "length xs > 1" "i < length xs" obtains ys where "σ ys = n" "xs ⊴ ys" "ys!i = xs!i" proof - define j where "j ≡ Suc i mod length xs" define xs1 where "xs1 = take j xs" define xs2 where "xs2 = drop (Suc j) xs" define x where "x = xs!j" have xs: "xs = xs1 @ [x] @ xs2" using assms apply (simp add: Cons_nth_drop_Suc assms x_def xs1_def xs2_def j_def) by (meson Suc_lessD id_take_nth_drop mod_less_divisor) define y where "y ≡ x + n - σ xs" define ys where "ys ≡ xs1 @ [y] @ xs2" have "x ≤ y" using assms y_def by linarith show thesis proof show "σ ys = n" using assms(1) xs y_def ys_def by auto show "xs ⊴ ys" using xs ys_def ‹x ≤ y› pointwise_append_le_iff pointwise_le_def by fastforce have "length xs1 ≠ i" using assms by (simp add: xs1_def j_def min_def mod_Suc) then show "ys!i = xs!i" by (auto simp: ys_def xs nth_append nth_Cons') qed qed text‹The proof of the main theorem will make use of the inclusion-exclusion formula, in addition to the previously shown results.› theorem Khovanskii: assumes "card A > 1" defines "f ≡ λn. card(sumset_iterated A n)" obtains N p where "real_polynomial_function p" "⋀n. n ≥ N ⟹ real (f n) = p (real n)" proof - define r where "r ≡ card A" define C where "C ≡ λn x'. {x. x' ⊴ x ∧ σ x = n}" define X where "X ≡ minimal_elements {x. useless x ∧ length x = r}" have "r > 1" "r ≠ 0" using assms r_def by auto have Csub: "C n x' ⊆ length_sum_set (length x') n" for n x' by (auto simp: C_def length_sum_set_def pointwise_le_iff) then have finC: "finite (C n x')" for n x' by (meson finite_length_sum_set finite_subset) have "finite X" using "minimal_elements_set_tuples_finite" X_def by force then have max_X: "⋀x'. x' ∈ X ⟹ σ x' ≤ σ (max_pointwise r X)" using X_def max_pointwise_ge minimal_elements.simps pointwise_le_imp_σ by force let ?z0 = "replicate r 0" have Cn0: "C n ?z0 = length_sum_set r n" for n by (auto simp: C_def length_sum_set_def) then obtain p0 where pf_p0: "real_polynomial_function p0" and p0: "⋀n. n>0 ⟹ p0 (real n) = real (card (C n ?z0))" by (metis real_polynomial_function_length_sum_set) obtain q where pf_q: "real_polynomial_function q" and q: "⋀x. q x = x gchoose (r-1)" using real_polynomial_function_gchoose by metis define p where "p ≡ λx::real. p0 x - (∑Y | Y ⊆ X ∧ Y ≠ {}. (- 1) ^ (card Y + 1) * q((x - real(σ (max_pointwise r Y)) + real r - 1)))" show thesis proof note pf_q' = real_polynomial_function_compose [OF _ pf_q, unfolded o_def] note pf_intros = real_polynomial_function_sum real_polynomial_function_diff real_polynomial_function.intros show "real_polynomial_function p" unfolding p_def using ‹finite X› by (intro pf_p0 pf_q' pf_intros | force)+ next fix n assume "n ≥ max 1 (σ (max_pointwise r X))" then have nlarge: "n ≥ σ (max_pointwise r X)" and "n > 0" by auto define U where "U ≡ λn. length_sum_set r n ∩ {x. useful x}" have 2: "(length_sum_set r n ∩ {x. useless x}) = (⋃x'∈X. C n x')" unfolding C_def X_def length_sum_set_def r_def using useless_leq_useless by (force simp: minimal_elements.simps pointwise_le_iff useless_iff) define SUM1 where "SUM1 ≡ ∑I | I ⊆ C n ` X ∧ I ≠ {}. (- 1) ^ (card I + 1) * int (card (⋂I))" define SUM2 where "SUM2 ≡ ∑Y | Y ⊆ X ∧ Y ≠ {}. (- 1) ^ (card Y + 1) * int (card (⋂(C n ` Y)))" have SUM1_card: "card(length_sum_set r n ∩ {x. useless x}) = nat SUM1" unfolding SUM1_def using ‹finite X› by (simp add: finC 2 card_UNION) have "SUM1 ≥ 0" unfolding SUM1_def using card_UNION_nonneg finC ‹finite X› by auto have C_empty_iff: "C n x' = {} ⟷ σ x' > n" if "length x' ≠ 0" for x' by (simp add: set_eq_iff C_def) (meson extend_tuple linorder_not_le pointwise_le_imp_σ that) have C_eq_1: "C n x' = {[n]}" if "σ x' ≤ n" "length x' = 1" for x' using that by (auto simp: C_def length_Suc_conv pointwise_le_def elim!: list.rel_cases) have n_ge_X: "σ x ≤ n" if "x ∈ X" for x by (meson le_trans max_X nlarge that) have len_X_r: "x ∈ X ⟹ length x = r" for x by (auto simp: X_def minimal_elements.simps) have "min_pointwise r (C n x') = x'" if "r > 1" "x' ∈ X" for x' proof (rule pointwise_le_antisym) have [simp]: "length x' = r" "σ x' ≤ n" using X_def minimal_elements.cases that(2) n_ge_X by auto have [simp]: "length (min_pointwise r (C n x')) = r" by (simp add: min_pointwise_def) show "min_pointwise r (C n x') ⊴ x'" proof (clarsimp simp add: pointwise_le_iff_nth) fix i assume "i < r" then obtain y where "σ y = n ∧ x' ⊴ y ∧ y!i ≤ x'!i" by (metis extend_preserving ‹1 < r› ‹length x' = r› ‹x' ∈ X› order.refl n_ge_X) then have "∃y∈C n x'. y!i ≤ x'!i" using C_def by blast with ‹i < r› show "min_pointwise r (C n x')!i ≤ x'!i" by (simp add: min_pointwise_def Min_le_iff finC C_empty_iff leD) qed have "x' ⊴ min_pointwise r (C n x')" if "σ x' ≤ n" "length x' = r" for x' by (smt (verit, del_insts) C_def C_empty_iff ‹r ≠ 0› finC leD mem_Collect_eq min_pointwise_ge_iff pointwise_le_iff that) then show "x' ⊴ min_pointwise r (C n x')" using X_def minimal_elements.cases that by force qed then have inj_C: "inj_on (C n) X" by (smt (verit, best) inj_onI mem_Collect_eq ‹r>1›) have inj_on_imageC: "inj_on (image (C n)) (Pow X - {{}})" by (simp add: inj_C inj_on_diff inj_on_image_Pow) have "Pow (C n ` X) - {{}} ⊆ (image (C n)) ` (Pow X - {{}})" by (metis Pow_empty image_Pow_surj image_diff_subset image_empty) then have "(image (C n)) ` (Pow X - {{}}) = Pow (C n ` X) - {{}}" by blast then have "SUM1 = sum (λI. (- 1) ^ (card I + 1) * int (card (⋂I))) ((image (C n)) ` (Pow X - {{}}))" unfolding SUM1_def by (auto intro: sum.cong) also have "… = sum ((λI. (- 1) ^ (card I + 1) * int (card (⋂ I))) ∘ (image (C n))) (Pow X - {{}})" by (simp add: sum.reindex inj_on_imageC) also have "… = SUM2" unfolding SUM2_def using subset_inj_on [OF inj_C] by (force simp: card_image intro: sum.cong) finally have "SUM1 = SUM2" . have "length_sum_set r n = (length_sum_set r n ∩ {x. useful x}) ∪ (length_sum_set r n ∩ {x. useless x})" by auto then have "card (length_sum_set r n) = card (length_sum_set r n ∩ {x. useful x}) + card (length_sum_set r n ∩ Collect useless)" by (simp add: finite_length_sum_set disjnt_iff flip: card_Un_disjnt) moreover have "C n ?z0 = length_sum_set r n" by (auto simp: C_def length_sum_set_def) ultimately have "card (C n ?z0) = card (U n) + nat SUM2" by (simp add: U_def flip: ‹SUM1 = SUM2› SUM1_card) then have SUM2_le: "nat SUM2 ≤ card (C n ?z0)" by arith have σ_max_pointwise_le: "⋀Y. ⟦Y ⊆ X; Y ≠ {}⟧ ⟹ σ (max_pointwise r Y) ≤ n" by (meson ‹finite X› le_trans max_pointwise_mono nlarge pointwise_le_imp_σ) have card_C_max: "card (C n (max_pointwise r Y)) = (n - σ (max_pointwise r Y) + r - Suc 0 choose (r - Suc 0))" if "Y ⊆ X" "Y ≠ {}" for Y proof - have [simp]: "length (max_pointwise r Y) = r" by (simp add: max_pointwise_def) then show ?thesis using ‹r ≠ 0› that C_def by (simp add: bound_sum_list_card [of r] σ_max_pointwise_le) qed define SUM3 where "SUM3 ≡ (∑Y | Y ⊆ X ∧ Y ≠ {}. - ((- 1) ^ (card Y) * ((n - σ (max_pointwise r Y) + r - 1 choose (r - 1)))))" have "⋂(C n ` Y) = C n (max_pointwise r Y)" if "Y ⊆ X" "Y ≠ {}" for Y proof show "⋂ (C n ` Y) ⊆ C n (max_pointwise r Y)" unfolding C_def proof clarsimp fix x assume "∀y∈Y. y ⊴ x ∧ σ x = n" moreover have "finite Y" using ‹finite X› infinite_super that by blast moreover have "⋀u. u ∈ Y ⟹ length u = r" using len_X_r that by blast ultimately show "max_pointwise r Y ⊴ x ∧ σ x = n" by (smt (verit, del_insts) all_not_in_conv max_pointwise_le_iff pointwise_le_iff_nth that(2)) qed next show "C n (max_pointwise r Y) ⊆ ⋂ (C n ` Y)" apply (clarsimp simp: C_def) by (metis ‹finite X› finite_subset len_X_r max_pointwise_ge pointwise_le_trans subsetD that(1)) qed then have "SUM2 = SUM3" by (simp add: SUM2_def SUM3_def card_C_max) have "U n = C n ?z0 - (length_sum_set r n ∩ {x. useless x})" by (auto simp: U_def C_def length_sum_set_def) then have "card (U n) = card (C n ?z0) - card(length_sum_set r n ∩ {x. useless x})" using finite_length_sum_set by (simp add: C_def Collect_mono_iff inf.coboundedI1 length_sum_set_def flip: card_Diff_subset) then have card_U_eq_diff: "card (U n) = card (C n ?z0) - nat SUM1" using SUM1_card by presburger have "SUM3 ≥ 0" using ‹0 ≤ SUM1› ‹SUM1 = SUM2› ‹SUM2 = SUM3› by blast have **: "⋀Y. ⟦Y ⊆ X; Y ≠ {}⟧ ⟹ Suc (σ (max_pointwise r Y)) ≤ n + r" by (metis ‹1 < r› σ_max_pointwise_le add.commute add_le_mono less_or_eq_imp_le plus_1_eq_Suc) have "real (f n) = card (U n)" unfolding f_def r_def U_def length_sum_set_def using card_sumset_iterated_length_sum_set_useful length_sum_set_def by presburger also have "… = card (C n ?z0) - nat SUM3" using card_U_eq_diff ‹SUM1 = SUM2› ‹SUM2 = SUM3› by presburger also have "… = real (card (C n (replicate r 0))) - real (nat SUM3)" using SUM2_le ‹SUM2 = SUM3› of_nat_diff by blast also have "… = p (real n)" using ‹1 < r› ‹n>0› apply (simp add: p_def p0 q ‹SUM3 ≥ 0›) apply (simp add: SUM3_def binomial_gbinomial of_nat_diff σ_max_pointwise_le algebra_simps **) done finally show "real (f n) = p (real n)" . qed qed end end