/-
Copyright 2025 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtilErdős Problem 509
namespace Erdos509
open Polynomialopen scoped Real
section BoundedDiscCover
universe u v
variable {M : Type u} [MetricSpace M]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$.
structure BoundedDiscCover (S : Set M) (r : ℝ) (ι : Type v) where
(C : ι → M)
(R : ι → ℝ)
(h_cover : S ⊆ ⋃ (i : ι), Metric.closedBall (C i) (R i))
(h_summable : Summable (fun i : ι => R i))
(h_bdd : ∑' i, R i ≤ r)
(h_pos : ∀ i, 0 < R i)
variable (S : Set M) (r : ℝ)
noncomputable def boundedDiscCover_empty [Nonempty M] (r : ℝ) (hr : 0 < r) :
(BoundedDiscCover (∅ : Set M) r (PUnit : Type v)) where
C := fun _ => Classical.ofNonempty
R := fun _ => r
h_cover := Set.empty_subset _
h_summable := (hasSum_fintype _).summable
h_bdd := M:Type uinst✝¹:MetricSpace MS:Set Mr✝:ℝinst✝:Nonempty Mr:ℝhr:0 < r⊢ ∑' (i : PUnit.{v + 1}), r ≤ r
M:Type uinst✝¹:MetricSpace MS:Set Mr✝:ℝinst✝:Nonempty Mr:ℝhr:0 < rthis:HasSum (fun x => if 0 ≤ r then -1 else r) (∑ b, if 0 ≤ r then -1 else r) := hasSum_fintype (fun x => if 0 ≤ r then -1 else r) (SummationFilter.unconditional PUnit.{v + 1})⊢ ∑' (i : PUnit.{v + 1}), r ≤ r
M:Type uinst✝¹:MetricSpace MS:Set Mr✝:ℝinst✝:Nonempty Mr:ℝhr:0 < rthis:HasSum (fun x => if 0 ≤ r then -1 else r) (∑ b, if 0 ≤ r then -1 else r) := hasSum_fintype (fun x => if 0 ≤ r then -1 else r) (SummationFilter.unconditional PUnit.{v + 1})⊢ r ≤ r
All goals completed! 🐙
h_pos := M:Type uinst✝¹:MetricSpace MS:Set Mr✝:ℝinst✝:Nonempty Mr:ℝhr:0 < r⊢ ∀ (i : PUnit.{v + 1}), 0 < r All goals completed! 🐙
@[category API, AMS 54]
lemma BoundedDiscCover.bound_nonneg_of_nonempty
(S : Set M) (hS : S.Nonempty) (r : ℝ) (ι : Type v)
(bdc : BoundedDiscCover S r ι) :
0 < r := M:Type uinst✝:MetricSpace MS:Set MhS:S.Nonemptyr:ℝι:Type vbdc:BoundedDiscCover S r ι⊢ 0 < r
M:Type uinst✝:MetricSpace MS:Set MhS:S.Nonemptyr:ℝι:Type vbdc:BoundedDiscCover S r ι⊢ 0 < ∑' (i : ι), bdc.R i
suffices Nonempty ι M:Type uinst✝:MetricSpace MS:Set MhS:S.Nonemptyr:ℝι:Type vbdc:BoundedDiscCover S r ιthis:Nonempty ι := ?m.20⊢ 0 < ∑' (i : ι), bdc.R i
All goals completed! 🐙
M:Type uinst✝:MetricSpace MS:Set MhS:S.Nonemptyr:ℝι:Type vbdc:BoundedDiscCover S r ιthis:IsEmpty ι⊢ False
M:Type uinst✝:MetricSpace MS:Set MhS:S.Nonemptyr:ℝι:Type vbdc:BoundedDiscCover S r ιthis:IsEmpty ι⊢ S ⊆ ∅
M:Type uinst✝:MetricSpace MS:Set MhS:S.Nonemptyr:ℝι:Type vbdc:BoundedDiscCover S r ιthis:IsEmpty ι⊢ ∅ = ⋃ i, Metric.closedBall (bdc.C i) (bdc.R i)
All goals completed! 🐙
end BoundedDiscCover
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$?
@[category research open, AMS 30]
theorem erdos_509 : answer(sorry) ↔ ∀ (f : ℂ[X]), f.Monic → f.natDegree ≠ 0 →
∃ (ι : Type), Nonempty (BoundedDiscCover {z | ‖f.eval z‖ ≤ 1} 2 ι) := ⊢ True ↔ ∀ (f : ℂ[X]), f.Monic → f.natDegree ≠ 0 → ∃ ι, Nonempty (BoundedDiscCover {z | ‖eval z f‖ ≤ 1} 2 ι)
All goals completed! 🐙
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
@[category research solved, AMS 30]
theorem erdos_509.variants.Cartan_bound : answer(True) ↔ ∀ (f : ℂ[X]), f.Monic → f.natDegree ≠ 0 →
∃ (ι : Type), Nonempty (BoundedDiscCover {z | ‖f.eval z‖ ≤ 1} (2*rexp 1) ι) := ⊢ True ↔ ∀ (f : ℂ[X]), f.Monic → f.natDegree ≠ 0 → ∃ ι, Nonempty (BoundedDiscCover {z | ‖eval z f‖ ≤ 1} (2 * rexp 1) ι)
All goals completed! 🐙
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.
@[category research solved, AMS 30]
theorem erdos_509.variants.Pommerenke_bound : answer(True) ↔ ∀ (f : ℂ[X]), f.Monic → f.natDegree ≠ 0 →
∃ (ι : Type), Nonempty (BoundedDiscCover {z | ‖f.eval z‖ ≤ 1} 2.59 ι) := ⊢ True ↔ ∀ (f : ℂ[X]), f.Monic → f.natDegree ≠ 0 → ∃ ι, Nonempty (BoundedDiscCover {z | ‖eval z f‖ ≤ 1} 2.59 ι)
All goals completed! 🐙
Let $f(z) ∈ ℂ[z]$ be a monic non-constant polynomial. If it is connected, can the set ${z ∈ ℂ : |f(z)| ≤ 1}$ be covered by a set of circles the sum of whose radii is $≤ 2$? Solution: True. This is due to Pommerenke.
@[category research solved, AMS 30]
theorem erdos_509.variants.Pommerenke_connected : answer(True) ↔ ∀ (f : ℂ[X]), f.Monic → f.natDegree ≠ 0 →
IsConnected {z | ‖f.eval z‖ ≤ 1} →
∃ (ι : Type), Nonempty (BoundedDiscCover {z | ‖f.eval z‖ ≤ 1} 2 ι) := ⊢ True ↔
∀ (f : ℂ[X]),
f.Monic →
f.natDegree ≠ 0 → IsConnected {z | ‖eval z f‖ ≤ 1} → ∃ ι, Nonempty (BoundedDiscCover {z | ‖eval z f‖ ≤ 1} 2 ι)
All goals completed! 🐙
end Erdos509