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"

definition Wetzel :: "(complex  complex) set  bool"
  where "Wetzel  λF. (fF. 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
    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)
  with W show ?thesis
    unfolding Wetzel_def by (meson countable uncountable_gcard_ge)

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 by (force simp: closure_approachable)
    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)
  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
        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
      show ?thesis 
        using ** [OF order_refl] η that gf 
        by (simp add: w_def bij_betw_iff_bijections inD_def) metis
      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)
      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)
        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)

      show ?thesis
        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)
          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. nN. B  (1 + real n) / (1 + norm z)" for B
              show "nnat 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)
            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" .
          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 .
        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)
    with f show ?thesis
      using inj by (rule_tac x="h" in exI) (auto simp: Φ_def inj_on_def)
  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)
  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
    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)
    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

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.›