FormalConjectures/ErdosProblems/1119.lean

GitHub source file

5 declarations, 4 contain sorry, 0 declared as axioms

1. theorem Erdos1119.erdos_1119 Let $\mathfrak{m}$ be an infinite cardinal with $\aleph_0 < \mathfrak{m} < \mathfrak{c} = 2^{\aleph_0}$ sorry line 61 source

   Source documentation

   Let $\mathfrak{m}$ be an infinite cardinal with $\aleph_0 < \mathfrak{m} < \mathfrak{c} = 2^{\aleph_0}$. Let $\{f_\alpha\}$ be a family of entire functions such that, for every $z_0 \in \mathbb{C}$, there are at most $\mathfrak{m}$ distinct values of $f_\alpha(z_0)$. Must $\{f_\alpha\}$ have cardinality at most $\mathfrak{m}$?

   This is Problem 2.46 in [Ha74], where it is attributed to Erdős. The question is independent of ZFC, so the headline statement carries answer(sorry): it is neither provable nor refutable from the usual axioms of set theory.

   The answer is yes if $\mathfrak{m}^+ < \mathfrak{c}$ (see erdos_1119.variants.easy_case), so the question reduces to the case $\mathfrak{m}^+ = \mathfrak{c}$, where it is undecidable: Kumar and Shelah [KuSh17] produced a model of $\mathfrak{c} = \aleph_2$ in which the answer is yes (with $\mathfrak{m} = \aleph_1$), while Schilhan and Weinert [ScWe24] produced a different model of $\mathfrak{c} = \aleph_2$ in which the answer is no.

   depends on sorry what this means

   Statement uses: Iff, True, Cardinal, LT.lt, Cardinal.aleph0, Cardinal.continuum, Set, Complex, Membership.mem, Differentiable, LE.le, Cardinal.mk, Set.ofPred, Exists, And, Eq

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat

   45 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem erdos_1119 : answer(sorry) ↔
       ∀ (m : Cardinal.{0}), ℵ₀ < m → m < 𝔠 →
       ∀ F : Set (ℂ → ℂ), (∀ f ∈ F, Differentiable ℂ f) →
         (∀ z₀ : ℂ, #{y : ℂ | ∃ f ∈ F, f z₀ = y} ≤ m) →
         #F ≤ m := by
   …

2. theorem Erdos1119.erdos_1119.variants.easy_case sorry line 93 source

   depends on sorry what this means

   Statement uses: Cardinal, LT.lt, Cardinal.aleph0, Order.succ, Cardinal.continuum, Set, Complex, Membership.mem, Differentiable, LE.le, Cardinal.mk, Set.ofPred, Exists, And, Eq

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat

   47 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

3. theorem Erdos1119.erdos_1119.variants.erdos_wetzel Documented declaration: erdos_wetzel sorry line 106 source

   Source documentation

   Erdős's theorem [Er64g], answering a question of Wetzel: if $\mathfrak{c} > \aleph_1$, then every family of entire functions taking only countably many distinct values at each point $z_0 \in \mathbb{C}$ is itself countable.

   depends on sorry what this means

   Statement uses: LT.lt, Cardinal, OrderEmbedding, Ordinal, Cardinal.aleph, OfNat.ofNat, Cardinal.continuum, Set, Complex, Membership.mem, Differentiable, Set.Countable, Set.ofPred, Exists, And, Eq

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat

   55 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem erdos_1119.variants.erdos_wetzel (h : ℵ_ 1 < 𝔠) (F : Set (ℂ → ℂ))
       (hF : ∀ f ∈ F, Differentiable ℂ f)
       (hval : ∀ z₀ : ℂ, {y : ℂ | ∃ f ∈ F, f z₀ = y}.Countable) :
       F.Countable := by
   …

4. theorem Erdos1119.erdos_1119.variants.erdos_wetzel_ch Documented declaration: erdos_wetzel_ch sorry line 119 source

   Source documentation

   Erdős [Er64g] also showed that the previous statement fails under the continuum hypothesis: if $\mathfrak{c} = \aleph_1$, then there is an uncountable family of entire functions taking only countably many distinct values at each point $z_0 \in \mathbb{C}$.

   depends on sorry what this means

   Statement uses: Eq, Cardinal, Cardinal.continuum, OrderEmbedding, Ordinal, Cardinal.aleph, OfNat.ofNat, Exists, Set, Complex, And, Membership.mem, Differentiable, Set.Countable, Set.ofPred, Not

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat

   51 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem erdos_1119.variants.erdos_wetzel_ch (h : 𝔠 = ℵ_ 1) :
       ∃ F : Set (ℂ → ℂ), (∀ f ∈ F, Differentiable ℂ f) ∧
         (∀ z₀ : ℂ, {y : ℂ | ∃ f ∈ F, f z₀ = y}.Countable) ∧
         ¬ F.Countable := by
   …

5. theorem Erdos1119.erdos_1119.test.empty_family Sanity check: the empty family of entire functions satisfies both the value-bound hypothesis and the cardinality conclusion of erdos_1119, for any infinite $\mathfrak{m}$ line 131 source

   Source documentation

   Sanity check: the empty family of entire functions satisfies both the value-bound hypothesis and the cardinality conclusion of erdos_1119, for any infinite $\mathfrak{m}$.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Cardinal, LT.lt, Cardinal.aleph0, And, Complex, Membership.mem, Set, EmptyCollection.emptyCollection, Differentiable, LE.le, Cardinal.mk, Set.ofPred, Exists, Eq

   Proof uses: And.intro, absurd, Set.notMem_empty, of_eq_true, Eq.trans, OfNat.ofNat, True, congrFun', congrArg, False, funext, false_and, Cardinal.mk_eq_zero

   64 instances, coercions and auxiliary constants left out.

   Tactic trace: 5 steps

   Open to load the checked before-and-after goal states.

   theorem erdos_1119.test.empty_family (m : Cardinal.{0}) (_hm : ℵ₀ < m) :
       (∀ f ∈ (∅ : Set (ℂ → ℂ)), Differentiable ℂ f) ∧
       (∀ z₀ : ℂ, #{y : ℂ | ∃ f ∈ (∅ : Set (ℂ → ℂ)), f z₀ = y} ≤ m) ∧
       #(∅ : Set (ℂ → ℂ)) ≤ m := by
   …