Theory Wetzels_Problem
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))"
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
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