Erdős Problem 509

Reference: erdosproblems.com/509

structure BoundedDiscCover {M : Type u} [MetricSpace M] (S : Set M) (r : ℝ) (ι : Type v) : Type (max u v)

An $r$-bounded disc cover of a subset of a metric space $M$ is an indexed family of closed discs whose radii sum to at most $r$.

• C : ι → M
• R : ι → ℝ
• h_cover : S ⊆ ⋃ (i : ι), Metric.closedBall (self.C i) (self.R i)
• h_summable : Summable fun (i : ι) => self.R i
• h_bdd : ∑' (i : ι), self.R i ≤ r
• h_pos (i : ι) : 0 < self.R i

noncomputable def boundedDiscCover_empty {M : Type u} [MetricSpace M] [Nonempty M] (r : ℝ) (hr : 0 < r) : BoundedDiscCover ∅ r PUnit.{v + 1}

Equations

• boundedDiscCover_empty r hr = { C := fun (x : PUnit.{?u.47 + 1}) => Classical.ofNonempty, R := fun (x : PUnit.{?u.47 + 1}) => r, h_cover := ⋯, h_summable := ⋯, h_bdd := ⋯, h_pos := ⋯ }

theorem BoundedDiscCover.bound_nonneg_of_nonempty {M : Type u} [MetricSpace M] (S : Set M) (hS : S.Nonempty) (r : ℝ) (ι : Type v) (bdc : BoundedDiscCover S r ι) : 0 < r

theorem erdos_509 : (∀ (f : Polynomial ℂ), f.Monic → f.natDegree ≠ 0 → ∃ (ι : Type), Nonempty (BoundedDiscCover {z : ℂ | ‖Polynomial.eval z f‖ ≤ 1} 2 ι)) ↔ sorry

Let $f(z) ∈ ℂ[z]$ be a monic non-constant polynomial. Can the set $\{z ∈ ℂ : |f(z)| ≤ 1\}$ be covered by a set of closed discs the sum of whose radii is $≤ 2$?

theorem erdos_509.variants.Cartan_bound : (∀ (f : Polynomial ℂ), f.Monic → f.natDegree ≠ 0 → ∃ (ι : Type), Nonempty (BoundedDiscCover {z : ℂ | ‖Polynomial.eval z f‖ ≤ 1} (2 * Real.exp 1) ι)) ↔ True

Let $f(z) ∈ ℂ[z]$ be a monic non-constant polynomial. Can the set $\{z ∈ ℂ : |f(z)| ≤ 1\}$ be covered by a set of closed discs the sum of whose radii is ≤2e? Solution: True. This is due to Cartan. See Sur les systèmes de fonctions holomorphes à variétés linéaires lacunaires et leurs applications, Henri Cartan, http://www.numdam.org/article/ASENS_1928_3_45__255_0.pdf

theorem erdos_509.variants.Pommerenke_bound : (∀ (f : Polynomial ℂ), f.Monic → f.natDegree ≠ 0 → ∃ (ι : Type), Nonempty (BoundedDiscCover {z : ℂ | ‖Polynomial.eval z f‖ ≤ 1} 2.59 ι)) ↔ True

Let $f(z) ∈ ℂ[z]$ be a monic non-constant polynomial. Can the set $\{z ∈ ℂ : |f(z)| ≤ 1\}$ be covered by a set of closed discs the sum of whose radii is $≤ 2.59$? Solution: True. This is due to Pommerenke.

theorem erdos_509.variants.Pommerenke_connected : (∀ (f : Polynomial ℂ), f.Monic → f.natDegree ≠ 0 → IsConnected {z : ℂ | ‖Polynomial.eval z f‖ ≤ 1} → ∃ (ι : Type), Nonempty (BoundedDiscCover {z : ℂ | ‖Polynomial.eval z f‖ ≤ 1} 2 ι)) ↔ True

Let $f(z) ∈ ℂ[z]$ be a monic non-constant polynomial. If it is connected, can the set $\{z ∈ C : |f(z)| ≤ 1\}$ be covered by a set of circles the sum of whose radii is $≤ 2$? Solution: True. This is due to Pommerenke.