section ‹Wetzel's Problem, Solved by Erdös› text ‹Martin Aigner and Günter M. Ziegler. Proofs from THE BOOK. (Springer, 2018). Chapter 19: Sets, functions, and the continuum hypothesis Theorem 5 (pages 137--8)› theory Wetzels_Problem imports "HOL-Complex_Analysis.Complex_Analysis" "ZFC_in_HOL.General_Cardinals" begin definition Wetzel :: "(complex ⇒ complex) set ⇒ bool" where "Wetzel ≡ λF. (∀f∈F. f analytic_on UNIV) ∧ (∀z. countable((λf. f z) ` F))" subsubsection ‹When the continuum hypothesis is false› proposition Erdos_Wetzel_nonCH: assumes W: "Wetzel F" and NCH: "C_continuum > ℵ1" shows "countable F" proof - have "∃z0. gcard ((λf. f z0) ` F) ≥ ℵ1" if "uncountable F" proof - have "gcard F ≥ ℵ1" using that uncountable_gcard_ge by force then obtain F' where "F' ⊆ F" and F': "gcard F' = ℵ1" by (meson Card_Aleph subset_smaller_gcard) then obtain φ where φ: "bij_betw φ (elts ω1) F'" by (metis TC_small eqpoll_def gcard_eqpoll) define S where "S ≡ λα β. {z. φ α z = φ β z}" have co_S: "gcard (S α β) ≤ ℵ0" if "α ∈ elts β" "β ∈ elts ω1" for α β proof - have "φ α holomorphic_on UNIV" "φ β holomorphic_on UNIV" using W ‹F' ⊆ F› unfolding Wetzel_def by (meson Ord_ω1 Ord_trans φ analytic_imp_holomorphic bij_betwE subsetD that)+ moreover have "φ α ≠ φ β" by (metis Ord_ω1 Ord_trans φ bij_betw_def inj_on_def mem_not_refl that) ultimately have "countable (S α β)" using holomorphic_countable_equal_UNIV unfolding S_def by blast then show ?thesis using countable_imp_g_le_Aleph0 by blast qed define SS where "SS ≡⨆β ∈ elts ω1. ⨆α ∈ elts β. S α β" have F'_eq: "F' = φ ` elts ω1" using φ bij_betw_imp_surj_on by auto have §: "⋀β. β ∈ elts ω1 ⟹ gcard (⋃α∈elts β. S α β) ≤ ω" by (metis Aleph_0 TC_small co_S countable_UN countable_iff_g_le_Aleph0 less_ω1_imp_countable) have "gcard SS ≤ gcard ((λβ. ⋃α∈elts β. S α β) ` elts ω1) ⊗ ℵ0" apply (simp add: SS_def) by (metis (no_types, lifting) "§" TC_small gcard_Union_le_cmult imageE) also have "… ≤ ℵ1" proof (rule cmult_InfCard_le) show "gcard ((λβ. ⋃α∈elts β. S α β) ` elts ω1) ≤ ω1" using gcard_image_le by fastforce qed auto finally have "gcard SS ≤ ℵ1" . with NCH obtain z0 where "z0 ∉ SS" by (metis Complex_gcard UNIV_eq_I less_le_not_le) then have "inj_on (λx. φ x z0) (elts ω1)" apply (simp add: SS_def S_def inj_on_def) by (metis Ord_ω1 Ord_in_Ord Ord_linear) then have "gcard ((λf. f z0) ` F') = ℵ1" by (smt (verit) F' F'_eq gcard_image imageE inj_on_def) then show ?thesis by (metis TC_small ‹F' ⊆ F› image_mono subset_imp_gcard_le) qed with W show ?thesis unfolding Wetzel_def by (meson countable uncountable_gcard_ge) qed subsubsection ‹When the continuum hypothesis is true› lemma Rats_closure_real2: "closure (ℚ×ℚ) = (UNIV::real set)×(UNIV::real set)" by (simp add: Rats_closure_real closure_Times) proposition Erdos_Wetzel_CH: assumes CH: "C_continuum = ℵ1" obtains F where "Wetzel F" and "uncountable F" proof - define D where "D ≡ {z. Re z ∈ ℚ ∧ Im z ∈ ℚ}" have Deq: "D = (⋃x∈ℚ. ⋃y∈ℚ. {Complex x y})" using complex.collapse by (force simp: D_def) with countable_rat have "countable D" by blast have "infinite D" unfolding Deq by (intro infinite_disjoint_family_imp_infinite_UNION Rats_infinite) (auto simp: disjoint_family_on_def) have "∃w. Re w ∈ ℚ ∧ Im w ∈ ℚ ∧ norm (w - z) < e" if "e > 0" for z and e::real proof - obtain x y where "x∈ℚ" "y∈ℚ" and xy: "dist (x,y) (Re z, Im z) < e" using ‹e > 0› Rats_closure_real2 unfolding closure_approachable set_eq_iff by blast moreover have "dist (x,y) (Re z, Im z) = norm (Complex x y - z)" by (simp add: norm_complex_def norm_prod_def dist_norm) ultimately show "∃w. Re w ∈ ℚ ∧ Im w ∈ ℚ ∧ norm (w - z) < e" by (metis complex.sel) qed then have cloD: "closure D = UNIV" by (auto simp: D_def closure_approachable dist_complex_def) obtain ζ where ζ: "bij_betw ζ (elts ω1) (UNIV::complex set)" by (metis Complex_gcard TC_small assms eqpoll_def gcard_eqpoll) define inD where "inD ≡ λβ f. (∀α ∈ elts β. f (ζ α) ∈ D)" define Φ where "Φ ≡ λβ f. f β analytic_on UNIV ∧ inD β (f β) ∧ inj_on f (elts (succ β))" have ind_step: "∃h. Φ γ ((restrict f (elts γ))(γ:=h))" if γ: "γ ∈ elts ω1" and "∀β ∈ elts γ. Φ β f" for γ f proof - have f: "∀β ∈ elts γ. f β analytic_on UNIV ∧ inD β (f β)" using that by (auto simp: Φ_def) have inj: "inj_on f (elts γ)" using that by (simp add: Φ_def inj_on_def) (meson Ord_ω1 Ord_in_Ord Ord_linear) obtain h where "h analytic_on UNIV" "inD γ h" "(∀β ∈ elts γ. h ≠ f β)" proof (cases "finite (elts γ)") case True then obtain η where η: "bij_betw η {..<card (elts γ)} (elts γ)" using bij_betw_from_nat_into_finite by blast define g where "g ≡ f o η" define w where "w ≡ ζ o η" have gf: "∀i<card (elts γ). h ≠ g i ⟹ ∀β∈elts γ. h ≠ f β" for h using η by (auto simp: bij_betw_iff_bijections g_def) have **: "∃h. h analytic_on UNIV ∧ (∀i<n. h (w i) ∈ D ∧ h (w i) ≠ g i (w i))" if "n ≤ card (elts γ)" for n using that proof (induction n) case 0 then show ?case using analytic_on_const by blast next case (Suc n) then obtain h where "h analytic_on UNIV" and hg: "∀i<n. h(w i) ∈ D ∧ h(w i) ≠ g i (w i)" using Suc_leD by blast define p where "p ≡ λz. ∏i<n. z - w i" have p0: "p z = 0 ⟷ (∃i<n. z = w i)" for z unfolding p_def by force obtain d where d: "d ∈ D - {g n (w n)}" using ‹infinite D› by (metis ex_in_conv finite.emptyI infinite_remove) define h' where "h' ≡ λz. h z + p z * (d - h (w n)) / p (w n)" have h'_eq: "h' (w i) = h (w i)" if "i<n" for i using that by (force simp: h'_def p0) show ?case proof (intro exI strip conjI) have nless: "n < card (elts γ)" using Suc.prems Suc_le_eq by blast with η have "η n ≠ η i" if "i<n" for i using that unfolding bij_betw_iff_bijections by (metis lessThan_iff less_not_refl order_less_trans) with ζ η γ have pwn_nonzero: "p (w n) ≠ 0" apply (clarsimp simp: p0 w_def bij_betw_iff_bijections) by (metis Ord_ω1 Ord_trans nless lessThan_iff order_less_trans) then show "h' analytic_on UNIV" unfolding h'_def p_def by (intro analytic_intros ‹h analytic_on UNIV›) fix i assume "i < Suc n" then have §: "i < n ∨ i = n" by linarith then show "h' (w i) ∈ D" using h'_eq hg d h'_def pwn_nonzero by force show "h' (w i) ≠ g i (w i)" using § h'_eq hg h'_def d pwn_nonzero by fastforce qed qed show ?thesis using ** [OF order_refl] η that gf by (simp add: w_def bij_betw_iff_bijections inD_def) metis next case False then obtain η where η: "bij_betw η (UNIV::nat set) (elts γ)" by (meson γ countable_infiniteE' less_ω1_imp_countable) then have η_inject [simp]: "η i = η j ⟷ i=j" for i j by (simp add: bij_betw_imp_inj_on inj_eq) define g where "g ≡ f o η" define w where "w ≡ ζ o η" then have w_inject [simp]: "w i = w j ⟷ i=j" for i j by (smt (verit) Ord_ω1 Ord_trans UNIV_I η γ ζ bij_betw_iff_bijections comp_apply) define p where "p ≡ λn z. ∏i<n. z - w i" define q where "q ≡ λn. ∏i<n. 1 + norm (w i)" define h where "h ≡ λn ε z. ∑i<n. ε i * p i z" define BALL where "BALL ≡ λn ε. ball (h n ε (w n)) (norm (p n (w n)) / (fact n * q n))" ― ‹The demonimator above is the key to keeping the epsilons small› define DD where "DD ≡ λn ε. D ∩ BALL n ε - {g n (w n)}" define dd where "dd ≡ λn ε. SOME x. x ∈ DD n ε" have p0: "p n z = 0 ⟷ (∃i<n. z = w i)" for z n unfolding p_def by force have [simp]: "p n (w i) = 0" if "i<n" for i n using that by (simp add: p0) have q_gt0: "0 < q n" for n unfolding q_def by (smt (verit) norm_not_less_zero prod_pos) have "DD n ε ≠ {}" for n ε proof - have "r > 0 ⟹ infinite (D ∩ ball z r)" for z r by (metis islimpt_UNIV limpt_of_closure islimpt_eq_infinite_ball cloD) then have "infinite (D ∩ BALL n ε)" for n ε by (simp add: BALL_def p0 q_gt0) then show ?thesis by (metis DD_def finite.emptyI infinite_remove) qed then have dd_in_DD: "dd n ε ∈ DD n ε" for n ε by (simp add: dd_def some_in_eq) have h_cong: "h n ε = h n ε'" if "⋀i. i<n ⟹ ε i = ε' i" for n ε ε' using that by (simp add: h_def) have dd_cong: "dd n ε = dd n ε'" if "⋀i. i<n ⟹ ε i = ε' i" for n ε ε' using that by (metis dd_def DD_def BALL_def h_cong) have [simp]: "h n (cut ε less_than n) = h n ε" for n ε by (meson cut_apply h_cong less_than_iff) have [simp]: "dd n (cut ε less_than n) = dd n ε" for n ε by (meson cut_apply dd_cong less_than_iff) define coeff where "coeff ≡ wfrec less_than (λε n. (dd n ε - h n ε (w n)) / p n (w n))" have coeff_eq: "coeff n = (dd n coeff - h n coeff (w n)) / p n (w n)" for n by (simp add: def_wfrec [OF coeff_def]) have norm_coeff: "norm (coeff n) < 1 / (fact n * q n)" for n using dd_in_DD [of n coeff] by (simp add: q_gt0 coeff_eq DD_def BALL_def dist_norm norm_minus_commute norm_divide divide_simps) have norm_p_bound: "norm (p n z') ≤ q n * (1 + norm z) ^ n" if "dist z z' ≤ 1" for n z z' proof (induction n) case 0 then show ?case by (auto simp: p_def q_def) next case (Suc n) have "norm z' - norm z ≤ 1" by (smt (verit) dist_norm norm_triangle_ineq3 that) then have §: "norm (z' - w n) ≤ (1 + norm (w n)) * (1 + norm z)" by (simp add: mult.commute add_mono distrib_left norm_triangle_le_diff) have "norm (p n z') * norm (z' - w n) ≤ (q n * (1 + norm z) ^ n) * norm (z' - w n)" by (metis Suc mult.commute mult_left_mono norm_ge_zero) also have "… ≤ (q n * (1 + norm z) ^ n) * (1 + norm (w n)) * ((1 + norm z))" by (smt (verit) "§" Suc mult.assoc mult_left_mono norm_ge_zero) also have "… ≤ q n * (1 + norm (w n)) * ((1 + norm z) * (1 + norm z) ^ n)" by auto finally show ?case by (auto simp: p_def q_def norm_mult simp del: fact_Suc) qed show ?thesis proof define hh where "hh ≡ λz. suminf (λi. coeff i * p i z)" have "hh holomorphic_on UNIV" proof (rule holomorphic_uniform_sequence) fix n ―‹Many thanks to Manuel Eberl for suggesting these approach› show "h n coeff holomorphic_on UNIV" unfolding h_def p_def by (intro holomorphic_intros) next fix z have "uniform_limit (cball z 1) (λn. h n coeff) hh sequentially" unfolding hh_def h_def proof (rule Weierstrass_m_test) let ?M = "λn. (1 + norm z) ^ n / fact n" have "∃N. ∀n≥N. B ≤ (1 + real n) / (1 + norm z)" for B proof show "∀n≥nat ⌈B * (1 + norm z)⌉. B ≤ (1 + real n) / (1 + norm z)" using norm_ge_zero [of z] by (auto simp: divide_simps simp del: norm_ge_zero) qed then have L: "liminf (λn. ereal ((1 + real n) / (1 + norm z))) = ∞" by (simp add: Lim_PInfty flip: liminf_PInfty) have "∀⇩_{F}n in sequentially. 0 < (1 + cmod z) ^ n / fact n" using norm_ge_zero [of z] by (simp del: norm_ge_zero) then show "summable ?M" by (rule ratio_test_convergence) (auto simp: add_nonneg_eq_0_iff L) fix n z' assume "z' ∈ cball z 1" then have "norm (coeff n * p n z') ≤ norm (coeff n) * q n * (1 + norm z) ^ n" by (simp add: mult.assoc mult_mono norm_mult norm_p_bound) also have "… ≤ (1 / fact n) * (1 + norm z) ^ n" proof (rule mult_right_mono) show "norm (coeff n) * q n ≤ 1 / fact n" using q_gt0 norm_coeff [of n] by (simp add: field_simps) qed auto also have "… ≤ ?M n" by (simp add: divide_simps) finally show "norm (coeff n * p n z') ≤ ?M n" . qed then show "∃d>0. cball z d ⊆ UNIV ∧ uniform_limit (cball z d) (λn. h n coeff) hh sequentially" using zero_less_one by blast qed auto then show "hh analytic_on UNIV" by (simp add: analytic_on_open) have hh_eq_dd: "hh (w n) = dd n coeff" for n proof - have "hh (w n) = h (Suc n) coeff (w n)" unfolding hh_def h_def by (intro suminf_finite) auto also have "… = dd n coeff" by (induction n) (auto simp add: p0 h_def p_def coeff_eq [of "Suc _"] coeff_eq [of 0]) finally show ?thesis . qed then have "hh (w n) ∈ D" for n using DD_def dd_in_DD by fastforce then show "inD γ hh" unfolding inD_def by (metis η bij_betw_iff_bijections comp_apply w_def) have "hh (w n) ≠ f (η n) (w n)" for n using DD_def dd_in_DD g_def hh_eq_dd by auto then show "∀β∈elts γ. hh ≠ f β" by (metis η bij_betw_imp_surj_on imageE) qed qed with f show ?thesis using inj by (rule_tac x="h" in exI) (auto simp: Φ_def inj_on_def) qed define G where "G ≡ λf γ. @h. Φ γ ((restrict f (elts γ))(γ:=h))" define f where "f ≡ transrec G" have Φf: "Φ β f" if "β ∈ elts ω1" for β using that proof (induction β rule: eps_induct) case (step γ) then have IH: "∀β∈elts γ. Φ β f" using Ord_ω1 Ord_trans by blast have "f γ = G f γ" by (metis G_def f_def restrict_apply' restrict_ext transrec) moreover have "Φ γ ((restrict f (elts γ))(γ := G f γ))" by (metis ind_step[OF step.prems] G_def IH someI) ultimately show ?case by (metis IH Φ_def elts_succ fun_upd_same fun_upd_triv inj_on_restrict_eq restrict_upd) qed then have anf: "⋀β. β ∈ elts ω1 ⟹ f β analytic_on UNIV" and inD: "⋀α β. ⟦β ∈ elts ω1; α ∈ elts β⟧ ⟹ f β (ζ α) ∈ D" using Φ_def inD_def by blast+ have injf: "inj_on f (elts ω1)" using Φf unfolding inj_on_def Φ_def by (metis Ord_ω1 Ord_in_Ord Ord_linear_le in_succ_iff) show ?thesis proof let ?F = "f ` elts ω1" have "countable ((λf. f z) ` f ` elts ω1)" for z proof - obtain α where α: "ζ α = z" "α ∈ elts ω1" "Ord α" by (meson Ord_ω1 Ord_in_Ord UNIV_I ζ bij_betw_iff_bijections) let ?B = "elts ω1 - elts (succ α)" have eq: "elts ω1 = elts (succ α) ∪ ?B" using α by (metis Diff_partition Ord_ω1 OrdmemD less_eq_V_def succ_le_iff) have "(λf. f z) ` f ` ?B ⊆ D" using α inD by clarsimp (meson Ord_ω1 Ord_in_Ord Ord_linear) then have "countable ((λf. f z) ` f ` ?B)" by (meson ‹countable D› countable_subset) moreover have "countable ((λf. f z) ` f ` elts (succ α))" by (simp add: α less_ω1_imp_countable) ultimately show ?thesis using eq by (metis countable_Un_iff image_Un) qed then show "Wetzel ?F" unfolding Wetzel_def by (blast intro: anf) show "uncountable ?F" using Ord_ω1 countable_iff_less_ω1 countable_image_inj_eq injf by blast qed qed theorem Erdos_Wetzel: "C_continuum = ℵ1 ⟷ (∃F. Wetzel F ∧ uncountable F)" by (metis C_continuum_ge Erdos_Wetzel_CH Erdos_Wetzel_nonCH less_V_def) text ‹The originally submitted version of this theory included the development of cardinals for general Isabelle/HOL sets (as opposed to ZF sets, elements of type V), as well as other generally useful library material. From March 2022, that material has been moved to the analysis libraries or to @{theory ZFC_in_HOL.General_Cardinals}, as appropriate.› end